Step |
Hyp |
Ref |
Expression |
1 |
|
ghmgrp.f |
|- ( ( ph /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) ) |
2 |
|
ghmgrp.x |
|- X = ( Base ` G ) |
3 |
|
ghmgrp.y |
|- Y = ( Base ` H ) |
4 |
|
ghmgrp.p |
|- .+ = ( +g ` G ) |
5 |
|
ghmgrp.q |
|- .+^ = ( +g ` H ) |
6 |
|
ghmgrp.1 |
|- ( ph -> F : X -onto-> Y ) |
7 |
|
ghmgrp.3 |
|- ( ph -> G e. Grp ) |
8 |
7
|
grpmndd |
|- ( ph -> G e. Mnd ) |
9 |
1 2 3 4 5 6 8
|
mhmmnd |
|- ( ph -> H e. Mnd ) |
10 |
|
fof |
|- ( F : X -onto-> Y -> F : X --> Y ) |
11 |
6 10
|
syl |
|- ( ph -> F : X --> Y ) |
12 |
11
|
ad3antrrr |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> F : X --> Y ) |
13 |
7
|
ad3antrrr |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> G e. Grp ) |
14 |
|
simplr |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> i e. X ) |
15 |
|
eqid |
|- ( invg ` G ) = ( invg ` G ) |
16 |
2 15
|
grpinvcl |
|- ( ( G e. Grp /\ i e. X ) -> ( ( invg ` G ) ` i ) e. X ) |
17 |
13 14 16
|
syl2anc |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( ( invg ` G ) ` i ) e. X ) |
18 |
12 17
|
ffvelrnd |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( F ` ( ( invg ` G ) ` i ) ) e. Y ) |
19 |
1
|
3adant1r |
|- ( ( ( ph /\ i e. X ) /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) ) |
20 |
7 16
|
sylan |
|- ( ( ph /\ i e. X ) -> ( ( invg ` G ) ` i ) e. X ) |
21 |
|
simpr |
|- ( ( ph /\ i e. X ) -> i e. X ) |
22 |
19 20 21
|
mhmlem |
|- ( ( ph /\ i e. X ) -> ( F ` ( ( ( invg ` G ) ` i ) .+ i ) ) = ( ( F ` ( ( invg ` G ) ` i ) ) .+^ ( F ` i ) ) ) |
23 |
22
|
ad4ant13 |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( F ` ( ( ( invg ` G ) ` i ) .+ i ) ) = ( ( F ` ( ( invg ` G ) ` i ) ) .+^ ( F ` i ) ) ) |
24 |
|
eqid |
|- ( 0g ` G ) = ( 0g ` G ) |
25 |
2 4 24 15
|
grplinv |
|- ( ( G e. Grp /\ i e. X ) -> ( ( ( invg ` G ) ` i ) .+ i ) = ( 0g ` G ) ) |
26 |
25
|
fveq2d |
|- ( ( G e. Grp /\ i e. X ) -> ( F ` ( ( ( invg ` G ) ` i ) .+ i ) ) = ( F ` ( 0g ` G ) ) ) |
27 |
13 14 26
|
syl2anc |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( F ` ( ( ( invg ` G ) ` i ) .+ i ) ) = ( F ` ( 0g ` G ) ) ) |
28 |
1 2 3 4 5 6 8 24
|
mhmid |
|- ( ph -> ( F ` ( 0g ` G ) ) = ( 0g ` H ) ) |
29 |
28
|
ad3antrrr |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( F ` ( 0g ` G ) ) = ( 0g ` H ) ) |
30 |
27 29
|
eqtrd |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( F ` ( ( ( invg ` G ) ` i ) .+ i ) ) = ( 0g ` H ) ) |
31 |
|
simpr |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( F ` i ) = a ) |
32 |
31
|
oveq2d |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( ( F ` ( ( invg ` G ) ` i ) ) .+^ ( F ` i ) ) = ( ( F ` ( ( invg ` G ) ` i ) ) .+^ a ) ) |
33 |
23 30 32
|
3eqtr3rd |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( ( F ` ( ( invg ` G ) ` i ) ) .+^ a ) = ( 0g ` H ) ) |
34 |
|
oveq1 |
|- ( f = ( F ` ( ( invg ` G ) ` i ) ) -> ( f .+^ a ) = ( ( F ` ( ( invg ` G ) ` i ) ) .+^ a ) ) |
35 |
34
|
eqeq1d |
|- ( f = ( F ` ( ( invg ` G ) ` i ) ) -> ( ( f .+^ a ) = ( 0g ` H ) <-> ( ( F ` ( ( invg ` G ) ` i ) ) .+^ a ) = ( 0g ` H ) ) ) |
36 |
35
|
rspcev |
|- ( ( ( F ` ( ( invg ` G ) ` i ) ) e. Y /\ ( ( F ` ( ( invg ` G ) ` i ) ) .+^ a ) = ( 0g ` H ) ) -> E. f e. Y ( f .+^ a ) = ( 0g ` H ) ) |
37 |
18 33 36
|
syl2anc |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> E. f e. Y ( f .+^ a ) = ( 0g ` H ) ) |
38 |
|
foelrni |
|- ( ( F : X -onto-> Y /\ a e. Y ) -> E. i e. X ( F ` i ) = a ) |
39 |
6 38
|
sylan |
|- ( ( ph /\ a e. Y ) -> E. i e. X ( F ` i ) = a ) |
40 |
37 39
|
r19.29a |
|- ( ( ph /\ a e. Y ) -> E. f e. Y ( f .+^ a ) = ( 0g ` H ) ) |
41 |
40
|
ralrimiva |
|- ( ph -> A. a e. Y E. f e. Y ( f .+^ a ) = ( 0g ` H ) ) |
42 |
|
eqid |
|- ( 0g ` H ) = ( 0g ` H ) |
43 |
3 5 42
|
isgrp |
|- ( H e. Grp <-> ( H e. Mnd /\ A. a e. Y E. f e. Y ( f .+^ a ) = ( 0g ` H ) ) ) |
44 |
9 41 43
|
sylanbrc |
|- ( ph -> H e. Grp ) |