Metamath Proof Explorer

Theorem ghmcyg

Description: The image of a cyclic group under a surjective group homomorphism is cyclic. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses cygctb.1 
|- B = ( Base ` G )
ghmcyg.1 
|- C = ( Base ` H )
Assertion ghmcyg 
|- ( ( F e. ( G GrpHom H ) /\ F : B -onto-> C ) -> ( G e. CycGrp -> H e. CycGrp ) )

Proof

Step Hyp Ref Expression
1 cygctb.1 
 |-  B = ( Base ` G )
2 ghmcyg.1 
 |-  C = ( Base ` H )
3 eqid 
 |-  ( .g ` G ) = ( .g ` G )
4 1 3 iscyg 
 |-  ( G e. CycGrp <-> ( G e. Grp /\ E. x e. B ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B ) )
5 4 simprbi 
 |-  ( G e. CycGrp -> E. x e. B ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B )
6 eqid 
 |-  ( .g ` H ) = ( .g ` H )
7 ghmgrp2 
 |-  ( F e. ( G GrpHom H ) -> H e. Grp )
8 7 ad2antrr 
 |-  ( ( ( F e. ( G GrpHom H ) /\ F : B -onto-> C ) /\ ( x e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B ) ) -> H e. Grp )
9 fof 
 |-  ( F : B -onto-> C -> F : B --> C )
10 9 ad2antlr 
 |-  ( ( ( F e. ( G GrpHom H ) /\ F : B -onto-> C ) /\ ( x e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B ) ) -> F : B --> C )
11 simprl 
 |-  ( ( ( F e. ( G GrpHom H ) /\ F : B -onto-> C ) /\ ( x e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B ) ) -> x e. B )
12 10 11 ffvelrnd 
 |-  ( ( ( F e. ( G GrpHom H ) /\ F : B -onto-> C ) /\ ( x e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B ) ) -> ( F ` x ) e. C )
13 simplr 
 |-  ( ( ( F e. ( G GrpHom H ) /\ F : B -onto-> C ) /\ ( x e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B ) ) -> F : B -onto-> C )
14 foeq2 
 |-  ( ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B -> ( F : ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) -onto-> C <-> F : B -onto-> C ) )
15 14 ad2antll 
 |-  ( ( ( F e. ( G GrpHom H ) /\ F : B -onto-> C ) /\ ( x e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B ) ) -> ( F : ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) -onto-> C <-> F : B -onto-> C ) )
16 13 15 mpbird 
 |-  ( ( ( F e. ( G GrpHom H ) /\ F : B -onto-> C ) /\ ( x e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B ) ) -> F : ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) -onto-> C )
17 foelrn 
 |-  ( ( F : ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) -onto-> C /\ y e. C ) -> E. z e. ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) y = ( F ` z ) )
18 16 17 sylan 
 |-  ( ( ( ( F e. ( G GrpHom H ) /\ F : B -onto-> C ) /\ ( x e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B ) ) /\ y e. C ) -> E. z e. ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) y = ( F ` z ) )
19 ovex 
 |-  ( m ( .g ` G ) x ) e. _V
20 19 rgenw 
 |-  A. m e. ZZ ( m ( .g ` G ) x ) e. _V
21 oveq1 
 |-  ( n = m -> ( n ( .g ` G ) x ) = ( m ( .g ` G ) x ) )
22 21 cbvmptv 
 |-  ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = ( m e. ZZ |-> ( m ( .g ` G ) x ) )
23 fveq2 
 |-  ( z = ( m ( .g ` G ) x ) -> ( F ` z ) = ( F ` ( m ( .g ` G ) x ) ) )
24 23 eqeq2d 
 |-  ( z = ( m ( .g ` G ) x ) -> ( y = ( F ` z ) <-> y = ( F ` ( m ( .g ` G ) x ) ) ) )
25 22 24 rexrnmptw 
 |-  ( A. m e. ZZ ( m ( .g ` G ) x ) e. _V -> ( E. z e. ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) y = ( F ` z ) <-> E. m e. ZZ y = ( F ` ( m ( .g ` G ) x ) ) ) )
26 20 25 ax-mp 
 |-  ( E. z e. ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) y = ( F ` z ) <-> E. m e. ZZ y = ( F ` ( m ( .g ` G ) x ) ) )
27 18 26 sylib 
 |-  ( ( ( ( F e. ( G GrpHom H ) /\ F : B -onto-> C ) /\ ( x e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B ) ) /\ y e. C ) -> E. m e. ZZ y = ( F ` ( m ( .g ` G ) x ) ) )
28 simp-4l 
 |-  ( ( ( ( ( F e. ( G GrpHom H ) /\ F : B -onto-> C ) /\ ( x e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B ) ) /\ y e. C ) /\ m e. ZZ ) -> F e. ( G GrpHom H ) )
29 simpr 
 |-  ( ( ( ( ( F e. ( G GrpHom H ) /\ F : B -onto-> C ) /\ ( x e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B ) ) /\ y e. C ) /\ m e. ZZ ) -> m e. ZZ )
30 11 ad2antrr 
 |-  ( ( ( ( ( F e. ( G GrpHom H ) /\ F : B -onto-> C ) /\ ( x e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B ) ) /\ y e. C ) /\ m e. ZZ ) -> x e. B )
31 1 3 6 ghmmulg 
 |-  ( ( F e. ( G GrpHom H ) /\ m e. ZZ /\ x e. B ) -> ( F ` ( m ( .g ` G ) x ) ) = ( m ( .g ` H ) ( F ` x ) ) )
32 28 29 30 31 syl3anc 
 |-  ( ( ( ( ( F e. ( G GrpHom H ) /\ F : B -onto-> C ) /\ ( x e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B ) ) /\ y e. C ) /\ m e. ZZ ) -> ( F ` ( m ( .g ` G ) x ) ) = ( m ( .g ` H ) ( F ` x ) ) )
33 32 eqeq2d 
 |-  ( ( ( ( ( F e. ( G GrpHom H ) /\ F : B -onto-> C ) /\ ( x e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B ) ) /\ y e. C ) /\ m e. ZZ ) -> ( y = ( F ` ( m ( .g ` G ) x ) ) <-> y = ( m ( .g ` H ) ( F ` x ) ) ) )
34 33 rexbidva 
 |-  ( ( ( ( F e. ( G GrpHom H ) /\ F : B -onto-> C ) /\ ( x e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B ) ) /\ y e. C ) -> ( E. m e. ZZ y = ( F ` ( m ( .g ` G ) x ) ) <-> E. m e. ZZ y = ( m ( .g ` H ) ( F ` x ) ) ) )
35 27 34 mpbid 
 |-  ( ( ( ( F e. ( G GrpHom H ) /\ F : B -onto-> C ) /\ ( x e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B ) ) /\ y e. C ) -> E. m e. ZZ y = ( m ( .g ` H ) ( F ` x ) ) )
36 2 6 8 12 35 iscygd 
 |-  ( ( ( F e. ( G GrpHom H ) /\ F : B -onto-> C ) /\ ( x e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B ) ) -> H e. CycGrp )
37 36 rexlimdvaa 
 |-  ( ( F e. ( G GrpHom H ) /\ F : B -onto-> C ) -> ( E. x e. B ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B -> H e. CycGrp ) )
38 5 37 syl5 
 |-  ( ( F e. ( G GrpHom H ) /\ F : B -onto-> C ) -> ( G e. CycGrp -> H e. CycGrp ) )