Metamath Proof Explorer


Theorem hvsubsub4i

Description: Hilbert vector space addition law. (Contributed by NM, 31-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses hvass.1 A
hvass.2 B
hvass.3 C
hvadd4.4 D
Assertion hvsubsub4i A - B - C - D = A - C - B - D

Proof

Step Hyp Ref Expression
1 hvass.1 A
2 hvass.2 B
3 hvass.3 C
4 hvadd4.4 D
5 neg1cn 1
6 5 2 hvmulcli -1 B
7 5 3 hvmulcli -1 C
8 5 4 hvmulcli -1 D
9 5 8 hvmulcli -1 -1 D
10 1 6 7 9 hvadd4i A + -1 B + -1 C + -1 -1 D = A + -1 C + -1 B + -1 -1 D
11 5 3 8 hvdistr1i -1 C + -1 D = -1 C + -1 -1 D
12 11 oveq2i A + -1 B + -1 C + -1 D = A + -1 B + -1 C + -1 -1 D
13 5 2 8 hvdistr1i -1 B + -1 D = -1 B + -1 -1 D
14 13 oveq2i A + -1 C + -1 B + -1 D = A + -1 C + -1 B + -1 -1 D
15 10 12 14 3eqtr4i A + -1 B + -1 C + -1 D = A + -1 C + -1 B + -1 D
16 1 6 hvaddcli A + -1 B
17 3 8 hvaddcli C + -1 D
18 16 17 hvsubvali A + -1 B - C + -1 D = A + -1 B + -1 C + -1 D
19 1 7 hvaddcli A + -1 C
20 2 8 hvaddcli B + -1 D
21 19 20 hvsubvali A + -1 C - B + -1 D = A + -1 C + -1 B + -1 D
22 15 18 21 3eqtr4i A + -1 B - C + -1 D = A + -1 C - B + -1 D
23 1 2 hvsubvali A - B = A + -1 B
24 3 4 hvsubvali C - D = C + -1 D
25 23 24 oveq12i A - B - C - D = A + -1 B - C + -1 D
26 1 3 hvsubvali A - C = A + -1 C
27 2 4 hvsubvali B - D = B + -1 D
28 26 27 oveq12i A - C - B - D = A + -1 C - B + -1 D
29 22 25 28 3eqtr4i A - B - C - D = A - C - B - D