Theorem lincvalsn

Description: The linear combination over a singleton. (Contributed by AV, 12-Apr-2019) (Proof shortened by AV, 25-May-2019)

	Ref	Expression
Hypotheses	lincvalsn.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	lincvalsn.s	⊢ 𝑆 = ( Scalar ‘ 𝑀 )
	lincvalsn.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
	lincvalsn.t	⊢ · = ( ·𝑠 ‘ 𝑀 )
	lincvalsn.f	⊢ 𝐹 = { ⟨ 𝑉 , 𝑌 ⟩ }
Assertion	lincvalsn	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( 𝐹 ( linC ‘ 𝑀 ) { 𝑉 } ) = ( 𝑌 · 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		lincvalsn.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		lincvalsn.s	⊢ 𝑆 = ( Scalar ‘ 𝑀 )
3		lincvalsn.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
4		lincvalsn.t	⊢ · = ( ·𝑠 ‘ 𝑀 )
5		lincvalsn.f	⊢ 𝐹 = { ⟨ 𝑉 , 𝑌 ⟩ }
6	5	oveq1i	⊢ ( 𝐹 ( linC ‘ 𝑀 ) { 𝑉 } ) = ( { ⟨ 𝑉 , 𝑌 ⟩ } ( linC ‘ 𝑀 ) { 𝑉 } )
7	1 2 3 4	lincvalsng	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( { ⟨ 𝑉 , 𝑌 ⟩ } ( linC ‘ 𝑀 ) { 𝑉 } ) = ( 𝑌 · 𝑉 ) )
8	6 7	eqtrid	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( 𝐹 ( linC ‘ 𝑀 ) { 𝑉 } ) = ( 𝑌 · 𝑉 ) )