66 and "N \<lhd> (G\<lparr>carrier := H\<rparr>)" |
66 and "N \<lhd> (G\<lparr>carrier := H\<rparr>)" |
67 shows "subgroup H (G\<lparr>carrier := normalizer G N\<rparr>)" |
67 shows "subgroup H (G\<lparr>carrier := normalizer G N\<rparr>)" |
68 proof- |
68 proof- |
69 have N_carrierG : "N \<subseteq> carrier(G)" |
69 have N_carrierG : "N \<subseteq> carrier(G)" |
70 using assms normal_imp_subgroup subgroup.subset |
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)) |
71 using incl_subgroup by blast |
72 {have "H \<subseteq> normalizer G N" unfolding normalizer_def stabilizer_def |
72 {have "H \<subseteq> normalizer G N" unfolding normalizer_def stabilizer_def |
73 proof |
73 proof |
74 fix x assume xH : "x \<in> H" |
74 fix x assume xH : "x \<in> H" |
75 hence xcarrierG : "x \<in> carrier(G)" using assms subgroup.subset by auto |
75 hence xcarrierG : "x \<in> carrier(G)" using assms subgroup.subset by auto |
76 have " N #> x = x <# N" using assms xH |
76 have " N #> x = x <# N" using assms xH |
111 using normalI B2 assms normal.coset_eq subgroup.subset by blast |
111 using normalI B2 assms normal.coset_eq subgroup.subset by blast |
112 hence "h1\<otimes>n2 \<in> N #> h1" |
112 hence "h1\<otimes>n2 \<in> N #> h1" |
113 using B2 B3 assms l_coset_def by fastforce |
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" |
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) |
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 |
116 have "\<And>a. a \<in> N \<Longrightarrow> a \<in> carrier G" "\<And>a. a \<in> H \<Longrightarrow> a \<in> carrier G" |
117 by (smt assms y2_prop m_assoc m_closed normal_imp_subgroup subgroup.mem_carrier) |
117 by (meson assms normal_def subgroup.mem_carrier)+ |
|
118 then have "x\<otimes>y = n1 \<otimes> y2 \<otimes> h1 \<otimes> h2" using y2_def B2 B3 |
|
119 by (metis (no_types) B2 B3 \<open>\<And>a. a \<in> N \<Longrightarrow> a \<in> carrier G\<close> m_assoc m_closed y2_def y2_prop) |
118 moreover have B4 :"n1 \<otimes> y2 \<in>N" |
120 moreover have B4 :"n1 \<otimes> y2 \<in>N" |
119 using B2 y2_def assms normal_imp_subgroup by (metis subgroup_def) |
121 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) |
122 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) " |
123 hence "(n1 \<otimes> y2) \<otimes> (h1 \<otimes> h2) \<in>(N<#>H) " |
122 using B4 unfolding set_mult_def by auto |
124 using B4 unfolding set_mult_def by auto |