Metamath Proof Explorer

Theorem hvaddcan

Description: Cancellation law for vector addition. (Contributed by NM, 18-May-2005) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → A + ℎ B = if A ∈ ℋ A 0 ℎ + ℎ B
2 oveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → A + ℎ C = if A ∈ ℋ A 0 ℎ + ℎ C
3 1 2 eqeq12d ⊢ A = if A ∈ ℋ A 0 ℎ → A + ℎ B = A + ℎ C ↔ if A ∈ ℋ A 0 ℎ + ℎ B = if A ∈ ℋ A 0 ℎ + ℎ C
4 3 bibi1d ⊢ A = if A ∈ ℋ A 0 ℎ → A + ℎ B = A + ℎ C ↔ B = C ↔ if A ∈ ℋ A 0 ℎ + ℎ B = if A ∈ ℋ A 0 ℎ + ℎ C ↔ B = C
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 = if A ∈ ℋ A 0 ℎ + ℎ C ↔ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ = if A ∈ ℋ A 0 ℎ + ℎ C
7 eqeq1 ⊢ B = if B ∈ ℋ B 0 ℎ → B = C ↔ if B ∈ ℋ B 0 ℎ = C
8 6 7 bibi12d ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ + ℎ B = if A ∈ ℋ A 0 ℎ + ℎ C ↔ B = C ↔ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ = if A ∈ ℋ A 0 ℎ + ℎ C ↔ if B ∈ ℋ B 0 ℎ = C
9 oveq2 ⊢ C = if C ∈ ℋ C 0 ℎ → if A ∈ ℋ A 0 ℎ + ℎ C = if A ∈ ℋ A 0 ℎ + ℎ if C ∈ ℋ C 0 ℎ
10 9 eqeq2d ⊢ C = if C ∈ ℋ C 0 ℎ → if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ = if A ∈ ℋ A 0 ℎ + ℎ C ↔ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ = if A ∈ ℋ A 0 ℎ + ℎ if C ∈ ℋ C 0 ℎ
11 eqeq2 ⊢ C = if C ∈ ℋ C 0 ℎ → if B ∈ ℋ B 0 ℎ = C ↔ if B ∈ ℋ B 0 ℎ = if C ∈ ℋ C 0 ℎ
12 10 11 bibi12d ⊢ C = if C ∈ ℋ C 0 ℎ → if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ = if A ∈ ℋ A 0 ℎ + ℎ C ↔ if B ∈ ℋ B 0 ℎ = C ↔ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ = if A ∈ ℋ A 0 ℎ + ℎ if C ∈ ℋ C 0 ℎ ↔ if B ∈ ℋ B 0 ℎ = if C ∈ ℋ C 0 ℎ
13 ifhvhv0 ⊢ if A ∈ ℋ A 0 ℎ ∈ ℋ
14 ifhvhv0 ⊢ if B ∈ ℋ B 0 ℎ ∈ ℋ
15 ifhvhv0 ⊢ if C ∈ ℋ C 0 ℎ ∈ ℋ
16 13 14 15 hvaddcani ⊢ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ = if A ∈ ℋ A 0 ℎ + ℎ if C ∈ ℋ C 0 ℎ ↔ if B ∈ ℋ B 0 ℎ = if C ∈ ℋ C 0 ℎ
17 4 8 12 16 dedth3h ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A + ℎ B = A + ℎ C ↔ B = C