Metamath Proof Explorer

Theorem ablsimpgfind

Description: An abelian simple group is finite. (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypotheses ablsimpgfind.1 
|- B = ( Base ` G )
ablsimpgfind.2 
|- ( ph -> G e. Abel )
ablsimpgfind.3 
|- ( ph -> G e. SimpGrp )
Assertion ablsimpgfind 
|- ( ph -> B e. Fin )

Proof

Step Hyp Ref Expression
1 ablsimpgfind.1 
 |-  B = ( Base ` G )
2 ablsimpgfind.2 
 |-  ( ph -> G e. Abel )
3 ablsimpgfind.3 
 |-  ( ph -> G e. SimpGrp )
4 simpr 
 |-  ( ( ph /\ -. B e. Fin ) -> -. B e. Fin )
5 4 iffalsed 
 |-  ( ( ph /\ -. B e. Fin ) -> if ( B e. Fin , ( # ` B ) , 0 ) = 0 )
6 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
7 1 6 3 simpgnideld 
 |-  ( ph -> E. x e. B -. x = ( 0g ` G ) )
8 neqne 
 |-  ( -. x = ( 0g ` G ) -> x =/= ( 0g ` G ) )
9 8 reximi 
 |-  ( E. x e. B -. x = ( 0g ` G ) -> E. x e. B x =/= ( 0g ` G ) )
10 7 9 syl 
 |-  ( ph -> E. x e. B x =/= ( 0g ` G ) )
11 eqid 
 |-  ( .g ` G ) = ( .g ` G )
12 eqid 
 |-  ( od ` G ) = ( od ` G )
13 3 simpggrpd 
 |-  ( ph -> G e. Grp )
14 13 adantr 
 |-  ( ( ph /\ ( x e. B /\ x =/= ( 0g ` G ) ) ) -> G e. Grp )
15 simprl 
 |-  ( ( ph /\ ( x e. B /\ x =/= ( 0g ` G ) ) ) -> x e. B )
16 2 ad2antrr 
 |-  ( ( ( ph /\ ( x e. B /\ x =/= ( 0g ` G ) ) ) /\ y e. B ) -> G e. Abel )
17 3 ad2antrr 
 |-  ( ( ( ph /\ ( x e. B /\ x =/= ( 0g ` G ) ) ) /\ y e. B ) -> G e. SimpGrp )
18 15 adantr 
 |-  ( ( ( ph /\ ( x e. B /\ x =/= ( 0g ` G ) ) ) /\ y e. B ) -> x e. B )
19 simplrr 
 |-  ( ( ( ph /\ ( x e. B /\ x =/= ( 0g ` G ) ) ) /\ y e. B ) -> x =/= ( 0g ` G ) )
20 19 neneqd 
 |-  ( ( ( ph /\ ( x e. B /\ x =/= ( 0g ` G ) ) ) /\ y e. B ) -> -. x = ( 0g ` G ) )
21 simpr 
 |-  ( ( ( ph /\ ( x e. B /\ x =/= ( 0g ` G ) ) ) /\ y e. B ) -> y e. B )
