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