Theorem clmvz

Description: Two ways to express the negative of a vector. (Contributed by NM, 29-Feb-2008) (Revised by AV, 7-Oct-2021)

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

Proof

Step	Hyp	Ref	Expression
1		clmvz.v	$$⊢V={\mathrm{Base}}_W$$
2		clmvz.m	$$⊢\underset{\dot{}}{-}={-}_W$$
3		clmvz.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
4		clmvz.0	$$⊢\underset{\dot{}}{0}=0_W$$
5		simpl	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\right)\to W\in \mathrm{CMod}$$
6		clmgrp	$$⊢W\in \mathrm{CMod}\to W\in \mathrm{Grp}$$
7	1 4	grpidcl	$$⊢W\in \mathrm{Grp}\to \underset{\dot{}}{0}\in V$$
8	6 7	syl	$$⊢W\in \mathrm{CMod}\to \underset{\dot{}}{0}\in V$$
9	8	adantr	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\right)\to \underset{\dot{}}{0}\in V$$
10		simpr	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\right)\to A\in V$$
11		eqid	$$⊢{+}_W={+}_W$$
12		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
13	1 11 2 12 3	clmvsubval2	$$⊢\left(W\in \mathrm{CMod}\wedge \underset{\dot{}}{0}\in V\wedge A\in V\right)\to \underset{\dot{}}{0}\underset{\dot{}}{-}A=\left(-1\underset{\dot{}}{·}A\right){+}_W\underset{\dot{}}{0}$$
14	5 9 10 13	syl3anc	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\right)\to \underset{\dot{}}{0}\underset{\dot{}}{-}A=\left(-1\underset{\dot{}}{·}A\right){+}_W\underset{\dot{}}{0}$$
15		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
16	12 15	clmneg1	$$⊢W\in \mathrm{CMod}\to -1\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
17	16	adantr	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\right)\to -1\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
18	1 12 3 15	clmvscl	$$⊢\left(W\in \mathrm{CMod}\wedge -1\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge A\in V\right)\to -1\underset{\dot{}}{·}A\in V$$
19	5 17 10 18	syl3anc	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\right)\to -1\underset{\dot{}}{·}A\in V$$
20	1 11 4	grprid	$$⊢\left(W\in \mathrm{Grp}\wedge -1\underset{\dot{}}{·}A\in V\right)\to \left(-1\underset{\dot{}}{·}A\right){+}_W\underset{\dot{}}{0}=-1\underset{\dot{}}{·}A$$
21	6 19 20	syl2an2r	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\right)\to \left(-1\underset{\dot{}}{·}A\right){+}_W\underset{\dot{}}{0}=-1\underset{\dot{}}{·}A$$
22	14 21	eqtrd	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\right)\to \underset{\dot{}}{0}\underset{\dot{}}{-}A=-1\underset{\dot{}}{·}A$$