Theorem hvsubsub4i

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

	Ref	Expression
Hypotheses	hvass.1	$$⊢A\in \mathscr{H}$$
	hvass.2	$$⊢B\in \mathscr{H}$$
	hvass.3	$$⊢C\in \mathscr{H}$$
	hvadd4.4	$$⊢D\in \mathscr{H}$$
Assertion	hvsubsub4i	$$⊢\left(A{-}_{ℎ}B\right){-}_{ℎ}\left(C{-}_{ℎ}D\right)=\left(A{-}_{ℎ}C\right){-}_{ℎ}\left(B{-}_{ℎ}D\right)$$

Proof

Step	Hyp	Ref	Expression
1		hvass.1	$$⊢A\in \mathscr{H}$$
2		hvass.2	$$⊢B\in \mathscr{H}$$
3		hvass.3	$$⊢C\in \mathscr{H}$$
4		hvadd4.4	$$⊢D\in \mathscr{H}$$
5		neg1cn	$$⊢-1\in ℂ$$
6	5 2	hvmulcli	$$⊢-1{\cdot }_{ℎ}B\in \mathscr{H}$$
7	5 3	hvmulcli	$$⊢-1{\cdot }_{ℎ}C\in \mathscr{H}$$
8	5 4	hvmulcli	$$⊢-1{\cdot }_{ℎ}D\in \mathscr{H}$$
9	5 8	hvmulcli	$$⊢-1{\cdot }_{ℎ}\left(-1{\cdot }_{ℎ}D\right)\in \mathscr{H}$$
10	1 6 7 9	hvadd4i	$$⊢\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right){+}_{ℎ}\left(\left(-1{\cdot }_{ℎ}C\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}\left(-1{\cdot }_{ℎ}D\right)\right)\right)=\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}C\right)\right){+}_{ℎ}\left(\left(-1{\cdot }_{ℎ}B\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}\left(-1{\cdot }_{ℎ}D\right)\right)\right)$$
11	5 3 8	hvdistr1i	$$⊢-1{\cdot }_{ℎ}\left(C{+}_{ℎ}\left(-1{\cdot }_{ℎ}D\right)\right)=\left(-1{\cdot }_{ℎ}C\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}\left(-1{\cdot }_{ℎ}D\right)\right)$$
12	11	oveq2i	$$⊢\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}\left(C{+}_{ℎ}\left(-1{\cdot }_{ℎ}D\right)\right)\right)=\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right){+}_{ℎ}\left(\left(-1{\cdot }_{ℎ}C\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}\left(-1{\cdot }_{ℎ}D\right)\right)\right)$$
13	5 2 8	hvdistr1i	$$⊢-1{\cdot }_{ℎ}\left(B{+}_{ℎ}\left(-1{\cdot }_{ℎ}D\right)\right)=\left(-1{\cdot }_{ℎ}B\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}\left(-1{\cdot }_{ℎ}D\right)\right)$$
14	13	oveq2i	$$⊢\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}C\right)\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}\left(B{+}_{ℎ}\left(-1{\cdot }_{ℎ}D\right)\right)\right)=\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}C\right)\right){+}_{ℎ}\left(\left(-1{\cdot }_{ℎ}B\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}\left(-1{\cdot }_{ℎ}D\right)\right)\right)$$
15	10 12 14	3eqtr4i	$$⊢\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}\left(C{+}_{ℎ}\left(-1{\cdot }_{ℎ}D\right)\right)\right)=\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}C\right)\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}\left(B{+}_{ℎ}\left(-1{\cdot }_{ℎ}D\right)\right)\right)$$
16	1 6	hvaddcli	$$⊢A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\in \mathscr{H}$$
17	3 8	hvaddcli	$$⊢C{+}_{ℎ}\left(-1{\cdot }_{ℎ}D\right)\in \mathscr{H}$$
18	16 17	hvsubvali	$$⊢\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right){-}_{ℎ}\left(C{+}_{ℎ}\left(-1{\cdot }_{ℎ}D\right)\right)=\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}\left(C{+}_{ℎ}\left(-1{\cdot }_{ℎ}D\right)\right)\right)$$
19	1 7	hvaddcli	$$⊢A{+}_{ℎ}\left(-1{\cdot }_{ℎ}C\right)\in \mathscr{H}$$
20	2 8	hvaddcli	$$⊢B{+}_{ℎ}\left(-1{\cdot }_{ℎ}D\right)\in \mathscr{H}$$
21	19 20	hvsubvali	$$⊢\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}C\right)\right){-}_{ℎ}\left(B{+}_{ℎ}\left(-1{\cdot }_{ℎ}D\right)\right)=\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}C\right)\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}\left(B{+}_{ℎ}\left(-1{\cdot }_{ℎ}D\right)\right)\right)$$
22	15 18 21	3eqtr4i	$$⊢\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right){-}_{ℎ}\left(C{+}_{ℎ}\left(-1{\cdot }_{ℎ}D\right)\right)=\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}C\right)\right){-}_{ℎ}\left(B{+}_{ℎ}\left(-1{\cdot }_{ℎ}D\right)\right)$$
23	1 2	hvsubvali	$$⊢A{-}_{ℎ}B=A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)$$
24	3 4	hvsubvali	$$⊢C{-}_{ℎ}D=C{+}_{ℎ}\left(-1{\cdot }_{ℎ}D\right)$$
25	23 24	oveq12i	$$⊢\left(A{-}_{ℎ}B\right){-}_{ℎ}\left(C{-}_{ℎ}D\right)=\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right){-}_{ℎ}\left(C{+}_{ℎ}\left(-1{\cdot }_{ℎ}D\right)\right)$$
26	1 3	hvsubvali	$$⊢A{-}_{ℎ}C=A{+}_{ℎ}\left(-1{\cdot }_{ℎ}C\right)$$
27	2 4	hvsubvali	$$⊢B{-}_{ℎ}D=B{+}_{ℎ}\left(-1{\cdot }_{ℎ}D\right)$$
28	26 27	oveq12i	$$⊢\left(A{-}_{ℎ}C\right){-}_{ℎ}\left(B{-}_{ℎ}D\right)=\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}C\right)\right){-}_{ℎ}\left(B{+}_{ℎ}\left(-1{\cdot }_{ℎ}D\right)\right)$$
29	22 25 28	3eqtr4i	$$⊢\left(A{-}_{ℎ}B\right){-}_{ℎ}\left(C{-}_{ℎ}D\right)=\left(A{-}_{ℎ}C\right){-}_{ℎ}\left(B{-}_{ℎ}D\right)$$