Step |
Hyp |
Ref |
Expression |
1 |
|
islmhmd.x |
|- X = ( Base ` S ) |
2 |
|
islmhmd.a |
|- .x. = ( .s ` S ) |
3 |
|
islmhmd.b |
|- .X. = ( .s ` T ) |
4 |
|
islmhmd.k |
|- K = ( Scalar ` S ) |
5 |
|
islmhmd.j |
|- J = ( Scalar ` T ) |
6 |
|
islmhmd.n |
|- N = ( Base ` K ) |
7 |
|
islmhmd.s |
|- ( ph -> S e. LMod ) |
8 |
|
islmhmd.t |
|- ( ph -> T e. LMod ) |
9 |
|
islmhmd.c |
|- ( ph -> J = K ) |
10 |
|
islmhmd.f |
|- ( ph -> F e. ( S GrpHom T ) ) |
11 |
|
islmhmd.l |
|- ( ( ph /\ ( x e. N /\ y e. X ) ) -> ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) |
12 |
11
|
ralrimivva |
|- ( ph -> A. x e. N A. y e. X ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) |
13 |
10 9 12
|
3jca |
|- ( ph -> ( F e. ( S GrpHom T ) /\ J = K /\ A. x e. N A. y e. X ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) ) |
14 |
4 5 6 1 2 3
|
islmhm |
|- ( F e. ( S LMHom T ) <-> ( ( S e. LMod /\ T e. LMod ) /\ ( F e. ( S GrpHom T ) /\ J = K /\ A. x e. N A. y e. X ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) ) ) |
15 |
7 8 13 14
|
syl21anbrc |
|- ( ph -> F e. ( S LMHom T ) ) |