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 |
|
mhmmnd.3 |
|- ( ph -> G e. Mnd ) |
8 |
|
mhmid.0 |
|- .0. = ( 0g ` G ) |
9 |
|
eqid |
|- ( 0g ` H ) = ( 0g ` H ) |
10 |
|
fof |
|- ( F : X -onto-> Y -> F : X --> Y ) |
11 |
6 10
|
syl |
|- ( ph -> F : X --> Y ) |
12 |
2 8
|
mndidcl |
|- ( G e. Mnd -> .0. e. X ) |
13 |
7 12
|
syl |
|- ( ph -> .0. e. X ) |
14 |
11 13
|
ffvelrnd |
|- ( ph -> ( F ` .0. ) e. Y ) |
15 |
|
simplll |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ph ) |
16 |
15 1
|
syl3an1 |
|- ( ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) ) |
17 |
7
|
ad3antrrr |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> G e. Mnd ) |
18 |
17 12
|
syl |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> .0. e. X ) |
19 |
|
simplr |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> i e. X ) |
20 |
16 18 19
|
mhmlem |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( F ` ( .0. .+ i ) ) = ( ( F ` .0. ) .+^ ( F ` i ) ) ) |
21 |
2 4 8
|
mndlid |
|- ( ( G e. Mnd /\ i e. X ) -> ( .0. .+ i ) = i ) |
22 |
17 19 21
|
syl2anc |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( .0. .+ i ) = i ) |
23 |
22
|
fveq2d |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( F ` ( .0. .+ i ) ) = ( F ` i ) ) |
24 |
20 23
|
eqtr3d |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( ( F ` .0. ) .+^ ( F ` i ) ) = ( F ` i ) ) |
25 |
|
simpr |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( F ` i ) = a ) |
26 |
25
|
oveq2d |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( ( F ` .0. ) .+^ ( F ` i ) ) = ( ( F ` .0. ) .+^ a ) ) |
27 |
24 26 25
|
3eqtr3d |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( ( F ` .0. ) .+^ a ) = a ) |
28 |
|
foelrni |
|- ( ( F : X -onto-> Y /\ a e. Y ) -> E. i e. X ( F ` i ) = a ) |
29 |
6 28
|
sylan |
|- ( ( ph /\ a e. Y ) -> E. i e. X ( F ` i ) = a ) |
30 |
27 29
|
r19.29a |
|- ( ( ph /\ a e. Y ) -> ( ( F ` .0. ) .+^ a ) = a ) |
31 |
16 19 18
|
mhmlem |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( F ` ( i .+ .0. ) ) = ( ( F ` i ) .+^ ( F ` .0. ) ) ) |
32 |
2 4 8
|
mndrid |
|- ( ( G e. Mnd /\ i e. X ) -> ( i .+ .0. ) = i ) |
33 |
17 19 32
|
syl2anc |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( i .+ .0. ) = i ) |
34 |
33
|
fveq2d |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( F ` ( i .+ .0. ) ) = ( F ` i ) ) |
35 |
31 34
|
eqtr3d |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( ( F ` i ) .+^ ( F ` .0. ) ) = ( F ` i ) ) |
36 |
25
|
oveq1d |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( ( F ` i ) .+^ ( F ` .0. ) ) = ( a .+^ ( F ` .0. ) ) ) |
37 |
35 36 25
|
3eqtr3d |
|- ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( a .+^ ( F ` .0. ) ) = a ) |
38 |
37 29
|
r19.29a |
|- ( ( ph /\ a e. Y ) -> ( a .+^ ( F ` .0. ) ) = a ) |
39 |
3 9 5 14 30 38
|
ismgmid2 |
|- ( ph -> ( F ` .0. ) = ( 0g ` H ) ) |