--- a/src/HOL/Algebra/Coset.thy Tue Jun 12 11:18:35 2018 +0100
+++ b/src/HOL/Algebra/Coset.thy Tue Jun 12 16:08:57 2018 +0100
@@ -38,346 +38,325 @@
normal_rel :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool" (infixl "\<lhd>" 60) where
"H \<lhd> G \<equiv> normal H G"
+(* ************************************************************************** *)
+(* Next two lemmas contributed by Martin Baillon. *)
+
+lemma l_coset_eq_set_mult:
+ fixes G (structure)
+ shows "x <# H = {x} <#> H"
+ unfolding l_coset_def set_mult_def by simp
+
+lemma r_coset_eq_set_mult:
+ fixes G (structure)
+ shows "H #> x = H <#> {x}"
+ unfolding r_coset_def set_mult_def by simp
+
+(* ************************************************************************** *)
+
+
+(* ************************************************************************** *)
+(* Next five lemmas contributed by Paulo Emílio de Vilhena. *)
+
+lemma (in subgroup) rcosets_not_empty:
+ assumes "R \<in> rcosets H"
+ shows "R \<noteq> {}"
+proof -
+ obtain g where "g \<in> carrier G" "R = H #> g"
+ using assms unfolding RCOSETS_def by blast
+ hence "\<one> \<otimes> g \<in> R"
+ using one_closed unfolding r_coset_def by blast
+ thus ?thesis by blast
+qed
+
+lemma (in group) diff_neutralizes:
+ assumes "subgroup H G" "R \<in> rcosets H"
+ shows "\<And>r1 r2. \<lbrakk> r1 \<in> R; r2 \<in> R \<rbrakk> \<Longrightarrow> r1 \<otimes> (inv r2) \<in> H"
+proof -
+ fix r1 r2 assume r1: "r1 \<in> R" and r2: "r2 \<in> R"
+ obtain g where g: "g \<in> carrier G" "R = H #> g"
+ using assms unfolding RCOSETS_def by blast
+ then obtain h1 h2 where h1: "h1 \<in> H" "r1 = h1 \<otimes> g"
+ and h2: "h2 \<in> H" "r2 = h2 \<otimes> g"
+ using r1 r2 unfolding r_coset_def by blast
+ hence "r1 \<otimes> (inv r2) = (h1 \<otimes> g) \<otimes> ((inv g) \<otimes> (inv h2))"
+ using inv_mult_group is_group assms(1) g(1) subgroup.mem_carrier by fastforce
+ also have " ... = (h1 \<otimes> (g \<otimes> inv g) \<otimes> inv h2)"
+ using h1 h2 assms(1) g(1) inv_closed m_closed monoid.m_assoc
+ monoid_axioms subgroup.mem_carrier by smt
+ finally have "r1 \<otimes> inv r2 = h1 \<otimes> inv h2"
+ using assms(1) g(1) h1(1) subgroup.mem_carrier by fastforce
+ thus "r1 \<otimes> inv r2 \<in> H" by (metis assms(1) h1(1) h2(1) subgroup_def)
+qed
+
+
+subsection \<open>Stable Operations for Subgroups\<close>
+
+lemma (in group) subgroup_set_mult_equality[simp]:
+ assumes "subgroup H G" "I \<subseteq> H" "J \<subseteq> H"
+ shows "I <#>\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> J = I <#> J"
+ unfolding set_mult_def subgroup_mult_equality[OF assms(1)] by auto
+
+lemma (in group) subgroup_rcos_equality[simp]:
+ assumes "subgroup H G" "I \<subseteq> H" "h \<in> H"
+ shows "I #>\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> h = I #> h"
+ using subgroup_set_mult_equality by (simp add: r_coset_eq_set_mult assms)
+
+lemma (in group) subgroup_lcos_equality[simp]:
+ assumes "subgroup H G" "I \<subseteq> H" "h \<in> H"
+ shows "h <#\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> I = h <# I"
+ using subgroup_set_mult_equality by (simp add: l_coset_eq_set_mult assms)
+
+(* ************************************************************************** *)
+
+
+subsection \<open>Basic Properties of set_mult\<close>
+
+lemma (in group) setmult_subset_G:
+ assumes "H \<subseteq> carrier G" "K \<subseteq> carrier G"
+ shows "H <#> K \<subseteq> carrier G" using assms
+ by (auto simp add: set_mult_def subsetD)
+
+lemma (in monoid) set_mult_closed:
+ assumes "H \<subseteq> carrier G" "K \<subseteq> carrier G"
+ shows "H <#> K \<subseteq> carrier G"
+ using assms by (auto simp add: set_mult_def subsetD)
+
+(* ************************************************************************** *)
+(* Next lemma contributed by Martin Baillon. *)
+
+lemma (in group) set_mult_assoc:
+ assumes "M \<subseteq> carrier G" "H \<subseteq> carrier G" "K \<subseteq> carrier G"
+ shows "(M <#> H) <#> K = M <#> (H <#> K)"
+proof
+ show "(M <#> H) <#> K \<subseteq> M <#> (H <#> K)"
+ proof
+ fix x assume "x \<in> (M <#> H) <#> K"
+ then obtain m h k where x: "m \<in> M" "h \<in> H" "k \<in> K" "x = (m \<otimes> h) \<otimes> k"
+ unfolding set_mult_def by blast
+ hence "x = m \<otimes> (h \<otimes> k)"
+ using assms m_assoc by blast
+ thus "x \<in> M <#> (H <#> K)"
+ unfolding set_mult_def using x by blast
+ qed
+next
+ show "M <#> (H <#> K) \<subseteq> (M <#> H) <#> K"
+ proof
+ fix x assume "x \<in> M <#> (H <#> K)"
+ then obtain m h k where x: "m \<in> M" "h \<in> H" "k \<in> K" "x = m \<otimes> (h \<otimes> k)"
+ unfolding set_mult_def by blast
+ hence "x = (m \<otimes> h) \<otimes> k"
+ using assms m_assoc rev_subsetD by metis
+ thus "x \<in> (M <#> H) <#> K"
+ unfolding set_mult_def using x by blast
+ qed
+qed
+
+(* ************************************************************************** *)
+
subsection \<open>Basic Properties of Cosets\<close>
lemma (in group) coset_mult_assoc:
- "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
- ==> (M #> g) #> h = M #> (g \<otimes> h)"
-by (force simp add: r_coset_def m_assoc)
+ assumes "M \<subseteq> carrier G" "g \<in> carrier G" "h \<in> carrier G"
+ shows "(M #> g) #> h = M #> (g \<otimes> h)"
+ using assms by (force simp add: r_coset_def m_assoc)
+
+lemma (in group) coset_assoc:
+ assumes "x \<in> carrier G" "y \<in> carrier G" "H \<subseteq> carrier G"
+ shows "x <# (H #> y) = (x <# H) #> y"
+ using set_mult_assoc[of "{x}" H "{y}"]
+ by (simp add: l_coset_eq_set_mult r_coset_eq_set_mult assms)
lemma (in group) coset_mult_one [simp]: "M \<subseteq> carrier G ==> M #> \<one> = M"
by (force simp add: r_coset_def)
lemma (in group) coset_mult_inv1:
- "[| M #> (x \<otimes> (inv y)) = M; x \<in> carrier G ; y \<in> carrier G;
- M \<subseteq> carrier G |] ==> M #> x = M #> y"
-apply (erule subst [of concl: "%z. M #> x = z #> y"])
-apply (simp add: coset_mult_assoc m_assoc)
-done
+ assumes "M #> (x \<otimes> (inv y)) = M"
+ and "x \<in> carrier G" "y \<in> carrier G" "M \<subseteq> carrier G"
+ shows "M #> x = M #> y" using assms
+ by (metis coset_mult_assoc group.inv_solve_right is_group subgroup_def subgroup_self)
lemma (in group) coset_mult_inv2:
- "[| M #> x = M #> y; x \<in> carrier G; y \<in> carrier G; M \<subseteq> carrier G |]
- ==> M #> (x \<otimes> (inv y)) = M "
-apply (simp add: coset_mult_assoc [symmetric])
-apply (simp add: coset_mult_assoc)
-done
+ assumes "M #> x = M #> y"
+ and "x \<in> carrier G" "y \<in> carrier G" "M \<subseteq> carrier G"
+ shows "M #> (x \<otimes> (inv y)) = M " using assms
+ by (metis group.coset_mult_assoc group.coset_mult_one inv_closed is_group r_inv)
lemma (in group) coset_join1:
- "[| H #> x = H; x \<in> carrier G; subgroup H G |] ==> x \<in> H"
-apply (erule subst)
-apply (simp add: r_coset_def)
-apply (blast intro: l_one subgroup.one_closed sym)
-done
+ assumes "H #> x = H"
+ and "x \<in> carrier G" "subgroup H G"
+ shows "x \<in> H"
+ using assms r_coset_def l_one subgroup.one_closed sym by fastforce
lemma (in group) solve_equation:
- "\<lbrakk>subgroup H G; x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. y = h \<otimes> x"
-apply (rule bexI [of _ "y \<otimes> (inv x)"])
-apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc
- subgroup.subset [THEN subsetD])
-done
+ assumes "subgroup H G" "x \<in> H" "y \<in> H"
+ shows "\<exists>h \<in> H. y = h \<otimes> x"
+proof -
+ have "y = (y \<otimes> (inv x)) \<otimes> x" using assms
+ by (simp add: m_assoc subgroup.mem_carrier)
+ moreover have "y \<otimes> (inv x) \<in> H" using assms
+ by (simp add: subgroup_def)
+ ultimately show ?thesis by blast
+qed
lemma (in group) repr_independence:
- "\<lbrakk>y \<in> H #> x; x \<in> carrier G; subgroup H G\<rbrakk> \<Longrightarrow> H #> x = H #> y"
+ assumes "y \<in> H #> x" "x \<in> carrier G" "subgroup H G"
+ shows "H #> x = H #> y" using assms
by (auto simp add: r_coset_def m_assoc [symmetric]
subgroup.subset [THEN subsetD]
subgroup.m_closed solve_equation)
lemma (in group) coset_join2:
- "\<lbrakk>x \<in> carrier G; subgroup H G; x\<in>H\<rbrakk> \<Longrightarrow> H #> x = H"
+ assumes "x \<in> carrier G" "subgroup H G" "x \<in> H"
+ shows "H #> x = H" using assms
\<comment> \<open>Alternative proof is to put @{term "x=\<one>"} in \<open>repr_independence\<close>.\<close>
by (force simp add: subgroup.m_closed r_coset_def solve_equation)
+lemma (in group) coset_join3:
+ assumes "x \<in> carrier G" "subgroup H G" "x \<in> H"
+ shows "x <# H = H"
+proof
+ have "\<And>h. h \<in> H \<Longrightarrow> x \<otimes> h \<in> H" using assms
+ by (simp add: subgroup.m_closed)
+ thus "x <# H \<subseteq> H" unfolding l_coset_def by blast
+next
+ have "\<And>h. h \<in> H \<Longrightarrow> x \<otimes> ((inv x) \<otimes> h) = h"
+ by (smt assms inv_closed l_one m_assoc r_inv subgroup.mem_carrier)
+ moreover have "\<And>h. h \<in> H \<Longrightarrow> (inv x) \<otimes> h \<in> H"
+ by (simp add: assms subgroup.m_closed subgroup.m_inv_closed)
+ ultimately show "H \<subseteq> x <# H" unfolding l_coset_def by blast
+qed
+
lemma (in monoid) r_coset_subset_G:
- "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> H #> x \<subseteq> carrier G"
+ "\<lbrakk> H \<subseteq> carrier G; x \<in> carrier G \<rbrakk> \<Longrightarrow> H #> x \<subseteq> carrier G"
by (auto simp add: r_coset_def)
lemma (in group) rcosI:
- "[| h \<in> H; H \<subseteq> carrier G; x \<in> carrier G|] ==> h \<otimes> x \<in> H #> x"
+ "\<lbrakk> h \<in> H; H \<subseteq> carrier G; x \<in> carrier G \<rbrakk> \<Longrightarrow> h \<otimes> x \<in> H #> x"
by (auto simp add: r_coset_def)
lemma (in group) rcosetsI:
"\<lbrakk>H \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow> H #> x \<in> rcosets H"
by (auto simp add: RCOSETS_def)
-text\<open>Really needed?\<close>
-lemma (in group) transpose_inv:
- "[| x \<otimes> y = z; x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |]
- ==> (inv x) \<otimes> z = y"
-by (force simp add: m_assoc [symmetric])
-
-lemma (in group) rcos_self: "[| x \<in> carrier G; subgroup H G |] ==> x \<in> H #> x"
-apply (simp add: r_coset_def)
-apply (blast intro: sym l_one subgroup.subset [THEN subsetD]
- subgroup.one_closed)
-done
+lemma (in group) rcos_self:
+ "\<lbrakk> x \<in> carrier G; subgroup H G \<rbrakk> \<Longrightarrow> x \<in> H #> x"
+ by (metis l_one rcosI subgroup_def)
text (in group) \<open>Opposite of @{thm [source] "repr_independence"}\<close>
lemma (in group) repr_independenceD:
- assumes "subgroup H G"
- assumes ycarr: "y \<in> carrier G"
- and repr: "H #> x = H #> y"
+ assumes "subgroup H G" "y \<in> carrier G"
+ and "H #> x = H #> y"
shows "y \<in> H #> x"
-proof -
- interpret subgroup H G by fact
- show ?thesis apply (subst repr)
- apply (intro rcos_self)
- apply (rule ycarr)
- apply (rule is_subgroup)
- done
-qed
+ using assms by (simp add: rcos_self)
text \<open>Elements of a right coset are in the carrier\<close>
lemma (in subgroup) elemrcos_carrier:
- assumes "group G"
- assumes acarr: "a \<in> carrier G"
- and a': "a' \<in> H #> a"
+ assumes "group G" "a \<in> carrier G"
+ and "a' \<in> H #> a"
shows "a' \<in> carrier G"
-proof -
- interpret group G by fact
- from subset and acarr
- have "H #> a \<subseteq> carrier G" by (rule r_coset_subset_G)
- from this and a'
- show "a' \<in> carrier G"
- by fast
-qed
+ by (meson assms group.is_monoid monoid.r_coset_subset_G subset subsetCE)
lemma (in subgroup) rcos_const:
- assumes "group G"
- assumes hH: "h \<in> H"
+ assumes "group G" "h \<in> H"
shows "H #> h = H"
-proof -
- interpret group G by fact
- show ?thesis apply (unfold r_coset_def)
- apply rule
- apply rule
- apply clarsimp
- apply (intro subgroup.m_closed)
- apply (rule is_subgroup)
- apply assumption
- apply (rule hH)
- apply rule
- apply simp
- proof -
- fix h'
- assume h'H: "h' \<in> H"
- note carr = hH[THEN mem_carrier] h'H[THEN mem_carrier]
- from carr
- have a: "h' = (h' \<otimes> inv h) \<otimes> h" by (simp add: m_assoc)
- from h'H hH
- have "h' \<otimes> inv h \<in> H" by simp
- from this and a
- show "\<exists>x\<in>H. h' = x \<otimes> h" by fast
- qed
-qed
+ using group.coset_join2[OF assms(1), of h H]
+ by (simp add: assms(2) subgroup_axioms)
-text \<open>Step one for lemma \<open>rcos_module\<close>\<close>
lemma (in subgroup) rcos_module_imp:
- assumes "group G"
- assumes xcarr: "x \<in> carrier G"
- and x'cos: "x' \<in> H #> x"
+ assumes "group G" "x \<in> carrier G"
+ and "x' \<in> H #> x"
shows "(x' \<otimes> inv x) \<in> H"
proof -
- interpret group G by fact
- from xcarr x'cos
- have x'carr: "x' \<in> carrier G"
- by (rule elemrcos_carrier[OF is_group])
- from xcarr
- have ixcarr: "inv x \<in> carrier G"
- by simp
- from x'cos
- have "\<exists>h\<in>H. x' = h \<otimes> x"
- unfolding r_coset_def
- by fast
- from this
- obtain h
- where hH: "h \<in> H"
- and x': "x' = h \<otimes> x"
- by auto
- from hH and subset
- have hcarr: "h \<in> carrier G" by fast
- note carr = xcarr x'carr hcarr
- from x' and carr
- have "x' \<otimes> (inv x) = (h \<otimes> x) \<otimes> (inv x)" by fast
- also from carr
- have "\<dots> = h \<otimes> (x \<otimes> inv x)" by (simp add: m_assoc)
- also from carr
- have "\<dots> = h \<otimes> \<one>" by simp
- also from carr
- have "\<dots> = h" by simp
- finally
- have "x' \<otimes> (inv x) = h" by simp
- from hH this
- show "x' \<otimes> (inv x) \<in> H" by simp
+ obtain h where h: "h \<in> H" "x' = h \<otimes> x"
+ using assms(3) unfolding r_coset_def by blast
+ hence "x' \<otimes> inv x = h"
+ by (metis assms elemrcos_carrier group.inv_solve_right mem_carrier)
+ thus ?thesis using h by blast
qed
-text \<open>Step two for lemma \<open>rcos_module\<close>\<close>
lemma (in subgroup) rcos_module_rev:
- assumes "group G"
- assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
- and xixH: "(x' \<otimes> inv x) \<in> H"
+ assumes "group G" "x \<in> carrier G" "x' \<in> carrier G"
+ and "(x' \<otimes> inv x) \<in> H"
shows "x' \<in> H #> x"
proof -
- interpret group G by fact
- from xixH
- have "\<exists>h\<in>H. x' \<otimes> (inv x) = h" by fast
- from this
- obtain h
- where hH: "h \<in> H"
- and hsym: "x' \<otimes> (inv x) = h"
- by fast
- from hH subset have hcarr: "h \<in> carrier G" by simp
- note carr = carr hcarr
- from hsym[symmetric] have "h \<otimes> x = x' \<otimes> (inv x) \<otimes> x" by fast
- also from carr
- have "\<dots> = x' \<otimes> ((inv x) \<otimes> x)" by (simp add: m_assoc)
- also from carr
- have "\<dots> = x' \<otimes> \<one>" by simp
- also from carr
- have "\<dots> = x'" by simp
- finally
- have "h \<otimes> x = x'" by simp
- from this[symmetric] and hH
- show "x' \<in> H #> x"
- unfolding r_coset_def
- by fast
+ obtain h where h: "h \<in> H" "x' \<otimes> inv x = h"
+ using assms(4) unfolding r_coset_def by blast
+ hence "x' = h \<otimes> x"
+ by (metis assms group.inv_solve_right mem_carrier)
+ thus ?thesis using h unfolding r_coset_def by blast
qed
text \<open>Module property of right cosets\<close>
lemma (in subgroup) rcos_module:
- assumes "group G"
- assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
+ assumes "group G" "x \<in> carrier G" "x' \<in> carrier G"
shows "(x' \<in> H #> x) = (x' \<otimes> inv x \<in> H)"
-proof -
- interpret group G by fact
- show ?thesis proof assume "x' \<in> H #> x"
- from this and carr
- show "x' \<otimes> inv x \<in> H"
- by (intro rcos_module_imp[OF is_group])
- next
- assume "x' \<otimes> inv x \<in> H"
- from this and carr
- show "x' \<in> H #> x"
- by (intro rcos_module_rev[OF is_group])
- qed
-qed
+ using rcos_module_rev rcos_module_imp assms by blast
text \<open>Right cosets are subsets of the carrier.\<close>
lemma (in subgroup) rcosets_carrier:
- assumes "group G"
- assumes XH: "X \<in> rcosets H"
+ assumes "group G" "X \<in> rcosets H"
shows "X \<subseteq> carrier G"
-proof -
- interpret group G by fact
- from XH have "\<exists>x\<in> carrier G. X = H #> x"
- unfolding RCOSETS_def
- by fast
- from this
- obtain x
- where xcarr: "x\<in> carrier G"
- and X: "X = H #> x"
- by fast
- from subset and xcarr
- show "X \<subseteq> carrier G"
- unfolding X
- by (rule r_coset_subset_G)
-qed
+ using assms elemrcos_carrier singletonD
+ subset_eq unfolding RCOSETS_def by force
+
text \<open>Multiplication of general subsets\<close>
-lemma (in monoid) set_mult_closed:
- assumes Acarr: "A \<subseteq> carrier G"
- and Bcarr: "B \<subseteq> carrier G"
- shows "A <#> B \<subseteq> carrier G"
-apply rule apply (simp add: set_mult_def, clarsimp)
-proof -
- fix a b
- assume "a \<in> A"
- from this and Acarr
- have acarr: "a \<in> carrier G" by fast
-
- assume "b \<in> B"
- from this and Bcarr
- have bcarr: "b \<in> carrier G" by fast
-
- from acarr bcarr
- show "a \<otimes> b \<in> carrier G" by (rule m_closed)
-qed
lemma (in comm_group) mult_subgroups:
- assumes subH: "subgroup H G"
- and subK: "subgroup K G"
+ assumes "subgroup H G" and "subgroup K G"
shows "subgroup (H <#> K) G"
-apply (rule subgroup.intro)
- apply (intro set_mult_closed subgroup.subset[OF subH] subgroup.subset[OF subK])
- apply (simp add: set_mult_def) apply clarsimp defer 1
- apply (simp add: set_mult_def) defer 1
- apply (simp add: set_mult_def, clarsimp) defer 1
-proof -
- fix ha hb ka kb
- assume haH: "ha \<in> H" and hbH: "hb \<in> H" and kaK: "ka \<in> K" and kbK: "kb \<in> K"
- note carr = haH[THEN subgroup.mem_carrier[OF subH]] hbH[THEN subgroup.mem_carrier[OF subH]]
- kaK[THEN subgroup.mem_carrier[OF subK]] kbK[THEN subgroup.mem_carrier[OF subK]]
- from carr
- have "(ha \<otimes> ka) \<otimes> (hb \<otimes> kb) = ha \<otimes> (ka \<otimes> hb) \<otimes> kb" by (simp add: m_assoc)
- also from carr
- have "\<dots> = ha \<otimes> (hb \<otimes> ka) \<otimes> kb" by (simp add: m_comm)
- also from carr
- have "\<dots> = (ha \<otimes> hb) \<otimes> (ka \<otimes> kb)" by (simp add: m_assoc)
- finally
- have eq: "(ha \<otimes> ka) \<otimes> (hb \<otimes> kb) = (ha \<otimes> hb) \<otimes> (ka \<otimes> kb)" .
-
- from haH hbH have hH: "ha \<otimes> hb \<in> H" by (simp add: subgroup.m_closed[OF subH])
- from kaK kbK have kK: "ka \<otimes> kb \<in> K" by (simp add: subgroup.m_closed[OF subK])
-
- from hH and kK and eq
- show "\<exists>h'\<in>H. \<exists>k'\<in>K. (ha \<otimes> ka) \<otimes> (hb \<otimes> kb) = h' \<otimes> k'" by fast
+proof (rule subgroup.intro)
+ show "H <#> K \<subseteq> carrier G"
+ by (simp add: setmult_subset_G assms subgroup_imp_subset)
+next
+ have "\<one> \<otimes> \<one> \<in> H <#> K"
+ unfolding set_mult_def using assms subgroup.one_closed by blast
+ thus "\<one> \<in> H <#> K" by simp
next
- have "\<one> = \<one> \<otimes> \<one>" by simp
- from subgroup.one_closed[OF subH] subgroup.one_closed[OF subK] this
- show "\<exists>h\<in>H. \<exists>k\<in>K. \<one> = h \<otimes> k" by fast
+ show "\<And>x. x \<in> H <#> K \<Longrightarrow> inv x \<in> H <#> K"
+ proof -
+ fix x assume "x \<in> H <#> K"
+ then obtain h k where hk: "h \<in> H" "k \<in> K" "x = h \<otimes> k"
+ unfolding set_mult_def by blast
+ hence "inv x = (inv k) \<otimes> (inv h)"
+ by (meson inv_mult_group assms subgroup.mem_carrier)
+ hence "inv x = (inv h) \<otimes> (inv k)"
+ by (metis hk inv_mult assms subgroup.mem_carrier)
+ thus "inv x \<in> H <#> K"
+ unfolding set_mult_def using hk assms
+ by (metis (no_types, lifting) UN_iff singletonI subgroup_def)
+ qed
next
- fix h k
- assume hH: "h \<in> H"
- and kK: "k \<in> K"
-
- from hH[THEN subgroup.mem_carrier[OF subH]] kK[THEN subgroup.mem_carrier[OF subK]]
- have "inv (h \<otimes> k) = inv h \<otimes> inv k" by (simp add: inv_mult_group m_comm)
-
- from subgroup.m_inv_closed[OF subH hH] and subgroup.m_inv_closed[OF subK kK] and this
- show "\<exists>ha\<in>H. \<exists>ka\<in>K. inv (h \<otimes> k) = ha \<otimes> ka" by fast
+ show "\<And>x y. x \<in> H <#> K \<Longrightarrow> y \<in> H <#> K \<Longrightarrow> x \<otimes> y \<in> H <#> K"
+ proof -
+ fix x y assume "x \<in> H <#> K" "y \<in> H <#> K"
+ then obtain h1 k1 h2 k2 where h1k1: "h1 \<in> H" "k1 \<in> K" "x = h1 \<otimes> k1"
+ and h2k2: "h2 \<in> H" "k2 \<in> K" "y = h2 \<otimes> k2"
+ unfolding set_mult_def by blast
+ hence "x \<otimes> y = (h1 \<otimes> k1) \<otimes> (h2 \<otimes> k2)" by simp
+ also have " ... = h1 \<otimes> (k1 \<otimes> h2) \<otimes> k2"
+ by (smt h1k1 h2k2 m_assoc m_closed assms subgroup.mem_carrier)
+ also have " ... = h1 \<otimes> (h2 \<otimes> k1) \<otimes> k2"
+ by (metis (no_types, hide_lams) assms m_comm h1k1(2) h2k2(1) subgroup.mem_carrier)
+ finally have "x \<otimes> y = (h1 \<otimes> h2) \<otimes> (k1 \<otimes> k2)"
+ by (smt assms h1k1 h2k2 m_assoc monoid.m_closed monoid_axioms subgroup.mem_carrier)
+ thus "x \<otimes> y \<in> H <#> K" unfolding set_mult_def
+ using subgroup.m_closed[OF assms(1) h1k1(1) h2k2(1)]
+ subgroup.m_closed[OF assms(2) h1k1(2) h2k2(2)] by blast
+ qed
qed
lemma (in subgroup) lcos_module_rev:
- assumes "group G"
- assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
- and xixH: "(inv x \<otimes> x') \<in> H"
+ assumes "group G" "x \<in> carrier G" "x' \<in> carrier G"
+ and "(inv x \<otimes> x') \<in> H"
shows "x' \<in> x <# H"
proof -
- interpret group G by fact
- from xixH
- have "\<exists>h\<in>H. (inv x) \<otimes> x' = h" by fast
- from this
- obtain h
- where hH: "h \<in> H"
- and hsym: "(inv x) \<otimes> x' = h"
- by fast
-
- from hH subset have hcarr: "h \<in> carrier G" by simp
- note carr = carr hcarr
- from hsym[symmetric] have "x \<otimes> h = x \<otimes> ((inv x) \<otimes> x')" by fast
- also from carr
- have "\<dots> = (x \<otimes> (inv x)) \<otimes> x'" by (simp add: m_assoc[symmetric])
- also from carr
- have "\<dots> = \<one> \<otimes> x'" by simp
- also from carr
- have "\<dots> = x'" by simp
- finally
- have "x \<otimes> h = x'" by simp
-
- from this[symmetric] and hH
- show "x' \<in> x <# H"
- unfolding l_coset_def
- by fast
+ obtain h where h: "h \<in> H" "inv x \<otimes> x' = h"
+ using assms(4) unfolding l_coset_def by blast
+ hence "x' = x \<otimes> h"
+ by (metis assms group.inv_solve_left mem_carrier)
+ thus ?thesis using h unfolding l_coset_def by blast
qed
@@ -391,21 +370,21 @@
by (simp add: normal_def normal_axioms_def is_group)
lemma (in normal) inv_op_closed1:
- "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<otimes> h \<otimes> x \<in> H"
-apply (insert coset_eq)
-apply (auto simp add: l_coset_def r_coset_def)
-apply (drule bspec, assumption)
-apply (drule equalityD1 [THEN subsetD], blast, clarify)
-apply (simp add: m_assoc)
-apply (simp add: m_assoc [symmetric])
-done
+ assumes "x \<in> carrier G" and "h \<in> H"
+ shows "(inv x) \<otimes> h \<otimes> x \<in> H"
+proof -
+ have "h \<otimes> x \<in> x <# H"
+ using assms coset_eq assms(1) unfolding r_coset_def by blast
+ then obtain h' where "h' \<in> H" "h \<otimes> x = x \<otimes> h'"
+ unfolding l_coset_def by blast
+ thus ?thesis by (metis assms inv_closed l_inv l_one m_assoc mem_carrier)
+qed
lemma (in normal) inv_op_closed2:
- "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> (inv x) \<in> H"
-apply (subgoal_tac "inv (inv x) \<otimes> h \<otimes> (inv x) \<in> H")
-apply (simp add: )
-apply (blast intro: inv_op_closed1)
-done
+ assumes "x \<in> carrier G" and "h \<in> H"
+ shows "x \<otimes> h \<otimes> (inv x) \<in> H"
+ using assms inv_op_closed1 by (metis inv_closed inv_inv)
+
text\<open>Alternative characterization of normal subgroups\<close>
lemma (in group) normal_inv_iff:
@@ -455,74 +434,81 @@
qed
qed
+corollary (in group) normal_invI:
+ assumes "subgroup N G" and "\<And>x h. \<lbrakk> x \<in> carrier G; h \<in> N \<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> inv x \<in> N"
+ shows "N \<lhd> G"
+ using assms normal_inv_iff by blast
-subsection\<open>More Properties of Cosets\<close>
+corollary (in group) normal_invE:
+ assumes "N \<lhd> G"
+ shows "subgroup N G" and "\<And>x h. \<lbrakk> x \<in> carrier G; h \<in> N \<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> inv x \<in> N"
+ using assms normal_inv_iff apply blast
+ by (simp add: assms normal.inv_op_closed2)
+
+
+lemma (in group) one_is_normal :
+ "{\<one>} \<lhd> G"
+proof(intro normal_invI )
+ show "subgroup {\<one>} G"
+ by (simp add: subgroup_def)
+ show "\<And>x h. x \<in> carrier G \<Longrightarrow> h \<in> {\<one>} \<Longrightarrow> x \<otimes> h \<otimes> inv x \<in> {\<one>}" by simp
+qed
+
+
+subsection\<open>More Properties of Left Cosets\<close>
+
+lemma (in group) l_repr_independence:
+ assumes "y \<in> x <# H" "x \<in> carrier G" "subgroup H G"
+ shows "x <# H = y <# H"
+proof -
+ obtain h' where h': "h' \<in> H" "y = x \<otimes> h'"
+ using assms(1) unfolding l_coset_def by blast
+ hence "\<And> h. h \<in> H \<Longrightarrow> x \<otimes> h = y \<otimes> ((inv h') \<otimes> h)"
+ by (smt assms(2-3) inv_closed inv_solve_right m_assoc m_closed subgroup.mem_carrier)
+ hence "\<And> xh. xh \<in> x <# H \<Longrightarrow> xh \<in> y <# H"
+ unfolding l_coset_def by (metis (no_types, lifting) UN_iff assms(3) h'(1) subgroup_def)
+ moreover have "\<And> h. h \<in> H \<Longrightarrow> y \<otimes> h = x \<otimes> (h' \<otimes> h)"
+ using h' by (meson assms(2) assms(3) m_assoc subgroup.mem_carrier)
+ hence "\<And> yh. yh \<in> y <# H \<Longrightarrow> yh \<in> x <# H"
+ unfolding l_coset_def using subgroup.m_closed[OF assms(3) h'(1)] by blast
+ ultimately show ?thesis by blast
+qed
lemma (in group) lcos_m_assoc:
- "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
- ==> g <# (h <# M) = (g \<otimes> h) <# M"
+ "\<lbrakk> M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G \<rbrakk> \<Longrightarrow> g <# (h <# M) = (g \<otimes> h) <# M"
by (force simp add: l_coset_def m_assoc)
-lemma (in group) lcos_mult_one: "M \<subseteq> carrier G ==> \<one> <# M = M"
+lemma (in group) lcos_mult_one: "M \<subseteq> carrier G \<Longrightarrow> \<one> <# M = M"
by (force simp add: l_coset_def)
lemma (in group) l_coset_subset_G:
- "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> x <# H \<subseteq> carrier G"
+ "\<lbrakk> H \<subseteq> carrier G; x \<in> carrier G \<rbrakk> \<Longrightarrow> x <# H \<subseteq> carrier G"
by (auto simp add: l_coset_def subsetD)
-lemma (in group) l_coset_swap:
- "\<lbrakk>y \<in> x <# H; x \<in> carrier G; subgroup H G\<rbrakk> \<Longrightarrow> x \<in> y <# H"
-proof (simp add: l_coset_def)
- assume "\<exists>h\<in>H. y = x \<otimes> h"
- and x: "x \<in> carrier G"
- and sb: "subgroup H G"
- then obtain h' where h': "h' \<in> H \<and> x \<otimes> h' = y" by blast
- show "\<exists>h\<in>H. x = y \<otimes> h"
- proof
- show "x = y \<otimes> inv h'" using h' x sb
- by (auto simp add: m_assoc subgroup.subset [THEN subsetD])
- show "inv h' \<in> H" using h' sb
- by (auto simp add: subgroup.subset [THEN subsetD] subgroup.m_inv_closed)
- qed
-qed
-
lemma (in group) l_coset_carrier:
- "[| y \<in> x <# H; x \<in> carrier G; subgroup H G |] ==> y \<in> carrier G"
-by (auto simp add: l_coset_def m_assoc
- subgroup.subset [THEN subsetD] subgroup.m_closed)
+ "\<lbrakk> y \<in> x <# H; x \<in> carrier G; subgroup H G \<rbrakk> \<Longrightarrow> y \<in> carrier G"
+ by (auto simp add: l_coset_def m_assoc subgroup.subset [THEN subsetD] subgroup.m_closed)
-lemma (in group) l_repr_imp_subset:
- assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
- shows "y <# H \<subseteq> x <# H"
-proof -
- from y
- obtain h' where "h' \<in> H" "x \<otimes> h' = y" by (auto simp add: l_coset_def)
- thus ?thesis using x sb
- by (auto simp add: l_coset_def m_assoc
- subgroup.subset [THEN subsetD] subgroup.m_closed)
-qed
+lemma (in group) l_coset_swap:
+ assumes "y \<in> x <# H" "x \<in> carrier G" "subgroup H G"
+ shows "x \<in> y <# H"
+ using assms(2) l_repr_independence[OF assms] subgroup.one_closed[OF assms(3)]
+ unfolding l_coset_def by fastforce
-lemma (in group) l_repr_independence:
- assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
- shows "x <# H = y <# H"
+lemma (in group) subgroup_mult_id:
+ assumes "subgroup H G"
+ shows "H <#> H = H"
proof
- show "x <# H \<subseteq> y <# H"
- by (rule l_repr_imp_subset,
- (blast intro: l_coset_swap l_coset_carrier y x sb)+)
- show "y <# H \<subseteq> x <# H" by (rule l_repr_imp_subset [OF y x sb])
+ show "H <#> H \<subseteq> H"
+ unfolding set_mult_def using subgroup.m_closed[OF assms] by (simp add: UN_subset_iff)
+ show "H \<subseteq> H <#> H"
+ proof
+ fix x assume x: "x \<in> H" thus "x \<in> H <#> H" unfolding set_mult_def
+ using subgroup.m_closed[OF assms subgroup.one_closed[OF assms] x] subgroup.one_closed[OF assms]
+ by (smt UN_iff assms coset_join3 l_coset_def subgroup.mem_carrier)
+ qed
qed
-lemma (in group) setmult_subset_G:
- "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G\<rbrakk> \<Longrightarrow> H <#> K \<subseteq> carrier G"
-by (auto simp add: set_mult_def subsetD)
-
-lemma (in group) subgroup_mult_id: "subgroup H G \<Longrightarrow> H <#> H = H"
-apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def)
-apply (rule_tac x = x in bexI)
-apply (rule bexI [of _ "\<one>"])
-apply (auto simp add: subgroup.one_closed subgroup.subset [THEN subsetD])
-done
-
subsubsection \<open>Set of Inverses of an \<open>r_coset\<close>.\<close>
@@ -552,20 +538,21 @@
subsubsection \<open>Theorems for \<open><#>\<close> with \<open>#>\<close> or \<open><#\<close>.\<close>
lemma (in group) setmult_rcos_assoc:
- "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
- \<Longrightarrow> H <#> (K #> x) = (H <#> K) #> x"
-by (force simp add: r_coset_def set_mult_def m_assoc)
+ "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow>
+ H <#> (K #> x) = (H <#> K) #> x"
+ using set_mult_assoc[of H K "{x}"] by (simp add: r_coset_eq_set_mult)
lemma (in group) rcos_assoc_lcos:
- "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
- \<Longrightarrow> (H #> x) <#> K = H <#> (x <# K)"
-by (force simp add: r_coset_def l_coset_def set_mult_def m_assoc)
+ "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow>
+ (H #> x) <#> K = H <#> (x <# K)"
+ using set_mult_assoc[of H "{x}" K]
+ by (simp add: l_coset_eq_set_mult r_coset_eq_set_mult)
lemma (in normal) rcos_mult_step1:
- "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
- \<Longrightarrow> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
-by (simp add: setmult_rcos_assoc subset
- r_coset_subset_G l_coset_subset_G rcos_assoc_lcos)
+ "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow>
+ (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
+ by (simp add: setmult_rcos_assoc r_coset_subset_G
+ subset l_coset_subset_G rcos_assoc_lcos)
lemma (in normal) rcos_mult_step2:
"\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
@@ -645,7 +632,7 @@
lemma (in subgroup) l_coset_eq_rcong:
assumes "group G"
assumes a: "a \<in> carrier G"
- shows "a <# H = rcong H `` {a}"
+ shows "a <# H = (rcong H) `` {a}"
proof -
interpret group G by fact
show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a )
@@ -661,9 +648,7 @@
proof -
interpret subgroup H G by fact
from p show ?thesis apply (rule_tac UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"])
- apply (simp add: )
- apply (simp add: m_assoc transpose_inv)
- done
+ apply blast by (simp add: inv_solve_left m_assoc)
qed
lemma (in group) rcos_disjoint:
@@ -793,28 +778,47 @@
"\<lbrakk>H \<subseteq> carrier G; a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> a) H"
by (force simp add: inj_on_def subsetD)
+(* ************************************************************************** *)
+
lemma (in group) card_cosets_equal:
- "\<lbrakk>c \<in> rcosets H; H \<subseteq> carrier G; finite(carrier G)\<rbrakk>
- \<Longrightarrow> card c = card H"
-apply (auto simp add: RCOSETS_def)
-apply (rule card_bij_eq)
- apply (rule inj_on_f, assumption+)
- apply (force simp add: m_assoc subsetD r_coset_def)
- apply (rule inj_on_g, assumption+)
- apply (force simp add: m_assoc subsetD r_coset_def)
- txt\<open>The sets @{term "H #> a"} and @{term "H"} are finite.\<close>
- apply (simp add: r_coset_subset_G [THEN finite_subset])
-apply (blast intro: finite_subset)
-done
+ assumes "R \<in> rcosets H" "H \<subseteq> carrier G"
+ shows "\<exists>f. bij_betw f H R"
+proof -
+ obtain g where g: "g \<in> carrier G" "R = H #> g"
+ using assms(1) unfolding RCOSETS_def by blast
+
+ let ?f = "\<lambda>h. h \<otimes> g"
+ have "\<And>r. r \<in> R \<Longrightarrow> \<exists>h \<in> H. ?f h = r"
+ proof -
+ fix r assume "r \<in> R"
+ then obtain h where "h \<in> H" "r = h \<otimes> g"
+ using g unfolding r_coset_def by blast
+ thus "\<exists>h \<in> H. ?f h = r" by blast
+ qed
+ hence "R \<subseteq> ?f ` H" by blast
+ moreover have "?f ` H \<subseteq> R"
+ using g unfolding r_coset_def by blast
+ ultimately show ?thesis using inj_on_g unfolding bij_betw_def
+ using assms(2) g(1) by auto
+qed
+
+corollary (in group) card_rcosets_equal:
+ assumes "R \<in> rcosets H" "H \<subseteq> carrier G"
+ shows "card H = card R"
+ using card_cosets_equal assms bij_betw_same_card by blast
+
+corollary (in group) rcosets_finite:
+ assumes "R \<in> rcosets H" "H \<subseteq> carrier G" "finite H"
+ shows "finite R"
+ using card_cosets_equal assms bij_betw_finite is_group by blast
+
+(* ************************************************************************** *)
lemma (in group) rcosets_subset_PowG:
"subgroup H G \<Longrightarrow> rcosets H \<subseteq> Pow(carrier G)"
-apply (simp add: RCOSETS_def)
-apply (blast dest: r_coset_subset_G subgroup.subset)
-done
+ using rcosets_part_G by auto
-
-theorem (in group) lagrange:
+proposition (in group) lagrange_finite:
"\<lbrakk>finite(carrier G); subgroup H G\<rbrakk>
\<Longrightarrow> card(rcosets H) * card(H) = order(G)"
apply (simp (no_asm_simp) add: order_def rcosets_part_G [symmetric])
@@ -822,10 +826,42 @@
apply (rule card_partition)
apply (simp add: rcosets_subset_PowG [THEN finite_subset])
apply (simp add: rcosets_part_G)
- apply (simp add: card_cosets_equal subgroup.subset)
+ apply (simp add: card_rcosets_equal subgroup_imp_subset)
apply (simp add: rcos_disjoint)
done
+theorem (in group) lagrange:
+ assumes "subgroup H G"
+ shows "card (rcosets H) * card H = order G"
+proof (cases "finite (carrier G)")
+ case True thus ?thesis using lagrange_finite assms by simp
+next
+ case False note inf_G = this
+ thus ?thesis
+ proof (cases "finite H")
+ case False thus ?thesis using inf_G by (simp add: order_def)
+ next
+ case True note finite_H = this
+ have "infinite (rcosets H)"
+ proof (rule ccontr)
+ assume "\<not> infinite (rcosets H)"
+ hence finite_rcos: "finite (rcosets H)" by simp
+ hence "card (\<Union>(rcosets H)) = (\<Sum>R\<in>(rcosets H). card R)"
+ using card_Union_disjoint[of "rcosets H"] finite_H rcos_disjoint[OF assms(1)]
+ rcosets_finite[where ?H = H] by (simp add: assms subgroup_imp_subset)
+ hence "order G = (\<Sum>R\<in>(rcosets H). card R)"
+ by (simp add: assms order_def rcosets_part_G)
+ hence "order G = (\<Sum>R\<in>(rcosets H). card H)"
+ using card_rcosets_equal by (simp add: assms subgroup_imp_subset)
+ hence "order G = (card H) * (card (rcosets H))" by simp
+ hence "order G \<noteq> 0" using finite_rcos finite_H assms ex_in_conv
+ rcosets_part_G subgroup.one_closed by fastforce
+ thus False using inf_G order_gt_0_iff_finite by blast
+ qed
+ thus ?thesis using inf_G by (simp add: order_def)
+ qed
+qed
+
subsection \<open>Quotient Groups: Factorization of a Group\<close>
@@ -845,7 +881,7 @@
lemma (in normal) rcosets_assoc:
"\<lbrakk>M1 \<in> rcosets H; M2 \<in> rcosets H; M3 \<in> rcosets H\<rbrakk>
\<Longrightarrow> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
-by (auto simp add: RCOSETS_def rcos_sum m_assoc)
+ by (simp add: group.set_mult_assoc is_group rcosets_carrier)
lemma (in subgroup) subgroup_in_rcosets:
assumes "group G"
@@ -1016,10 +1052,111 @@
text\<open>If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.\<close>
-theorem (in group_hom) FactGroup_iso:
+theorem (in group_hom) FactGroup_iso_set:
"h ` carrier G = carrier H
- \<Longrightarrow> (\<lambda>X. the_elem (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H"
+ \<Longrightarrow> (\<lambda>X. the_elem (h`X)) \<in> iso (G Mod (kernel G H h)) H"
by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def
FactGroup_onto)
+corollary (in group_hom) FactGroup_iso :
+ "h ` carrier G = carrier H
+ \<Longrightarrow> (G Mod (kernel G H h))\<cong> H"
+ using FactGroup_iso_set unfolding is_iso_def by auto
+
+
+(* Next two lemmas contributed by Paulo Emílio de Vilhena. *)
+
+lemma (in group_hom) trivial_hom_iff:
+ "(h ` (carrier G) = { \<one>\<^bsub>H\<^esub> }) = (kernel G H h = carrier G)"
+ unfolding kernel_def using one_closed by force
+
+lemma (in group_hom) trivial_ker_imp_inj:
+ assumes "kernel G H h = { \<one> }"
+ shows "inj_on h (carrier G)"
+proof (rule inj_onI)
+ fix g1 g2 assume A: "g1 \<in> carrier G" "g2 \<in> carrier G" "h g1 = h g2"
+ hence "h (g1 \<otimes> (inv g2)) = \<one>\<^bsub>H\<^esub>" by simp
+ hence "g1 \<otimes> (inv g2) = \<one>"
+ using A assms unfolding kernel_def by blast
+ thus "g1 = g2"
+ using A G.inv_equality G.inv_inv by blast
+qed
+
+
+(* Next subsection contributed by Martin Baillon. *)
+
+subsection \<open>Theorems about Factor Groups and Direct product\<close>
+
+
+lemma (in group) DirProd_normal :
+ assumes "group K"
+ and "H \<lhd> G"
+ and "N \<lhd> K"
+ shows "H \<times> N \<lhd> G \<times>\<times> K"
+proof (intro group.normal_invI[OF DirProd_group[OF group_axioms assms(1)]])
+ show sub : "subgroup (H \<times> N) (G \<times>\<times> K)"
+ using DirProd_subgroups[OF group_axioms normal_imp_subgroup[OF assms(2)]assms(1)
+ normal_imp_subgroup[OF assms(3)]].
+ show "\<And>x h. x \<in> carrier (G\<times>\<times>K) \<Longrightarrow> h \<in> H\<times>N \<Longrightarrow> x \<otimes>\<^bsub>G\<times>\<times>K\<^esub> h \<otimes>\<^bsub>G\<times>\<times>K\<^esub> inv\<^bsub>G\<times>\<times>K\<^esub> x \<in> H\<times>N"
+ proof-
+ fix x h assume xGK : "x \<in> carrier (G \<times>\<times> K)" and hHN : " h \<in> H \<times> N"
+ hence hGK : "h \<in> carrier (G \<times>\<times> K)" using subgroup_imp_subset[OF sub] by auto
+ from xGK obtain x1 x2 where x1x2 :"x1 \<in> carrier G" "x2 \<in> carrier K" "x = (x1,x2)"
+ unfolding DirProd_def by fastforce
+ from hHN obtain h1 h2 where h1h2 : "h1 \<in> H" "h2 \<in> N" "h = (h1,h2)"
+ unfolding DirProd_def by fastforce
+ hence h1h2GK : "h1 \<in> carrier G" "h2 \<in> carrier K"
+ using normal_imp_subgroup subgroup_imp_subset assms apply blast+.
+ have "inv\<^bsub>G \<times>\<times> K\<^esub> x = (inv\<^bsub>G\<^esub> x1,inv\<^bsub>K\<^esub> x2)"
+ using inv_DirProd[OF group_axioms assms(1) x1x2(1)x1x2(2)] x1x2 by auto
+ hence "x \<otimes>\<^bsub>G \<times>\<times> K\<^esub> h \<otimes>\<^bsub>G \<times>\<times> K\<^esub> inv\<^bsub>G \<times>\<times> K\<^esub> x = (x1 \<otimes> h1 \<otimes> inv x1,x2 \<otimes>\<^bsub>K\<^esub> h2 \<otimes>\<^bsub>K\<^esub> inv\<^bsub>K\<^esub> x2)"
+ using h1h2 x1x2 h1h2GK by auto
+ moreover have "x1 \<otimes> h1 \<otimes> inv x1 \<in> H" "x2 \<otimes>\<^bsub>K\<^esub> h2 \<otimes>\<^bsub>K\<^esub> inv\<^bsub>K\<^esub> x2 \<in> N"
+ using normal_invE group.normal_invE[OF assms(1)] assms x1x2 h1h2 apply auto.
+ hence "(x1 \<otimes> h1 \<otimes> inv x1, x2 \<otimes>\<^bsub>K\<^esub> h2 \<otimes>\<^bsub>K\<^esub> inv\<^bsub>K\<^esub> x2)\<in> H \<times> N" by auto
+ ultimately show " x \<otimes>\<^bsub>G \<times>\<times> K\<^esub> h \<otimes>\<^bsub>G \<times>\<times> K\<^esub> inv\<^bsub>G \<times>\<times> K\<^esub> x \<in> H \<times> N" by auto
+ qed
+qed
+
+lemma (in group) FactGroup_DirProd_multiplication_iso_set :
+ assumes "group K"
+ and "H \<lhd> G"
+ and "N \<lhd> K"
+ shows "(\<lambda> (X, Y). X \<times> Y) \<in> iso ((G Mod H) \<times>\<times> (K Mod N)) (G \<times>\<times> K Mod H \<times> N)"
+
+proof-
+ have R :"(\<lambda>(X, Y). X \<times> Y) \<in> carrier (G Mod H) \<times> carrier (K Mod N) \<rightarrow> carrier (G \<times>\<times> K Mod H \<times> N)"
+ unfolding r_coset_def Sigma_def DirProd_def FactGroup_def RCOSETS_def apply simp by blast
+ moreover have "(\<forall>x\<in>carrier (G Mod H). \<forall>y\<in>carrier (K Mod N). \<forall>xa\<in>carrier (G Mod H).
+ \<forall>ya\<in>carrier (K Mod N). (x <#> xa) \<times> (y <#>\<^bsub>K\<^esub> ya) = x \<times> y <#>\<^bsub>G \<times>\<times> K\<^esub> xa \<times> ya)"
+ unfolding set_mult_def apply auto apply blast+.
+ moreover have "(\<forall>x\<in>carrier (G Mod H). \<forall>y\<in>carrier (K Mod N). \<forall>xa\<in>carrier (G Mod H).
+ \<forall>ya\<in>carrier (K Mod N). x \<times> y = xa \<times> ya \<longrightarrow> x = xa \<and> y = ya)"
+ unfolding FactGroup_def using times_eq_iff subgroup.rcosets_not_empty
+ by (metis assms(2) assms(3) normal_def partial_object.select_convs(1))
+ moreover have "(\<lambda>(X, Y). X \<times> Y) ` (carrier (G Mod H) \<times> carrier (K Mod N)) =
+ carrier (G \<times>\<times> K Mod H \<times> N)"
+ unfolding image_def apply auto using R apply force
+ unfolding DirProd_def FactGroup_def RCOSETS_def r_coset_def apply auto apply force.
+ ultimately show ?thesis
+ unfolding iso_def hom_def bij_betw_def inj_on_def by simp
+qed
+
+corollary (in group) FactGroup_DirProd_multiplication_iso_1 :
+ assumes "group K"
+ and "H \<lhd> G"
+ and "N \<lhd> K"
+ shows " ((G Mod H) \<times>\<times> (K Mod N)) \<cong> (G \<times>\<times> K Mod H \<times> N)"
+ unfolding is_iso_def using FactGroup_DirProd_multiplication_iso_set assms by auto
+
+corollary (in group) FactGroup_DirProd_multiplication_iso_2 :
+ assumes "group K"
+ and "H \<lhd> G"
+ and "N \<lhd> K"
+ shows "(G \<times>\<times> K Mod H \<times> N) \<cong> ((G Mod H) \<times>\<times> (K Mod N))"
+ using FactGroup_DirProd_multiplication_iso_1 group.iso_sym assms
+ DirProd_group[OF normal.factorgroup_is_group normal.factorgroup_is_group]
+ by blast
+
+
end