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 โŠข ๐พ = ( Scalar โ€˜ ๐‘† )
lmhmlin.b โŠข ๐ต = ( Base โ€˜ ๐พ )
lmhmlin.e โŠข ๐ธ = ( Base โ€˜ ๐‘† )
lmhmlin.m โŠข ยท = ( ยท๐‘  โ€˜ ๐‘† )
lmhmlin.n โŠข ร— = ( ยท๐‘  โ€˜ ๐‘‡ )
Assertion lmhmlin ( ( ๐น โˆˆ ( ๐‘† LMHom ๐‘‡ ) โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ธ ) โ†’ ( ๐น โ€˜ ( ๐‘‹ ยท ๐‘Œ ) ) = ( ๐‘‹ ร— ( ๐น โ€˜ ๐‘Œ ) ) )

Proof

Step Hyp Ref Expression
1 lmhmlin.k โŠข ๐พ = ( Scalar โ€˜ ๐‘† )
2 lmhmlin.b โŠข ๐ต = ( Base โ€˜ ๐พ )
3 lmhmlin.e โŠข ๐ธ = ( Base โ€˜ ๐‘† )
4 lmhmlin.m โŠข ยท = ( ยท๐‘  โ€˜ ๐‘† )
5 lmhmlin.n โŠข ร— = ( ยท๐‘  โ€˜ ๐‘‡ )
6 eqid โŠข ( Scalar โ€˜ ๐‘‡ ) = ( Scalar โ€˜ ๐‘‡ )
7 1 6 2 3 4 5 islmhm โŠข ( ๐น โˆˆ ( ๐‘† LMHom ๐‘‡ ) โ†” ( ( ๐‘† โˆˆ LMod โˆง ๐‘‡ โˆˆ LMod ) โˆง ( ๐น โˆˆ ( ๐‘† GrpHom ๐‘‡ ) โˆง ( Scalar โ€˜ ๐‘‡ ) = ๐พ โˆง โˆ€ ๐‘Ž โˆˆ ๐ต โˆ€ ๐‘ โˆˆ ๐ธ ( ๐น โ€˜ ( ๐‘Ž ยท ๐‘ ) ) = ( ๐‘Ž ร— ( ๐น โ€˜ ๐‘ ) ) ) ) )
8 7 simprbi โŠข ( ๐น โˆˆ ( ๐‘† LMHom ๐‘‡ ) โ†’ ( ๐น โˆˆ ( ๐‘† GrpHom ๐‘‡ ) โˆง ( Scalar โ€˜ ๐‘‡ ) = ๐พ โˆง โˆ€ ๐‘Ž โˆˆ ๐ต โˆ€ ๐‘ โˆˆ ๐ธ ( ๐น โ€˜ ( ๐‘Ž ยท ๐‘ ) ) = ( ๐‘Ž ร— ( ๐น โ€˜ ๐‘ ) ) ) )
9 8 simp3d โŠข ( ๐น โˆˆ ( ๐‘† LMHom ๐‘‡ ) โ†’ โˆ€ ๐‘Ž โˆˆ ๐ต โˆ€ ๐‘ โˆˆ ๐ธ ( ๐น โ€˜ ( ๐‘Ž ยท ๐‘ ) ) = ( ๐‘Ž ร— ( ๐น โ€˜ ๐‘ ) ) )
10 fvoveq1 โŠข ( ๐‘Ž = ๐‘‹ โ†’ ( ๐น โ€˜ ( ๐‘Ž ยท ๐‘ ) ) = ( ๐น โ€˜ ( ๐‘‹ ยท ๐‘ ) ) )
11 oveq1 โŠข ( ๐‘Ž = ๐‘‹ โ†’ ( ๐‘Ž ร— ( ๐น โ€˜ ๐‘ ) ) = ( ๐‘‹ ร— ( ๐น โ€˜ ๐‘ ) ) )
12 10 11 eqeq12d โŠข ( ๐‘Ž = ๐‘‹ โ†’ ( ( ๐น โ€˜ ( ๐‘Ž ยท ๐‘ ) ) = ( ๐‘Ž ร— ( ๐น โ€˜ ๐‘ ) ) โ†” ( ๐น โ€˜ ( ๐‘‹ ยท ๐‘ ) ) = ( ๐‘‹ ร— ( ๐น โ€˜ ๐‘ ) ) ) )
13 oveq2 โŠข ( ๐‘ = ๐‘Œ โ†’ ( ๐‘‹ ยท ๐‘ ) = ( ๐‘‹ ยท ๐‘Œ ) )
14 13 fveq2d โŠข ( ๐‘ = ๐‘Œ โ†’ ( ๐น โ€˜ ( ๐‘‹ ยท ๐‘ ) ) = ( ๐น โ€˜ ( ๐‘‹ ยท ๐‘Œ ) ) )
15 fveq2 โŠข ( ๐‘ = ๐‘Œ โ†’ ( ๐น โ€˜ ๐‘ ) = ( ๐น โ€˜ ๐‘Œ ) )
16 15 oveq2d โŠข ( ๐‘ = ๐‘Œ โ†’ ( ๐‘‹ ร— ( ๐น โ€˜ ๐‘ ) ) = ( ๐‘‹ ร— ( ๐น โ€˜ ๐‘Œ ) ) )
17 14 16 eqeq12d โŠข ( ๐‘ = ๐‘Œ โ†’ ( ( ๐น โ€˜ ( ๐‘‹ ยท ๐‘ ) ) = ( ๐‘‹ ร— ( ๐น โ€˜ ๐‘ ) ) โ†” ( ๐น โ€˜ ( ๐‘‹ ยท ๐‘Œ ) ) = ( ๐‘‹ ร— ( ๐น โ€˜ ๐‘Œ ) ) ) )
18 12 17 rspc2v โŠข ( ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ธ ) โ†’ ( โˆ€ ๐‘Ž โˆˆ ๐ต โˆ€ ๐‘ โˆˆ ๐ธ ( ๐น โ€˜ ( ๐‘Ž ยท ๐‘ ) ) = ( ๐‘Ž ร— ( ๐น โ€˜ ๐‘ ) ) โ†’ ( ๐น โ€˜ ( ๐‘‹ ยท ๐‘Œ ) ) = ( ๐‘‹ ร— ( ๐น โ€˜ ๐‘Œ ) ) ) )
19 9 18 syl5com โŠข ( ๐น โˆˆ ( ๐‘† LMHom ๐‘‡ ) โ†’ ( ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ธ ) โ†’ ( ๐น โ€˜ ( ๐‘‹ ยท ๐‘Œ ) ) = ( ๐‘‹ ร— ( ๐น โ€˜ ๐‘Œ ) ) ) )
20 19 3impib โŠข ( ( ๐น โˆˆ ( ๐‘† LMHom ๐‘‡ ) โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ธ ) โ†’ ( ๐น โ€˜ ( ๐‘‹ ยท ๐‘Œ ) ) = ( ๐‘‹ ร— ( ๐น โ€˜ ๐‘Œ ) ) )