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

Proof

Step Hyp Ref Expression
1 ablsimpgprmd.1 ⊢ B = Base G
2 ablsimpgprmd.2 ⊢ φ → G ∈ Abel
3 ablsimpgprmd.3 ⊢ φ → G ∈ SimpGrp
4 simpr ⊢ φ ∧ B = 1 → B = 1
5 3 simpggrpd ⊢ φ → G ∈ Grp
6 eqid ⊢ 0 G = 0 G
7 1 6 grpidcl ⊢ G ∈ Grp → 0 G ∈ B
8 5 7 syl ⊢ φ → 0 G ∈ B
9 8 adantr ⊢ φ ∧ B = 1 → 0 G ∈ B
10 1 2 3 ablsimpgfind ⊢ φ → B ∈ Fin
11 10 adantr ⊢ φ ∧ B = 1 → B ∈ Fin
12 4 9 11 hash1elsn ⊢ φ ∧ B = 1 → B = 0 G
13 3 adantr ⊢ φ ∧ B = 1 → G ∈ SimpGrp
14 1 6 13 simpgntrivd ⊢ φ ∧ B = 1 → ¬ B = 0 G
15 12 14 pm2.65da ⊢ φ → ¬ B = 1
16 1 5 10 hashfingrpnn ⊢ φ → B ∈ ℕ
17 elnn1uz2 ⊢ B ∈ ℕ ↔ B = 1 ∨ B ∈ ℤ ≥ 2
18 16 17 sylib ⊢ φ → B = 1 ∨ B ∈ ℤ ≥ 2
19 18 ord ⊢ φ → ¬ B = 1 → B ∈ ℤ ≥ 2
20 15 19 mpd ⊢ φ → B ∈ ℤ ≥ 2
21 2 3 ablsimpgcygd ⊢ φ → G ∈ CycGrp
22 21 3ad2ant1 ⊢ φ ∧ y ∈ ℕ ∧ y ∥ B → G ∈ CycGrp
23 simp3 ⊢ φ ∧ y ∈ ℕ ∧ y ∥ B → y ∥ B
24 10 3ad2ant1 ⊢ φ ∧ y ∈ ℕ ∧ y ∥ B → B ∈ Fin
25 simp2 ⊢ φ ∧ y ∈ ℕ ∧ y ∥ B → y ∈ ℕ
26 1 22 23 24 25 fincygsubgodexd ⊢ φ ∧ y ∈ ℕ ∧ y ∥ B → ∃ x ∈ SubGrp ⁡ G x = y
27 simpl1 ⊢ φ ∧ y ∈ ℕ ∧ y ∥ B ∧ x ∈ SubGrp ⁡ G ∧ x = y → φ
28 27 3 syl ⊢ φ ∧ y ∈ ℕ ∧ y ∥ B ∧ x ∈ SubGrp ⁡ G ∧ x = y → G ∈ SimpGrp
29 simprl ⊢ φ ∧ y ∈ ℕ ∧ y ∥ B ∧ x ∈ SubGrp ⁡ G ∧ x = y → x ∈ SubGrp ⁡ G
30 ablnsg ⊢ G ∈ Abel → NrmSGrp ⁡ G = SubGrp ⁡ G
31 27 2 30 3syl ⊢ φ ∧ y ∈ ℕ ∧ y ∥ B ∧ x ∈ SubGrp ⁡ G ∧ x = y → NrmSGrp ⁡ G = SubGrp ⁡ G
32 29 31 eleqtrrd ⊢ φ ∧ y ∈ ℕ ∧ y ∥ B ∧ x ∈ SubGrp ⁡ G ∧ x = y → x ∈ NrmSGrp ⁡ G
33 1 6 28 32 simpgnsgeqd ⊢ φ ∧ y ∈ ℕ ∧ y ∥ B ∧ x ∈ SubGrp ⁡ G ∧ x = y → x = 0 G ∨ x = B
34 simpr ⊢ φ ∧ y ∈ ℕ ∧ y ∥ B ∧ x ∈ SubGrp ⁡ G ∧ x = y ∧ x = 0 G → x = 0 G
35 34 fveq2d ⊢ φ ∧ y ∈ ℕ ∧ y ∥ B ∧ x ∈ SubGrp ⁡ G ∧ x = y ∧ x = 0 G → x = 0 G
36 simplrr ⊢ φ ∧ y ∈ ℕ ∧ y ∥ B ∧ x ∈ SubGrp ⁡ G ∧ x = y ∧ x = 0 G → x = y
37 6 fvexi ⊢ 0 G ∈ V
38 hashsng ⊢ 0 G ∈ V → 0 G = 1
39 37 38 mp1i ⊢ φ ∧ y ∈ ℕ ∧ y ∥ B ∧ x ∈ SubGrp ⁡ G ∧ x = y ∧ x = 0 G → 0 G = 1
40 35 36 39 3eqtr3d ⊢ φ ∧ y ∈ ℕ ∧ y ∥ B ∧ x ∈ SubGrp ⁡ G ∧ x = y ∧ x = 0 G → y = 1
41 40 ex ⊢ φ ∧ y ∈ ℕ ∧ y ∥ B ∧ x ∈ SubGrp ⁡ G ∧ x = y → x = 0 G → y = 1
42 simplrr ⊢ φ ∧ y ∈ ℕ ∧ y ∥ B ∧ x ∈ SubGrp ⁡ G ∧ x = y ∧ x = B → x = y
43 simpr ⊢ φ ∧ y ∈ ℕ ∧ y ∥ B ∧ x ∈ SubGrp ⁡ G ∧ x = y ∧ x = B → x = B
44 43 fveq2d ⊢ φ ∧ y ∈ ℕ ∧ y ∥ B ∧ x ∈ SubGrp ⁡ G ∧ x = y ∧ x = B → x = B
45 42 44 eqtr3d ⊢ φ ∧ y ∈ ℕ ∧ y ∥ B ∧ x ∈ SubGrp ⁡ G ∧ x = y ∧ x = B → y = B
46 45 ex ⊢ φ ∧ y ∈ ℕ ∧ y ∥ B ∧ x ∈ SubGrp ⁡ G ∧ x = y → x = B → y = B
47 41 46 orim12d ⊢ φ ∧ y ∈ ℕ ∧ y ∥ B ∧ x ∈ SubGrp ⁡ G ∧ x = y → x = 0 G ∨ x = B → y = 1 ∨ y = B
48 33 47 mpd ⊢ φ ∧ y ∈ ℕ ∧ y ∥ B ∧ x ∈ SubGrp ⁡ G ∧ x = y → y = 1 ∨ y = B
49 26 48 rexlimddv ⊢ φ ∧ y ∈ ℕ ∧ y ∥ B → y = 1 ∨ y = B
50 49 3exp ⊢ φ → y ∈ ℕ → y ∥ B → y = 1 ∨ y = B
51 50 ralrimiv ⊢ φ → ∀ y ∈ ℕ y ∥ B → y = 1 ∨ y = B
52 isprm2 ⊢ B ∈ ℙ ↔ B ∈ ℤ ≥ 2 ∧ ∀ y ∈ ℕ y ∥ B → y = 1 ∨ y = B
53 20 51 52 sylanbrc ⊢ φ → B ∈ ℙ