204 apply (rule finite_G) |
204 apply (rule finite_G) |
205 done |
205 done |
206 |
206 |
207 lemma (in sylow_central) M1_cardeq_rcosetGM1g: |
207 lemma (in sylow_central) M1_cardeq_rcosetGM1g: |
208 "g \<in> carrier G ==> card(M1 #> g) = card(M1)" |
208 "g \<in> carrier G ==> card(M1 #> g) = card(M1)" |
209 by (simp (no_asm_simp) add: M1_subset_G card_cosets_equal setrcosI) |
209 by (simp (no_asm_simp) add: M1_subset_G card_cosets_equal rcosetsI) |
210 |
210 |
211 lemma (in sylow_central) M1_RelM_rcosetGM1g: |
211 lemma (in sylow_central) M1_RelM_rcosetGM1g: |
212 "g \<in> carrier G ==> (M1, M1 #> g) \<in> RelM" |
212 "g \<in> carrier G ==> (M1, M1 #> g) \<in> RelM" |
213 apply (simp (no_asm) add: RelM_def calM_def card_M1 M1_subset_G) |
213 apply (simp (no_asm) add: RelM_def calM_def card_M1 M1_subset_G) |
214 apply (rule conjI) |
214 apply (rule conjI) |
217 apply (rule bexI [of _ "inv g"]) |
217 apply (rule bexI [of _ "inv g"]) |
218 apply (simp_all add: coset_mult_assoc M1_subset_G) |
218 apply (simp_all add: coset_mult_assoc M1_subset_G) |
219 done |
219 done |
220 |
220 |
221 |
221 |
222 |
222 subsection{*Equal Cardinalities of @{term M} and the Set of Cosets*} |
223 subsection{*Equal Cardinalities of @{term M} and @{term "rcosets G H"}*} |
223 |
224 |
224 text{*Injections between @{term M} and @{term "rcosets\<^bsub>G\<^esub> H"} show that |
225 text{*Injections between @{term M} and @{term "rcosets G H"} show that |
|
226 their cardinalities are equal.*} |
225 their cardinalities are equal.*} |
227 |
226 |
228 lemma ElemClassEquiv: |
227 lemma ElemClassEquiv: |
229 "[| equiv A r; C\<in>A // r |] ==> \<forall>x \<in> C. \<forall>y \<in> C. (x,y)\<in>r" |
228 "[| equiv A r; C \<in> A // r |] ==> \<forall>x \<in> C. \<forall>y \<in> C. (x,y)\<in>r" |
230 apply (unfold equiv_def quotient_def sym_def trans_def, blast) |
229 by (unfold equiv_def quotient_def sym_def trans_def, blast) |
231 done |
|
232 |
230 |
233 lemma (in sylow_central) M_elem_map: |
231 lemma (in sylow_central) M_elem_map: |
234 "M2 \<in> M ==> \<exists>g. g \<in> carrier G & M1 #> g = M2" |
232 "M2 \<in> M ==> \<exists>g. g \<in> carrier G & M1 #> g = M2" |
235 apply (cut_tac M1_in_M M_in_quot [THEN RelM_equiv [THEN ElemClassEquiv]]) |
233 apply (cut_tac M1_in_M M_in_quot [THEN RelM_equiv [THEN ElemClassEquiv]]) |
236 apply (simp add: RelM_def) |
234 apply (simp add: RelM_def) |
241 M_elem_map [THEN someI_ex, THEN conjunct1] |
239 M_elem_map [THEN someI_ex, THEN conjunct1] |
242 |
240 |
243 lemmas (in sylow_central) M_elem_map_eq = |
241 lemmas (in sylow_central) M_elem_map_eq = |
244 M_elem_map [THEN someI_ex, THEN conjunct2] |
242 M_elem_map [THEN someI_ex, THEN conjunct2] |
245 |
243 |
246 lemma (in sylow_central) M_funcset_setrcos_H: |
244 lemma (in sylow_central) M_funcset_rcosets_H: |
247 "(%x:M. H #> (SOME g. g \<in> carrier G & M1 #> g = x)) \<in> M \<rightarrow> rcosets G H" |
245 "(%x:M. H #> (SOME g. g \<in> carrier G & M1 #> g = x)) \<in> M \<rightarrow> rcosets H" |
248 apply (rule setrcosI [THEN restrictI]) |
246 apply (rule rcosetsI [THEN restrictI]) |
249 apply (rule H_is_subgroup [THEN subgroup.subset]) |
247 apply (rule H_is_subgroup [THEN subgroup.subset]) |
250 apply (erule M_elem_map_carrier) |
248 apply (erule M_elem_map_carrier) |
251 done |
249 done |
252 |
250 |
253 lemma (in sylow_central) inj_M_GmodH: "\<exists>f \<in> M\<rightarrow>rcosets G H. inj_on f M" |
251 lemma (in sylow_central) inj_M_GmodH: "\<exists>f \<in> M\<rightarrow>rcosets H. inj_on f M" |
254 apply (rule bexI) |
252 apply (rule bexI) |
255 apply (rule_tac [2] M_funcset_setrcos_H) |
253 apply (rule_tac [2] M_funcset_rcosets_H) |
256 apply (rule inj_onI, simp) |
254 apply (rule inj_onI, simp) |
257 apply (rule trans [OF _ M_elem_map_eq]) |
255 apply (rule trans [OF _ M_elem_map_eq]) |
258 prefer 2 apply assumption |
256 prefer 2 apply assumption |
259 apply (rule M_elem_map_eq [symmetric, THEN trans], assumption) |
257 apply (rule M_elem_map_eq [symmetric, THEN trans], assumption) |
260 apply (rule coset_mult_inv1) |
258 apply (rule coset_mult_inv1) |
265 prefer 2 apply (blast intro: m_closed M_elem_map_carrier inv_closed) |
263 prefer 2 apply (blast intro: m_closed M_elem_map_carrier inv_closed) |
266 apply (simp add: coset_mult_inv2 H_def M_elem_map_carrier subset_def) |
264 apply (simp add: coset_mult_inv2 H_def M_elem_map_carrier subset_def) |
267 done |
265 done |
268 |
266 |
269 |
267 |
270 (** the opposite injection **) |
268 subsubsection{*The opposite injection*} |
271 |
269 |
272 lemma (in sylow_central) H_elem_map: |
270 lemma (in sylow_central) H_elem_map: |
273 "H1\<in>rcosets G H ==> \<exists>g. g \<in> carrier G & H #> g = H1" |
271 "H1 \<in> rcosets H ==> \<exists>g. g \<in> carrier G & H #> g = H1" |
274 by (auto simp add: setrcos_eq) |
272 by (auto simp add: RCOSETS_def) |
275 |
273 |
276 lemmas (in sylow_central) H_elem_map_carrier = |
274 lemmas (in sylow_central) H_elem_map_carrier = |
277 H_elem_map [THEN someI_ex, THEN conjunct1] |
275 H_elem_map [THEN someI_ex, THEN conjunct1] |
278 |
276 |
279 lemmas (in sylow_central) H_elem_map_eq = |
277 lemmas (in sylow_central) H_elem_map_eq = |
280 H_elem_map [THEN someI_ex, THEN conjunct2] |
278 H_elem_map [THEN someI_ex, THEN conjunct2] |
281 |
279 |
282 |
280 |
283 lemma EquivElemClass: |
281 lemma EquivElemClass: |
284 "[|equiv A r; M\<in>A // r; M1\<in>M; (M1, M2)\<in>r |] ==> M2\<in>M" |
282 "[|equiv A r; M \<in> A//r; M1\<in>M; (M1,M2) \<in> r |] ==> M2 \<in> M" |
285 apply (unfold equiv_def quotient_def sym_def trans_def, blast) |
283 by (unfold equiv_def quotient_def sym_def trans_def, blast) |
286 done |
284 |
287 |
285 |
288 lemma (in sylow_central) setrcos_H_funcset_M: |
286 lemma (in sylow_central) rcosets_H_funcset_M: |
289 "(\<lambda>C \<in> rcosets G H. M1 #> (@g. g \<in> carrier G \<and> H #> g = C)) |
287 "(\<lambda>C \<in> rcosets H. M1 #> (@g. g \<in> carrier G \<and> H #> g = C)) \<in> rcosets H \<rightarrow> M" |
290 \<in> rcosets G H \<rightarrow> M" |
288 apply (simp add: RCOSETS_def) |
291 apply (simp add: setrcos_eq) |
|
292 apply (fast intro: someI2 |
289 apply (fast intro: someI2 |
293 intro!: restrictI M1_in_M |
290 intro!: restrictI M1_in_M |
294 EquivElemClass [OF RelM_equiv M_in_quot _ M1_RelM_rcosetGM1g]) |
291 EquivElemClass [OF RelM_equiv M_in_quot _ M1_RelM_rcosetGM1g]) |
295 done |
292 done |
296 |
293 |
297 text{*close to a duplicate of @{text inj_M_GmodH}*} |
294 text{*close to a duplicate of @{text inj_M_GmodH}*} |
298 lemma (in sylow_central) inj_GmodH_M: |
295 lemma (in sylow_central) inj_GmodH_M: |
299 "\<exists>g \<in> rcosets G H\<rightarrow>M. inj_on g (rcosets G H)" |
296 "\<exists>g \<in> rcosets H\<rightarrow>M. inj_on g (rcosets H)" |
300 apply (rule bexI) |
297 apply (rule bexI) |
301 apply (rule_tac [2] setrcos_H_funcset_M) |
298 apply (rule_tac [2] rcosets_H_funcset_M) |
302 apply (rule inj_onI) |
299 apply (rule inj_onI) |
303 apply (simp) |
300 apply (simp) |
304 apply (rule trans [OF _ H_elem_map_eq]) |
301 apply (rule trans [OF _ H_elem_map_eq]) |
305 prefer 2 apply assumption |
302 prefer 2 apply assumption |
306 apply (rule H_elem_map_eq [symmetric, THEN trans], assumption) |
303 apply (rule H_elem_map_eq [symmetric, THEN trans], assumption) |
321 apply (rule finite_subset) |
318 apply (rule finite_subset) |
322 apply (rule M_subset_calM [THEN subset_trans]) |
319 apply (rule M_subset_calM [THEN subset_trans]) |
323 apply (rule calM_subset_PowG, blast) |
320 apply (rule calM_subset_PowG, blast) |
324 done |
321 done |
325 |
322 |
326 lemma (in sylow_central) cardMeqIndexH: "card(M) = card(rcosets G H)" |
323 lemma (in sylow_central) cardMeqIndexH: "card(M) = card(rcosets H)" |
327 apply (insert inj_M_GmodH inj_GmodH_M) |
324 apply (insert inj_M_GmodH inj_GmodH_M) |
328 apply (blast intro: card_bij finite_M H_is_subgroup |
325 apply (blast intro: card_bij finite_M H_is_subgroup |
329 setrcos_subset_PowG [THEN finite_subset] |
326 rcosets_subset_PowG [THEN finite_subset] |
330 finite_Pow_iff [THEN iffD2]) |
327 finite_Pow_iff [THEN iffD2]) |
331 done |
328 done |
332 |
329 |
333 lemma (in sylow_central) index_lem: "card(M) * card(H) = order(G)" |
330 lemma (in sylow_central) index_lem: "card(M) * card(H) = order(G)" |
334 by (simp add: cardMeqIndexH lagrange H_is_subgroup) |
331 by (simp add: cardMeqIndexH lagrange H_is_subgroup) |