Metamath Proof Explorer

Theorem lmhmlin

Description: A homomorphism of left modules is K -linear. (Contributed by Stefan O'Rear, 1-Jan-2015)

Ref Expression
Hypotheses lmhmlin.k 
|- K = ( Scalar ` S )
lmhmlin.b 
|- B = ( Base ` K )
lmhmlin.e 
|- E = ( Base ` S )
lmhmlin.m 
|- .x. = ( .s ` S )
lmhmlin.n 
|- .X. = ( .s ` T )
Assertion lmhmlin 
|- ( ( F e. ( S LMHom T ) /\ X e. B /\ Y e. E ) -> ( F ` ( X .x. Y ) ) = ( X .X. ( F ` Y ) ) )

Proof

Step Hyp Ref Expression
1 lmhmlin.k 
 |-  K = ( Scalar ` S )
2 lmhmlin.b 
 |-  B = ( Base ` K )
3 lmhmlin.e 
 |-  E = ( Base ` S )
4 lmhmlin.m 
 |-  .x. = ( .s ` S )
5 lmhmlin.n 
 |-  .X. = ( .s ` T )
6 eqid 
 |-  ( Scalar ` T ) = ( Scalar ` T )
7 1 6 2 3 4 5 islmhm 
 |-  ( F e. ( S LMHom T ) <-> ( ( S e. LMod /\ T e. LMod ) /\ ( F e. ( S GrpHom T ) /\ ( Scalar ` T ) = K /\ A. a e. B A. b e. E ( F ` ( a .x. b ) ) = ( a .X. ( F ` b ) ) ) ) )
8 7 simprbi 
 |-  ( F e. ( S LMHom T ) -> ( F e. ( S GrpHom T ) /\ ( Scalar ` T ) = K /\ A. a e. B A. b e. E ( F ` ( a .x. b ) ) = ( a .X. ( F ` b ) ) ) )
9 8 simp3d 
 |-  ( F e. ( S LMHom T ) -> A. a e. B A. b e. E ( F ` ( a .x. b ) ) = ( a .X. ( F ` b ) ) )
10 fvoveq1 
 |-  ( a = X -> ( F ` ( a .x. b ) ) = ( F ` ( X .x. b ) ) )
11 oveq1 
 |-  ( a = X -> ( a .X. ( F ` b ) ) = ( X .X. ( F ` b ) ) )
12 10 11 eqeq12d 
 |-  ( a = X -> ( ( F ` ( a .x. b ) ) = ( a .X. ( F ` b ) ) <-> ( F ` ( X .x. b ) ) = ( X .X. ( F ` b ) ) ) )
13 oveq2 
 |-  ( b = Y -> ( X .x. b ) = ( X .x. Y ) )
14 13 fveq2d 
 |-  ( b = Y -> ( F ` ( X .x. b ) ) = ( F ` ( X .x. Y ) ) )
15 fveq2 
 |-  ( b = Y -> ( F ` b ) = ( F ` Y ) )
16 15 oveq2d 
 |-  ( b = Y -> ( X .X. ( F ` b ) ) = ( X .X. ( F ` Y ) ) )
17 14 16 eqeq12d 
 |-  ( b = Y -> ( ( F ` ( X .x. b ) ) = ( X .X. ( F ` b ) ) <-> ( F ` ( X .x. Y ) ) = ( X .X. ( F ` Y ) ) ) )
18 12 17 rspc2v 
 |-  ( ( X e. B /\ Y e. E ) -> ( A. a e. B A. b e. E ( F ` ( a .x. b ) ) = ( a .X. ( F ` b ) ) -> ( F ` ( X .x. Y ) ) = ( X .X. ( F ` Y ) ) ) )
19 9 18 syl5com 
 |-  ( F e. ( S LMHom T ) -> ( ( X e. B /\ Y e. E ) -> ( F ` ( X .x. Y ) ) = ( X .X. ( F ` Y ) ) ) )
20 19 3impib 
 |-  ( ( F e. ( S LMHom T ) /\ X e. B /\ Y e. E ) -> ( F ` ( X .x. Y ) ) = ( X .X. ( F ` Y ) ) )