| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ismhmd.b |
|- B = ( Base ` S ) |
| 2 |
|
ismhmd.c |
|- C = ( Base ` T ) |
| 3 |
|
ismhmd.p |
|- .+ = ( +g ` S ) |
| 4 |
|
ismhmd.q |
|- .+^ = ( +g ` T ) |
| 5 |
|
ismhmd.0 |
|- .0. = ( 0g ` S ) |
| 6 |
|
ismhmd.z |
|- Z = ( 0g ` T ) |
| 7 |
|
ismhmd.s |
|- ( ph -> S e. Mnd ) |
| 8 |
|
ismhmd.t |
|- ( ph -> T e. Mnd ) |
| 9 |
|
ismhmd.f |
|- ( ph -> F : B --> C ) |
| 10 |
|
ismhmd.a |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) ) |
| 11 |
|
ismhmd.h |
|- ( ph -> ( F ` .0. ) = Z ) |
| 12 |
10
|
ralrimivva |
|- ( ph -> A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) ) |
| 13 |
9 12 11
|
3jca |
|- ( ph -> ( F : B --> C /\ A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` .0. ) = Z ) ) |
| 14 |
1 2 3 4 5 6
|
ismhm |
|- ( F e. ( S MndHom T ) <-> ( ( S e. Mnd /\ T e. Mnd ) /\ ( F : B --> C /\ A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` .0. ) = Z ) ) ) |
| 15 |
7 8 13 14
|
syl21anbrc |
|- ( ph -> F e. ( S MndHom T ) ) |