Metamath Proof Explorer

Theorem cyggic

Description: Cyclic groups are isomorphic precisely when they have the same order. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses cygctb.b 
|- B = ( Base ` G )
cygctb.c 
|- C = ( Base ` H )
Assertion cyggic 
|- ( ( G e. CycGrp /\ H e. CycGrp ) -> ( G ~=g H <-> B ~~ C ) )

Proof

Step Hyp Ref Expression
1 cygctb.b 
 |-  B = ( Base ` G )
2 cygctb.c 
 |-  C = ( Base ` H )
3 1 2 gicen 
 |-  ( G ~=g H -> B ~~ C )
4 eqid 
 |-  if ( B e. Fin , ( # ` B ) , 0 ) = if ( B e. Fin , ( # ` B ) , 0 )
5 eqid 
 |-  ( Z/nZ ` if ( B e. Fin , ( # ` B ) , 0 ) ) = ( Z/nZ ` if ( B e. Fin , ( # ` B ) , 0 ) )
6 1 4 5 cygzn 
 |-  ( G e. CycGrp -> G ~=g ( Z/nZ ` if ( B e. Fin , ( # ` B ) , 0 ) ) )
7 6 ad2antrr 
 |-  ( ( ( G e. CycGrp /\ H e. CycGrp ) /\ B ~~ C ) -> G ~=g ( Z/nZ ` if ( B e. Fin , ( # ` B ) , 0 ) ) )
8 enfi 
 |-  ( B ~~ C -> ( B e. Fin <-> C e. Fin ) )
9 8 adantl 
 |-  ( ( ( G e. CycGrp /\ H e. CycGrp ) /\ B ~~ C ) -> ( B e. Fin <-> C e. Fin ) )
10 hasheni 
 |-  ( B ~~ C -> ( # ` B ) = ( # ` C ) )
11 10 adantl 
 |-  ( ( ( G e. CycGrp /\ H e. CycGrp ) /\ B ~~ C ) -> ( # ` B ) = ( # ` C ) )
12 9 11 ifbieq1d 
 |-  ( ( ( G e. CycGrp /\ H e. CycGrp ) /\ B ~~ C ) -> if ( B e. Fin , ( # ` B ) , 0 ) = if ( C e. Fin , ( # ` C ) , 0 ) )
13 12 fveq2d 
 |-  ( ( ( G e. CycGrp /\ H e. CycGrp ) /\ B ~~ C ) -> ( Z/nZ ` if ( B e. Fin , ( # ` B ) , 0 ) ) = ( Z/nZ ` if ( C e. Fin , ( # ` C ) , 0 ) ) )
14 eqid 
 |-  if ( C e. Fin , ( # ` C ) , 0 ) = if ( C e. Fin , ( # ` C ) , 0 )
15 eqid 
 |-  ( Z/nZ ` if ( C e. Fin , ( # ` C ) , 0 ) ) = ( Z/nZ ` if ( C e. Fin , ( # ` C ) , 0 ) )
16 2 14 15 cygzn 
 |-  ( H e. CycGrp -> H ~=g ( Z/nZ ` if ( C e. Fin , ( # ` C ) , 0 ) ) )
17 16 ad2antlr 
 |-  ( ( ( G e. CycGrp /\ H e. CycGrp ) /\ B ~~ C ) -> H ~=g ( Z/nZ ` if ( C e. Fin , ( # ` C ) , 0 ) ) )
18 gicsym 
 |-  ( H ~=g ( Z/nZ ` if ( C e. Fin , ( # ` C ) , 0 ) ) -> ( Z/nZ ` if ( C e. Fin , ( # ` C ) , 0 ) ) ~=g H )
19 17 18 syl 
 |-  ( ( ( G e. CycGrp /\ H e. CycGrp ) /\ B ~~ C ) -> ( Z/nZ ` if ( C e. Fin , ( # ` C ) , 0 ) ) ~=g H )
20 13 19 eqbrtrd 
 |-  ( ( ( G e. CycGrp /\ H e. CycGrp ) /\ B ~~ C ) -> ( Z/nZ ` if ( B e. Fin , ( # ` B ) , 0 ) ) ~=g H )
21 gictr 
 |-  ( ( G ~=g ( Z/nZ ` if ( B e. Fin , ( # ` B ) , 0 ) ) /\ ( Z/nZ ` if ( B e. Fin , ( # ` B ) , 0 ) ) ~=g H ) -> G ~=g H )
22 7 20 21 syl2anc 
 |-  ( ( ( G e. CycGrp /\ H e. CycGrp ) /\ B ~~ C ) -> G ~=g H )
23 22 ex 
 |-  ( ( G e. CycGrp /\ H e. CycGrp ) -> ( B ~~ C -> G ~=g H ) )
24 3 23 impbid2 
 |-  ( ( G e. CycGrp /\ H e. CycGrp ) -> ( G ~=g H <-> B ~~ C ) )