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 𝑇 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐸 ) → ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) = ( 𝑋 × ( 𝐹 ‘ 𝑌 ) ) )