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 ) )