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	$$⊢B={\mathrm{Base}}_M$$
	lincvalsn.s	$$⊢S=\mathrm{Scalar}\left(M\right)$$
	lincvalsn.r	$$⊢R={\mathrm{Base}}_S$$
	lincvalsn.t	$$⊢\underset{\dot{}}{·}={\cdot }_M$$
	lincvalsn.f	$$⊢F=\left\{⟨V,Y⟩\right\}$$
Assertion	lincvalsn	$$⊢\left(M\in \mathrm{LMod}\wedge V\in B\wedge Y\in R\right)\to F\mathrm{linC}\left(M\right)\left\{V\right\}=Y\underset{\dot{}}{·}V$$

Proof

Step	Hyp	Ref	Expression
1		lincvalsn.b	$$⊢B={\mathrm{Base}}_M$$
2		lincvalsn.s	$$⊢S=\mathrm{Scalar}\left(M\right)$$
3		lincvalsn.r	$$⊢R={\mathrm{Base}}_S$$
4		lincvalsn.t	$$⊢\underset{\dot{}}{·}={\cdot }_M$$
5		lincvalsn.f	$$⊢F=\left\{⟨V,Y⟩\right\}$$
6	5	oveq1i	$$⊢F\mathrm{linC}\left(M\right)\left\{V\right\}=\left\{⟨V,Y⟩\right\}\mathrm{linC}\left(M\right)\left\{V\right\}$$
7	1 2 3 4	lincvalsng	$$⊢\left(M\in \mathrm{LMod}\wedge V\in B\wedge Y\in R\right)\to \left\{⟨V,Y⟩\right\}\mathrm{linC}\left(M\right)\left\{V\right\}=Y\underset{\dot{}}{·}V$$
8	6 7	syl5eq	$$⊢\left(M\in \mathrm{LMod}\wedge V\in B\wedge Y\in R\right)\to F\mathrm{linC}\left(M\right)\left\{V\right\}=Y\underset{\dot{}}{·}V$$