# Metamath Proof Explorer

Description: Relationship between vector subtraction and addition. (Contributed by NM, 30-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion hvsubadd ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \left({A}{-}_{ℎ}{B}={C}↔{B}{+}_{ℎ}{C}={A}\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}={C}↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}={C}\right)$
3 eqeq2 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left({B}{+}_{ℎ}{C}={A}↔{B}{+}_{ℎ}{C}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)$
4 2 3 bibi12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left(\left({A}{-}_{ℎ}{B}={C}↔{B}{+}_{ℎ}{C}={A}\right)↔\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}={C}↔{B}{+}_{ℎ}{C}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\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}={C}↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)={C}\right)$
7 oveq1 ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to {B}{+}_{ℎ}{C}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right){+}_{ℎ}{C}$
8 7 eqeq1d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to \left({B}{+}_{ℎ}{C}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)↔if\left({B}\in ℋ,{B},{0}_{ℎ}\right){+}_{ℎ}{C}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)$
9 6 8 bibi12d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to \left(\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}{B}={C}↔{B}{+}_{ℎ}{C}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)↔\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)={C}↔if\left({B}\in ℋ,{B},{0}_{ℎ}\right){+}_{ℎ}{C}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)\right)$
10 eqeq2 ${⊢}{C}=if\left({C}\in ℋ,{C},{0}_{ℎ}\right)\to \left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)={C}↔if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)=if\left({C}\in ℋ,{C},{0}_{ℎ}\right)\right)$
11 oveq2 ${⊢}{C}=if\left({C}\in ℋ,{C},{0}_{ℎ}\right)\to if\left({B}\in ℋ,{B},{0}_{ℎ}\right){+}_{ℎ}{C}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right){+}_{ℎ}if\left({C}\in ℋ,{C},{0}_{ℎ}\right)$
12 11 eqeq1d ${⊢}{C}=if\left({C}\in ℋ,{C},{0}_{ℎ}\right)\to \left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right){+}_{ℎ}{C}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)↔if\left({B}\in ℋ,{B},{0}_{ℎ}\right){+}_{ℎ}if\left({C}\in ℋ,{C},{0}_{ℎ}\right)=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)$
13 10 12 bibi12d ${⊢}{C}=if\left({C}\in ℋ,{C},{0}_{ℎ}\right)\to \left(\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)={C}↔if\left({B}\in ℋ,{B},{0}_{ℎ}\right){+}_{ℎ}{C}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)↔\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)=if\left({C}\in ℋ,{C},{0}_{ℎ}\right)↔if\left({B}\in ℋ,{B},{0}_{ℎ}\right){+}_{ℎ}if\left({C}\in ℋ,{C},{0}_{ℎ}\right)=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)\right)$
14 ifhvhv0 ${⊢}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\in ℋ$
15 ifhvhv0 ${⊢}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\in ℋ$
16 ifhvhv0 ${⊢}if\left({C}\in ℋ,{C},{0}_{ℎ}\right)\in ℋ$
17 14 15 16 hvsubaddi ${⊢}if\left({A}\in ℋ,{A},{0}_{ℎ}\right){-}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)=if\left({C}\in ℋ,{C},{0}_{ℎ}\right)↔if\left({B}\in ℋ,{B},{0}_{ℎ}\right){+}_{ℎ}if\left({C}\in ℋ,{C},{0}_{ℎ}\right)=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)$
18 4 9 13 17 dedth3h ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \left({A}{-}_{ℎ}{B}={C}↔{B}{+}_{ℎ}{C}={A}\right)$