src/HOL/Algebra/Zassenhaus.thy
 author paulson Mon Jun 18 15:56:03 2018 +0100 (14 months ago) changeset 68466 3d8241f4198b parent 68452 c027dfbfad30 child 68555 22d51874f37d permissions -rw-r--r--
corrections to markup
```     1 (*  Title:      HOL/Algebra/Zassenhaus.thy
```
```     2     Author:     Martin Baillon
```
```     3 *)
```
```     4
```
```     5 section \<open>The Zassenhaus Lemma\<close>
```
```     6
```
```     7 theory Zassenhaus
```
```     8   imports Coset Group_Action
```
```     9 begin
```
```    10
```
```    11 text \<open>Proves the second isomorphism theorem and the Zassenhaus lemma.\<close>
```
```    12
```
```    13 subsection \<open>Lemmas about normalizer\<close>
```
```    14
```
```    15 lemma (in group) subgroup_in_normalizer:
```
```    16   assumes "subgroup H G"
```
```    17   shows "normal H (G\<lparr>carrier:= (normalizer G H)\<rparr>)"
```
```    18 proof(intro group.normal_invI)
```
```    19   show "Group.group (G\<lparr>carrier := normalizer G H\<rparr>)"
```
```    20     by (simp add: assms group.normalizer_imp_subgroup is_group subgroup_imp_group subgroup.subset)
```
```    21   have K:"H \<subseteq> (normalizer G H)" unfolding normalizer_def
```
```    22   proof
```
```    23     fix x assume xH: "x \<in> H"
```
```    24     from xH have xG : "x \<in> carrier G" using subgroup.subset assms by auto
```
```    25     have "x <# H = H"
```
```    26       by (metis \<open>x \<in> H\<close> assms group.lcos_mult_one is_group
```
```    27          l_repr_independence one_closed subgroup.subset)
```
```    28     moreover have "H #> inv x = H"
```
```    29       by (simp add: xH assms is_group subgroup.rcos_const subgroup.m_inv_closed)
```
```    30     ultimately have "x <# H #> (inv x) = H" by simp
```
```    31     thus " x \<in> stabilizer G (\<lambda>g. \<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) H"
```
```    32       using assms xG subgroup.subset unfolding stabilizer_def by auto
```
```    33   qed
```
```    34   thus "subgroup H (G\<lparr>carrier:= (normalizer G H)\<rparr>)"
```
```    35     using subgroup_incl normalizer_imp_subgroup assms by (simp add: subgroup.subset)
```
```    36   show  " \<And>x h. x \<in> carrier (G\<lparr>carrier := normalizer G H\<rparr>) \<Longrightarrow> h \<in> H \<Longrightarrow>
```
```    37              x \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> h
```
```    38                \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> x \<in> H"
```
```    39     proof-
```
```    40     fix x h assume xnorm : "x \<in> carrier (G\<lparr>carrier := normalizer G H\<rparr>)" and hH : "h \<in> H"
```
```    41     have xnormalizer:"x \<in> normalizer G H" using xnorm by simp
```
```    42     moreover have hnormalizer:"h \<in> normalizer G H" using hH K by auto
```
```    43     ultimately have "x \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> h = x \<otimes> h" by simp
```
```    44     moreover have " inv\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> x =  inv x"
```
```    45       using xnormalizer
```
```    46       by (simp add: assms normalizer_imp_subgroup subgroup.subset subgroup_inv_equality)
```
```    47     ultimately  have xhxegal: "x \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> h
```
```    48                 \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> x
```
```    49                   = x \<otimes>h \<otimes> inv x"
```
```    50       using  hnormalizer by simp
```
```    51     have  "x \<otimes>h \<otimes> inv x \<in> (x <# H #> inv x)"
```
```    52       unfolding l_coset_def r_coset_def using hH  by auto
```
```    53     moreover have "x <# H #> inv x = H"
```
```    54       using xnormalizer assms subgroup.subset[OF assms]
```
```    55       unfolding normalizer_def stabilizer_def by auto
```
```    56     ultimately have "x \<otimes>h \<otimes> inv x \<in> H" by simp
```
```    57     thus  " x \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> h
```
```    58                \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> x \<in> H"
```
```    59       using xhxegal hH xnorm by simp
```
```    60   qed
```
```    61 qed
```
```    62
```
```    63
```
```    64 lemma (in group) normal_imp_subgroup_normalizer:
```
```    65   assumes "subgroup H G"
```
```    66     and "N \<lhd> (G\<lparr>carrier := H\<rparr>)"
```
```    67   shows "subgroup H (G\<lparr>carrier := normalizer G N\<rparr>)"
```
```    68 proof-
```
```    69   have N_carrierG : "N \<subseteq> carrier(G)"
```
```    70     using assms normal_imp_subgroup subgroup.subset
```
```    71     by (smt monoid.cases_scheme order_trans partial_object.simps(1) partial_object.update_convs(1))
```
```    72   {have "H \<subseteq> normalizer G N" unfolding normalizer_def stabilizer_def
```
```    73     proof
```
```    74       fix x assume xH : "x \<in> H"
```
```    75       hence xcarrierG : "x \<in> carrier(G)" using assms subgroup.subset  by auto
```
```    76       have "   N #> x = x <# N" using assms xH
```
```    77         unfolding r_coset_def l_coset_def normal_def normal_axioms_def subgroup_imp_group by auto
```
```    78       hence "x <# N #> inv x =(N #> x) #> inv x"
```
```    79         by simp
```
```    80       also have "... = N #> \<one>"
```
```    81         using  assms r_inv xcarrierG coset_mult_assoc[OF N_carrierG] by simp
```
```    82       finally have "x <# N #> inv x = N" by (simp add: N_carrierG)
```
```    83       thus "x \<in> {g \<in> carrier G. (\<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) N = N}"
```
```    84         using xcarrierG by (simp add : N_carrierG)
```
```    85     qed}
```
```    86   thus "subgroup H (G\<lparr>carrier := normalizer G N\<rparr>)"
```
```    87     using subgroup_incl[OF assms(1) normalizer_imp_subgroup]
```
```    88       assms normal_imp_subgroup subgroup.subset
```
```    89     by (metis  group.incl_subgroup is_group)
```
```    90 qed
```
```    91
```
```    92
```
```    93 subsection \<open>Second Isomorphism Theorem\<close>
```
```    94
```
```    95 lemma (in group) mult_norm_subgroup:
```
```    96   assumes "normal N G"
```
```    97     and "subgroup H G"
```
```    98   shows "subgroup (N<#>H) G" unfolding subgroup_def
```
```    99 proof-
```
```   100   have  A :"N <#> H \<subseteq> carrier G"
```
```   101     using assms  setmult_subset_G by (simp add: normal_imp_subgroup subgroup.subset)
```
```   102
```
```   103   have B :"\<And> x y. \<lbrakk>x \<in> (N <#> H); y \<in> (N <#> H)\<rbrakk> \<Longrightarrow> (x \<otimes> y) \<in> (N<#>H)"
```
```   104   proof-
```
```   105     fix x y assume B1a: "x \<in> (N <#> H)"  and B1b: "y \<in> (N <#> H)"
```
```   106     obtain n1 h1 where B2:"n1 \<in> N \<and> h1 \<in> H \<and> n1\<otimes>h1 = x"
```
```   107       using set_mult_def B1a by (metis (no_types, lifting) UN_E singletonD)
```
```   108     obtain n2 h2 where B3:"n2 \<in> N \<and> h2 \<in> H \<and> n2\<otimes>h2 = y"
```
```   109       using set_mult_def B1b by (metis (no_types, lifting) UN_E singletonD)
```
```   110     have "N #> h1 = h1 <# N"
```
```   111       using normalI B2 assms normal.coset_eq subgroup.subset by blast
```
```   112     hence "h1\<otimes>n2 \<in> N #> h1"
```
```   113       using B2 B3 assms l_coset_def by fastforce
```
```   114     from this obtain y2 where y2_def:"y2 \<in> N" and y2_prop:"y2\<otimes>h1 = h1\<otimes>n2"
```
```   115       using singletonD by (metis (no_types, lifting) UN_E r_coset_def)
```
```   116     have " x\<otimes>y =  n1 \<otimes> y2 \<otimes> h1 \<otimes> h2" using y2_def B2 B3
```
```   117       by (smt assms y2_prop m_assoc m_closed normal_imp_subgroup subgroup.mem_carrier)
```
```   118     moreover have B4 :"n1 \<otimes> y2 \<in>N"
```
```   119       using B2 y2_def assms normal_imp_subgroup by (metis subgroup_def)
```
```   120     moreover have "h1 \<otimes> h2 \<in>H" using B2 B3 assms by (simp add: subgroup.m_closed)
```
```   121     hence "(n1 \<otimes> y2) \<otimes> (h1 \<otimes> h2) \<in>(N<#>H) "
```
```   122       using B4  unfolding set_mult_def by auto
```
```   123     hence "n1 \<otimes> y2 \<otimes> h1 \<otimes> h2 \<in>(N<#>H)"
```
```   124       using m_assoc B2 B3 assms  normal_imp_subgroup by (metis B4 subgroup.mem_carrier)
```
```   125     ultimately show  "x \<otimes> y \<in> N <#> H" by auto
```
```   126   qed
```
```   127   have C :"\<And> x. x\<in>(N<#>H)  \<Longrightarrow> (inv x)\<in>(N<#>H)"
```
```   128
```
```   129   proof-
```
```   130     fix x assume C1 : "x \<in> (N<#>H)"
```
```   131     obtain n h where C2:"n \<in> N \<and> h \<in> H \<and> n\<otimes>h = x"
```
```   132       using set_mult_def C1 by (metis (no_types, lifting) UN_E singletonD)
```
```   133     have C3 :"inv(n\<otimes>h) = inv(h)\<otimes>inv(n)"
```
```   134       by (meson C2  assms inv_mult_group normal_imp_subgroup subgroup.mem_carrier)
```
```   135     hence "... \<otimes>h \<in> N"
```
```   136       using assms C2
```
```   137       by (meson normal.inv_op_closed1 normal_def subgroup.m_inv_closed subgroup.mem_carrier)
```
```   138     hence  C4:"(inv h \<otimes> inv n \<otimes> h) \<otimes> inv h \<in> (N<#>H)"
```
```   139       using   C2 assms subgroup.m_inv_closed[of H G h] unfolding set_mult_def by auto
```
```   140     have "inv h \<otimes> inv n \<otimes> h \<otimes> inv h = inv h \<otimes> inv n"
```
```   141       using  subgroup.subset[OF assms(2)]
```
```   142       by (metis A C1 C2 C3 inv_closed inv_solve_right m_closed subsetCE)
```
```   143     thus "inv(x)\<in>N<#>H" using C4 C2 C3 by simp
```
```   144   qed
```
```   145
```
```   146   have D : "\<one> \<in> N <#> H"
```
```   147   proof-
```
```   148     have D1 : "\<one> \<in> N"
```
```   149       using assms by (simp add: normal_def subgroup.one_closed)
```
```   150      have D2 :"\<one> \<in> H"
```
```   151       using assms by (simp add: subgroup.one_closed)
```
```   152     thus "\<one> \<in> (N <#> H)"
```
```   153       using set_mult_def D1 assms by fastforce
```
```   154   qed
```
```   155   thus "(N <#> H \<subseteq> carrier G \<and> (\<forall>x y. x \<in> N <#> H \<longrightarrow> y \<in> N <#> H \<longrightarrow> x \<otimes> y \<in> N <#> H)) \<and>
```
```   156     \<one> \<in> N <#> H \<and> (\<forall>x. x \<in> N <#> H \<longrightarrow> inv x \<in> N <#> H)" using A B C D assms by blast
```
```   157 qed
```
```   158
```
```   159
```
```   160 lemma (in group) mult_norm_sub_in_sub:
```
```   161   assumes "normal N (G\<lparr>carrier:=K\<rparr>)"
```
```   162   assumes "subgroup H (G\<lparr>carrier:=K\<rparr>)"
```
```   163   assumes "subgroup K G"
```
```   164   shows  "subgroup (N<#>H) (G\<lparr>carrier:=K\<rparr>)"
```
```   165 proof-
```
```   166   have Hyp:"subgroup (N <#>\<^bsub>G\<lparr>carrier := K\<rparr>\<^esub> H) (G\<lparr>carrier := K\<rparr>)"
```
```   167     using group.mult_norm_subgroup[where ?G = "G\<lparr>carrier := K\<rparr>"] assms subgroup_imp_group by auto
```
```   168   have "H \<subseteq> carrier(G\<lparr>carrier := K\<rparr>)" using assms subgroup.subset by blast
```
```   169   also have "... \<subseteq> K" by simp
```
```   170   finally have Incl1:"H \<subseteq> K" by simp
```
```   171   have "N \<subseteq> carrier(G\<lparr>carrier := K\<rparr>)" using assms normal_imp_subgroup subgroup.subset by blast
```
```   172   also have "... \<subseteq> K" by simp
```
```   173   finally have Incl2:"N \<subseteq> K" by simp
```
```   174   have "(N <#>\<^bsub>G\<lparr>carrier := K\<rparr>\<^esub> H) = (N <#> H)"
```
```   175     using subgroup_set_mult_equality[of K] assms Incl1 Incl2 by simp
```
```   176   thus "subgroup (N<#>H) (G\<lparr>carrier:=K\<rparr>)" using Hyp by auto
```
```   177 qed
```
```   178
```
```   179
```
```   180 lemma (in group) subgroup_of_normal_set_mult:
```
```   181   assumes "normal N G"
```
```   182 and "subgroup H G"
```
```   183 shows "subgroup H (G\<lparr>carrier := N <#> H\<rparr>)"
```
```   184 proof-
```
```   185   have "\<one> \<in> N" using normal_imp_subgroup assms(1) subgroup_def by blast
```
```   186   hence "\<one> <# H \<subseteq> N <#> H" unfolding set_mult_def l_coset_def by blast
```
```   187   hence H_incl : "H \<subseteq> N <#> H"
```
```   188     by (metis assms(2) lcos_mult_one subgroup_def)
```
```   189   show "subgroup H (G\<lparr>carrier := N <#> H\<rparr>)"
```
```   190   using subgroup_incl[OF assms(2) mult_norm_subgroup[OF assms(1) assms(2)] H_incl] .
```
```   191 qed
```
```   192
```
```   193
```
```   194 lemma (in group) normal_in_normal_set_mult:
```
```   195   assumes "normal N G"
```
```   196 and "subgroup H G"
```
```   197 shows "normal N (G\<lparr>carrier := N <#> H\<rparr>)"
```
```   198 proof-
```
```   199   have "\<one> \<in> H" using  assms(2) subgroup_def by blast
```
```   200   hence "N #> \<one>  \<subseteq> N <#> H" unfolding set_mult_def r_coset_def by blast
```
```   201   hence N_incl : "N \<subseteq> N <#> H"
```
```   202     by (metis assms(1) normal_imp_subgroup coset_mult_one subgroup_def)
```
```   203   thus "normal N (G\<lparr>carrier := N <#> H\<rparr>)"
```
```   204     using normal_inter_subgroup[OF mult_norm_subgroup[OF assms] assms(1)]
```
```   205     by (simp add : inf_absorb1)
```
```   206 qed
```
```   207
```
```   208
```
```   209 proposition (in group) weak_snd_iso_thme:
```
```   210   assumes "subgroup  H G"
```
```   211     and "N\<lhd>G"
```
```   212   shows "(G\<lparr>carrier := N<#>H\<rparr> Mod N \<cong> G\<lparr>carrier:=H\<rparr> Mod (N\<inter>H))"
```
```   213 proof-
```
```   214   define f where "f =  (#>) N"
```
```   215   have GroupNH : "Group.group (G\<lparr>carrier := N<#>H\<rparr>)"
```
```   216     using subgroup_imp_group assms mult_norm_subgroup by simp
```
```   217   have  HcarrierNH :"H \<subseteq> carrier(G\<lparr>carrier := N<#>H\<rparr>)"
```
```   218     using assms subgroup_of_normal_set_mult subgroup.subset by blast
```
```   219   hence HNH :"H \<subseteq> N<#>H" by simp
```
```   220   have op_hom : "f \<in> hom (G\<lparr>carrier := H\<rparr>) (G\<lparr>carrier := N <#> H\<rparr> Mod N)" unfolding hom_def
```
```   221   proof
```
```   222     have "\<And>x . x \<in> carrier (G\<lparr>carrier :=H\<rparr>) \<Longrightarrow>
```
```   223        (#>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub>) N x \<in>  carrier (G\<lparr>carrier := N <#> H\<rparr> Mod N)"
```
```   224     proof-
```
```   225       fix x assume  "x \<in> carrier (G\<lparr>carrier :=H\<rparr>)"
```
```   226       hence xH : "x \<in> H" by simp
```
```   227       hence "(#>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub>) N x \<in> rcosets\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub> N"
```
```   228         using HcarrierNH RCOSETS_def[where ?G = "G\<lparr>carrier := N <#> H\<rparr>"] by blast
```
```   229       thus "(#>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub>) N x \<in>  carrier (G\<lparr>carrier := N <#> H\<rparr> Mod N)"
```
```   230         unfolding FactGroup_def by simp
```
```   231     qed
```
```   232     hence "(#>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub>) N \<in> carrier (G\<lparr>carrier :=H\<rparr>) \<rightarrow>
```
```   233             carrier (G\<lparr>carrier := N <#> H\<rparr> Mod N)" by auto
```
```   234     hence "f \<in> carrier (G\<lparr>carrier :=H\<rparr>) \<rightarrow> carrier (G\<lparr>carrier := N <#> H\<rparr> Mod N)"
```
```   235       unfolding r_coset_def f_def  by simp
```
```   236     moreover have "\<And>x y. x\<in>carrier (G\<lparr>carrier := H\<rparr>) \<Longrightarrow> y\<in>carrier (G\<lparr>carrier := H\<rparr>) \<Longrightarrow>
```
```   237                   f (x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y) =  f(x) \<otimes>\<^bsub>G\<lparr>carrier := N <#> H\<rparr> Mod N\<^esub> f(y)"
```
```   238     proof-
```
```   239       fix x y assume "x\<in>carrier (G\<lparr>carrier := H\<rparr>)" "y\<in>carrier (G\<lparr>carrier := H\<rparr>)"
```
```   240       hence xHyH :"x \<in> H" "y \<in> H" by auto
```
```   241       have Nxeq :"N #>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub> x = N #>x" unfolding r_coset_def by simp
```
```   242       have Nyeq :"N #>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub> y = N #>y" unfolding r_coset_def by simp
```
```   243
```
```   244       have "x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y =x \<otimes>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub> y" by simp
```
```   245       hence "N #>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub> x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y
```
```   246              = N #>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub> x \<otimes>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub> y" by simp
```
```   247       also have "... = (N #>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub> x) <#>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub>
```
```   248                        (N #>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub> y)"
```
```   249         using normal.rcos_sum[OF normal_in_normal_set_mult[OF assms(2) assms(1)], of x y]
```
```   250              xHyH assms HcarrierNH by auto
```
```   251       finally show "f (x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y) =  f(x) \<otimes>\<^bsub>G\<lparr>carrier := N <#> H\<rparr> Mod N\<^esub> f(y)"
```
```   252         unfolding  FactGroup_def r_coset_def f_def  using Nxeq Nyeq  by auto
```
```   253     qed
```
```   254     hence "(\<forall>x\<in>carrier (G\<lparr>carrier := H\<rparr>). \<forall>y\<in>carrier (G\<lparr>carrier := H\<rparr>).
```
```   255            f (x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y) =  f(x) \<otimes>\<^bsub>G\<lparr>carrier := N <#> H\<rparr> Mod N\<^esub> f(y))" by blast
```
```   256     ultimately show  " f \<in> carrier (G\<lparr>carrier := H\<rparr>) \<rightarrow> carrier (G\<lparr>carrier := N <#> H\<rparr> Mod N) \<and>
```
```   257     (\<forall>x\<in>carrier (G\<lparr>carrier := H\<rparr>). \<forall>y\<in>carrier (G\<lparr>carrier := H\<rparr>).
```
```   258      f (x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y) =  f(x) \<otimes>\<^bsub>G\<lparr>carrier := N <#> H\<rparr> Mod N\<^esub> f(y))"
```
```   259       by auto
```
```   260   qed
```
```   261   hence homomorphism : "group_hom (G\<lparr>carrier := H\<rparr>) (G\<lparr>carrier := N <#> H\<rparr> Mod N) f"
```
```   262     unfolding group_hom_def group_hom_axioms_def using subgroup_imp_group[OF assms(1)]
```
```   263              normal.factorgroup_is_group[OF normal_in_normal_set_mult[OF assms(2) assms(1)]] by auto
```
```   264   moreover have im_f :  "(f  ` carrier(G\<lparr>carrier:=H\<rparr>)) = carrier(G\<lparr>carrier := N <#> H\<rparr> Mod N)"
```
```   265   proof
```
```   266     show  "f ` carrier (G\<lparr>carrier := H\<rparr>) \<subseteq> carrier (G\<lparr>carrier := N <#> H\<rparr> Mod N)"
```
```   267       using op_hom unfolding hom_def using funcset_image by blast
```
```   268   next
```
```   269     show "carrier (G\<lparr>carrier := N <#> H\<rparr> Mod N) \<subseteq> f ` carrier (G\<lparr>carrier := H\<rparr>)"
```
```   270     proof
```
```   271       fix x assume p : " x \<in> carrier (G\<lparr>carrier := N <#> H\<rparr> Mod N)"
```
```   272       hence "x \<in> \<Union>{y. \<exists>x\<in>carrier (G\<lparr>carrier := N <#> H\<rparr>). y = {N #>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub> x}}"
```
```   273         unfolding FactGroup_def RCOSETS_def by auto
```
```   274       hence hyp :"\<exists>y. \<exists>h\<in>carrier (G\<lparr>carrier := N <#> H\<rparr>). y = {N #>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub> h} \<and> x \<in> y"
```
```   275         using Union_iff by blast
```
```   276       from hyp obtain nh where nhNH:"nh \<in>carrier (G\<lparr>carrier := N <#> H\<rparr>)"
```
```   277                           and "x \<in> {N #>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub> nh}"
```
```   278         by blast
```
```   279       hence K: "x = (#>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub>) N nh" by simp
```
```   280       have "nh \<in> N <#> H" using nhNH by simp
```
```   281       from this obtain n h where nN : "n \<in> N" and hH : " h \<in> H" and nhnh: "n \<otimes> h = nh"
```
```   282         unfolding set_mult_def by blast
```
```   283       have  "x = (#>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub>) N (n \<otimes> h)" using K nhnh by simp
```
```   284       hence  "x = (#>) N (n \<otimes> h)" using K nhnh unfolding r_coset_def by auto
```
```   285       also have "... = (N #> n) #>h"
```
```   286         using coset_mult_assoc hH nN assms subgroup.subset normal_imp_subgroup
```
```   287         by (metis subgroup.mem_carrier)
```
```   288       finally have "x = (#>) N h"
```
```   289         using coset_join2[of n N] nN assms by (simp add: normal_imp_subgroup subgroup.mem_carrier)
```
```   290       thus "x \<in> f ` carrier (G\<lparr>carrier := H\<rparr>)" using hH unfolding f_def by simp
```
```   291     qed
```
```   292   qed
```
```   293   moreover have ker_f :"kernel (G\<lparr>carrier := H\<rparr>) (G\<lparr>carrier := N<#>H\<rparr> Mod N) f  = N\<inter>H"
```
```   294     unfolding kernel_def f_def
```
```   295     proof-
```
```   296       have "{x \<in> carrier (G\<lparr>carrier := H\<rparr>). N #> x = \<one>\<^bsub>G\<lparr>carrier := N <#> H\<rparr> Mod N\<^esub>} =
```
```   297             {x \<in> carrier (G\<lparr>carrier := H\<rparr>). N #> x = N}" unfolding FactGroup_def by simp
```
```   298       also have "... = {x \<in> carrier (G\<lparr>carrier := H\<rparr>). x \<in> N}"
```
```   299         using coset_join1
```
```   300         by (metis (no_types, lifting) assms group.subgroup_self incl_subgroup is_group
```
```   301           normal_imp_subgroup subgroup.mem_carrier subgroup.rcos_const subgroup_imp_group)
```
```   302       also have "... =N \<inter> (carrier(G\<lparr>carrier := H\<rparr>))" by auto
```
```   303       finally show "{x \<in> carrier (G\<lparr>carrier := H\<rparr>). N#>x = \<one>\<^bsub>G\<lparr>carrier := N <#> H\<rparr> Mod N\<^esub>} = N \<inter> H"
```
```   304         by simp
```
```   305     qed
```
```   306     ultimately have "(G\<lparr>carrier := H\<rparr> Mod N \<inter> H) \<cong> (G\<lparr>carrier := N <#> H\<rparr> Mod N)"
```
```   307       using group_hom.FactGroup_iso[OF homomorphism im_f] by auto
```
```   308     hence "G\<lparr>carrier := N <#> H\<rparr> Mod N \<cong> G\<lparr>carrier := H\<rparr> Mod N \<inter> H"
```
```   309       by (simp add: group.iso_sym assms normal.factorgroup_is_group normal_inter_subgroup)
```
```   310     thus "G\<lparr>carrier := N <#> H\<rparr> Mod N \<cong> G\<lparr>carrier := H\<rparr> Mod N \<inter> H" by auto
```
```   311 qed
```
```   312
```
```   313
```
```   314 theorem (in group) snd_iso_thme:
```
```   315   assumes "subgroup H G"
```
```   316     and "subgroup N G"
```
```   317     and "subgroup H (G\<lparr>carrier:= (normalizer G N)\<rparr>)"
```
```   318   shows "(G\<lparr>carrier:= N<#>H\<rparr> Mod N)  \<cong> (G\<lparr>carrier:= H\<rparr> Mod (H\<inter>N))"
```
```   319 proof-
```
```   320   have "G\<lparr>carrier := normalizer G N, carrier := H\<rparr>
```
```   321        = G\<lparr>carrier := H\<rparr>"  by simp
```
```   322   hence "G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H =
```
```   323          G\<lparr>carrier := H\<rparr> Mod N \<inter> H" by auto
```
```   324   moreover have "G\<lparr>carrier := normalizer G N,
```
```   325                     carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> =
```
```   326                 G\<lparr>carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr>" by simp
```
```   327   hence "G\<lparr>carrier := normalizer G N,
```
```   328           carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> Mod N =
```
```   329           G\<lparr>carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> Mod N" by auto
```
```   330   hence "G\<lparr>carrier := normalizer G N,
```
```   331           carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> Mod N  \<cong>
```
```   332          G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H =
```
```   333           (G\<lparr>carrier:= N<#>H\<rparr> Mod N)  \<cong>
```
```   334          G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H"
```
```   335     using subgroup_set_mult_equality[OF  normalizer_imp_subgroup[OF subgroup.subset[OF assms(2)]], of N H]
```
```   336           subgroup.subset[OF assms(3)]
```
```   337           subgroup.subset[OF normal_imp_subgroup[OF subgroup_in_normalizer[OF assms(2)]]]
```
```   338     by simp
```
```   339   ultimately have "G\<lparr>carrier := normalizer G N,
```
```   340                     carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> Mod N  \<cong>
```
```   341                   G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H =
```
```   342                  (G\<lparr>carrier:= N<#>H\<rparr> Mod N)  \<cong>  G\<lparr>carrier := H\<rparr> Mod N \<inter> H" by auto
```
```   343   moreover have "G\<lparr>carrier := normalizer G N,
```
```   344                     carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> Mod N  \<cong>
```
```   345                   G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H"
```
```   346     using group.weak_snd_iso_thme[OF subgroup_imp_group[OF normalizer_imp_subgroup[OF
```
```   347           subgroup.subset[OF assms(2)]]] assms(3) subgroup_in_normalizer[OF assms(2)]]
```
```   348     by simp
```
```   349   moreover have "H\<inter>N = N\<inter>H" using assms  by auto
```
```   350   ultimately show "(G\<lparr>carrier:= N<#>H\<rparr> Mod N)  \<cong>  G\<lparr>carrier := H\<rparr> Mod H \<inter> N" by auto
```
```   351 qed
```
```   352
```
```   353
```
```   354 corollary (in group) snd_iso_thme_recip :
```
```   355   assumes "subgroup H G"
```
```   356     and "subgroup N G"
```
```   357     and "subgroup H (G\<lparr>carrier:= (normalizer G N)\<rparr>)"
```
```   358   shows "(G\<lparr>carrier:= H<#>N\<rparr> Mod N)  \<cong> (G\<lparr>carrier:= H\<rparr> Mod (H\<inter>N))"
```
```   359   by (metis assms commut_normal_subgroup group.subgroup_in_normalizer is_group subgroup.subset
```
```   360       normalizer_imp_subgroup snd_iso_thme)
```
```   361
```
```   362
```
```   363 subsection\<open>The Zassenhaus Lemma\<close>
```
```   364
```
```   365
```
```   366 lemma (in group) distinc:
```
```   367   assumes "subgroup  H G"
```
```   368     and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
```
```   369     and  "subgroup K G"
```
```   370     and "K1\<lhd>G\<lparr>carrier:=K\<rparr>"
```
```   371   shows "subgroup (H\<inter>K) (G\<lparr>carrier:=(normalizer G (H1<#>(H\<inter>K1))) \<rparr>)"
```
```   372 proof (intro subgroup_incl[OF subgroups_Inter_pair[OF assms(1) assms(3)]])
```
```   373   show "subgroup (normalizer G (H1 <#> H \<inter> K1)) G"
```
```   374     using normalizer_imp_subgroup assms normal_imp_subgroup subgroup.subset
```
```   375     by (metis group.incl_subgroup is_group setmult_subset_G subgroups_Inter_pair)
```
```   376 next
```
```   377   show "H \<inter> K \<subseteq> normalizer G (H1 <#> H \<inter> K1)" unfolding normalizer_def stabilizer_def
```
```   378   proof
```
```   379     fix x assume xHK : "x \<in> H \<inter> K"
```
```   380     hence xG : "{x} \<subseteq> carrier G" "{inv x} \<subseteq> carrier G"
```
```   381       using subgroup.subset assms inv_closed xHK by auto
```
```   382     have allG : "H \<subseteq> carrier G" "K \<subseteq> carrier G" "H1 \<subseteq> carrier G"  "K1 \<subseteq> carrier G"
```
```   383       using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+ .
```
```   384     have HK1_normal: "H\<inter>K1 \<lhd> (G\<lparr>carrier :=  H \<inter> K\<rparr>)" using normal_inter[OF assms(3)assms(1)assms(4)]
```
```   385       by (simp add : inf_commute)
```
```   386     have "H \<inter> K \<subseteq> normalizer G (H \<inter> K1)"
```
```   387       using subgroup.subset[OF normal_imp_subgroup_normalizer[OF subgroups_Inter_pair[OF
```
```   388             assms(1)assms(3)]HK1_normal]] by auto
```
```   389     hence "x <# (H \<inter> K1) #> inv x = (H \<inter> K1)"
```
```   390       using xHK subgroup.subset[OF subgroups_Inter_pair[OF assms(1) incl_subgroup[OF assms(3)
```
```   391                                                             normal_imp_subgroup[OF assms(4)]]]]
```
```   392       unfolding normalizer_def stabilizer_def by auto
```
```   393     moreover have "H \<subseteq>  normalizer G H1"
```
```   394       using subgroup.subset[OF normal_imp_subgroup_normalizer[OF assms(1)assms(2)]] by auto
```
```   395     hence "x <# H1 #> inv x = H1"
```
```   396       using xHK subgroup.subset[OF  incl_subgroup[OF assms(1) normal_imp_subgroup[OF assms(2)]]]
```
```   397       unfolding normalizer_def stabilizer_def by auto
```
```   398     ultimately have "H1 <#> H \<inter> K1 = (x <# H1 #> inv x) <#> (x <#  H \<inter> K1 #> inv x)" by auto
```
```   399     also have "... = ({x} <#> H1) <#> {inv x} <#> ({x} <#>  H \<inter> K1 <#> {inv x})"
```
```   400       by (simp add : r_coset_eq_set_mult l_coset_eq_set_mult)
```
```   401     also have "... = ({x} <#> H1 <#> {inv x} <#> {x}) <#>  (H \<inter> K1 <#> {inv x})"
```
```   402       by (smt Int_lower1 allG xG set_mult_assoc subset_trans setmult_subset_G)
```
```   403     also have "... = ({x} <#> H1 <#> {\<one>}) <#>  (H \<inter> K1 <#> {inv x})"
```
```   404       using allG xG coset_mult_assoc by (simp add: r_coset_eq_set_mult setmult_subset_G)
```
```   405     also have "... =({x} <#> H1) <#>  (H \<inter> K1 <#> {inv x})"
```
```   406       using coset_mult_one r_coset_eq_set_mult[of G H1 \<one>] set_mult_assoc[OF xG(1) allG(3)] allG
```
```   407       by auto
```
```   408     also have "... = {x} <#> (H1 <#> H \<inter> K1) <#> {inv x}"
```
```   409       using allG xG set_mult_assoc setmult_subset_G by (metis inf.coboundedI2)
```
```   410     finally have "H1 <#> H \<inter> K1 = x <# (H1 <#> H \<inter> K1) #> inv x"
```
```   411       using xG setmult_subset_G allG by (simp add: l_coset_eq_set_mult r_coset_eq_set_mult)
```
```   412     thus "x \<in> {g \<in> carrier G. (\<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) (H1 <#> H \<inter> K1)
```
```   413                                                                        = H1 <#> H \<inter> K1}"
```
```   414       using xG allG setmult_subset_G[OF allG(3), where ?K = "H\<inter>K1"] xHK
```
```   415       by auto
```
```   416   qed
```
```   417 qed
```
```   418
```
```   419 lemma (in group) preliminary1:
```
```   420   assumes "subgroup  H G"
```
```   421     and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
```
```   422     and  "subgroup K G"
```
```   423     and "K1\<lhd>G\<lparr>carrier:=K\<rparr>"
```
```   424   shows " (H\<inter>K) \<inter> (H1<#>(H\<inter>K1)) = (H1\<inter>K)<#>(H\<inter>K1)"
```
```   425 proof
```
```   426   have all_inclG : "H \<subseteq> carrier G" "H1 \<subseteq> carrier G" "K \<subseteq> carrier G" "K1 \<subseteq> carrier G"
```
```   427     using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+.
```
```   428   show "H \<inter> K \<inter> (H1 <#> H \<inter> K1) \<subseteq> H1 \<inter> K <#> H \<inter> K1"
```
```   429   proof
```
```   430     fix x assume x_def : "x \<in> (H \<inter> K) \<inter> (H1 <#> (H \<inter> K1))"
```
```   431     from x_def have x_incl : "x \<in> H" "x \<in> K" "x \<in> (H1 <#> (H \<inter> K1))" by auto
```
```   432     then obtain h1 hk1 where h1hk1_def : "h1 \<in> H1" "hk1 \<in> H \<inter> K1" "h1 \<otimes> hk1 = x"
```
```   433       using assms unfolding set_mult_def by blast
```
```   434     hence "hk1 \<in> H \<inter> K" using subgroup.subset[OF normal_imp_subgroup[OF assms(4)]] by auto
```
```   435     hence "inv hk1 \<in> H \<inter> K" using subgroup.m_inv_closed[OF subgroups_Inter_pair] assms by auto
```
```   436     moreover have "h1 \<otimes> hk1 \<in> H \<inter> K" using x_incl h1hk1_def by auto
```
```   437     ultimately have "h1 \<otimes> hk1 \<otimes> inv hk1 \<in> H \<inter> K"
```
```   438       using subgroup.m_closed[OF subgroups_Inter_pair] assms by auto
```
```   439     hence "h1 \<in> H \<inter> K" using  h1hk1_def assms subgroup.subset incl_subgroup normal_imp_subgroup
```
```   440       by (metis Int_iff contra_subsetD inv_solve_right m_closed)
```
```   441     hence "h1 \<in> H1 \<inter> H \<inter> K" using h1hk1_def by auto
```
```   442     hence "h1 \<in> H1 \<inter> K" using subgroup.subset[OF normal_imp_subgroup[OF assms(2)]] by auto
```
```   443     hence "h1 \<otimes> hk1 \<in> (H1\<inter>K)<#>(H\<inter>K1)"
```
```   444       using h1hk1_def unfolding set_mult_def by auto
```
```   445     thus " x \<in> (H1\<inter>K)<#>(H\<inter>K1)" using h1hk1_def x_def by auto
```
```   446   qed
```
```   447   show "H1 \<inter> K <#> H \<inter> K1 \<subseteq> H \<inter> K \<inter> (H1 <#> H \<inter> K1)"
```
```   448   proof-
```
```   449     have "H1 \<inter> K \<subseteq> H \<inter> K" using subgroup.subset[OF normal_imp_subgroup[OF assms(2)]] by auto
```
```   450     moreover have "H \<inter> K1 \<subseteq> H \<inter> K"
```
```   451       using subgroup.subset[OF normal_imp_subgroup[OF assms(4)]] by auto
```
```   452     ultimately have "H1 \<inter> K <#> H \<inter> K1 \<subseteq> H \<inter> K" unfolding set_mult_def
```
```   453       using subgroup.m_closed[OF subgroups_Inter_pair [OF assms(1)assms(3)]] by blast
```
```   454     moreover have "H1 \<inter> K \<subseteq> H1" by auto
```
```   455     hence "H1 \<inter> K <#> H \<inter> K1 \<subseteq> (H1 <#> H \<inter> K1)" unfolding set_mult_def by auto
```
```   456     ultimately show "H1 \<inter> K <#> H \<inter> K1 \<subseteq> H \<inter> K \<inter> (H1 <#> H \<inter> K1)" by auto
```
```   457   qed
```
```   458 qed
```
```   459
```
```   460 lemma (in group) preliminary2:
```
```   461   assumes "subgroup  H G"
```
```   462     and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
```
```   463     and  "subgroup K G"
```
```   464     and "K1\<lhd>G\<lparr>carrier:=K\<rparr>"
```
```   465   shows "(H1<#>(H\<inter>K1)) \<lhd> G\<lparr>carrier:=(H1<#>(H\<inter>K))\<rparr>"
```
```   466 proof-
```
```   467   have all_inclG : "H \<subseteq> carrier G" "H1 \<subseteq> carrier G" "K \<subseteq> carrier G" "K1 \<subseteq> carrier G"
```
```   468     using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+.
```
```   469   have subH1:"subgroup (H1 <#> H \<inter> K) (G\<lparr>carrier := H\<rparr>)"
```
```   470     using mult_norm_sub_in_sub[OF assms(2)subgroup_incl[OF subgroups_Inter_pair[OF assms(1)assms(3)]
```
```   471           assms(1)]] assms by auto
```
```   472   have "Group.group (G\<lparr>carrier:=(H1<#>(H\<inter>K))\<rparr>)"
```
```   473     using  subgroup_imp_group[OF incl_subgroup[OF assms(1) subH1]].
```
```   474   moreover have subH2 : "subgroup (H1 <#> H \<inter> K1) (G\<lparr>carrier := H\<rparr>)"
```
```   475     using mult_norm_sub_in_sub[OF assms(2) subgroup_incl[OF subgroups_Inter_pair[OF
```
```   476            assms(1) incl_subgroup[OF assms(3)normal_imp_subgroup[OF assms(4)]]]]] assms by auto
```
```   477   hence "(H\<inter>K1) \<subseteq> (H\<inter>K)"
```
```   478     using assms subgroup.subset normal_imp_subgroup monoid.cases_scheme
```
```   479     by (metis inf.mono  partial_object.simps(1) partial_object.update_convs(1) subset_refl)
```
```   480   hence incl:"(H1<#>(H\<inter>K1)) \<subseteq> H1<#>(H\<inter>K)" using assms subgroup.subset normal_imp_subgroup
```
```   481     unfolding set_mult_def by blast
```
```   482   hence "subgroup (H1 <#> H \<inter> K1) (G\<lparr>carrier := (H1<#>(H\<inter>K))\<rparr>)"
```
```   483     using assms subgroup_incl[OF incl_subgroup[OF assms(1)subH2]incl_subgroup[OF assms(1)
```
```   484           subH1]] normal_imp_subgroup subgroup.subset unfolding set_mult_def by blast
```
```   485   moreover have " (\<And> x. x\<in>carrier (G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>) \<Longrightarrow>
```
```   486         H1 <#> H\<inter>K1 #>\<^bsub>G\<lparr>carrier := H1 <#> H\<inter>K\<rparr>\<^esub> x = x <#\<^bsub>G\<lparr>carrier := H1 <#> H\<inter>K\<rparr>\<^esub> (H1 <#> H\<inter>K1))"
```
```   487   proof-
```
```   488     fix x assume  "x \<in>carrier (G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>)"
```
```   489     hence x_def : "x \<in> H1 <#> H \<inter> K" by simp
```
```   490     from this obtain h1 hk where h1hk_def :"h1 \<in> H1" "hk \<in> H \<inter> K" "h1 \<otimes> hk = x"
```
```   491       unfolding set_mult_def by blast
```
```   492     have xH : "x \<in> H" using subgroup.subset[OF subH1] using x_def by auto
```
```   493     hence allG : "h1 \<in> carrier G" "hk \<in> carrier G" "x \<in> carrier G"
```
```   494       using assms subgroup.subset h1hk_def normal_imp_subgroup incl_subgroup apply blast+.
```
```   495     hence "x <#\<^bsub>G\<lparr>carrier := H1 <#> H\<inter>K\<rparr>\<^esub> (H1 <#> H\<inter>K1) =h1 \<otimes> hk <# (H1 <#> H\<inter>K1)"
```
```   496       using subgroup_set_mult_equality subgroup.subset xH h1hk_def by (simp add: l_coset_def)
```
```   497     also have "... = h1 <# (hk <# (H1 <#> H\<inter>K1))"
```
```   498       using lcos_m_assoc[OF subgroup.subset[OF incl_subgroup[OF assms(1) subH1]]allG(1)allG(2)]
```
```   499       by (metis allG(1) allG(2) assms(1) incl_subgroup lcos_m_assoc subH2 subgroup.subset)
```
```   500     also have "... = h1 <# (hk <# H1 <#> H\<inter>K1)"
```
```   501       using set_mult_assoc all_inclG allG by (simp add: l_coset_eq_set_mult inf.coboundedI1)
```
```   502     also have "... = h1 <# (hk <# H1 #> \<one> <#> H\<inter>K1 #> \<one>)"
```
```   503       using coset_mult_one allG all_inclG l_coset_subset_G
```
```   504       by (smt inf_le2 setmult_subset_G subset_trans)
```
```   505     also have "... = h1 <# (hk <# H1 #> inv hk #> hk <#> H\<inter>K1 #> inv hk #> hk)"
```
```   506       using all_inclG allG coset_mult_assoc l_coset_subset_G
```
```   507       by (simp add: inf.coboundedI1 setmult_subset_G)
```
```   508     finally  have "x <#\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> (H1 <#> H \<inter> K1) =
```
```   509                     h1 <# ((hk <# H1 #> inv hk) <#> (hk <# H\<inter>K1 #> inv hk) #> hk)"
```
```   510       using rcos_assoc_lcos allG all_inclG
```
```   511       by (smt inf_le1 inv_closed l_coset_subset_G r_coset_subset_G setmult_rcos_assoc subset_trans)
```
```   512     moreover have "H \<subseteq>  normalizer G H1"
```
```   513       using assms h1hk_def subgroup.subset[OF normal_imp_subgroup_normalizer] by simp
```
```   514     hence "\<And>g. g \<in> H \<Longrightarrow>  g \<in> {g \<in> carrier G. (\<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) H1 = H1}"
```
```   515       using all_inclG assms unfolding normalizer_def stabilizer_def by auto
```
```   516     hence "\<And>g. g \<in> H \<Longrightarrow>  g <# H1 #> inv g = H1" using all_inclG by simp
```
```   517     hence "(hk <# H1 #> inv hk) = H1" using h1hk_def all_inclG by simp
```
```   518     moreover have "H\<inter>K \<subseteq> normalizer G (H\<inter>K1)"
```
```   519       using normal_inter[OF assms(3)assms(1)assms(4)] assms subgroups_Inter_pair
```
```   520             subgroup.subset[OF normal_imp_subgroup_normalizer] by (simp add: inf_commute)
```
```   521     hence "\<And>g. g\<in>H\<inter>K \<Longrightarrow> g\<in>{g\<in>carrier G. (\<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) (H\<inter>K1) = H\<inter>K1}"
```
```   522       using all_inclG assms unfolding normalizer_def stabilizer_def by auto
```
```   523     hence "\<And>g. g \<in> H\<inter>K \<Longrightarrow>  g <# (H\<inter>K1) #> inv g = H\<inter>K1"
```
```   524       using subgroup.subset[OF subgroups_Inter_pair[OF assms(1) incl_subgroup[OF
```
```   525             assms(3)normal_imp_subgroup[OF assms(4)]]]] by auto
```
```   526     hence "(hk <# H\<inter>K1 #> inv hk) = H\<inter>K1" using h1hk_def by simp
```
```   527     ultimately have "x <#\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> (H1 <#> H \<inter> K1) = h1 <#(H1 <#> (H \<inter> K1)#> hk)"
```
```   528       by auto
```
```   529     also have "... = h1 <# H1 <#> ((H \<inter> K1)#> hk)"
```
```   530       using set_mult_assoc[where ?M = "{h1}" and ?H = "H1" and ?K = "(H \<inter> K1)#> hk"] allG all_inclG
```
```   531       by (simp add: l_coset_eq_set_mult inf.coboundedI2 r_coset_subset_G setmult_rcos_assoc)
```
```   532     also have "... = H1 <#> ((H \<inter> K1)#> hk)"
```
```   533       using coset_join3 allG incl_subgroup[OF assms(1)normal_imp_subgroup[OF assms(2)]] h1hk_def
```
```   534       by auto
```
```   535     finally have eq1 : "x <#\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> (H1 <#> H \<inter> K1) = H1 <#> (H \<inter> K1) #> hk"
```
```   536       by (simp add: allG(2) all_inclG inf.coboundedI2 setmult_rcos_assoc)
```
```   537     have "H1 <#> H \<inter> K1 #>\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> x = H1 <#> H \<inter> K1 #> (h1 \<otimes> hk)"
```
```   538       using subgroup_set_mult_equality subgroup.subset xH h1hk_def by (simp add: r_coset_def)
```
```   539     also have "... = H1 <#> H \<inter> K1 #> h1 #> hk"
```
```   540       using coset_mult_assoc by (simp add: allG all_inclG inf.coboundedI2 setmult_subset_G)
```
```   541     also have"... =  H \<inter> K1 <#> H1 #> h1 #> hk"
```
```   542       using commut_normal_subgroup[OF assms(1)assms(2)subgroup_incl[OF subgroups_Inter_pair[OF
```
```   543            assms(1)incl_subgroup[OF assms(3)normal_imp_subgroup[OF assms(4)]]]assms(1)]] by simp
```
```   544     also have "... = H \<inter> K1 <#> H1  #> hk"
```
```   545       using coset_join2[OF allG(1)incl_subgroup[OF assms(1)normal_imp_subgroup]
```
```   546             h1hk_def(1)] all_inclG allG assms by (metis inf.coboundedI2 setmult_rcos_assoc)
```
```   547     finally  have "H1 <#> H \<inter> K1 #>\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> x =H1 <#> H \<inter> K1  #> hk"
```
```   548       using commut_normal_subgroup[OF assms(1)assms(2)subgroup_incl[OF subgroups_Inter_pair[OF
```
```   549            assms(1)incl_subgroup[OF assms(3)normal_imp_subgroup[OF assms(4)]]]assms(1)]] by simp
```
```   550     thus " H1 <#> H \<inter> K1 #>\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> x =
```
```   551              x <#\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> (H1 <#> H \<inter> K1)" using eq1 by simp
```
```   552   qed
```
```   553   ultimately show "H1 <#> H \<inter> K1 \<lhd> G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>"
```
```   554     unfolding normal_def normal_axioms_def by auto
```
```   555 qed
```
```   556
```
```   557
```
```   558 proposition (in group)  Zassenhaus_1:
```
```   559   assumes "subgroup  H G"
```
```   560     and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
```
```   561     and  "subgroup K G"
```
```   562     and "K1\<lhd>G\<lparr>carrier:=K\<rparr>"
```
```   563   shows "(G\<lparr>carrier:= H1 <#> (H\<inter>K)\<rparr> Mod (H1<#>H\<inter>K1)) \<cong> (G\<lparr>carrier:= (H\<inter>K)\<rparr> Mod  ((H1\<inter>K)<#>(H\<inter>K1)))"
```
```   564 proof-
```
```   565   define N  and N1 where "N = (H\<inter>K)" and "N1 =H1<#>(H\<inter>K1)"
```
```   566   have normal_N_N1 : "subgroup N (G\<lparr>carrier:=(normalizer G N1)\<rparr>)"
```
```   567     by (simp add: N1_def N_def assms distinc normal_imp_subgroup)
```
```   568   have Hp:"(G\<lparr>carrier:= N<#>N1\<rparr> Mod N1)  \<cong> (G\<lparr>carrier:= N\<rparr> Mod (N\<inter>N1))"
```
```   569   by (metis N1_def N_def assms incl_subgroup inf_le1 mult_norm_sub_in_sub
```
```   570         normal_N_N1 normal_imp_subgroup snd_iso_thme_recip subgroup_incl subgroups_Inter_pair)
```
```   571   have H_simp: "N<#>N1 = H1<#> (H\<inter>K)"
```
```   572   proof-
```
```   573     have H1_incl_G : "H1 \<subseteq> carrier G"
```
```   574       using assms normal_imp_subgroup incl_subgroup subgroup.subset by blast
```
```   575     have K1_incl_G :"K1 \<subseteq> carrier G"
```
```   576       using assms normal_imp_subgroup incl_subgroup subgroup.subset by blast
```
```   577     have "N<#>N1=  (H\<inter>K)<#> (H1<#>(H\<inter>K1))" by (auto simp add: N_def N1_def)
```
```   578     also have "... = ((H\<inter>K)<#>H1) <#>(H\<inter>K1)"
```
```   579       using set_mult_assoc[where ?M = "H\<inter>K"] K1_incl_G H1_incl_G assms
```
```   580       by (simp add: inf.coboundedI2 subgroup.subset)
```
```   581     also have "... = (H1<#>(H\<inter>K))<#>(H\<inter>K1)"
```
```   582       using commut_normal_subgroup assms subgroup_incl subgroups_Inter_pair by auto
```
```   583     also have "... =  H1 <#> ((H\<inter>K)<#>(H\<inter>K1))"
```
```   584       using set_mult_assoc K1_incl_G H1_incl_G assms
```
```   585       by (simp add: inf.coboundedI2 subgroup.subset)
```
```   586     also have " ((H\<inter>K)<#>(H\<inter>K1)) = (H\<inter>K)"
```
```   587     proof (intro set_mult_subgroup_idem[where ?H = "H\<inter>K" and ?N="H\<inter>K1",
```
```   588              OF subgroups_Inter_pair[OF assms(1) assms(3)]])
```
```   589       show "subgroup (H \<inter> K1) (G\<lparr>carrier := H \<inter> K\<rparr>)"
```
```   590         using subgroup_incl[where ?I = "H\<inter>K1" and ?J = "H\<inter>K",OF subgroups_Inter_pair[OF assms(1)
```
```   591               incl_subgroup[OF assms(3) normal_imp_subgroup]] subgroups_Inter_pair] assms
```
```   592               normal_imp_subgroup by (metis inf_commute normal_inter)
```
```   593     qed
```
```   594     hence " H1 <#> ((H\<inter>K)<#>(H\<inter>K1)) =  H1 <#> ((H\<inter>K))"
```
```   595       by simp
```
```   596     thus "N <#> N1 = H1 <#> H \<inter> K"
```
```   597       by (simp add: calculation)
```
```   598   qed
```
```   599
```
```   600   have "N\<inter>N1 = (H1\<inter>K)<#>(H\<inter>K1)"
```
```   601     using preliminary1 assms N_def N1_def by simp
```
```   602   thus  "(G\<lparr>carrier:= H1 <#> (H\<inter>K)\<rparr> Mod N1)  \<cong> (G\<lparr>carrier:= N\<rparr> Mod  ((H1\<inter>K)<#>(H\<inter>K1)))"
```
```   603     using H_simp Hp by auto
```
```   604 qed
```
```   605
```
```   606
```
```   607 theorem (in group) Zassenhaus:
```
```   608   assumes "subgroup  H G"
```
```   609     and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
```
```   610     and  "subgroup K G"
```
```   611     and "K1\<lhd>G\<lparr>carrier:=K\<rparr>"
```
```   612   shows "(G\<lparr>carrier:= H1 <#> (H\<inter>K)\<rparr> Mod (H1<#>(H\<inter>K1)))  \<cong>
```
```   613          (G\<lparr>carrier:= K1 <#> (H\<inter>K)\<rparr> Mod (K1<#>(K\<inter>H1)))"
```
```   614 proof-
```
```   615   define Gmod1 Gmod2 Gmod3 Gmod4
```
```   616     where "Gmod1 = (G\<lparr>carrier:= H1 <#> (H\<inter>K)\<rparr> Mod (H1<#>(H\<inter>K1))) "
```
```   617       and "Gmod2 = (G\<lparr>carrier:= K1 <#> (K\<inter>H)\<rparr> Mod (K1<#>(K\<inter>H1)))"
```
```   618       and "Gmod3 = (G\<lparr>carrier:= (H\<inter>K)\<rparr> Mod  ((H1\<inter>K)<#>(H\<inter>K1)))"
```
```   619       and "Gmod4 = (G\<lparr>carrier:= (K\<inter>H)\<rparr> Mod  ((K1\<inter>H)<#>(K\<inter>H1)))"
```
```   620   have Hyp :  "Gmod1  \<cong> Gmod3" "Gmod2  \<cong>  Gmod4"
```
```   621     using Zassenhaus_1 assms Gmod1_def Gmod2_def Gmod3_def Gmod4_def by auto
```
```   622   have Hp : "Gmod3 = G\<lparr>carrier:= (K\<inter>H)\<rparr> Mod ((K\<inter>H1)<#>(K1\<inter>H))"
```
```   623     by (simp add: Gmod3_def inf_commute)
```
```   624   have "(K\<inter>H1)<#>(K1\<inter>H) = (K1\<inter>H)<#>(K\<inter>H1)"
```
```   625   proof (intro commut_normal_subgroup[OF subgroups_Inter_pair[OF assms(1)assms(3)]])
```
```   626     show "K1 \<inter> H \<lhd> G\<lparr>carrier := H \<inter> K\<rparr>"
```
```   627       using normal_inter[OF assms(3)assms(1)assms(4)] by (simp add: inf_commute)
```
```   628    next
```
```   629     show "subgroup (K \<inter> H1) (G\<lparr>carrier := H \<inter> K\<rparr>)"
```
```   630       using subgroup_incl by (simp add: assms inf_commute normal_imp_subgroup normal_inter)
```
```   631   qed
```
```   632   hence  "Gmod3  = Gmod4" using Hp Gmod4_def by simp
```
```   633   hence "Gmod1 \<cong> Gmod2"
```
```   634     using group.iso_sym group.iso_trans Hyp normal.factorgroup_is_group
```
```   635     by (metis assms Gmod1_def Gmod2_def preliminary2)
```
```   636   thus ?thesis using Gmod1_def Gmod2_def by (simp add: inf_commute)
```
```   637 qed
```
```   638
```
```   639 end
```