Theorem lincval1

Description: The linear combination over a singleton mapping to 0. (Contributed by AV, 12-Apr-2019)

	Ref	Expression
Hypotheses	lincval1.b	|- B = ( Base ` M )
	lincval1.s	|- S = ( Scalar ` M )
	lincval1.r	|- R = ( Base ` S )
	lincval1.f	|- F = { <. V , ( 0g ` S ) >. }
Assertion	lincval1	|- ( ( M e. LMod /\ V e. B ) -> ( F ( linC ` M ) { V } ) = ( 0g ` M ) )

Proof

Step	Hyp	Ref	Expression
1		lincval1.b	|- B = ( Base ` M )
2		lincval1.s	|- S = ( Scalar ` M )
3		lincval1.r	|- R = ( Base ` S )
4		lincval1.f	|- F = { <. V , ( 0g ` S ) >. }
5		eqid	|- ( 0g ` S ) = ( 0g ` S )
6	2 3 5	lmod0cl	|- ( M e. LMod -> ( 0g ` S ) e. R )
7	6	adantr	|- ( ( M e. LMod /\ V e. B ) -> ( 0g ` S ) e. R )
8		eqid	|- ( .s ` M ) = ( .s ` M )
9	1 2 3 8 4	lincvalsn	|- ( ( M e. LMod /\ V e. B /\ ( 0g ` S ) e. R ) -> ( F ( linC ` M ) { V } ) = ( ( 0g ` S ) ( .s ` M ) V ) )
10	7 9	mpd3an3	|- ( ( M e. LMod /\ V e. B ) -> ( F ( linC ` M ) { V } ) = ( ( 0g ` S ) ( .s ` M ) V ) )
11		eqid	|- ( 0g ` M ) = ( 0g ` M )
12	1 2 8 5 11	lmod0vs	|- ( ( M e. LMod /\ V e. B ) -> ( ( 0g ` S ) ( .s ` M ) V ) = ( 0g ` M ) )
13	10 12	eqtrd	|- ( ( M e. LMod /\ V e. B ) -> ( F ( linC ` M ) { V } ) = ( 0g ` M ) )