Metamath Proof Explorer

Theorem ablsimpgcygd

Description: An abelian simple group is cyclic. (Contributed by Rohan Ridenour, 3-Aug-2023) (Proof shortened by Rohan Ridenour, 31-Oct-2023)

Ref Expression
Hypotheses ablsimpgcygd.1 
|- ( ph -> G e. Abel )
ablsimpgcygd.2 
|- ( ph -> G e. SimpGrp )
Assertion ablsimpgcygd 
|- ( ph -> G e. CycGrp )

Proof

Step Hyp Ref Expression
1 ablsimpgcygd.1 
 |-  ( ph -> G e. Abel )
2 ablsimpgcygd.2 
 |-  ( ph -> G e. SimpGrp )
3 eqid 
 |-  ( Base ` G ) = ( Base ` G )
4 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
5 3 4 2 simpgnideld 
 |-  ( ph -> E. x e. ( Base ` G ) -. x = ( 0g ` G ) )
6 eqid 
 |-  ( .g ` G ) = ( .g ` G )
7 2 simpggrpd 
 |-  ( ph -> G e. Grp )
8 7 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` G ) /\ -. x = ( 0g ` G ) ) ) -> G e. Grp )
9 simprl 
 |-  ( ( ph /\ ( x e. ( Base ` G ) /\ -. x = ( 0g ` G ) ) ) -> x e. ( Base ` G ) )
10 1 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` G ) /\ -. x = ( 0g ` G ) ) ) /\ y e. ( Base ` G ) ) -> G e. Abel )
11 2 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` G ) /\ -. x = ( 0g ` G ) ) ) /\ y e. ( Base ` G ) ) -> G e. SimpGrp )
12 simplrl 
 |-  ( ( ( ph /\ ( x e. ( Base ` G ) /\ -. x = ( 0g ` G ) ) ) /\ y e. ( Base ` G ) ) -> x e. ( Base ` G ) )
13 simplrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` G ) /\ -. x = ( 0g ` G ) ) ) /\ y e. ( Base ` G ) ) -> -. x = ( 0g ` G ) )
14 simpr 
 |-  ( ( ( ph /\ ( x e. ( Base ` G ) /\ -. x = ( 0g ` G ) ) ) /\ y e. ( Base ` G ) ) -> y e. ( Base ` G ) )
15 3 4 6 10 11 12 13 14 ablsimpg1gend 
 |-  ( ( ( ph /\ ( x e. ( Base ` G ) /\ -. x = ( 0g ` G ) ) ) /\ y e. ( Base ` G ) ) -> E. z e. ZZ y = ( z ( .g ` G ) x ) )
16 3 6 8 9 15 iscygd 
 |-  ( ( ph /\ ( x e. ( Base ` G ) /\ -. x = ( 0g ` G ) ) ) -> G e. CycGrp )
17 5 16 rexlimddv 
 |-  ( ph -> G e. CycGrp )