Theorem clmvsneg

Description: Multiplication of a vector by a negated scalar. ( lmodvsneg analog.) (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	clmvsneg.b	$$⊢B={\mathrm{Base}}_W$$
	clmvsneg.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	clmvsneg.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	clmvsneg.n	$$⊢N={inv}_g\left(W\right)$$
	clmvsneg.k	$$⊢K={\mathrm{Base}}_F$$
	clmvsneg.w	$$⊢\phi \to W\in \mathrm{CMod}$$
	clmvsneg.x	$$⊢\phi \to X\in B$$
	clmvsneg.r	$$⊢\phi \to R\in K$$
Assertion	clmvsneg	$$⊢\phi \to N\left(R\underset{\dot{}}{·}X\right)=\left(-R\right)\underset{\dot{}}{·}X$$

Proof

Step	Hyp	Ref	Expression
1		clmvsneg.b	$$⊢B={\mathrm{Base}}_W$$
2		clmvsneg.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
3		clmvsneg.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
4		clmvsneg.n	$$⊢N={inv}_g\left(W\right)$$
5		clmvsneg.k	$$⊢K={\mathrm{Base}}_F$$
6		clmvsneg.w	$$⊢\phi \to W\in \mathrm{CMod}$$
7		clmvsneg.x	$$⊢\phi \to X\in B$$
8		clmvsneg.r	$$⊢\phi \to R\in K$$
9		eqid	$$⊢{inv}_g\left(F\right)={inv}_g\left(F\right)$$
10		clmlmod	$$⊢W\in \mathrm{CMod}\to W\in \mathrm{LMod}$$
11	6 10	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
12	1 2 3 4 5 9 11 7 8	lmodvsneg	$$⊢\phi \to N\left(R\underset{\dot{}}{·}X\right)={inv}_g\left(F\right)\left(R\right)\underset{\dot{}}{·}X$$
13	2 5	clmneg	$$⊢\left(W\in \mathrm{CMod}\wedge R\in K\right)\to -R={inv}_g\left(F\right)\left(R\right)$$
14	6 8 13	syl2anc	$$⊢\phi \to -R={inv}_g\left(F\right)\left(R\right)$$
15	14	oveq1d	$$⊢\phi \to \left(-R\right)\underset{\dot{}}{·}X={inv}_g\left(F\right)\left(R\right)\underset{\dot{}}{·}X$$
16	12 15	eqtr4d	$$⊢\phi \to N\left(R\underset{\dot{}}{·}X\right)=\left(-R\right)\underset{\dot{}}{·}X$$