Metamath Proof Explorer

Theorem cygth

Description: The "fundamental theorem of cyclic groups". Cyclic groups are exactly the additive groups ZZ / n ZZ , for 0 <_ n (where n = 0 is the infinite cyclic group ZZ ), up to isomorphism. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Assertion cygth 
|- ( G e. CycGrp <-> E. n e. NN0 G ~=g ( Z/nZ ` n ) )

Proof

Step Hyp Ref Expression
1 hashcl 
 |-  ( ( Base ` G ) e. Fin -> ( # ` ( Base ` G ) ) e. NN0 )
2 1 adantl 
 |-  ( ( G e. CycGrp /\ ( Base ` G ) e. Fin ) -> ( # ` ( Base ` G ) ) e. NN0 )
3 0nn0 
 |-  0 e. NN0
4 3 a1i 
 |-  ( ( G e. CycGrp /\ -. ( Base ` G ) e. Fin ) -> 0 e. NN0 )
5 2 4 ifclda 
 |-  ( G e. CycGrp -> if ( ( Base ` G ) e. Fin , ( # ` ( Base ` G ) ) , 0 ) e. NN0 )
6 eqid 
 |-  ( Base ` G ) = ( Base ` G )
7 eqid 
 |-  if ( ( Base ` G ) e. Fin , ( # ` ( Base ` G ) ) , 0 ) = if ( ( Base ` G ) e. Fin , ( # ` ( Base ` G ) ) , 0 )
8 eqid 
 |-  ( Z/nZ ` if ( ( Base ` G ) e. Fin , ( # ` ( Base ` G ) ) , 0 ) ) = ( Z/nZ ` if ( ( Base ` G ) e. Fin , ( # ` ( Base ` G ) ) , 0 ) )
9 6 7 8 cygzn 
 |-  ( G e. CycGrp -> G ~=g ( Z/nZ ` if ( ( Base ` G ) e. Fin , ( # ` ( Base ` G ) ) , 0 ) ) )
10 fveq2 
 |-  ( n = if ( ( Base ` G ) e. Fin , ( # ` ( Base ` G ) ) , 0 ) -> ( Z/nZ ` n ) = ( Z/nZ ` if ( ( Base ` G ) e. Fin , ( # ` ( Base ` G ) ) , 0 ) ) )
11 10 breq2d 
 |-  ( n = if ( ( Base ` G ) e. Fin , ( # ` ( Base ` G ) ) , 0 ) -> ( G ~=g ( Z/nZ ` n ) <-> G ~=g ( Z/nZ ` if ( ( Base ` G ) e. Fin , ( # ` ( Base ` G ) ) , 0 ) ) ) )
12 11 rspcev 
 |-  ( ( if ( ( Base ` G ) e. Fin , ( # ` ( Base ` G ) ) , 0 ) e. NN0 /\ G ~=g ( Z/nZ ` if ( ( Base ` G ) e. Fin , ( # ` ( Base ` G ) ) , 0 ) ) ) -> E. n e. NN0 G ~=g ( Z/nZ ` n ) )
13 5 9 12 syl2anc 
 |-  ( G e. CycGrp -> E. n e. NN0 G ~=g ( Z/nZ ` n ) )
14 gicsym 
 |-  ( G ~=g ( Z/nZ ` n ) -> ( Z/nZ ` n ) ~=g G )
15 eqid 
 |-  ( Z/nZ ` n ) = ( Z/nZ ` n )
16 15 zncyg 
 |-  ( n e. NN0 -> ( Z/nZ ` n ) e. CycGrp )
17 giccyg 
 |-  ( ( Z/nZ ` n ) ~=g G -> ( ( Z/nZ ` n ) e. CycGrp -> G e. CycGrp ) )
18 14 16 17 syl2imc 
 |-  ( n e. NN0 -> ( G ~=g ( Z/nZ ` n ) -> G e. CycGrp ) )
19 18 rexlimiv 
 |-  ( E. n e. NN0 G ~=g ( Z/nZ ` n ) -> G e. CycGrp )
20 13 19 impbii 
 |-  ( G e. CycGrp <-> E. n e. NN0 G ~=g ( Z/nZ ` n ) )