Theorem cph2subdi

Description: Distributive law for inner product subtraction. Complex version of ip2subdi . (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	cphipcj.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	cphipcj.v	$$⊢V={\mathrm{Base}}_W$$
	cphsubdir.m	$$⊢\underset{\dot{}}{-}={-}_W$$
	cph2subdi.1	$$⊢\phi \to W\in \mathrm{CPreHil}$$
	cph2subdi.2	$$⊢\phi \to A\in V$$
	cph2subdi.3	$$⊢\phi \to B\in V$$
	cph2subdi.4	$$⊢\phi \to C\in V$$
	cph2subdi.5	$$⊢\phi \to D\in V$$
Assertion	cph2subdi	$$⊢\phi \to \left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{,}\left(C\underset{\dot{}}{-}D\right)=\left(A\underset{\dot{}}{,}C\right)+\left(B\underset{\dot{}}{,}D\right)-\left(\left(A\underset{\dot{}}{,}D\right)+\left(B\underset{\dot{}}{,}C\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		cphipcj.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
2		cphipcj.v	$$⊢V={\mathrm{Base}}_W$$
3		cphsubdir.m	$$⊢\underset{\dot{}}{-}={-}_W$$
4		cph2subdi.1	$$⊢\phi \to W\in \mathrm{CPreHil}$$
5		cph2subdi.2	$$⊢\phi \to A\in V$$
6		cph2subdi.3	$$⊢\phi \to B\in V$$
7		cph2subdi.4	$$⊢\phi \to C\in V$$
8		cph2subdi.5	$$⊢\phi \to D\in V$$
9		cphclm	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{CMod}$$
10	4 9	syl	$$⊢\phi \to W\in \mathrm{CMod}$$
11		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
12	11	clmadd	$$⊢W\in \mathrm{CMod}\to +={+}_{\mathrm{Scalar}\left(W\right)}$$
13	10 12	syl	$$⊢\phi \to +={+}_{\mathrm{Scalar}\left(W\right)}$$
14	13	oveqd	$$⊢\phi \to \left(A\underset{\dot{}}{,}C\right)+\left(B\underset{\dot{}}{,}D\right)=\left(A\underset{\dot{}}{,}C\right){+}_{\mathrm{Scalar}\left(W\right)}\left(B\underset{\dot{}}{,}D\right)$$
15	13	oveqd	$$⊢\phi \to \left(A\underset{\dot{}}{,}D\right)+\left(B\underset{\dot{}}{,}C\right)=\left(A\underset{\dot{}}{,}D\right){+}_{\mathrm{Scalar}\left(W\right)}\left(B\underset{\dot{}}{,}C\right)$$
16	14 15	oveq12d	$$⊢\phi \to \left(\left(A\underset{\dot{}}{,}C\right)+\left(B\underset{\dot{}}{,}D\right)\right){-}_{\mathrm{Scalar}\left(W\right)}\left(\left(A\underset{\dot{}}{,}D\right)+\left(B\underset{\dot{}}{,}C\right)\right)=\left(\left(A\underset{\dot{}}{,}C\right){+}_{\mathrm{Scalar}\left(W\right)}\left(B\underset{\dot{}}{,}D\right)\right){-}_{\mathrm{Scalar}\left(W\right)}\left(\left(A\underset{\dot{}}{,}D\right){+}_{\mathrm{Scalar}\left(W\right)}\left(B\underset{\dot{}}{,}C\right)\right)$$
17		cphphl	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{PreHil}$$
18	4 17	syl	$$⊢\phi \to W\in \mathrm{PreHil}$$
19		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
20	11 1 2 19	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge C\in V\right)\to A\underset{\dot{}}{,}C\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
21	18 5 7 20	syl3anc	$$⊢\phi \to A\underset{\dot{}}{,}C\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
22	11 1 2 19	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge B\in V\wedge D\in V\right)\to B\underset{\dot{}}{,}D\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
23	18 6 8 22	syl3anc	$$⊢\phi \to B\underset{\dot{}}{,}D\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
24	11 19	clmacl	$$⊢\left(W\in \mathrm{CMod}\wedge A\underset{\dot{}}{,}C\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge B\underset{\dot{}}{,}D\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\right)\to \left(A\underset{\dot{}}{,}C\right)+\left(B\underset{\dot{}}{,}D\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
25	10 21 23 24	syl3anc	$$⊢\phi \to \left(A\underset{\dot{}}{,}C\right)+\left(B\underset{\dot{}}{,}D\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
26	11 1 2 19	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge D\in V\right)\to A\underset{\dot{}}{,}D\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
27	18 5 8 26	syl3anc	$$⊢\phi \to A\underset{\dot{}}{,}D\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
28	11 1 2 19	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge B\in V\wedge C\in V\right)\to B\underset{\dot{}}{,}C\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
29	18 6 7 28	syl3anc	$$⊢\phi \to B\underset{\dot{}}{,}C\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
30	11 19	clmacl	$$⊢\left(W\in \mathrm{CMod}\wedge A\underset{\dot{}}{,}D\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge B\underset{\dot{}}{,}C\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\right)\to \left(A\underset{\dot{}}{,}D\right)+\left(B\underset{\dot{}}{,}C\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
31	10 27 29 30	syl3anc	$$⊢\phi \to \left(A\underset{\dot{}}{,}D\right)+\left(B\underset{\dot{}}{,}C\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
32	11 19	clmsub	$$⊢\left(W\in \mathrm{CMod}\wedge \left(A\underset{\dot{}}{,}C\right)+\left(B\underset{\dot{}}{,}D\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge \left(A\underset{\dot{}}{,}D\right)+\left(B\underset{\dot{}}{,}C\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\right)\to \left(A\underset{\dot{}}{,}C\right)+\left(B\underset{\dot{}}{,}D\right)-\left(\left(A\underset{\dot{}}{,}D\right)+\left(B\underset{\dot{}}{,}C\right)\right)=\left(\left(A\underset{\dot{}}{,}C\right)+\left(B\underset{\dot{}}{,}D\right)\right){-}_{\mathrm{Scalar}\left(W\right)}\left(\left(A\underset{\dot{}}{,}D\right)+\left(B\underset{\dot{}}{,}C\right)\right)$$
33	10 25 31 32	syl3anc	$$⊢\phi \to \left(A\underset{\dot{}}{,}C\right)+\left(B\underset{\dot{}}{,}D\right)-\left(\left(A\underset{\dot{}}{,}D\right)+\left(B\underset{\dot{}}{,}C\right)\right)=\left(\left(A\underset{\dot{}}{,}C\right)+\left(B\underset{\dot{}}{,}D\right)\right){-}_{\mathrm{Scalar}\left(W\right)}\left(\left(A\underset{\dot{}}{,}D\right)+\left(B\underset{\dot{}}{,}C\right)\right)$$
34		eqid	$$⊢{-}_{\mathrm{Scalar}\left(W\right)}={-}_{\mathrm{Scalar}\left(W\right)}$$
35		eqid	$$⊢{+}_{\mathrm{Scalar}\left(W\right)}={+}_{\mathrm{Scalar}\left(W\right)}$$
36	11 1 2 3 34 35 18 5 6 7 8	ip2subdi	$$⊢\phi \to \left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{,}\left(C\underset{\dot{}}{-}D\right)=\left(\left(A\underset{\dot{}}{,}C\right){+}_{\mathrm{Scalar}\left(W\right)}\left(B\underset{\dot{}}{,}D\right)\right){-}_{\mathrm{Scalar}\left(W\right)}\left(\left(A\underset{\dot{}}{,}D\right){+}_{\mathrm{Scalar}\left(W\right)}\left(B\underset{\dot{}}{,}C\right)\right)$$
37	16 33 36	3eqtr4rd	$$⊢\phi \to \left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{,}\left(C\underset{\dot{}}{-}D\right)=\left(A\underset{\dot{}}{,}C\right)+\left(B\underset{\dot{}}{,}D\right)-\left(\left(A\underset{\dot{}}{,}D\right)+\left(B\underset{\dot{}}{,}C\right)\right)$$