Theorem clmvslinv

Description: Minus a vector plus itself. (Contributed by NM, 4-Dec-2006) (Revised by AV, 28-Sep-2021)

	Ref	Expression
Hypotheses	clmpm1dir.v	$$⊢V={\mathrm{Base}}_W$$
	clmpm1dir.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	clmpm1dir.a	$$⊢\underset{\dot{}}{+}={+}_W$$
	clmvsrinv.0	$$⊢\underset{\dot{}}{0}=0_W$$
Assertion	clmvslinv	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\right)\to \left(-1\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}A=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		clmpm1dir.v	$$⊢V={\mathrm{Base}}_W$$
2		clmpm1dir.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
3		clmpm1dir.a	$$⊢\underset{\dot{}}{+}={+}_W$$
4		clmvsrinv.0	$$⊢\underset{\dot{}}{0}=0_W$$
5		eqid	$$⊢{inv}_g\left(W\right)={inv}_g\left(W\right)$$
6		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
7	1 5 6 2	clmvneg1	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\right)\to -1\underset{\dot{}}{·}A={inv}_g\left(W\right)\left(A\right)$$
8	7	oveq1d	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\right)\to \left(-1\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}A={inv}_g\left(W\right)\left(A\right)\underset{\dot{}}{+}A$$
9		clmgrp	$$⊢W\in \mathrm{CMod}\to W\in \mathrm{Grp}$$
10	1 3 4 5	grplinv	$$⊢\left(W\in \mathrm{Grp}\wedge A\in V\right)\to {inv}_g\left(W\right)\left(A\right)\underset{\dot{}}{+}A=\underset{\dot{}}{0}$$
11	9 10	sylan	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\right)\to {inv}_g\left(W\right)\left(A\right)\underset{\dot{}}{+}A=\underset{\dot{}}{0}$$
12	8 11	eqtrd	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\right)\to \left(-1\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}A=\underset{\dot{}}{0}$$