Metamath Proof Explorer

Theorem nvmeq0

Description: The difference between two vectors is zero iff they are equal. (Contributed by NM, 24-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 nvmeq0 
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A M B ) = Z <-> A = B ) )

Proof

Step Hyp Ref Expression
1 nvmeq0.1 
 |-  X = ( BaseSet ` U )
2 nvmeq0.3 
 |-  M = ( -v ` U )
3 nvmeq0.5 
 |-  Z = ( 0vec ` U )
4 1 2 nvmcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A M B ) e. X )
5 4 3expb 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) ) -> ( A M B ) e. X )
6 1 3 nvzcl 
 |-  ( U e. NrmCVec -> Z e. X )
7 6 adantr 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) ) -> Z e. X )
8 simprr 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) ) -> B e. X )
9 5 7 8 3jca 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) ) -> ( ( A M B ) e. X /\ Z e. X /\ B e. X ) )
10 eqid 
 |-  ( +v ` U ) = ( +v ` U )
11 1 10 nvrcan 
 |-  ( ( U e. NrmCVec /\ ( ( A M B ) e. X /\ Z e. X /\ B e. X ) ) -> ( ( ( A M B ) ( +v ` U ) B ) = ( Z ( +v ` U ) B ) <-> ( A M B ) = Z ) )
12 9 11 syldan 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) ) -> ( ( ( A M B ) ( +v ` U ) B ) = ( Z ( +v ` U ) B ) <-> ( A M B ) = Z ) )
13 12 3impb 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( A M B ) ( +v ` U ) B ) = ( Z ( +v ` U ) B ) <-> ( A M B ) = Z ) )
14 1 10 2 nvnpcan 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A M B ) ( +v ` U ) B ) = A )
15 1 10 3 nv0lid 
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( Z ( +v ` U ) B ) = B )
16 15 3adant2 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( Z ( +v ` U ) B ) = B )
17 14 16 eqeq12d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( A M B ) ( +v ` U ) B ) = ( Z ( +v ` U ) B ) <-> A = B ) )
18 13 17 bitr3d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A M B ) = Z <-> A = B ) )