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 ) )