Metamath Proof Explorer


Theorem islmhmd

Description: Deduction for a module homomorphism. (Contributed by Stefan O'Rear, 4-Feb-2015)

Ref Expression
Hypotheses islmhmd.x
|- X = ( Base ` S )
islmhmd.a
|- .x. = ( .s ` S )
islmhmd.b
|- .X. = ( .s ` T )
islmhmd.k
|- K = ( Scalar ` S )
islmhmd.j
|- J = ( Scalar ` T )
islmhmd.n
|- N = ( Base ` K )
islmhmd.s
|- ( ph -> S e. LMod )
islmhmd.t
|- ( ph -> T e. LMod )
islmhmd.c
|- ( ph -> J = K )
islmhmd.f
|- ( ph -> F e. ( S GrpHom T ) )
islmhmd.l
|- ( ( ph /\ ( x e. N /\ y e. X ) ) -> ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) )
Assertion islmhmd
|- ( ph -> F e. ( S LMHom T ) )

Proof

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