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

Proof

Step Hyp Ref Expression
1 prmgrpsimpgd.1 ⊢ B = Base G
2 prmgrpsimpgd.2 ⊢ φ → G ∈ Grp
3 prmgrpsimpgd.3 ⊢ φ → B ∈ ℙ
4 eqid ⊢ 0 G = 0 G
5 fveq2 ⊢ 0 G = B → 0 G = B
6 5 adantl ⊢ φ ∧ 0 G = B → 0 G = B
7 4 fvexi ⊢ 0 G ∈ V
8 hashsng ⊢ 0 G ∈ V → 0 G = 1
9 7 8 mp1i ⊢ φ ∧ 0 G = B → 0 G = 1
10 6 9 eqtr3d ⊢ φ ∧ 0 G = B → B = 1
11 3 adantr ⊢ φ ∧ 0 G = B → B ∈ ℙ
12 10 11 eqeltrrd ⊢ φ ∧ 0 G = B → 1 ∈ ℙ
13 1nprm ⊢ ¬ 1 ∈ ℙ
14 13 a1i ⊢ φ ∧ 0 G = B → ¬ 1 ∈ ℙ
15 12 14 pm2.65da ⊢ φ → ¬ 0 G = 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 = 0 G ∨ x = B
32 simpr ⊢ φ ∧ x ∈ SubGrp ⁡ G ∧ x = 1 → x = 1
33 4 subg0cl ⊢ x ∈ SubGrp ⁡ G → 0 G ∈ x
34 33 ad2antlr ⊢ φ ∧ x ∈ SubGrp ⁡ G ∧ x = 1 → 0 G ∈ 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 = 0 G
38 37 orcd ⊢ φ ∧ x ∈ SubGrp ⁡ G ∧ x = 1 → x = 0 G ∨ 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 → 0 G ∈ 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 = 0 G ∨ x = B
58 16 57 sylan2 ⊢ φ ∧ x ∈ NrmSGrp ⁡ G → x = 0 G ∨ x = B
59 1 4 2 15 58 2nsgsimpgd ⊢ φ → G ∈ SimpGrp