22 1 6 11 16 17 18 20 21 ablsimpg1gend 
 |-  ( ( ( ph /\ ( x e. B /\ x =/= ( 0g ` G ) ) ) /\ y e. B ) -> E. n e. ZZ y = ( n ( .g ` G ) x ) )
23 22 ex 
 |-  ( ( ph /\ ( x e. B /\ x =/= ( 0g ` G ) ) ) -> ( y e. B -> E. n e. ZZ y = ( n ( .g ` G ) x ) ) )
24 simprr 
 |-  ( ( ( ph /\ ( x e. B /\ x =/= ( 0g ` G ) ) ) /\ ( n e. ZZ /\ y = ( n ( .g ` G ) x ) ) ) -> y = ( n ( .g ` G ) x ) )
25 13 ad2antrr 
 |-  ( ( ( ph /\ ( x e. B /\ x =/= ( 0g ` G ) ) ) /\ ( n e. ZZ /\ y = ( n ( .g ` G ) x ) ) ) -> G e. Grp )
26 simprl 
 |-  ( ( ( ph /\ ( x e. B /\ x =/= ( 0g ` G ) ) ) /\ ( n e. ZZ /\ y = ( n ( .g ` G ) x ) ) ) -> n e. ZZ )
27 15 adantr 
 |-  ( ( ( ph /\ ( x e. B /\ x =/= ( 0g ` G ) ) ) /\ ( n e. ZZ /\ y = ( n ( .g ` G ) x ) ) ) -> x e. B )
28 1 11 25 26 27 mulgcld 
 |-  ( ( ( ph /\ ( x e. B /\ x =/= ( 0g ` G ) ) ) /\ ( n e. ZZ /\ y = ( n ( .g ` G ) x ) ) ) -> ( n ( .g ` G ) x ) e. B )
29 24 28 eqeltrd 
 |-  ( ( ( ph /\ ( x e. B /\ x =/= ( 0g ` G ) ) ) /\ ( n e. ZZ /\ y = ( n ( .g ` G ) x ) ) ) -> y e. B )
30 29 rexlimdvaa 
 |-  ( ( ph /\ ( x e. B /\ x =/= ( 0g ` G ) ) ) -> ( E. n e. ZZ y = ( n ( .g ` G ) x ) -> y e. B ) )
31 23 30 impbid 
 |-  ( ( ph /\ ( x e. B /\ x =/= ( 0g ` G ) ) ) -> ( y e. B <-> E. n e. ZZ y = ( n ( .g ` G ) x ) ) )
32 31 abbi2dv 
 |-  ( ( ph /\ ( x e. B /\ x =/= ( 0g ` G ) ) ) -> B = { y | E. n e. ZZ y = ( n ( .g ` G ) x ) } )
33 eqid 
 |-  ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = ( n e. ZZ |-> ( n ( .g ` G ) x ) )
34 33 rnmpt 
 |-  ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = { y | E. n e. ZZ y = ( n ( .g ` G ) x ) }
35 32 34 eqtr4di 
 |-  ( ( ph /\ ( x e. B /\ x =/= ( 0g ` G ) ) ) -> B = ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) )
36 1 11 12 14 15 35 cycsubggenodd 
 |-  ( ( ph /\ ( x e. B /\ x =/= ( 0g ` G ) ) ) -> ( ( od ` G ) ` x ) = if ( B e. Fin , ( # ` B ) , 0 ) )
37 1 6 11 12 2 3 ablsimpgfindlem2 
 |-  ( ( ( ph /\ x e. B ) /\ ( 2 ( .g ` G ) x ) = ( 0g ` G ) ) -> ( ( od ` G ) ` x ) =/= 0 )
38 1 6 11 12 2 3 ablsimpgfindlem1 
 |-  ( ( ( ph /\ x e. B ) /\ ( 2 ( .g ` G ) x ) =/= ( 0g ` G ) ) -> ( ( od ` G ) ` x ) =/= 0 )
39 37 38 pm2.61dane 
 |-  ( ( ph /\ x e. B ) -> ( ( od ` G ) ` x ) =/= 0 )
40 39 adantrr 
 |-  ( ( ph /\ ( x e. B /\ x =/= ( 0g ` G ) ) ) -> ( ( od ` G ) ` x ) =/= 0 )
41 36 40 eqnetrrd 
 |-  ( ( ph /\ ( x e. B /\ x =/= ( 0g ` G ) ) ) -> if ( B e. Fin , ( # ` B ) , 0 ) =/= 0 )
42 10 41 rexlimddv 
 |-  ( ph -> if ( B e. Fin , ( # ` B ) , 0 ) =/= 0 )
43 42 adantr 
 |-  ( ( ph /\ -. B e. Fin ) -> if ( B e. Fin , ( # ` B ) , 0 ) =/= 0 )
44 5 43 pm2.21ddne 
 |-  ( ( ph /\ -. B e. Fin ) -> F. )
45 44 efald 
 |-  ( ph -> B e. Fin )