70 by force |
70 by force |
71 |
71 |
72 lemma (in sylow_central) exists_x_in_M1: "\<exists>x. x\<in>M1" |
72 lemma (in sylow_central) exists_x_in_M1: "\<exists>x. x\<in>M1" |
73 apply (subgoal_tac "0 < card M1") |
73 apply (subgoal_tac "0 < card M1") |
74 apply (blast dest: card_nonempty) |
74 apply (blast dest: card_nonempty) |
75 apply (cut_tac prime_p [THEN prime_imp_one_less]) |
75 apply (cut_tac prime_p [THEN prime_gt_Suc_0_nat]) |
76 apply (simp (no_asm_simp) add: card_M1) |
76 apply (simp (no_asm_simp) add: card_M1) |
77 done |
77 done |
78 |
78 |
79 lemma (in sylow_central) M1_subset_G [simp]: "M1 \<subseteq> carrier G" |
79 lemma (in sylow_central) M1_subset_G [simp]: "M1 \<subseteq> carrier G" |
80 apply (rule subsetD [THEN PowD]) |
80 apply (rule subsetD [THEN PowD]) |
206 "g \<in> carrier G ==> card(M1 #> g) = card(M1)" |
206 "g \<in> carrier G ==> card(M1 #> g) = card(M1)" |
207 by (simp (no_asm_simp) add: card_cosets_equal rcosetsI) |
207 by (simp (no_asm_simp) add: card_cosets_equal rcosetsI) |
208 |
208 |
209 lemma (in sylow_central) M1_RelM_rcosetGM1g: |
209 lemma (in sylow_central) M1_RelM_rcosetGM1g: |
210 "g \<in> carrier G ==> (M1, M1 #> g) \<in> RelM" |
210 "g \<in> carrier G ==> (M1, M1 #> g) \<in> RelM" |
211 apply (simp (no_asm) add: RelM_def calM_def card_M1) |
211 apply (simp add: RelM_def calM_def card_M1) |
212 apply (rule conjI) |
212 apply (rule conjI) |
213 apply (blast intro: rcosetGM1g_subset_G) |
213 apply (blast intro: rcosetGM1g_subset_G) |
214 apply (simp (no_asm_simp) add: card_M1 M1_cardeq_rcosetGM1g) |
214 apply (simp add: card_M1 M1_cardeq_rcosetGM1g) |
215 apply (rule bexI [of _ "inv g"]) |
215 apply (metis M1_subset_G coset_mult_assoc coset_mult_one r_inv_ex) |
216 apply (simp_all add: coset_mult_assoc) |
|
217 done |
216 done |
218 |
217 |
219 |
218 |
220 subsection{*Equal Cardinalities of @{term M} and the Set of Cosets*} |
219 subsection{*Equal Cardinalities of @{term M} and the Set of Cosets*} |
221 |
220 |
239 lemmas (in sylow_central) M_elem_map_eq = |
238 lemmas (in sylow_central) M_elem_map_eq = |
240 M_elem_map [THEN someI_ex, THEN conjunct2] |
239 M_elem_map [THEN someI_ex, THEN conjunct2] |
241 |
240 |
242 lemma (in sylow_central) M_funcset_rcosets_H: |
241 lemma (in sylow_central) M_funcset_rcosets_H: |
243 "(%x:M. H #> (SOME g. g \<in> carrier G & M1 #> g = x)) \<in> M \<rightarrow> rcosets H" |
242 "(%x:M. H #> (SOME g. g \<in> carrier G & M1 #> g = x)) \<in> M \<rightarrow> rcosets H" |
244 apply (rule rcosetsI [THEN restrictI]) |
243 by (metis (lifting) H_is_subgroup M_elem_map_carrier rcosetsI restrictI subgroup_imp_subset) |
245 apply (rule H_is_subgroup [THEN subgroup.subset]) |
|
246 apply (erule M_elem_map_carrier) |
|
247 done |
|
248 |
244 |
249 lemma (in sylow_central) inj_M_GmodH: "\<exists>f \<in> M\<rightarrow>rcosets H. inj_on f M" |
245 lemma (in sylow_central) inj_M_GmodH: "\<exists>f \<in> M\<rightarrow>rcosets H. inj_on f M" |
250 apply (rule bexI) |
246 apply (rule bexI) |
251 apply (rule_tac [2] M_funcset_rcosets_H) |
247 apply (rule_tac [2] M_funcset_rcosets_H) |
252 apply (rule inj_onI, simp) |
248 apply (rule inj_onI, simp) |
273 H_elem_map [THEN someI_ex, THEN conjunct1] |
269 H_elem_map [THEN someI_ex, THEN conjunct1] |
274 |
270 |
275 lemmas (in sylow_central) H_elem_map_eq = |
271 lemmas (in sylow_central) H_elem_map_eq = |
276 H_elem_map [THEN someI_ex, THEN conjunct2] |
272 H_elem_map [THEN someI_ex, THEN conjunct2] |
277 |
273 |
278 |
|
279 lemma EquivElemClass: |
|
280 "[|equiv A r; M \<in> A//r; M1\<in>M; (M1,M2) \<in> r |] ==> M2 \<in> M" |
|
281 by (unfold equiv_def quotient_def sym_def trans_def, blast) |
|
282 |
|
283 |
|
284 lemma (in sylow_central) rcosets_H_funcset_M: |
274 lemma (in sylow_central) rcosets_H_funcset_M: |
285 "(\<lambda>C \<in> rcosets H. M1 #> (@g. g \<in> carrier G \<and> H #> g = C)) \<in> rcosets H \<rightarrow> M" |
275 "(\<lambda>C \<in> rcosets H. M1 #> (@g. g \<in> carrier G \<and> H #> g = C)) \<in> rcosets H \<rightarrow> M" |
286 apply (simp add: RCOSETS_def) |
276 apply (simp add: RCOSETS_def) |
287 apply (fast intro: someI2 |
277 apply (fast intro: someI2 |
288 intro!: M1_in_M EquivElemClass [OF RelM_equiv M_in_quot _ M1_RelM_rcosetGM1g]) |
278 intro!: M1_in_M in_quotient_imp_closed [OF RelM_equiv M_in_quot _ M1_RelM_rcosetGM1g]) |
289 done |
279 done |
290 |
280 |
291 text{*close to a duplicate of @{text inj_M_GmodH}*} |
281 text{*close to a duplicate of @{text inj_M_GmodH}*} |
292 lemma (in sylow_central) inj_GmodH_M: |
282 lemma (in sylow_central) inj_GmodH_M: |
293 "\<exists>g \<in> rcosets H\<rightarrow>M. inj_on g (rcosets H)" |
283 "\<exists>g \<in> rcosets H\<rightarrow>M. inj_on g (rcosets H)" |
310 lemma (in sylow_central) calM_subset_PowG: "calM \<subseteq> Pow(carrier G)" |
300 lemma (in sylow_central) calM_subset_PowG: "calM \<subseteq> Pow(carrier G)" |
311 by (auto simp add: calM_def) |
301 by (auto simp add: calM_def) |
312 |
302 |
313 |
303 |
314 lemma (in sylow_central) finite_M: "finite M" |
304 lemma (in sylow_central) finite_M: "finite M" |
315 apply (rule finite_subset) |
305 by (metis M_subset_calM finite_calM rev_finite_subset) |
316 apply (rule M_subset_calM [THEN subset_trans]) |
|
317 apply (rule calM_subset_PowG, blast) |
|
318 done |
|
319 |
306 |
320 lemma (in sylow_central) cardMeqIndexH: "card(M) = card(rcosets H)" |
307 lemma (in sylow_central) cardMeqIndexH: "card(M) = card(rcosets H)" |
321 apply (insert inj_M_GmodH inj_GmodH_M) |
308 apply (insert inj_M_GmodH inj_GmodH_M) |
322 apply (blast intro: card_bij finite_M H_is_subgroup |
309 apply (blast intro: card_bij finite_M H_is_subgroup |
323 rcosets_subset_PowG [THEN finite_subset] |
310 rcosets_subset_PowG [THEN finite_subset] |