Theorem ip2di

Description: Distributive law for inner product. (Contributed by NM, 17-Apr-2008) (Revised by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypotheses	phlsrng.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	phllmhm.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	phllmhm.v	$$⊢V={\mathrm{Base}}_W$$
	ipdir.g	$$⊢\underset{\dot{}}{+}={+}_W$$
	ipdir.p	$$⊢\underset{\dot{}}{⨣}={+}_F$$
	ip2di.1	$$⊢\phi \to W\in \mathrm{PreHil}$$
	ip2di.2	$$⊢\phi \to A\in V$$
	ip2di.3	$$⊢\phi \to B\in V$$
	ip2di.4	$$⊢\phi \to C\in V$$
	ip2di.5	$$⊢\phi \to D\in V$$
Assertion	ip2di	$$⊢\phi \to \left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{,}\left(C\underset{\dot{}}{+}D\right)=\left(\left(A\underset{\dot{}}{,}C\right)\underset{\dot{}}{⨣}\left(B\underset{\dot{}}{,}D\right)\right)\underset{\dot{}}{⨣}\left(\left(A\underset{\dot{}}{,}D\right)\underset{\dot{}}{⨣}\left(B\underset{\dot{}}{,}C\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		phlsrng.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		phllmhm.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
3		phllmhm.v	$$⊢V={\mathrm{Base}}_W$$
4		ipdir.g	$$⊢\underset{\dot{}}{+}={+}_W$$
5		ipdir.p	$$⊢\underset{\dot{}}{⨣}={+}_F$$
6		ip2di.1	$$⊢\phi \to W\in \mathrm{PreHil}$$
7		ip2di.2	$$⊢\phi \to A\in V$$
8		ip2di.3	$$⊢\phi \to B\in V$$
9		ip2di.4	$$⊢\phi \to C\in V$$
10		ip2di.5	$$⊢\phi \to D\in V$$
11		phllmod	$$⊢W\in \mathrm{PreHil}\to W\in \mathrm{LMod}$$
12	6 11	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
13	3 4	lmodvacl	$$⊢\left(W\in \mathrm{LMod}\wedge C\in V\wedge D\in V\right)\to C\underset{\dot{}}{+}D\in V$$
14	12 9 10 13	syl3anc	$$⊢\phi \to C\underset{\dot{}}{+}D\in V$$
15	1 2 3 4 5	ipdir	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\underset{\dot{}}{+}D\in V\right)\right)\to \left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{,}\left(C\underset{\dot{}}{+}D\right)=\left(A\underset{\dot{}}{,}\left(C\underset{\dot{}}{+}D\right)\right)\underset{\dot{}}{⨣}\left(B\underset{\dot{}}{,}\left(C\underset{\dot{}}{+}D\right)\right)$$
16	6 7 8 14 15	syl13anc	$$⊢\phi \to \left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{,}\left(C\underset{\dot{}}{+}D\right)=\left(A\underset{\dot{}}{,}\left(C\underset{\dot{}}{+}D\right)\right)\underset{\dot{}}{⨣}\left(B\underset{\dot{}}{,}\left(C\underset{\dot{}}{+}D\right)\right)$$
17	1 2 3 4 5	ipdi	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge C\in V\wedge D\in V\right)\right)\to A\underset{\dot{}}{,}\left(C\underset{\dot{}}{+}D\right)=\left(A\underset{\dot{}}{,}C\right)\underset{\dot{}}{⨣}\left(A\underset{\dot{}}{,}D\right)$$
18	6 7 9 10 17	syl13anc	$$⊢\phi \to A\underset{\dot{}}{,}\left(C\underset{\dot{}}{+}D\right)=\left(A\underset{\dot{}}{,}C\right)\underset{\dot{}}{⨣}\left(A\underset{\dot{}}{,}D\right)$$
19	1 2 3 4 5	ipdi	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(B\in V\wedge C\in V\wedge D\in V\right)\right)\to B\underset{\dot{}}{,}\left(C\underset{\dot{}}{+}D\right)=\left(B\underset{\dot{}}{,}C\right)\underset{\dot{}}{⨣}\left(B\underset{\dot{}}{,}D\right)$$
20	6 8 9 10 19	syl13anc	$$⊢\phi \to B\underset{\dot{}}{,}\left(C\underset{\dot{}}{+}D\right)=\left(B\underset{\dot{}}{,}C\right)\underset{\dot{}}{⨣}\left(B\underset{\dot{}}{,}D\right)$$
21	1	phlsrng	$$⊢W\in \mathrm{PreHil}\to F\in \mathrm{*-Ring}$$
22		srngring	$$⊢F\in \mathrm{*-Ring}\to F\in \mathrm{Ring}$$
23		ringcmn	$$⊢F\in \mathrm{Ring}\to F\in \mathrm{CMnd}$$
24	6 21 22 23	4syl	$$⊢\phi \to F\in \mathrm{CMnd}$$
25		eqid	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
26	1 2 3 25	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge B\in V\wedge C\in V\right)\to B\underset{\dot{}}{,}C\in {\mathrm{Base}}_F$$
27	6 8 9 26	syl3anc	$$⊢\phi \to B\underset{\dot{}}{,}C\in {\mathrm{Base}}_F$$
28	1 2 3 25	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge B\in V\wedge D\in V\right)\to B\underset{\dot{}}{,}D\in {\mathrm{Base}}_F$$
29	6 8 10 28	syl3anc	$$⊢\phi \to B\underset{\dot{}}{,}D\in {\mathrm{Base}}_F$$
30	25 5	cmncom	$$⊢\left(F\in \mathrm{CMnd}\wedge B\underset{\dot{}}{,}C\in {\mathrm{Base}}_F\wedge B\underset{\dot{}}{,}D\in {\mathrm{Base}}_F\right)\to \left(B\underset{\dot{}}{,}C\right)\underset{\dot{}}{⨣}\left(B\underset{\dot{}}{,}D\right)=\left(B\underset{\dot{}}{,}D\right)\underset{\dot{}}{⨣}\left(B\underset{\dot{}}{,}C\right)$$
31	24 27 29 30	syl3anc	$$⊢\phi \to \left(B\underset{\dot{}}{,}C\right)\underset{\dot{}}{⨣}\left(B\underset{\dot{}}{,}D\right)=\left(B\underset{\dot{}}{,}D\right)\underset{\dot{}}{⨣}\left(B\underset{\dot{}}{,}C\right)$$
32	20 31	eqtrd	$$⊢\phi \to B\underset{\dot{}}{,}\left(C\underset{\dot{}}{+}D\right)=\left(B\underset{\dot{}}{,}D\right)\underset{\dot{}}{⨣}\left(B\underset{\dot{}}{,}C\right)$$
33	18 32	oveq12d	$$⊢\phi \to \left(A\underset{\dot{}}{,}\left(C\underset{\dot{}}{+}D\right)\right)\underset{\dot{}}{⨣}\left(B\underset{\dot{}}{,}\left(C\underset{\dot{}}{+}D\right)\right)=\left(\left(A\underset{\dot{}}{,}C\right)\underset{\dot{}}{⨣}\left(A\underset{\dot{}}{,}D\right)\right)\underset{\dot{}}{⨣}\left(\left(B\underset{\dot{}}{,}D\right)\underset{\dot{}}{⨣}\left(B\underset{\dot{}}{,}C\right)\right)$$
34	1 2 3 25	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge C\in V\right)\to A\underset{\dot{}}{,}C\in {\mathrm{Base}}_F$$
35	6 7 9 34	syl3anc	$$⊢\phi \to A\underset{\dot{}}{,}C\in {\mathrm{Base}}_F$$
36	1 2 3 25	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge D\in V\right)\to A\underset{\dot{}}{,}D\in {\mathrm{Base}}_F$$
37	6 7 10 36	syl3anc	$$⊢\phi \to A\underset{\dot{}}{,}D\in {\mathrm{Base}}_F$$
38	25 5	cmn4	$$⊢\left(F\in \mathrm{CMnd}\wedge \left(A\underset{\dot{}}{,}C\in {\mathrm{Base}}_F\wedge A\underset{\dot{}}{,}D\in {\mathrm{Base}}_F\right)\wedge \left(B\underset{\dot{}}{,}D\in {\mathrm{Base}}_F\wedge B\underset{\dot{}}{,}C\in {\mathrm{Base}}_F\right)\right)\to \left(\left(A\underset{\dot{}}{,}C\right)\underset{\dot{}}{⨣}\left(A\underset{\dot{}}{,}D\right)\right)\underset{\dot{}}{⨣}\left(\left(B\underset{\dot{}}{,}D\right)\underset{\dot{}}{⨣}\left(B\underset{\dot{}}{,}C\right)\right)=\left(\left(A\underset{\dot{}}{,}C\right)\underset{\dot{}}{⨣}\left(B\underset{\dot{}}{,}D\right)\right)\underset{\dot{}}{⨣}\left(\left(A\underset{\dot{}}{,}D\right)\underset{\dot{}}{⨣}\left(B\underset{\dot{}}{,}C\right)\right)$$
39	24 35 37 29 27 38	syl122anc	$$⊢\phi \to \left(\left(A\underset{\dot{}}{,}C\right)\underset{\dot{}}{⨣}\left(A\underset{\dot{}}{,}D\right)\right)\underset{\dot{}}{⨣}\left(\left(B\underset{\dot{}}{,}D\right)\underset{\dot{}}{⨣}\left(B\underset{\dot{}}{,}C\right)\right)=\left(\left(A\underset{\dot{}}{,}C\right)\underset{\dot{}}{⨣}\left(B\underset{\dot{}}{,}D\right)\right)\underset{\dot{}}{⨣}\left(\left(A\underset{\dot{}}{,}D\right)\underset{\dot{}}{⨣}\left(B\underset{\dot{}}{,}C\right)\right)$$
40	16 33 39	3eqtrd	$$⊢\phi \to \left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{,}\left(C\underset{\dot{}}{+}D\right)=\left(\left(A\underset{\dot{}}{,}C\right)\underset{\dot{}}{⨣}\left(B\underset{\dot{}}{,}D\right)\right)\underset{\dot{}}{⨣}\left(\left(A\underset{\dot{}}{,}D\right)\underset{\dot{}}{⨣}\left(B\underset{\dot{}}{,}C\right)\right)$$