# Metamath Proof Explorer

## Theorem ablsimpgprmd

Description: An abelian simple group has prime order. (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypotheses ablsimpgprmd.1 ${⊢}{B}={\mathrm{Base}}_{{G}}$
ablsimpgprmd.2 ${⊢}{\phi }\to {G}\in \mathrm{Abel}$
ablsimpgprmd.3 ${⊢}{\phi }\to {G}\in \mathrm{SimpGrp}$
Assertion ablsimpgprmd ${⊢}{\phi }\to \left|{B}\right|\in ℙ$

### Proof

Step Hyp Ref Expression
1 ablsimpgprmd.1 ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 ablsimpgprmd.2 ${⊢}{\phi }\to {G}\in \mathrm{Abel}$
3 ablsimpgprmd.3 ${⊢}{\phi }\to {G}\in \mathrm{SimpGrp}$
4 simpr ${⊢}\left({\phi }\wedge \left|{B}\right|=1\right)\to \left|{B}\right|=1$
5 3 simpggrpd ${⊢}{\phi }\to {G}\in \mathrm{Grp}$
6 eqid ${⊢}{0}_{{G}}={0}_{{G}}$
7 1 6 grpidcl ${⊢}{G}\in \mathrm{Grp}\to {0}_{{G}}\in {B}$
8 5 7 syl ${⊢}{\phi }\to {0}_{{G}}\in {B}$
9 8 adantr ${⊢}\left({\phi }\wedge \left|{B}\right|=1\right)\to {0}_{{G}}\in {B}$
10 1 2 3 ablsimpgfind ${⊢}{\phi }\to {B}\in \mathrm{Fin}$
11 10 adantr ${⊢}\left({\phi }\wedge \left|{B}\right|=1\right)\to {B}\in \mathrm{Fin}$
12 4 9 11 hash1elsn ${⊢}\left({\phi }\wedge \left|{B}\right|=1\right)\to {B}=\left\{{0}_{{G}}\right\}$
13 3 adantr ${⊢}\left({\phi }\wedge \left|{B}\right|=1\right)\to {G}\in \mathrm{SimpGrp}$
14 1 6 13 simpgntrivd ${⊢}\left({\phi }\wedge \left|{B}\right|=1\right)\to ¬{B}=\left\{{0}_{{G}}\right\}$
15 12 14 pm2.65da ${⊢}{\phi }\to ¬\left|{B}\right|=1$
16 1 5 10 hashfingrpnn ${⊢}{\phi }\to \left|{B}\right|\in ℕ$
17 elnn1uz2 ${⊢}\left|{B}\right|\in ℕ↔\left(\left|{B}\right|=1\vee \left|{B}\right|\in {ℤ}_{\ge 2}\right)$
18 16 17 sylib ${⊢}{\phi }\to \left(\left|{B}\right|=1\vee \left|{B}\right|\in {ℤ}_{\ge 2}\right)$
19 18 ord ${⊢}{\phi }\to \left(¬\left|{B}\right|=1\to \left|{B}\right|\in {ℤ}_{\ge 2}\right)$
20 15 19 mpd ${⊢}{\phi }\to \left|{B}\right|\in {ℤ}_{\ge 2}$
21 2 3 ablsimpgcygd ${⊢}{\phi }\to {G}\in \mathrm{CycGrp}$
22 21 3ad2ant1 ${⊢}\left({\phi }\wedge {y}\in ℕ\wedge {y}\parallel \left|{B}\right|\right)\to {G}\in \mathrm{CycGrp}$
23 simp3 ${⊢}\left({\phi }\wedge {y}\in ℕ\wedge {y}\parallel \left|{B}\right|\right)\to {y}\parallel \left|{B}\right|$
24 10 3ad2ant1 ${⊢}\left({\phi }\wedge {y}\in ℕ\wedge {y}\parallel \left|{B}\right|\right)\to {B}\in \mathrm{Fin}$
25 simp2 ${⊢}\left({\phi }\wedge {y}\in ℕ\wedge {y}\parallel \left|{B}\right|\right)\to {y}\in ℕ$
26 1 22 23 24 25 fincygsubgodexd ${⊢}\left({\phi }\wedge {y}\in ℕ\wedge {y}\parallel \left|{B}\right|\right)\to \exists {x}\in \mathrm{SubGrp}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left|{x}\right|={y}$
27 simpl1 ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\wedge {y}\parallel \left|{B}\right|\right)\wedge \left({x}\in \mathrm{SubGrp}\left({G}\right)\wedge \left|{x}\right|={y}\right)\right)\to {\phi }$
28 27 3 syl ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\wedge {y}\parallel \left|{B}\right|\right)\wedge \left({x}\in \mathrm{SubGrp}\left({G}\right)\wedge \left|{x}\right|={y}\right)\right)\to {G}\in \mathrm{SimpGrp}$
29 simprl ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\wedge {y}\parallel \left|{B}\right|\right)\wedge \left({x}\in \mathrm{SubGrp}\left({G}\right)\wedge \left|{x}\right|={y}\right)\right)\to {x}\in \mathrm{SubGrp}\left({G}\right)$
30 ablnsg ${⊢}{G}\in \mathrm{Abel}\to \mathrm{NrmSGrp}\left({G}\right)=\mathrm{SubGrp}\left({G}\right)$
31 27 2 30 3syl ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\wedge {y}\parallel \left|{B}\right|\right)\wedge \left({x}\in \mathrm{SubGrp}\left({G}\right)\wedge \left|{x}\right|={y}\right)\right)\to \mathrm{NrmSGrp}\left({G}\right)=\mathrm{SubGrp}\left({G}\right)$
32 29 31 eleqtrrd ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\wedge {y}\parallel \left|{B}\right|\right)\wedge \left({x}\in \mathrm{SubGrp}\left({G}\right)\wedge \left|{x}\right|={y}\right)\right)\to {x}\in \mathrm{NrmSGrp}\left({G}\right)$
33 1 6 28 32 simpgnsgeqd ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\wedge {y}\parallel \left|{B}\right|\right)\wedge \left({x}\in \mathrm{SubGrp}\left({G}\right)\wedge \left|{x}\right|={y}\right)\right)\to \left({x}=\left\{{0}_{{G}}\right\}\vee {x}={B}\right)$
34 simpr ${⊢}\left(\left(\left({\phi }\wedge {y}\in ℕ\wedge {y}\parallel \left|{B}\right|\right)\wedge \left({x}\in \mathrm{SubGrp}\left({G}\right)\wedge \left|{x}\right|={y}\right)\right)\wedge {x}=\left\{{0}_{{G}}\right\}\right)\to {x}=\left\{{0}_{{G}}\right\}$
35 34 fveq2d ${⊢}\left(\left(\left({\phi }\wedge {y}\in ℕ\wedge {y}\parallel \left|{B}\right|\right)\wedge \left({x}\in \mathrm{SubGrp}\left({G}\right)\wedge \left|{x}\right|={y}\right)\right)\wedge {x}=\left\{{0}_{{G}}\right\}\right)\to \left|{x}\right|=\left|\left\{{0}_{{G}}\right\}\right|$
36 simplrr ${⊢}\left(\left(\left({\phi }\wedge {y}\in ℕ\wedge {y}\parallel \left|{B}\right|\right)\wedge \left({x}\in \mathrm{SubGrp}\left({G}\right)\wedge \left|{x}\right|={y}\right)\right)\wedge {x}=\left\{{0}_{{G}}\right\}\right)\to \left|{x}\right|={y}$
37 6 fvexi ${⊢}{0}_{{G}}\in \mathrm{V}$
38 hashsng ${⊢}{0}_{{G}}\in \mathrm{V}\to \left|\left\{{0}_{{G}}\right\}\right|=1$
39 37 38 mp1i ${⊢}\left(\left(\left({\phi }\wedge {y}\in ℕ\wedge {y}\parallel \left|{B}\right|\right)\wedge \left({x}\in \mathrm{SubGrp}\left({G}\right)\wedge \left|{x}\right|={y}\right)\right)\wedge {x}=\left\{{0}_{{G}}\right\}\right)\to \left|\left\{{0}_{{G}}\right\}\right|=1$
40 35 36 39 3eqtr3d ${⊢}\left(\left(\left({\phi }\wedge {y}\in ℕ\wedge {y}\parallel \left|{B}\right|\right)\wedge \left({x}\in \mathrm{SubGrp}\left({G}\right)\wedge \left|{x}\right|={y}\right)\right)\wedge {x}=\left\{{0}_{{G}}\right\}\right)\to {y}=1$
41 40 ex ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\wedge {y}\parallel \left|{B}\right|\right)\wedge \left({x}\in \mathrm{SubGrp}\left({G}\right)\wedge \left|{x}\right|={y}\right)\right)\to \left({x}=\left\{{0}_{{G}}\right\}\to {y}=1\right)$
42 simplrr ${⊢}\left(\left(\left({\phi }\wedge {y}\in ℕ\wedge {y}\parallel \left|{B}\right|\right)\wedge \left({x}\in \mathrm{SubGrp}\left({G}\right)\wedge \left|{x}\right|={y}\right)\right)\wedge {x}={B}\right)\to \left|{x}\right|={y}$
43 simpr ${⊢}\left(\left(\left({\phi }\wedge {y}\in ℕ\wedge {y}\parallel \left|{B}\right|\right)\wedge \left({x}\in \mathrm{SubGrp}\left({G}\right)\wedge \left|{x}\right|={y}\right)\right)\wedge {x}={B}\right)\to {x}={B}$
44 43 fveq2d ${⊢}\left(\left(\left({\phi }\wedge {y}\in ℕ\wedge {y}\parallel \left|{B}\right|\right)\wedge \left({x}\in \mathrm{SubGrp}\left({G}\right)\wedge \left|{x}\right|={y}\right)\right)\wedge {x}={B}\right)\to \left|{x}\right|=\left|{B}\right|$
45 42 44 eqtr3d ${⊢}\left(\left(\left({\phi }\wedge {y}\in ℕ\wedge {y}\parallel \left|{B}\right|\right)\wedge \left({x}\in \mathrm{SubGrp}\left({G}\right)\wedge \left|{x}\right|={y}\right)\right)\wedge {x}={B}\right)\to {y}=\left|{B}\right|$
46 45 ex ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\wedge {y}\parallel \left|{B}\right|\right)\wedge \left({x}\in \mathrm{SubGrp}\left({G}\right)\wedge \left|{x}\right|={y}\right)\right)\to \left({x}={B}\to {y}=\left|{B}\right|\right)$
47 41 46 orim12d ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\wedge {y}\parallel \left|{B}\right|\right)\wedge \left({x}\in \mathrm{SubGrp}\left({G}\right)\wedge \left|{x}\right|={y}\right)\right)\to \left(\left({x}=\left\{{0}_{{G}}\right\}\vee {x}={B}\right)\to \left({y}=1\vee {y}=\left|{B}\right|\right)\right)$
48 33 47 mpd ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\wedge {y}\parallel \left|{B}\right|\right)\wedge \left({x}\in \mathrm{SubGrp}\left({G}\right)\wedge \left|{x}\right|={y}\right)\right)\to \left({y}=1\vee {y}=\left|{B}\right|\right)$
49 26 48 rexlimddv ${⊢}\left({\phi }\wedge {y}\in ℕ\wedge {y}\parallel \left|{B}\right|\right)\to \left({y}=1\vee {y}=\left|{B}\right|\right)$
50 49 3exp ${⊢}{\phi }\to \left({y}\in ℕ\to \left({y}\parallel \left|{B}\right|\to \left({y}=1\vee {y}=\left|{B}\right|\right)\right)\right)$
51 50 ralrimiv ${⊢}{\phi }\to \forall {y}\in ℕ\phantom{\rule{.4em}{0ex}}\left({y}\parallel \left|{B}\right|\to \left({y}=1\vee {y}=\left|{B}\right|\right)\right)$
52 isprm2 ${⊢}\left|{B}\right|\in ℙ↔\left(\left|{B}\right|\in {ℤ}_{\ge 2}\wedge \forall {y}\in ℕ\phantom{\rule{.4em}{0ex}}\left({y}\parallel \left|{B}\right|\to \left({y}=1\vee {y}=\left|{B}\right|\right)\right)\right)$
53 20 51 52 sylanbrc ${⊢}{\phi }\to \left|{B}\right|\in ℙ$