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 
|- ( ph -> G e. Abel )
ablsimpgprmd.3 
|- ( ph -> G e. SimpGrp )
Assertion ablsimpgprmd 
|- ( ph -> ( # ` B ) e. Prime )

Proof

Step Hyp Ref Expression
1 ablsimpgprmd.1 
 |-  B = ( Base ` G )
2 ablsimpgprmd.2 
 |-  ( ph -> G e. Abel )
3 ablsimpgprmd.3 
 |-  ( ph -> G e. SimpGrp )
4 simpr 
 |-  ( ( ph /\ ( # ` B ) = 1 ) -> ( # ` B ) = 1 )
5 3 simpggrpd 
 |-  ( ph -> G e. Grp )
6 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
7 1 6 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. B )
8 5 7 syl 
 |-  ( ph -> ( 0g ` G ) e. B )
9 8 adantr 
 |-  ( ( ph /\ ( # ` B ) = 1 ) -> ( 0g ` G ) e. B )
10 1 2 3 ablsimpgfind 
 |-  ( ph -> B e. Fin )
11 10 adantr 
 |-  ( ( ph /\ ( # ` B ) = 1 ) -> B e. Fin )
12 4 9 11 hash1elsn 
 |-  ( ( ph /\ ( # ` B ) = 1 ) -> B = { ( 0g ` G ) } )
13 3 adantr 
 |-  ( ( ph /\ ( # ` B ) = 1 ) -> G e. SimpGrp )
14 1 6 13 simpgntrivd 
 |-  ( ( ph /\ ( # ` B ) = 1 ) -> -. B = { ( 0g ` G ) } )
15 12 14 pm2.65da 
 |-  ( ph -> -. ( # ` B ) = 1 )
16 1 5 10 hashfingrpnn 
 |-  ( ph -> ( # ` B ) e. NN )
17 elnn1uz2 
 |-  ( ( # ` B ) e. NN <-> ( ( # ` B ) = 1 \/ ( # ` B ) e. ( ZZ>= ` 2 ) ) )
18 16 17 sylib 
 |-  ( ph -> ( ( # ` B ) = 1 \/ ( # ` B ) e. ( ZZ>= ` 2 ) ) )
19 18 ord 
 |-  ( ph -> ( -. ( # ` B ) = 1 -> ( # ` B ) e. ( ZZ>= ` 2 ) ) )
20 15 19 mpd 
 |-  ( ph -> ( # ` B ) e. ( ZZ>= ` 2 ) )
21 2 3 ablsimpgcygd 
 |-  ( ph -> G e. CycGrp )
22 21 3ad2ant1 
 |-  ( ( ph /\ y e. NN /\ y || ( # ` B ) ) -> G e. CycGrp )
23 simp3 
 |-  ( ( ph /\ y e. NN /\ y || ( # ` B ) ) -> y || ( # ` B ) )
24 10 3ad2ant1 
 |-  ( ( ph /\ y e. NN /\ y || ( # ` B ) ) -> B e. Fin )
25 simp2 
 |-  ( ( ph /\ y e. NN /\ y || ( # ` B ) ) -> y e. NN )
26 1 22 23 24 25 fincygsubgodexd 
 |-  ( ( ph /\ y e. NN /\ y || ( # ` B ) ) -> E. x e. ( SubGrp ` G ) ( # ` x ) = y )
27 simpl1 
 |-  ( ( ( ph /\ y e. NN /\ y || ( # ` B ) ) /\ ( x e. ( SubGrp ` G ) /\ ( # ` x ) = y ) ) -> ph )
28 27 3 syl 
 |-  ( ( ( ph /\ y e. NN /\ y || ( # ` B ) ) /\ ( x e. ( SubGrp ` G ) /\ ( # ` x ) = y ) ) -> G e. SimpGrp )
29 simprl 
 |-  ( ( ( ph /\ y e. NN /\ y || ( # ` B ) ) /\ ( x e. ( SubGrp ` G ) /\ ( # ` x ) = y ) ) -> x e. ( SubGrp ` G ) )
30 ablnsg 
 |-  ( G e. Abel -> ( NrmSGrp ` G ) = ( SubGrp ` G ) )
31 27 2 30 3syl 
 |-  ( ( ( ph /\ y e. NN /\ y || ( # ` B ) ) /\ ( x e. ( SubGrp ` G ) /\ ( # ` x ) = y ) ) -> ( NrmSGrp ` G ) = ( SubGrp ` G ) )
32 29 31 eleqtrrd 
 |-  ( ( ( ph /\ y e. NN /\ y || ( # ` B ) ) /\ ( x e. ( SubGrp ` G ) /\ ( # ` x ) = y ) ) -> x e. ( NrmSGrp ` G ) )
33 1 6 28 32 simpgnsgeqd 
 |-  ( ( ( ph /\ y e. NN /\ y || ( # ` B ) ) /\ ( x e. ( SubGrp ` G ) /\ ( # ` x ) = y ) ) -> ( x = { ( 0g ` G ) } \/ x = B ) )
34 simpr 
 |-  ( ( ( ( ph /\ y e. NN /\ y || ( # ` B ) ) /\ ( x e. ( SubGrp ` G ) /\ ( # ` x ) = y ) ) /\ x = { ( 0g ` G ) } ) -> x = { ( 0g ` G ) } )
35 34 fveq2d 
 |-  ( ( ( ( ph /\ y e. NN /\ y || ( # ` B ) ) /\ ( x e. ( SubGrp ` G ) /\ ( # ` x ) = y ) ) /\ x = { ( 0g ` G ) } ) -> ( # ` x ) = ( # ` { ( 0g ` G ) } ) )
36 simplrr 
 |-  ( ( ( ( ph /\ y e. NN /\ y || ( # ` B ) ) /\ ( x e. ( SubGrp ` G ) /\ ( # ` x ) = y ) ) /\ x = { ( 0g ` G ) } ) -> ( # ` x ) = y )
37 6 fvexi 
 |-  ( 0g ` G ) e. _V
38 hashsng 
 |-  ( ( 0g ` G ) e. _V -> ( # ` { ( 0g ` G ) } ) = 1 )
39 37 38 mp1i 
 |-  ( ( ( ( ph /\ y e. NN /\ y || ( # ` B ) ) /\ ( x e. ( SubGrp ` G ) /\ ( # ` x ) = y ) ) /\ x = { ( 0g ` G ) } ) -> ( # ` { ( 0g ` G ) } ) = 1 )
40 35 36 39 3eqtr3d 
 |-  ( ( ( ( ph /\ y e. NN /\ y || ( # ` B ) ) /\ ( x e. ( SubGrp ` G ) /\ ( # ` x ) = y ) ) /\ x = { ( 0g ` G ) } ) -> y = 1 )
41 40 ex 
 |-  ( ( ( ph /\ y e. NN /\ y || ( # ` B ) ) /\ ( x e. ( SubGrp ` G ) /\ ( # ` x ) = y ) ) -> ( x = { ( 0g ` G ) } -> y = 1 ) )
42 simplrr 
 |-  ( ( ( ( ph /\ y e. NN /\ y || ( # ` B ) ) /\ ( x e. ( SubGrp ` G ) /\ ( # ` x ) = y ) ) /\ x = B ) -> ( # ` x ) = y )
43 simpr 
 |-  ( ( ( ( ph /\ y e. NN /\ y || ( # ` B ) ) /\ ( x e. ( SubGrp ` G ) /\ ( # ` x ) = y ) ) /\ x = B ) -> x = B )
44 43 fveq2d 
 |-  ( ( ( ( ph /\ y e. NN /\ y || ( # ` B ) ) /\ ( x e. ( SubGrp ` G ) /\ ( # ` x ) = y ) ) /\ x = B ) -> ( # ` x ) = ( # ` B ) )
45 42 44 eqtr3d 
 |-  ( ( ( ( ph /\ y e. NN /\ y || ( # ` B ) ) /\ ( x e. ( SubGrp ` G ) /\ ( # ` x ) = y ) ) /\ x = B ) -> y = ( # ` B ) )
46 45 ex 
 |-  ( ( ( ph /\ y e. NN /\ y || ( # ` B ) ) /\ ( x e. ( SubGrp ` G ) /\ ( # ` x ) = y ) ) -> ( x = B -> y = ( # ` B ) ) )
47 41 46 orim12d 
 |-  ( ( ( ph /\ y e. NN /\ y || ( # ` B ) ) /\ ( x e. ( SubGrp ` G ) /\ ( # ` x ) = y ) ) -> ( ( x = { ( 0g ` G ) } \/ x = B ) -> ( y = 1 \/ y = ( # ` B ) ) ) )
48 33 47 mpd 
 |-  ( ( ( ph /\ y e. NN /\ y || ( # ` B ) ) /\ ( x e. ( SubGrp ` G ) /\ ( # ` x ) = y ) ) -> ( y = 1 \/ y = ( # ` B ) ) )
49 26 48 rexlimddv 
 |-  ( ( ph /\ y e. NN /\ y || ( # ` B ) ) -> ( y = 1 \/ y = ( # ` B ) ) )
50 49 3exp 
 |-  ( ph -> ( y e. NN -> ( y || ( # ` B ) -> ( y = 1 \/ y = ( # ` B ) ) ) ) )
51 50 ralrimiv 
 |-  ( ph -> A. y e. NN ( y || ( # ` B ) -> ( y = 1 \/ y = ( # ` B ) ) ) )
52 isprm2 
 |-  ( ( # ` B ) e. Prime <-> ( ( # ` B ) e. ( ZZ>= ` 2 ) /\ A. y e. NN ( y || ( # ` B ) -> ( y = 1 \/ y = ( # ` B ) ) ) ) )
53 20 51 52 sylanbrc 
 |-  ( ph -> ( # ` B ) e. Prime )