This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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