Theorem clmnegneg

Description: Double negative of a vector. (Contributed by NM, 6-Aug-2007) (Revised by AV, 21-Sep-2021)

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

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		neg1mulneg1e1	$$⊢-1-1=1$$
5	4	oveq1i	$$⊢-1-1\underset{\dot{}}{·}A=1\underset{\dot{}}{·}A$$
6		simpl	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\right)\to W\in \mathrm{CMod}$$
7		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
8		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
9	7 8	clmneg1	$$⊢W\in \mathrm{CMod}\to -1\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
10	9	adantr	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\right)\to -1\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
11		simpr	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\right)\to A\in V$$
12	1 7 2 8	clmvsass	$$⊢\left(W\in \mathrm{CMod}\wedge \left(-1\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge -1\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge A\in V\right)\right)\to -1-1\underset{\dot{}}{·}A=-1\underset{\dot{}}{·}\left(-1\underset{\dot{}}{·}A\right)$$
13	6 10 10 11 12	syl13anc	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\right)\to -1-1\underset{\dot{}}{·}A=-1\underset{\dot{}}{·}\left(-1\underset{\dot{}}{·}A\right)$$
14	1 2	clmvs1	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\right)\to 1\underset{\dot{}}{·}A=A$$
15	5 13 14	3eqtr3a	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\right)\to -1\underset{\dot{}}{·}\left(-1\underset{\dot{}}{·}A\right)=A$$