Metamath Proof Explorer

Theorem hvsubadd

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

Ref Expression
Assertion hvsubadd ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A - ℎ B = C ↔ B + ℎ C = A

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → A - ℎ B = if A ∈ ℋ A 0 ℎ - ℎ B
2 1 eqeq1d ⊢ A = if A ∈ ℋ A 0 ℎ → A - ℎ B = C ↔ if A ∈ ℋ A 0 ℎ - ℎ B = C
3 eqeq2 ⊢ A = if A ∈ ℋ A 0 ℎ → B + ℎ C = A ↔ B + ℎ C = if A ∈ ℋ A 0 ℎ
4 2 3 bibi12d ⊢ A = if A ∈ ℋ A 0 ℎ → A - ℎ B = C ↔ B + ℎ C = A ↔ if A ∈ ℋ A 0 ℎ - ℎ B = C ↔ B + ℎ C = if A ∈ ℋ A 0 ℎ
5 oveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ B = if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ
6 5 eqeq1d ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ B = C ↔ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ = C
7 oveq1 ⊢ B = if B ∈ ℋ B 0 ℎ → B + ℎ C = if B ∈ ℋ B 0 ℎ + ℎ C
8 7 eqeq1d ⊢ B = if B ∈ ℋ B 0 ℎ → B + ℎ C = if A ∈ ℋ A 0 ℎ ↔ if B ∈ ℋ B 0 ℎ + ℎ C = if A ∈ ℋ A 0 ℎ
9 6 8 bibi12d ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ B = C ↔ B + ℎ C = if A ∈ ℋ A 0 ℎ ↔ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ = C ↔ if B ∈ ℋ B 0 ℎ + ℎ C = if A ∈ ℋ A 0 ℎ
10 eqeq2 ⊢ C = if C ∈ ℋ C 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ = C ↔ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ = if C ∈ ℋ C 0 ℎ
11 oveq2 ⊢ C = if C ∈ ℋ C 0 ℎ → if B ∈ ℋ B 0 ℎ + ℎ C = if B ∈ ℋ B 0 ℎ + ℎ if C ∈ ℋ C 0 ℎ
12 11 eqeq1d ⊢ C = if C ∈ ℋ C 0 ℎ → if B ∈ ℋ B 0 ℎ + ℎ C = if A ∈ ℋ A 0 ℎ ↔ if B ∈ ℋ B 0 ℎ + ℎ if C ∈ ℋ C 0 ℎ = if A ∈ ℋ A 0 ℎ
13 10 12 bibi12d ⊢ C = if C ∈ ℋ C 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ = C ↔ if B ∈ ℋ B 0 ℎ + ℎ C = if A ∈ ℋ A 0 ℎ ↔ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ = if C ∈ ℋ C 0 ℎ ↔ if B ∈ ℋ B 0 ℎ + ℎ if C ∈ ℋ C 0 ℎ = if A ∈ ℋ A 0 ℎ
14 ifhvhv0 ⊢ if A ∈ ℋ A 0 ℎ ∈ ℋ
15 ifhvhv0 ⊢ if B ∈ ℋ B 0 ℎ ∈ ℋ
16 ifhvhv0 ⊢ if C ∈ ℋ C 0 ℎ ∈ ℋ
17 14 15 16 hvsubaddi ⊢ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ = if C ∈ ℋ C 0 ℎ ↔ if B ∈ ℋ B 0 ℎ + ℎ if C ∈ ℋ C 0 ℎ = if A ∈ ℋ A 0 ℎ
18 4 9 13 17 dedth3h ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A - ℎ B = C ↔ B + ℎ C = A