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