# Metamath Proof Explorer

## Theorem hvsubeq0

Description: If the difference between two vectors is zero, they are equal. (Contributed by NM, 23-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion hvsubeq0 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to \left({A}{-}_{ℎ}{B}={0}_{ℎ}↔{A}={B}\right)$

### Proof

Step Hyp Ref Expression
1 oveq1 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {A}{-}_{ℎ}{B}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}$
2 1 eqeq1d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left({A}{-}_{ℎ}{B}={0}_{ℎ}↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}={0}_{ℎ}\right)$
3 eqeq1 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left({A}={B}↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right)={B}\right)$
4 2 3 bibi12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left(\left({A}{-}_{ℎ}{B}={0}_{ℎ}↔{A}={B}\right)↔\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}={0}_{ℎ}↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right)={B}\right)\right)$
5 oveq2 ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)$
6 5 eqeq1d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to \left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}={0}_{ℎ}↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)={0}_{ℎ}\right)$
7 eqeq2 ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to \left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)={B}↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right)=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)$
8 6 7 bibi12d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to \left(\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}={0}_{ℎ}↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right)={B}\right)↔\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)={0}_{ℎ}↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right)=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)$
9 ifhvhv0 ${⊢}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\in ℋ$
10 ifhvhv0 ${⊢}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\in ℋ$
11 9 10 hvsubeq0i ${⊢}if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)={0}_{ℎ}↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right)=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)$
12 4 8 11 dedth2h ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to \left({A}{-}_{ℎ}{B}={0}_{ℎ}↔{A}={B}\right)$