Metamath Proof Explorer


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 )