# Metamath Proof Explorer

## Theorem prmgrpsimpgd

Description: A group of prime order is simple. (Contributed by Rohan Ridenour, 3-Aug-2023)

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

### Proof

Step Hyp Ref Expression
1 prmgrpsimpgd.1 ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 prmgrpsimpgd.2 ${⊢}{\phi }\to {G}\in \mathrm{Grp}$
3 prmgrpsimpgd.3 ${⊢}{\phi }\to \left|{B}\right|\in ℙ$
4 eqid ${⊢}{0}_{{G}}={0}_{{G}}$
5 fveq2 ${⊢}\left\{{0}_{{G}}\right\}={B}\to \left|\left\{{0}_{{G}}\right\}\right|=\left|{B}\right|$
6 5 adantl ${⊢}\left({\phi }\wedge \left\{{0}_{{G}}\right\}={B}\right)\to \left|\left\{{0}_{{G}}\right\}\right|=\left|{B}\right|$
7 4 fvexi ${⊢}{0}_{{G}}\in \mathrm{V}$
8 hashsng ${⊢}{0}_{{G}}\in \mathrm{V}\to \left|\left\{{0}_{{G}}\right\}\right|=1$
9 7 8 mp1i ${⊢}\left({\phi }\wedge \left\{{0}_{{G}}\right\}={B}\right)\to \left|\left\{{0}_{{G}}\right\}\right|=1$
10 6 9 eqtr3d ${⊢}\left({\phi }\wedge \left\{{0}_{{G}}\right\}={B}\right)\to \left|{B}\right|=1$
11 3 adantr ${⊢}\left({\phi }\wedge \left\{{0}_{{G}}\right\}={B}\right)\to \left|{B}\right|\in ℙ$
12 10 11 eqeltrrd ${⊢}\left({\phi }\wedge \left\{{0}_{{G}}\right\}={B}\right)\to 1\in ℙ$
13 1nprm ${⊢}¬1\in ℙ$
14 13 a1i ${⊢}\left({\phi }\wedge \left\{{0}_{{G}}\right\}={B}\right)\to ¬1\in ℙ$
15 12 14 pm2.65da ${⊢}{\phi }\to ¬\left\{{0}_{{G}}\right\}={B}$
16 nsgsubg ${⊢}{x}\in \mathrm{NrmSGrp}\left({G}\right)\to {x}\in \mathrm{SubGrp}\left({G}\right)$
17 eqid ${⊢}\left|{B}\right|=\left|{B}\right|$
18 1 fvexi ${⊢}{B}\in \mathrm{V}$
19 18 a1i ${⊢}{\phi }\to {B}\in \mathrm{V}$
20 prmnn ${⊢}\left|{B}\right|\in ℙ\to \left|{B}\right|\in ℕ$
21 3 20 syl ${⊢}{\phi }\to \left|{B}\right|\in ℕ$
22 21 nnnn0d ${⊢}{\phi }\to \left|{B}\right|\in {ℕ}_{0}$
23 hashvnfin ${⊢}\left({B}\in \mathrm{V}\wedge \left|{B}\right|\in {ℕ}_{0}\right)\to \left(\left|{B}\right|=\left|{B}\right|\to {B}\in \mathrm{Fin}\right)$
24 19 22 23 syl2anc ${⊢}{\phi }\to \left(\left|{B}\right|=\left|{B}\right|\to {B}\in \mathrm{Fin}\right)$
25 17 24 mpi ${⊢}{\phi }\to {B}\in \mathrm{Fin}$
26 25 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge \left|{x}\right|=\left|{B}\right|\right)\to {B}\in \mathrm{Fin}$
27 1 subgss ${⊢}{x}\in \mathrm{SubGrp}\left({G}\right)\to {x}\subseteq {B}$
28 27 ad2antlr ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge \left|{x}\right|=\left|{B}\right|\right)\to {x}\subseteq {B}$
29 simpr ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge \left|{x}\right|=\left|{B}\right|\right)\to \left|{x}\right|=\left|{B}\right|$
30 26 28 29 phphashrd ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge \left|{x}\right|=\left|{B}\right|\right)\to {x}={B}$
31 30 olcd ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge \left|{x}\right|=\left|{B}\right|\right)\to \left({x}=\left\{{0}_{{G}}\right\}\vee {x}={B}\right)$
32 simpr ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge \left|{x}\right|=1\right)\to \left|{x}\right|=1$
33 4 subg0cl ${⊢}{x}\in \mathrm{SubGrp}\left({G}\right)\to {0}_{{G}}\in {x}$
34 33 ad2antlr ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge \left|{x}\right|=1\right)\to {0}_{{G}}\in {x}$
35 vex ${⊢}{x}\in \mathrm{V}$
36 35 a1i ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge \left|{x}\right|=1\right)\to {x}\in \mathrm{V}$
37 32 34 36 hash1elsn ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge \left|{x}\right|=1\right)\to {x}=\left\{{0}_{{G}}\right\}$
38 37 orcd ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge \left|{x}\right|=1\right)\to \left({x}=\left\{{0}_{{G}}\right\}\vee {x}={B}\right)$
39 1 lagsubg ${⊢}\left({x}\in \mathrm{SubGrp}\left({G}\right)\wedge {B}\in \mathrm{Fin}\right)\to \left|{x}\right|\parallel \left|{B}\right|$
40 25 39 sylan2 ${⊢}\left({x}\in \mathrm{SubGrp}\left({G}\right)\wedge {\phi }\right)\to \left|{x}\right|\parallel \left|{B}\right|$
41 40 ancoms ${⊢}\left({\phi }\wedge {x}\in \mathrm{SubGrp}\left({G}\right)\right)\to \left|{x}\right|\parallel \left|{B}\right|$
42 3 adantr ${⊢}\left({\phi }\wedge {x}\in \mathrm{SubGrp}\left({G}\right)\right)\to \left|{B}\right|\in ℙ$
43 25 adantr ${⊢}\left({\phi }\wedge {x}\in \mathrm{SubGrp}\left({G}\right)\right)\to {B}\in \mathrm{Fin}$
44 27 adantl ${⊢}\left({\phi }\wedge {x}\in \mathrm{SubGrp}\left({G}\right)\right)\to {x}\subseteq {B}$
45 43 44 ssfid ${⊢}\left({\phi }\wedge {x}\in \mathrm{SubGrp}\left({G}\right)\right)\to {x}\in \mathrm{Fin}$
46 hashcl ${⊢}{x}\in \mathrm{Fin}\to \left|{x}\right|\in {ℕ}_{0}$
47 45 46 syl ${⊢}\left({\phi }\wedge {x}\in \mathrm{SubGrp}\left({G}\right)\right)\to \left|{x}\right|\in {ℕ}_{0}$
48 33 adantl ${⊢}\left({\phi }\wedge {x}\in \mathrm{SubGrp}\left({G}\right)\right)\to {0}_{{G}}\in {x}$
49 35 a1i ${⊢}\left({\phi }\wedge {x}\in \mathrm{SubGrp}\left({G}\right)\right)\to {x}\in \mathrm{V}$
50 48 49 hashelne0d ${⊢}\left({\phi }\wedge {x}\in \mathrm{SubGrp}\left({G}\right)\right)\to ¬\left|{x}\right|=0$
51 50 neqned ${⊢}\left({\phi }\wedge {x}\in \mathrm{SubGrp}\left({G}\right)\right)\to \left|{x}\right|\ne 0$
52 elnnne0 ${⊢}\left|{x}\right|\in ℕ↔\left(\left|{x}\right|\in {ℕ}_{0}\wedge \left|{x}\right|\ne 0\right)$
53 47 51 52 sylanbrc ${⊢}\left({\phi }\wedge {x}\in \mathrm{SubGrp}\left({G}\right)\right)\to \left|{x}\right|\in ℕ$
54 dvdsprime ${⊢}\left(\left|{B}\right|\in ℙ\wedge \left|{x}\right|\in ℕ\right)\to \left(\left|{x}\right|\parallel \left|{B}\right|↔\left(\left|{x}\right|=\left|{B}\right|\vee \left|{x}\right|=1\right)\right)$
55 42 53 54 syl2anc ${⊢}\left({\phi }\wedge {x}\in \mathrm{SubGrp}\left({G}\right)\right)\to \left(\left|{x}\right|\parallel \left|{B}\right|↔\left(\left|{x}\right|=\left|{B}\right|\vee \left|{x}\right|=1\right)\right)$
56 41 55 mpbid ${⊢}\left({\phi }\wedge {x}\in \mathrm{SubGrp}\left({G}\right)\right)\to \left(\left|{x}\right|=\left|{B}\right|\vee \left|{x}\right|=1\right)$
57 31 38 56 mpjaodan ${⊢}\left({\phi }\wedge {x}\in \mathrm{SubGrp}\left({G}\right)\right)\to \left({x}=\left\{{0}_{{G}}\right\}\vee {x}={B}\right)$
58 16 57 sylan2 ${⊢}\left({\phi }\wedge {x}\in \mathrm{NrmSGrp}\left({G}\right)\right)\to \left({x}=\left\{{0}_{{G}}\right\}\vee {x}={B}\right)$
59 1 4 2 15 58 2nsgsimpgd ${⊢}{\phi }\to {G}\in \mathrm{SimpGrp}$