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 -1B
7 5 3 hvmulcli -1C
8 5 4 hvmulcli -1D
9 5 8 hvmulcli -1-1D
10 1 6 7 9 hvadd4i A+-1B+-1C+-1-1D=A+-1C+-1B+-1-1D
11 5 3 8 hvdistr1i -1C+-1D=-1C+-1-1D
12 11 oveq2i A+-1B+-1C+-1D=A+-1B+-1C+-1-1D
13 5 2 8 hvdistr1i -1B+-1D=-1B+-1-1D
14 13 oveq2i A+-1C+-1B+-1D=A+-1C+-1B+-1-1D
15 10 12 14 3eqtr4i A+-1B+-1C+-1D=A+-1C+-1B+-1D
16 1 6 hvaddcli A+-1B
17 3 8 hvaddcli C+-1D
18 16 17 hvsubvali A+-1B-C+-1D=A+-1B+-1C+-1D
19 1 7 hvaddcli A+-1C
20 2 8 hvaddcli B+-1D
21 19 20 hvsubvali A+-1C-B+-1D=A+-1C+-1B+-1D
22 15 18 21 3eqtr4i A+-1B-C+-1D=A+-1C-B+-1D
23 1 2 hvsubvali A-B=A+-1B
24 3 4 hvsubvali C-D=C+-1D
25 23 24 oveq12i A-B-C-D=A+-1B-C+-1D
26 1 3 hvsubvali A-C=A+-1C
27 2 4 hvsubvali B-D=B+-1D
28 26 27 oveq12i A-C-B-D=A+-1C-B+-1D
29 22 25 28 3eqtr4i A-B-C-D=A-C-B-D