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 = 0 vec ⁡ U
Assertion nvmeq0 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ 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 = 0 vec ⁡ U
4 1 2 nvmcl ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A M B ∈ X
5 4 3expb ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A M B ∈ X
6 1 3 nvzcl ⊢ U ∈ NrmCVec → Z ∈ X
7 6 adantr ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → Z ∈ X
8 simprr ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → B ∈ X
9 5 7 8 3jca ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A M B ∈ X ∧ Z ∈ X ∧ B ∈ X
10 eqid ⊢ + v ⁡ U = + v ⁡ U
11 1 10 nvrcan ⊢ U ∈ NrmCVec ∧ A M B ∈ X ∧ Z ∈ X ∧ B ∈ X → A M B + v ⁡ U B = Z + v ⁡ U B ↔ A M B = Z
12 9 11 syldan ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A M B + v ⁡ U B = Z + v ⁡ U B ↔ A M B = Z
13 12 3impb ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A M B + v ⁡ U B = Z + v ⁡ U B ↔ A M B = Z
14 1 10 2 nvnpcan ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A M B + v ⁡ U B = A
15 1 10 3 nv0lid ⊢ U ∈ NrmCVec ∧ B ∈ X → Z + v ⁡ U B = B
16 15 3adant2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → Z + v ⁡ U B = B
17 14 16 eqeq12d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A M B + v ⁡ U B = Z + v ⁡ U B ↔ A = B
18 13 17 bitr3d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A M B = Z ↔ A = B