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=BaseG
prmgrpsimpgd.2 ⊢φ→G∈Grp
prmgrpsimpgd.3 ⊢φ→B∈ℙ
Assertion prmgrpsimpgd ⊢φ→G∈SimpGrp

Proof

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