Theorem lincval1

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

	Ref	Expression
Hypotheses	lincval1.b	$$⊢B={\mathrm{Base}}_M$$
	lincval1.s	$$⊢S=\mathrm{Scalar}\left(M\right)$$
	lincval1.r	$$⊢R={\mathrm{Base}}_S$$
	lincval1.f	$$⊢F=\left\{⟨V,0_S⟩\right\}$$
Assertion	lincval1	$$⊢\left(M\in \mathrm{LMod}\wedge V\in B\right)\to F\mathrm{linC}\left(M\right)\left\{V\right\}=0_M$$

Proof

Step	Hyp	Ref	Expression
1		lincval1.b	$$⊢B={\mathrm{Base}}_M$$
2		lincval1.s	$$⊢S=\mathrm{Scalar}\left(M\right)$$
3		lincval1.r	$$⊢R={\mathrm{Base}}_S$$
4		lincval1.f	$$⊢F=\left\{⟨V,0_S⟩\right\}$$
5		eqid	$$⊢0_S=0_S$$
6	2 3 5	lmod0cl	$$⊢M\in \mathrm{LMod}\to 0_S\in R$$
7	6	adantr	$$⊢\left(M\in \mathrm{LMod}\wedge V\in B\right)\to 0_S\in R$$
8		eqid	$$⊢{\cdot }_M={\cdot }_M$$
9	1 2 3 8 4	lincvalsn	$$⊢\left(M\in \mathrm{LMod}\wedge V\in B\wedge 0_S\in R\right)\to F\mathrm{linC}\left(M\right)\left\{V\right\}=0_S{\cdot }_{M}V$$
10	7 9	mpd3an3	$$⊢\left(M\in \mathrm{LMod}\wedge V\in B\right)\to F\mathrm{linC}\left(M\right)\left\{V\right\}=0_S{\cdot }_{M}V$$
11		eqid	$$⊢0_M=0_M$$
12	1 2 8 5 11	lmod0vs	$$⊢\left(M\in \mathrm{LMod}\wedge V\in B\right)\to 0_S{\cdot }_{M}V=0_M$$
13	10 12	eqtrd	$$⊢\left(M\in \mathrm{LMod}\wedge V\in B\right)\to F\mathrm{linC}\left(M\right)\left\{V\right\}=0_M$$