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 = ( BaseSet ` U )
	nvmeq0.3	|- M = ( -v ` U )
	nvmeq0.5	|- Z = ( 0vec ` U )
Assertion	nvmid	|- ( ( U e. NrmCVec /\ A e. X ) -> ( A M A ) = Z )

Proof

Step	Hyp	Ref	Expression
1		nvmeq0.1	|- X = ( BaseSet ` U )
2		nvmeq0.3	|- M = ( -v ` U )
3		nvmeq0.5	|- Z = ( 0vec ` U )
4		eqid	|- A = A
5	1 2 3	nvmeq0	|- ( ( U e. NrmCVec /\ A e. X /\ A e. X ) -> ( ( A M A ) = Z <-> A = A ) )
6	5	3anidm23	|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( A M A ) = Z <-> A = A ) )
7	4 6	mpbiri	|- ( ( U e. NrmCVec /\ A e. X ) -> ( A M A ) = Z )