Theorem ip2subdi

Description: Distributive law for inner product subtraction. (Contributed by Mario Carneiro, 8-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$$
	ipsubdir.m	$$⊢\underset{\dot{}}{-}={-}_W$$
	ipsubdir.s	$$⊢S={-}_F$$
	ip2subdi.p	$$⊢\underset{\dot{}}{+}={+}_F$$
	ip2subdi.1	$$⊢\phi \to W\in \mathrm{PreHil}$$
	ip2subdi.2	$$⊢\phi \to A\in V$$
	ip2subdi.3	$$⊢\phi \to B\in V$$
	ip2subdi.4	$$⊢\phi \to C\in V$$
	ip2subdi.5	$$⊢\phi \to D\in V$$
Assertion	ip2subdi	$$⊢\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)S\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		ipsubdir.m	$$⊢\underset{\dot{}}{-}={-}_W$$
5		ipsubdir.s	$$⊢S={-}_F$$
6		ip2subdi.p	$$⊢\underset{\dot{}}{+}={+}_F$$
7		ip2subdi.1	$$⊢\phi \to W\in \mathrm{PreHil}$$
8		ip2subdi.2	$$⊢\phi \to A\in V$$
9		ip2subdi.3	$$⊢\phi \to B\in V$$
10		ip2subdi.4	$$⊢\phi \to C\in V$$
11		ip2subdi.5	$$⊢\phi \to D\in V$$
12		eqid	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
13		phllmod	$$⊢W\in \mathrm{PreHil}\to W\in \mathrm{LMod}$$
14	7 13	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
15	1	lmodring	$$⊢W\in \mathrm{LMod}\to F\in \mathrm{Ring}$$
16	14 15	syl	$$⊢\phi \to F\in \mathrm{Ring}$$
17		ringabl	$$⊢F\in \mathrm{Ring}\to F\in \mathrm{Abel}$$
18	16 17	syl	$$⊢\phi \to F\in \mathrm{Abel}$$
19	1 2 3 12	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge C\in V\right)\to A\underset{\dot{}}{,}C\in {\mathrm{Base}}_F$$
20	7 8 10 19	syl3anc	$$⊢\phi \to A\underset{\dot{}}{,}C\in {\mathrm{Base}}_F$$
21	1 2 3 12	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge D\in V\right)\to A\underset{\dot{}}{,}D\in {\mathrm{Base}}_F$$
22	7 8 11 21	syl3anc	$$⊢\phi \to A\underset{\dot{}}{,}D\in {\mathrm{Base}}_F$$
23	1 2 3 12	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge B\in V\wedge C\in V\right)\to B\underset{\dot{}}{,}C\in {\mathrm{Base}}_F$$
24	7 9 10 23	syl3anc	$$⊢\phi \to B\underset{\dot{}}{,}C\in {\mathrm{Base}}_F$$
25	12 6 5 18 20 22 24	ablsubsub4	$$⊢\phi \to \left(\left(A\underset{\dot{}}{,}C\right)S\left(A\underset{\dot{}}{,}D\right)\right)S\left(B\underset{\dot{}}{,}C\right)=\left(A\underset{\dot{}}{,}C\right)S\left(\left(A\underset{\dot{}}{,}D\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{,}C\right)\right)$$
26	25	oveq1d	$$⊢\phi \to \left(\left(\left(A\underset{\dot{}}{,}C\right)S\left(A\underset{\dot{}}{,}D\right)\right)S\left(B\underset{\dot{}}{,}C\right)\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{,}D\right)=\left(\left(A\underset{\dot{}}{,}C\right)S\left(\left(A\underset{\dot{}}{,}D\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{,}C\right)\right)\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{,}D\right)$$
27	3 4	lmodvsubcl	$$⊢\left(W\in \mathrm{LMod}\wedge C\in V\wedge D\in V\right)\to C\underset{\dot{}}{-}D\in V$$
28	14 10 11 27	syl3anc	$$⊢\phi \to C\underset{\dot{}}{-}D\in V$$
29	1 2 3 4 5	ipsubdir	$$⊢\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)S\left(B\underset{\dot{}}{,}\left(C\underset{\dot{}}{-}D\right)\right)$$
30	7 8 9 28 29	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)S\left(B\underset{\dot{}}{,}\left(C\underset{\dot{}}{-}D\right)\right)$$
31	1 2 3 4 5	ipsubdi	$$⊢\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)S\left(A\underset{\dot{}}{,}D\right)$$
32	7 8 10 11 31	syl13anc	$$⊢\phi \to A\underset{\dot{}}{,}\left(C\underset{\dot{}}{-}D\right)=\left(A\underset{\dot{}}{,}C\right)S\left(A\underset{\dot{}}{,}D\right)$$
33	1 2 3 4 5	ipsubdi	$$⊢\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)S\left(B\underset{\dot{}}{,}D\right)$$
34	7 9 10 11 33	syl13anc	$$⊢\phi \to B\underset{\dot{}}{,}\left(C\underset{\dot{}}{-}D\right)=\left(B\underset{\dot{}}{,}C\right)S\left(B\underset{\dot{}}{,}D\right)$$
35	32 34	oveq12d	$$⊢\phi \to \left(A\underset{\dot{}}{,}\left(C\underset{\dot{}}{-}D\right)\right)S\left(B\underset{\dot{}}{,}\left(C\underset{\dot{}}{-}D\right)\right)=\left(\left(A\underset{\dot{}}{,}C\right)S\left(A\underset{\dot{}}{,}D\right)\right)S\left(\left(B\underset{\dot{}}{,}C\right)S\left(B\underset{\dot{}}{,}D\right)\right)$$
36		ringgrp	$$⊢F\in \mathrm{Ring}\to F\in \mathrm{Grp}$$
37	16 36	syl	$$⊢\phi \to F\in \mathrm{Grp}$$
38	12 5	grpsubcl	$$⊢\left(F\in \mathrm{Grp}\wedge A\underset{\dot{}}{,}C\in {\mathrm{Base}}_F\wedge A\underset{\dot{}}{,}D\in {\mathrm{Base}}_F\right)\to \left(A\underset{\dot{}}{,}C\right)S\left(A\underset{\dot{}}{,}D\right)\in {\mathrm{Base}}_F$$
39	37 20 22 38	syl3anc	$$⊢\phi \to \left(A\underset{\dot{}}{,}C\right)S\left(A\underset{\dot{}}{,}D\right)\in {\mathrm{Base}}_F$$
40	1 2 3 12	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge B\in V\wedge D\in V\right)\to B\underset{\dot{}}{,}D\in {\mathrm{Base}}_F$$
41	7 9 11 40	syl3anc	$$⊢\phi \to B\underset{\dot{}}{,}D\in {\mathrm{Base}}_F$$
42	12 6 5 18 39 24 41	ablsubsub	$$⊢\phi \to \left(\left(A\underset{\dot{}}{,}C\right)S\left(A\underset{\dot{}}{,}D\right)\right)S\left(\left(B\underset{\dot{}}{,}C\right)S\left(B\underset{\dot{}}{,}D\right)\right)=\left(\left(\left(A\underset{\dot{}}{,}C\right)S\left(A\underset{\dot{}}{,}D\right)\right)S\left(B\underset{\dot{}}{,}C\right)\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{,}D\right)$$
43	30 35 42	3eqtrd	$$⊢\phi \to \left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{,}\left(C\underset{\dot{}}{-}D\right)=\left(\left(\left(A\underset{\dot{}}{,}C\right)S\left(A\underset{\dot{}}{,}D\right)\right)S\left(B\underset{\dot{}}{,}C\right)\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{,}D\right)$$
44	12 6	ringacl	$$⊢\left(F\in \mathrm{Ring}\wedge A\underset{\dot{}}{,}D\in {\mathrm{Base}}_F\wedge B\underset{\dot{}}{,}C\in {\mathrm{Base}}_F\right)\to \left(A\underset{\dot{}}{,}D\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{,}C\right)\in {\mathrm{Base}}_F$$
45	16 22 24 44	syl3anc	$$⊢\phi \to \left(A\underset{\dot{}}{,}D\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{,}C\right)\in {\mathrm{Base}}_F$$
46	12 6 5	abladdsub	$$⊢\left(F\in \mathrm{Abel}\wedge \left(A\underset{\dot{}}{,}C\in {\mathrm{Base}}_F\wedge B\underset{\dot{}}{,}D\in {\mathrm{Base}}_F\wedge \left(A\underset{\dot{}}{,}D\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{,}C\right)\in {\mathrm{Base}}_F\right)\right)\to \left(\left(A\underset{\dot{}}{,}C\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{,}D\right)\right)S\left(\left(A\underset{\dot{}}{,}D\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{,}C\right)\right)=\left(\left(A\underset{\dot{}}{,}C\right)S\left(\left(A\underset{\dot{}}{,}D\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{,}C\right)\right)\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{,}D\right)$$
47	18 20 41 45 46	syl13anc	$$⊢\phi \to \left(\left(A\underset{\dot{}}{,}C\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{,}D\right)\right)S\left(\left(A\underset{\dot{}}{,}D\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{,}C\right)\right)=\left(\left(A\underset{\dot{}}{,}C\right)S\left(\left(A\underset{\dot{}}{,}D\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{,}C\right)\right)\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{,}D\right)$$
48	26 43 47	3eqtr4d	$$⊢\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)S\left(\left(A\underset{\dot{}}{,}D\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{,}C\right)\right)$$