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

Metamath Proof Explorer

Theorem lmhmlin

Proof