Theorem cph2di

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

	Ref	Expression
Hypotheses	cphipcj.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	cphipcj.v	$$⊢V={\mathrm{Base}}_W$$
	cphdir.P	$$⊢\underset{\dot{}}{+}={+}_W$$
	cph2di.1	$$⊢\phi \to W\in \mathrm{CPreHil}$$
	cph2di.2	$$⊢\phi \to A\in V$$
	cph2di.3	$$⊢\phi \to B\in V$$
	cph2di.4	$$⊢\phi \to C\in V$$
	cph2di.5	$$⊢\phi \to D\in V$$
Assertion	cph2di	$$⊢\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(A\underset{\dot{}}{,}D\right)+\left(B\underset{\dot{}}{,}C\right)$$

Proof

Step	Hyp	Ref	Expression
1		cphipcj.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
2		cphipcj.v	$$⊢V={\mathrm{Base}}_W$$
3		cphdir.P	$$⊢\underset{\dot{}}{+}={+}_W$$
4		cph2di.1	$$⊢\phi \to W\in \mathrm{CPreHil}$$
5		cph2di.2	$$⊢\phi \to A\in V$$
6		cph2di.3	$$⊢\phi \to B\in V$$
7		cph2di.4	$$⊢\phi \to C\in V$$
8		cph2di.5	$$⊢\phi \to D\in V$$
9		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
10		eqid	$$⊢{+}_{\mathrm{Scalar}\left(W\right)}={+}_{\mathrm{Scalar}\left(W\right)}$$
11		cphphl	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{PreHil}$$
12	4 11	syl	$$⊢\phi \to W\in \mathrm{PreHil}$$
13	9 1 2 3 10 12 5 6 7 8	ip2di	$$⊢\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)$$
14		cphclm	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{CMod}$$
15	9	clmadd	$$⊢W\in \mathrm{CMod}\to +={+}_{\mathrm{Scalar}\left(W\right)}$$
16	4 14 15	3syl	$$⊢\phi \to +={+}_{\mathrm{Scalar}\left(W\right)}$$
17	16	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)$$
18	16	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)$$
19	16 17 18	oveq123d	$$⊢\phi \to \left(A\underset{\dot{}}{,}C\right)+\left(B\underset{\dot{}}{,}D\right)+\left(A\underset{\dot{}}{,}D\right)+\left(B\underset{\dot{}}{,}C\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)$$
20	13 19	eqtr4d	$$⊢\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(A\underset{\dot{}}{,}D\right)+\left(B\underset{\dot{}}{,}C\right)$$