# Theory Sylow

Up to index of Isabelle/HOL/HOL-Algebra

theory Sylow
imports Coset
begin

    (*  Title:      HOL/Algebra/Sylow.thy
        ID:         $Id: Sylow.thy,v 1.9 2005/07/01 15:41:10 nipkow Exp $
        Author:     Florian Kammueller, with new proofs by L C Paulson
    *)

    header {* Sylow's theorem *}

    theory Sylow imports Coset begin

    text {*
      See also \cite{Kammueller-Paulson:1999}.
    *}

    text{*The combinatorial argument is in theory Exponent*}

    locale sylow = group +
      fixes p and a and m and calM and RelM
      assumes prime_p:   "prime p"
          and order_G:   "order(G) = (p^a) * m"
          and finite_G [iff]:  "finite (carrier G)"
      defines "calM == {s. s ⊆ carrier(G) & card(s) = p^a}"
          and "RelM == {(N1,N2). N1 ∈ calM & N2 ∈ calM &
                                 (∃g ∈ carrier(G). N1 = (N2 #> g) )}"

    lemma (in sylow) RelM_refl: "refl calM RelM"
    apply (auto simp add: refl_def RelM_def calM_def)
    apply (blast intro!: coset_mult_one [symmetric])
    done

    lemma (in sylow) RelM_sym: "sym RelM"
    proof (unfold sym_def RelM_def, clarify)
      fix y g
      assume   "y ∈ calM"
        and g: "g ∈ carrier G"
      hence "y = y #> g #> (inv g)" by (simp add: coset_mult_assoc calM_def)
      thus "∃g'∈carrier G. y = y #> g #> g'"
       by (blast intro: g inv_closed)
    qed

    lemma (in sylow) RelM_trans: "trans RelM"
    by (auto simp add: trans_def RelM_def calM_def coset_mult_assoc)

    lemma (in sylow) RelM_equiv: "equiv calM RelM"
    apply (unfold equiv_def)
    apply (blast intro: RelM_refl RelM_sym RelM_trans)
    done

    lemma (in sylow) M_subset_calM_prep: "M' ∈ calM // RelM  ==> M' ⊆ calM"
    apply (unfold RelM_def)
    apply (blast elim!: quotientE)
    done

    subsection{*Main Part of the Proof*}

    locale sylow_central = sylow +
      fixes H and M1 and M
      assumes M_in_quot:  "M ∈ calM // RelM"
          and not_dvd_M:  "~(p ^ Suc(exponent p m) dvd card(M))"
          and M1_in_M:    "M1 ∈ M"
      defines "H == {g. g∈carrier G & M1 #> g = M1}"

    lemma (in sylow_central) M_subset_calM: "M ⊆ calM"
    by (rule M_in_quot [THEN M_subset_calM_prep])

    lemma (in sylow_central) card_M1: "card(M1) = p^a"
    apply (cut_tac M_subset_calM M1_in_M)
    apply (simp add: calM_def, blast)
    done

    lemma card_nonempty: "0 < card(S) ==> S ≠ {}"
    by force

    lemma (in sylow_central) exists_x_in_M1: "∃x. x∈M1"
    apply (subgoal_tac "0 < card M1")
     apply (blast dest: card_nonempty)
    apply (cut_tac prime_p [THEN prime_imp_one_less])
    apply (simp (no_asm_simp) add: card_M1)
    done

    lemma (in sylow_central) M1_subset_G [simp]: "M1 ⊆ carrier G"
    apply (rule subsetD [THEN PowD])
    apply (rule_tac [2] M1_in_M)
    apply (rule M_subset_calM [THEN subset_trans])
    apply (auto simp add: calM_def)
    done

    lemma (in sylow_central) M1_inj_H: "∃f ∈ H->M1. inj_on f H"
      proof -
        from exists_x_in_M1 obtain m1 where m1M: "m1 ∈ M1"..
        have m1G: "m1 ∈ carrier G" by (simp add: m1M M1_subset_G [THEN subsetD])
        show ?thesis
        proof
          show "inj_on (λz∈H. m1 ⊗ z) H"
            by (simp add: inj_on_def l_cancel [of m1 x y, THEN iffD1] H_def m1G)
          show "restrict (op ⊗ m1) H ∈ H -> M1"
          proof (rule restrictI)
            fix z assume zH: "z ∈ H"
            show "m1 ⊗ z ∈ M1"
            proof -
              from zH
              have zG: "z ∈ carrier G" and M1zeq: "M1 #> z = M1"
                by (auto simp add: H_def)
              show ?thesis
                by (rule subst [OF M1zeq], simp add: m1M zG rcosI)
            qed
          qed
        qed
      qed

    subsection{*Discharging the Assumptions of @{text sylow_central}*}

    lemma (in sylow) EmptyNotInEquivSet: "{} ∉ calM // RelM"
    by (blast elim!: quotientE dest: RelM_equiv [THEN equiv_class_self])

    lemma (in sylow) existsM1inM: "M ∈ calM // RelM ==> ∃M1. M1 ∈ M"
    apply (subgoal_tac "M ≠ {}")
     apply blast
    apply (cut_tac EmptyNotInEquivSet, blast)
    done

    lemma (in sylow) zero_less_o_G: "0 < order(G)"
    apply (unfold order_def)
    apply (blast intro: one_closed zero_less_card_empty)
    done

    lemma (in sylow) zero_less_m: "0 < m"
    apply (cut_tac zero_less_o_G)
    apply (simp add: order_G)
    done

    lemma (in sylow) card_calM: "card(calM) = (p^a) * m choose p^a"
    by (simp add: calM_def n_subsets order_G [symmetric] order_def)

    lemma (in sylow) zero_less_card_calM: "0 < card calM"
    by (simp add: card_calM zero_less_binomial le_extend_mult zero_less_m)

    lemma (in sylow) max_p_div_calM:
         "~ (p ^ Suc(exponent p m) dvd card(calM))"
    apply (subgoal_tac "exponent p m = exponent p (card calM) ")
     apply (cut_tac zero_less_card_calM prime_p)
     apply (force dest: power_Suc_exponent_Not_dvd)
    apply (simp add: card_calM zero_less_m [THEN const_p_fac])
    done

    lemma (in sylow) finite_calM: "finite calM"
    apply (unfold calM_def)
    apply (rule_tac B = "Pow (carrier G) " in finite_subset)
    apply auto
    done

    lemma (in sylow) lemma_A1:
         "∃M ∈ calM // RelM. ~ (p ^ Suc(exponent p m) dvd card(M))"
    apply (rule max_p_div_calM [THEN contrapos_np])
    apply (simp add: finite_calM equiv_imp_dvd_card [OF _ RelM_equiv])
    done

    subsubsection{*Introduction and Destruct Rules for @{term H}*}

    lemma (in sylow_central) H_I: "[|g ∈ carrier G; M1 #> g = M1|] ==> g ∈ H"
    by (simp add: H_def)

    lemma (in sylow_central) H_into_carrier_G: "x ∈ H ==> x ∈ carrier G"
    by (simp add: H_def)

    lemma (in sylow_central) in_H_imp_eq: "g : H ==> M1 #> g = M1"
    by (simp add: H_def)

    lemma (in sylow_central) H_m_closed: "[| x∈H; y∈H|] ==> x ⊗ y ∈ H"
    apply (unfold H_def)
    apply (simp add: coset_mult_assoc [symmetric] m_closed)
    done

    lemma (in sylow_central) H_not_empty: "H ≠ {}"
    apply (simp add: H_def)
    apply (rule exI [of _ \<one>], simp)
    done

    lemma (in sylow_central) H_is_subgroup: "subgroup H G"
    apply (rule subgroupI)
    apply (rule subsetI)
    apply (erule H_into_carrier_G)
    apply (rule H_not_empty)
    apply (simp add: H_def, clarify)
    apply (erule_tac P = "%z. ?lhs(z) = M1" in subst)
    apply (simp add: coset_mult_assoc )
    apply (blast intro: H_m_closed)
    done

    lemma (in sylow_central) rcosetGM1g_subset_G:
         "[| g ∈ carrier G; x ∈ M1 #>  g |] ==> x ∈ carrier G"
    by (blast intro: M1_subset_G [THEN r_coset_subset_G, THEN subsetD])

    lemma (in sylow_central) finite_M1: "finite M1"
    by (rule finite_subset [OF M1_subset_G finite_G])

    lemma (in sylow_central) finite_rcosetGM1g: "g∈carrier G ==> finite (M1 #> g)"
    apply (rule finite_subset)
    apply (rule subsetI)
    apply (erule rcosetGM1g_subset_G, assumption)
    apply (rule finite_G)
    done

    lemma (in sylow_central) M1_cardeq_rcosetGM1g:
         "g ∈ carrier G ==> card(M1 #> g) = card(M1)"
    by (simp (no_asm_simp) add: M1_subset_G card_cosets_equal rcosetsI)

    lemma (in sylow_central) M1_RelM_rcosetGM1g:
         "g ∈ carrier G ==> (M1, M1 #> g) ∈ RelM"
    apply (simp (no_asm) add: RelM_def calM_def card_M1 M1_subset_G)
    apply (rule conjI)
     apply (blast intro: rcosetGM1g_subset_G)
    apply (simp (no_asm_simp) add: card_M1 M1_cardeq_rcosetGM1g)
    apply (rule bexI [of _ "inv g"])
    apply (simp_all add: coset_mult_assoc M1_subset_G)
    done

    subsection{*Equal Cardinalities of @{term M} and the Set of Cosets*}

    text{*Injections between @{term M} and @{term "rcosetsG H"} show that
     their cardinalities are equal.*}

    lemma ElemClassEquiv:
         "[| equiv A r; C ∈ A // r |] ==> ∀x ∈ C. ∀y ∈ C. (x,y)∈r"
    by (unfold equiv_def quotient_def sym_def trans_def, blast)

    lemma (in sylow_central) M_elem_map:
         "M2 ∈ M ==> ∃g. g ∈ carrier G & M1 #> g = M2"
    apply (cut_tac M1_in_M M_in_quot [THEN RelM_equiv [THEN ElemClassEquiv]])
    apply (simp add: RelM_def)
    apply (blast dest!: bspec)
    done

    lemmas (in sylow_central) M_elem_map_carrier =
            M_elem_map [THEN someI_ex, THEN conjunct1]

    lemmas (in sylow_central) M_elem_map_eq =
            M_elem_map [THEN someI_ex, THEN conjunct2]

    lemma (in sylow_central) M_funcset_rcosets_H:
         "(%x:M. H #> (SOME g. g ∈ carrier G & M1 #> g = x)) ∈ M -> rcosets H"
    apply (rule rcosetsI [THEN restrictI])
    apply (rule H_is_subgroup [THEN subgroup.subset])
    apply (erule M_elem_map_carrier)
    done

    lemma (in sylow_central) inj_M_GmodH: "∃f ∈ M->rcosets H. inj_on f M"
    apply (rule bexI)
    apply (rule_tac [2] M_funcset_rcosets_H)
    apply (rule inj_onI, simp)
    apply (rule trans [OF _ M_elem_map_eq])
    prefer 2 apply assumption
    apply (rule M_elem_map_eq [symmetric, THEN trans], assumption)
    apply (rule coset_mult_inv1)
    apply (erule_tac [2] M_elem_map_carrier)+
    apply (rule_tac [2] M1_subset_G)
    apply (rule coset_join1 [THEN in_H_imp_eq])
    apply (rule_tac [3] H_is_subgroup)
    prefer 2 apply (blast intro: m_closed M_elem_map_carrier inv_closed)
    apply (simp add: coset_mult_inv2 H_def M_elem_map_carrier subset_def)
    done

    subsubsection{*The opposite injection*}

    lemma (in sylow_central) H_elem_map:
         "H1 ∈ rcosets H ==> ∃g. g ∈ carrier G & H #> g = H1"
    by (auto simp add: RCOSETS_def)

    lemmas (in sylow_central) H_elem_map_carrier =
            H_elem_map [THEN someI_ex, THEN conjunct1]

    lemmas (in sylow_central) H_elem_map_eq =
            H_elem_map [THEN someI_ex, THEN conjunct2]

    lemma EquivElemClass:
         "[|equiv A r; M ∈ A//r; M1∈M; (M1,M2) ∈ r |] ==> M2 ∈ M"
    by (unfold equiv_def quotient_def sym_def trans_def, blast)

    lemma (in sylow_central) rcosets_H_funcset_M:
      "(λC ∈ rcosets H. M1 #> (@g. g ∈ carrier G ∧ H #> g = C)) ∈ rcosets H -> M"
    apply (simp add: RCOSETS_def)
    apply (fast intro: someI2
                intro!: restrictI M1_in_M
                  EquivElemClass [OF RelM_equiv M_in_quot _  M1_RelM_rcosetGM1g])
    done

    text{*close to a duplicate of @{text inj_M_GmodH}*}
    lemma (in sylow_central) inj_GmodH_M:
         "∃g ∈ rcosets H->M. inj_on g (rcosets H)"
    apply (rule bexI)
    apply (rule_tac [2] rcosets_H_funcset_M)
    apply (rule inj_onI)
    apply (simp)
    apply (rule trans [OF _ H_elem_map_eq])
    prefer 2 apply assumption
    apply (rule H_elem_map_eq [symmetric, THEN trans], assumption)
    apply (rule coset_mult_inv1)
    apply (erule_tac [2] H_elem_map_carrier)+
    apply (rule_tac [2] H_is_subgroup [THEN subgroup.subset])
    apply (rule coset_join2)
    apply (blast intro: m_closed inv_closed H_elem_map_carrier)
    apply (rule H_is_subgroup)
    apply (simp add: H_I coset_mult_inv2 M1_subset_G H_elem_map_carrier)
    done

    lemma (in sylow_central) calM_subset_PowG: "calM ⊆ Pow(carrier G)"
    by (auto simp add: calM_def)

    lemma (in sylow_central) finite_M: "finite M"
    apply (rule finite_subset)
    apply (rule M_subset_calM [THEN subset_trans])
    apply (rule calM_subset_PowG, blast)
    done

    lemma (in sylow_central) cardMeqIndexH: "card(M) = card(rcosets H)"
    apply (insert inj_M_GmodH inj_GmodH_M)
    apply (blast intro: card_bij finite_M H_is_subgroup
                 rcosets_subset_PowG [THEN finite_subset]
                 finite_Pow_iff [THEN iffD2])
    done

    lemma (in sylow_central) index_lem: "card(M) * card(H) = order(G)"
    by (simp add: cardMeqIndexH lagrange H_is_subgroup)

    lemma (in sylow_central) lemma_leq1: "p^a ≤ card(H)"
    apply (rule dvd_imp_le)
     apply (rule div_combine [OF prime_p not_dvd_M])
     prefer 2 apply (blast intro: subgroup.finite_imp_card_positive H_is_subgroup)
    apply (simp add: index_lem order_G power_add mult_dvd_mono power_exponent_dvd
                     zero_less_m)
    done

    lemma (in sylow_central) lemma_leq2: "card(H) ≤ p^a"
    apply (subst card_M1 [symmetric])
    apply (cut_tac M1_inj_H)
    apply (blast intro!: M1_subset_G intro:
                 card_inj H_into_carrier_G finite_subset [OF _ finite_G])
    done

    lemma (in sylow_central) card_H_eq: "card(H) = p^a"
    by (blast intro: le_anti_sym lemma_leq1 lemma_leq2)

    lemma (in sylow) sylow_thm: "∃H. subgroup H G & card(H) = p^a"
    apply (cut_tac lemma_A1, clarify)
    apply (frule existsM1inM, clarify)
    apply (subgoal_tac "sylow_central G p a m M1 M")
     apply (blast dest:  sylow_central.H_is_subgroup sylow_central.card_H_eq)
    apply (simp add: sylow_central_def sylow_central_axioms_def prems)
    done

    text{*Needed because the locale's automatic definition refers to
       @{term "semigroup G"} and @{term "group_axioms G"} rather than
      simply to @{term "group G"}.*}
    lemma sylow_eq: "sylow G p a m = (group G & sylow_axioms G p a m)"
    by (simp add: sylow_def group_def)

    theorem sylow_thm:
         "[| prime p;  group(G);  order(G) = (p^a) * m; finite (carrier G)|]
          ==> ∃H. subgroup H G & card(H) = p^a"
    apply (rule sylow.sylow_thm [of G p a m])
    apply (simp add: sylow_eq sylow_axioms_def)
    done

    end

lemma RelM_refl:

      sylow G p a m
      ==> refl {s. s ⊆ carrier G ∧ card s = p ^ a}
           {(N1, N2).
            N1 ∈ {s. s ⊆ carrier G ∧ card s = p ^ a} ∧
            N2 ∈ {s. s ⊆ carrier G ∧ card s = p ^ a} ∧ (∃g∈carrier G. N1 = N2 #>G g)}

lemma RelM_sym:

      sylow G p a m
      ==> sym {(N1, N2).
               N1 ∈ {s. s ⊆ carrier G ∧ card s = p ^ a} ∧
               N2 ∈ {s. s ⊆ carrier G ∧ card s = p ^ a} ∧
               (∃g∈carrier G. N1 = N2 #>G g)}

lemma RelM_trans:

      sylow G p a m
      ==> trans
           {(N1, N2).
            N1 ∈ {s. s ⊆ carrier G ∧ card s = p ^ a} ∧
            N2 ∈ {s. s ⊆ carrier G ∧ card s = p ^ a} ∧ (∃g∈carrier G. N1 = N2 #>G g)}

lemma RelM_equiv:

      sylow G p a m
      ==> equiv {s. s ⊆ carrier G ∧ card s = p ^ a}
           {(N1, N2).
            N1 ∈ {s. s ⊆ carrier G ∧ card s = p ^ a} ∧
            N2 ∈ {s. s ⊆ carrier G ∧ card s = p ^ a} ∧ (∃g∈carrier G. N1 = N2 #>G g)}

lemma M_subset_calM_prep:

      [| sylow G p a m;
         M' ∈ {s. s ⊆ carrier G ∧ card s = p ^ a} //
              {(N1, N2).
               N1 ∈ {s. s ⊆ carrier G ∧ card s = p ^ a} ∧
               N2 ∈ {s. s ⊆ carrier G ∧ card s = p ^ a} ∧
               (∃g∈carrier G. N1 = N2 #>G g)} |]
      ==> M' ⊆ {s. s ⊆ carrier G ∧ card s = p ^ a}

### Main Part of the Proof

lemma M_subset_calM:

      sylow_central G p a m M1.0 M ==> M ⊆ {s. s ⊆ carrier G ∧ card s = p ^ a}

lemma card_M1:

      sylow_central G p a m M1.0 M ==> card M1.0 = p ^ a

lemma card_nonempty:

      0 < card S ==> S ≠ {}

lemma exists_x_in_M1:

      sylow_central G p a m M1.0 M ==> ∃x. x ∈ M1.0

lemma M1_subset_G:

      sylow_central G p a m M1.0 M ==> M1.0 ⊆ carrier G

lemma M1_inj_H:

      sylow_central G p a m M1.0 M
      ==> ∃f∈{g : carrier G. M1.0 #>G g = M1.0} -> M1.0.
             inj_on f {g : carrier G. M1.0 #>G g = M1.0}

### Discharging the Assumptions of @{text sylow_central}

lemma EmptyNotInEquivSet:

      sylow G p a m
      ==> {} ∉ {s. s ⊆ carrier G ∧ card s = p ^ a} //
               {(N1, N2).
                N1 ∈ {s. s ⊆ carrier G ∧ card s = p ^ a} ∧
                N2 ∈ {s. s ⊆ carrier G ∧ card s = p ^ a} ∧
                (∃g∈carrier G. N1 = N2 #>G g)}

lemma existsM1inM:

      [| sylow G p a m;
         M ∈ {s. s ⊆ carrier G ∧ card s = p ^ a} //
             {(N1, N2).
              N1 ∈ {s. s ⊆ carrier G ∧ card s = p ^ a} ∧
              N2 ∈ {s. s ⊆ carrier G ∧ card s = p ^ a} ∧
              (∃g∈carrier G. N1 = N2 #>G g)} |]
      ==> ∃M1. M1 ∈ M

lemma zero_less_o_G:

      sylow G p a m ==> 0 < order G

lemma zero_less_m:

      sylow G p a m ==> 0 < m

lemma card_calM:

      sylow G p a m
      ==> card {s. s ⊆ carrier G ∧ card s = p ^ a} = p ^ a * m choose p ^ a

lemma zero_less_card_calM:

      sylow G p a m ==> 0 < card {s. s ⊆ carrier G ∧ card s = p ^ a}

lemma max_p_div_calM:

      sylow G p a m
      ==> ¬ p ^ Suc (exponent p m) dvd card {s. s ⊆ carrier G ∧ card s = p ^ a}

lemma finite_calM:

      sylow G p a m ==> finite {s. s ⊆ carrier G ∧ card s = p ^ a}

lemma lemma_A1:

      sylow G p a m
      ==> ∃M∈{s. s ⊆ carrier G ∧ card s = p ^ a} //
             {(N1, N2).
              N1 ∈ {s. s ⊆ carrier G ∧ card s = p ^ a} ∧
              N2 ∈ {s. s ⊆ carrier G ∧ card s = p ^ a} ∧
              (∃g∈carrier G. N1 = N2 #>G g)}.
             ¬ p ^ Suc (exponent p m) dvd card M

#### Introduction and Destruct Rules for @{term H}

lemma H_I:

      [| sylow_central G p a m M1.0 M; g ∈ carrier G; M1.0 #>G g = M1.0 |]
      ==> g ∈ {g : carrier G. M1.0 #>G g = M1.0}

lemma H_into_carrier_G:

      [| sylow_central G p a m M1.0 M; x ∈ {g : carrier G. M1.0 #>G g = M1.0} |]
      ==> x ∈ carrier G

lemma in_H_imp_eq:

      [| sylow_central G p a m M1.0 M; g ∈ {g : carrier G. M1.0 #>G g = M1.0} |]
      ==> M1.0 #>G g = M1.0

lemma H_m_closed:

      [| sylow_central G p a m M1.0 M; x ∈ {g : carrier G. M1.0 #>G g = M1.0};
         y ∈ {g : carrier G. M1.0 #>G g = M1.0} |]
      ==> x ⊗G y ∈ {g : carrier G. M1.0 #>G g = M1.0}

lemma H_not_empty:

      sylow_central G p a m M1.0 M ==> {g : carrier G. M1.0 #>G g = M1.0} ≠ {}

lemma H_is_subgroup:

      sylow_central G p a m M1.0 M ==> subgroup {g : carrier G. M1.0 #>G g = M1.0} G

lemma rcosetGM1g_subset_G:

      [| sylow_central G p a m M1.0 M; g ∈ carrier G; x ∈ M1.0 #>G g |]
      ==> x ∈ carrier G

lemma finite_M1:

      sylow_central G p a m M1.0 M ==> finite M1.0

lemma finite_rcosetGM1g:

      [| sylow_central G p a m M1.0 M; g ∈ carrier G |] ==> finite (M1.0 #>G g)

lemma M1_cardeq_rcosetGM1g:

      [| sylow_central G p a m M1.0 M; g ∈ carrier G |]
      ==> card (M1.0 #>G g) = card M1.0

lemma M1_RelM_rcosetGM1g:

      [| sylow_central G p a m M1.0 M; g ∈ carrier G |]
      ==> (M1.0, M1.0 #>G g)
          ∈ {(N1, N2).
             N1 ∈ {s. s ⊆ carrier G ∧ card s = p ^ a} ∧
             N2 ∈ {s. s ⊆ carrier G ∧ card s = p ^ a} ∧ (∃g∈carrier G. N1 = N2 #>G g)}

### Equal Cardinalities of @{term M} and the Set of Cosets

lemma ElemClassEquiv:

      [| equiv A r; C ∈ A // r |] ==> ∀x∈C. ∀y∈C. (x, y) ∈ r

lemma M_elem_map:

      [| sylow_central G p a m M1.0 M; M2.0 ∈ M |]
      ==> ∃g. g ∈ carrier G ∧ M1.0 #>G g = M2.0

lemmas M_elem_map_carrier:

      [| sylow_central G p a m M1.0 M; M2.0 ∈ M |]
      ==> (SOME x. x ∈ carrier G ∧ M1.0 #>G x = M2.0) ∈ carrier G

lemmas M_elem_map_eq:

      [| sylow_central G p a m M1.0 M; M2.0 ∈ M |]
      ==> M1.0 #>G (SOME x. x ∈ carrier G ∧ M1.0 #>G x = M2.0) = M2.0

lemma M_funcset_rcosets_H:

      sylow_central G p a m M1.0 M
      ==> (λx∈M. {g : carrier G. M1.0 #>G g = M1.0} #>G
                 (SOME g. g ∈ carrier G ∧ M1.0 #>G g = x))
          ∈ M -> rcosetsG {g : carrier G. M1.0 #>G g = M1.0}

lemma inj_M_GmodH:

      sylow_central G p a m M1.0 M
      ==> ∃f∈M -> rcosetsG {g : carrier G. M1.0 #>G g = M1.0}. inj_on f M

#### The opposite injection

lemma H_elem_map:

      [| sylow_central G p a m M1.0 M;
         H1.0 ∈ rcosetsG {g : carrier G. M1.0 #>G g = M1.0} |]
      ==> ∃g. g ∈ carrier G ∧ {g : carrier G. M1.0 #>G g = M1.0} #>G g = H1.0

lemmas H_elem_map_carrier:

      [| sylow_central G p a m M1.0 M;
         H1.0 ∈ rcosetsG {g : carrier G. M1.0 #>G g = M1.0} |]
      ==> (SOME x. x ∈ carrier G ∧ {g : carrier G. M1.0 #>G g = M1.0} #>G x = H1.0)
          ∈ carrier G

lemmas H_elem_map_eq:

      [| sylow_central G p a m M1.0 M;
         H1.0 ∈ rcosetsG {g : carrier G. M1.0 #>G g = M1.0} |]
      ==> {g : carrier G. M1.0 #>G g = M1.0} #>G
          (SOME x. x ∈ carrier G ∧ {g : carrier G. M1.0 #>G g = M1.0} #>G x = H1.0) =
          H1.0

lemma EquivElemClass:

      [| equiv A r; M ∈ A // r; M1.0 ∈ M; (M1.0, M2.0) ∈ r |] ==> M2.0 ∈ M

lemma rcosets_H_funcset_M:

      sylow_central G p a m M1.0 M
      ==> (λC∈rcosetsG {g : carrier G. M1.0 #>G g = M1.0}.
              M1.0 #>G
              (SOME g. g ∈ carrier G ∧ {g : carrier G. M1.0 #>G g = M1.0} #>G g = C))
          ∈ rcosetsG {g : carrier G. M1.0 #>G g = M1.0} -> M

lemma inj_GmodH_M:

      sylow_central G p a m M1.0 M
      ==> ∃g∈rcosetsG {g : carrier G. M1.0 #>G g = M1.0} -> M.
             inj_on g (rcosetsG {g : carrier G. M1.0 #>G g = M1.0})

lemma calM_subset_PowG:

      sylow_central G p a m M1.0 M
      ==> {s. s ⊆ carrier G ∧ card s = p ^ a} ⊆ Pow (carrier G)

lemma finite_M:

      sylow_central G p a m M1.0 M ==> finite M

lemma cardMeqIndexH:

      sylow_central G p a m M1.0 M
      ==> card M = card (rcosetsG {g : carrier G. M1.0 #>G g = M1.0})

lemma index_lem:

      sylow_central G p a m M1.0 M
      ==> card M * card {g : carrier G. M1.0 #>G g = M1.0} = order G

lemma lemma_leq1:

      sylow_central G p a m M1.0 M ==> p ^ a ≤ card {g : carrier G. M1.0 #>G g = M1.0}

lemma lemma_leq2:

      sylow_central G p a m M1.0 M ==> card {g : carrier G. M1.0 #>G g = M1.0} ≤ p ^ a

lemma card_H_eq:

      sylow_central G p a m M1.0 M ==> card {g : carrier G. M1.0 #>G g = M1.0} = p ^ a

lemma sylow_thm:

      sylow G p a m ==> ∃H. subgroup H G ∧ card H = p ^ a

lemma sylow_eq:

      sylow G p a m = (group G ∧ sylow_axioms G p a m)

theorem sylow_thm:

      [| prime p; group G; order G = p ^ a * m; finite (carrier G) |]
      ==> ∃H. subgroup H G ∧ card H = p ^ a