Metamath Proof Explorer


Theorem hvsubsub4

Description: Hilbert vector space addition/subtraction law. (Contributed by NM, 2-Apr-2000) (New usage is discouraged.)

Ref Expression
Assertion hvsubsub4 A B C D A - B - C - D = A - C - B - D

Proof

Step Hyp Ref Expression
1 oveq1 A = if A A 0 A - B = if A A 0 - B
2 1 oveq1d A = if A A 0 A - B - C - D = if A A 0 - B - C - D
3 oveq1 A = if A A 0 A - C = if A A 0 - C
4 3 oveq1d A = if A A 0 A - C - B - D = if A A 0 - C - B - D
5 2 4 eqeq12d A = if A A 0 A - B - C - D = A - C - B - D if A A 0 - B - C - D = if A A 0 - C - B - D
6 oveq2 B = if B B 0 if A A 0 - B = if A A 0 - if B B 0
7 6 oveq1d B = if B B 0 if A A 0 - B - C - D = if A A 0 - if B B 0 - C - D
8 oveq1 B = if B B 0 B - D = if B B 0 - D
9 8 oveq2d B = if B B 0 if A A 0 - C - B - D = if A A 0 - C - if B B 0 - D
10 7 9 eqeq12d B = if B B 0 if A A 0 - B - C - D = if A A 0 - C - B - D if A A 0 - if B B 0 - C - D = if A A 0 - C - if B B 0 - D
11 oveq1 C = if C C 0 C - D = if C C 0 - D
12 11 oveq2d C = if C C 0 if A A 0 - if B B 0 - C - D = if A A 0 - if B B 0 - if C C 0 - D
13 oveq2 C = if C C 0 if A A 0 - C = if A A 0 - if C C 0
14 13 oveq1d C = if C C 0 if A A 0 - C - if B B 0 - D = if A A 0 - if C C 0 - if B B 0 - D
15 12 14 eqeq12d C = if C C 0 if A A 0 - if B B 0 - C - D = if A A 0 - C - if B B 0 - D if A A 0 - if B B 0 - if C C 0 - D = if A A 0 - if C C 0 - if B B 0 - D
16 oveq2 D = if D D 0 if C C 0 - D = if C C 0 - if D D 0
17 16 oveq2d D = if D D 0 if A A 0 - if B B 0 - if C C 0 - D = if A A 0 - if B B 0 - if C C 0 - if D D 0
18 oveq2 D = if D D 0 if B B 0 - D = if B B 0 - if D D 0
19 18 oveq2d D = if D D 0 if A A 0 - if C C 0 - if B B 0 - D = if A A 0 - if C C 0 - if B B 0 - if D D 0
20 17 19 eqeq12d D = if D D 0 if A A 0 - if B B 0 - if C C 0 - D = if A A 0 - if C C 0 - if B B 0 - D if A A 0 - if B B 0 - if C C 0 - if D D 0 = if A A 0 - if C C 0 - if B B 0 - if D D 0
21 ifhvhv0 if A A 0
22 ifhvhv0 if B B 0
23 ifhvhv0 if C C 0
24 ifhvhv0 if D D 0
25 21 22 23 24 hvsubsub4i if A A 0 - if B B 0 - if C C 0 - if D D 0 = if A A 0 - if C C 0 - if B B 0 - if D D 0
26 5 10 15 20 25 dedth4h A B C D A - B - C - D = A - C - B - D