Metamath Proof Explorer

Theorem giccyg

Description: Cyclicity is a group property, i.e. it is preserved under isomorphism. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Assertion giccyg 
|- ( G ~=g H -> ( G e. CycGrp -> H e. CycGrp ) )

Proof

Step Hyp Ref Expression
1 brgic 
 |-  ( G ~=g H <-> ( G GrpIso H ) =/= (/) )
2 n0 
 |-  ( ( G GrpIso H ) =/= (/) <-> E. f f e. ( G GrpIso H ) )
3 gimghm 
 |-  ( f e. ( G GrpIso H ) -> f e. ( G GrpHom H ) )
4 eqid 
 |-  ( Base ` G ) = ( Base ` G )
5 eqid 
 |-  ( Base ` H ) = ( Base ` H )
6 4 5 gimf1o 
 |-  ( f e. ( G GrpIso H ) -> f : ( Base ` G ) -1-1-onto-> ( Base ` H ) )
7 f1ofo 
 |-  ( f : ( Base ` G ) -1-1-onto-> ( Base ` H ) -> f : ( Base ` G ) -onto-> ( Base ` H ) )
8 6 7 syl 
 |-  ( f e. ( G GrpIso H ) -> f : ( Base ` G ) -onto-> ( Base ` H ) )
9 4 5 ghmcyg 
 |-  ( ( f e. ( G GrpHom H ) /\ f : ( Base ` G ) -onto-> ( Base ` H ) ) -> ( G e. CycGrp -> H e. CycGrp ) )
10 3 8 9 syl2anc 
 |-  ( f e. ( G GrpIso H ) -> ( G e. CycGrp -> H e. CycGrp ) )
11 10 exlimiv 
 |-  ( E. f f e. ( G GrpIso H ) -> ( G e. CycGrp -> H e. CycGrp ) )
12 2 11 sylbi 
 |-  ( ( G GrpIso H ) =/= (/) -> ( G e. CycGrp -> H e. CycGrp ) )
13 1 12 sylbi 
 |-  ( G ~=g H -> ( G e. CycGrp -> H e. CycGrp ) )