Theorem nvmid

Description: A vector minus itself is the zero vector. (Contributed by NM, 28-Jan-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvmeq0.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
	nvmeq0.3	$$⊢M={-}_v\left(U\right)$$
	nvmeq0.5	$$⊢Z=0_{\mathrm{vec}}\left(U\right)$$
Assertion	nvmid	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\right)\to AMA=Z$$

Proof

Step	Hyp	Ref	Expression
1		nvmeq0.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
2		nvmeq0.3	$$⊢M={-}_v\left(U\right)$$
3		nvmeq0.5	$$⊢Z=0_{\mathrm{vec}}\left(U\right)$$
4		eqid	$$⊢A=A$$
5	1 2 3	nvmeq0	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\wedge A\in X\right)\to \left(AMA=Z\leftrightarrow A=A\right)$$
6	5	3anidm23	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\right)\to \left(AMA=Z\leftrightarrow A=A\right)$$
7	4 6	mpbiri	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\right)\to AMA=Z$$