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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
ablsimpgprmd.2 ⊢ ( 𝜑 → 𝐺 ∈ Abel )
ablsimpgprmd.3 ⊢ ( 𝜑 → 𝐺 ∈ SimpGrp )
Assertion ablsimpgprmd ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℙ )

Proof

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