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 = ( Base ` M )
	lincvalsn.s	|- S = ( Scalar ` M )
	lincvalsn.r	|- R = ( Base ` S )
	lincvalsn.t	|- .x. = ( .s ` M )
	lincvalsn.f	|- F = { <. V , Y >. }
Assertion	lincvalsn	|- ( ( M e. LMod /\ V e. B /\ Y e. R ) -> ( F ( linC ` M ) { V } ) = ( Y .x. V ) )

Proof

Step	Hyp	Ref	Expression
1		lincvalsn.b	|- B = ( Base ` M )
2		lincvalsn.s	|- S = ( Scalar ` M )
3		lincvalsn.r	|- R = ( Base ` S )
4		lincvalsn.t	|- .x. = ( .s ` M )
5		lincvalsn.f	|- F = { <. V , Y >. }
6	5	oveq1i	|- ( F ( linC ` M ) { V } ) = ( { <. V , Y >. } ( linC ` M ) { V } )
7	1 2 3 4	lincvalsng	|- ( ( M e. LMod /\ V e. B /\ Y e. R ) -> ( { <. V , Y >. } ( linC ` M ) { V } ) = ( Y .x. V ) )
8	6 7	syl5eq	|- ( ( M e. LMod /\ V e. B /\ Y e. R ) -> ( F ( linC ` M ) { V } ) = ( Y .x. V ) )