Theorem ip2subdi

Description: Distributive law for inner product subtraction. (Contributed by Mario Carneiro, 8-Oct-2015)

	Ref	Expression
Hypotheses	phlsrng.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	phllmhm.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
	phllmhm.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	ipsubdir.m	⊢ − = ( -g ‘ 𝑊 )
	ipsubdir.s	⊢ 𝑆 = ( -g ‘ 𝐹 )
	ip2subdi.p	⊢ + = ( +g ‘ 𝐹 )
	ip2subdi.1	⊢ ( 𝜑 → 𝑊 ∈ PreHil )
	ip2subdi.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	ip2subdi.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	ip2subdi.4	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	ip2subdi.5	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
Assertion	ip2subdi	⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) , ( 𝐶 − 𝐷 ) ) = ( ( ( 𝐴 , 𝐶 ) + ( 𝐵 , 𝐷 ) ) 𝑆 ( ( 𝐴 , 𝐷 ) + ( 𝐵 , 𝐶 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		phlsrng.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		phllmhm.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
3		phllmhm.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
4		ipsubdir.m	⊢ − = ( -g ‘ 𝑊 )
5		ipsubdir.s	⊢ 𝑆 = ( -g ‘ 𝐹 )
6		ip2subdi.p	⊢ + = ( +g ‘ 𝐹 )
7		ip2subdi.1	⊢ ( 𝜑 → 𝑊 ∈ PreHil )
8		ip2subdi.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
9		ip2subdi.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
10		ip2subdi.4	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
11		ip2subdi.5	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
12		eqid	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
13		phllmod	⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
14	7 13	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
15	1	lmodring	⊢ ( 𝑊 ∈ LMod → 𝐹 ∈ Ring )
16	14 15	syl	⊢ ( 𝜑 → 𝐹 ∈ Ring )
17		ringabl	⊢ ( 𝐹 ∈ Ring → 𝐹 ∈ Abel )
18	16 17	syl	⊢ ( 𝜑 → 𝐹 ∈ Abel )
19	1 2 3 12	ipcl	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐴 , 𝐶 ) ∈ ( Base ‘ 𝐹 ) )
20	7 8 10 19	syl3anc	⊢ ( 𝜑 → ( 𝐴 , 𝐶 ) ∈ ( Base ‘ 𝐹 ) )
21	1 2 3 12	ipcl	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) → ( 𝐴 , 𝐷 ) ∈ ( Base ‘ 𝐹 ) )
22	7 8 11 21	syl3anc	⊢ ( 𝜑 → ( 𝐴 , 𝐷 ) ∈ ( Base ‘ 𝐹 ) )
23	1 2 3 12	ipcl	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐵 , 𝐶 ) ∈ ( Base ‘ 𝐹 ) )
24	7 9 10 23	syl3anc	⊢ ( 𝜑 → ( 𝐵 , 𝐶 ) ∈ ( Base ‘ 𝐹 ) )
25	12 6 5 18 20 22 24	ablsubsub4	⊢ ( 𝜑 → ( ( ( 𝐴 , 𝐶 ) 𝑆 ( 𝐴 , 𝐷 ) ) 𝑆 ( 𝐵 , 𝐶 ) ) = ( ( 𝐴 , 𝐶 ) 𝑆 ( ( 𝐴 , 𝐷 ) + ( 𝐵 , 𝐶 ) ) ) )
26	25	oveq1d	⊢ ( 𝜑 → ( ( ( ( 𝐴 , 𝐶 ) 𝑆 ( 𝐴 , 𝐷 ) ) 𝑆 ( 𝐵 , 𝐶 ) ) + ( 𝐵 , 𝐷 ) ) = ( ( ( 𝐴 , 𝐶 ) 𝑆 ( ( 𝐴 , 𝐷 ) + ( 𝐵 , 𝐶 ) ) ) + ( 𝐵 , 𝐷 ) ) )
27	3 4	lmodvsubcl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) → ( 𝐶 − 𝐷 ) ∈ 𝑉 )
28	14 10 11 27	syl3anc	⊢ ( 𝜑 → ( 𝐶 − 𝐷 ) ∈ 𝑉 )
29	1 2 3 4 5	ipsubdir	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐶 − 𝐷 ) ∈ 𝑉 ) ) → ( ( 𝐴 − 𝐵 ) , ( 𝐶 − 𝐷 ) ) = ( ( 𝐴 , ( 𝐶 − 𝐷 ) ) 𝑆 ( 𝐵 , ( 𝐶 − 𝐷 ) ) ) )
30	7 8 9 28 29	syl13anc	⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) , ( 𝐶 − 𝐷 ) ) = ( ( 𝐴 , ( 𝐶 − 𝐷 ) ) 𝑆 ( 𝐵 , ( 𝐶 − 𝐷 ) ) ) )
31	1 2 3 4 5	ipsubdi	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( 𝐴 , ( 𝐶 − 𝐷 ) ) = ( ( 𝐴 , 𝐶 ) 𝑆 ( 𝐴 , 𝐷 ) ) )
32	7 8 10 11 31	syl13anc	⊢ ( 𝜑 → ( 𝐴 , ( 𝐶 − 𝐷 ) ) = ( ( 𝐴 , 𝐶 ) 𝑆 ( 𝐴 , 𝐷 ) ) )
33	1 2 3 4 5	ipsubdi	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( 𝐵 , ( 𝐶 − 𝐷 ) ) = ( ( 𝐵 , 𝐶 ) 𝑆 ( 𝐵 , 𝐷 ) ) )
34	7 9 10 11 33	syl13anc	⊢ ( 𝜑 → ( 𝐵 , ( 𝐶 − 𝐷 ) ) = ( ( 𝐵 , 𝐶 ) 𝑆 ( 𝐵 , 𝐷 ) ) )
35	32 34	oveq12d	⊢ ( 𝜑 → ( ( 𝐴 , ( 𝐶 − 𝐷 ) ) 𝑆 ( 𝐵 , ( 𝐶 − 𝐷 ) ) ) = ( ( ( 𝐴 , 𝐶 ) 𝑆 ( 𝐴 , 𝐷 ) ) 𝑆 ( ( 𝐵 , 𝐶 ) 𝑆 ( 𝐵 , 𝐷 ) ) ) )
36		ringgrp	⊢ ( 𝐹 ∈ Ring → 𝐹 ∈ Grp )
37	16 36	syl	⊢ ( 𝜑 → 𝐹 ∈ Grp )
38	12 5	grpsubcl	⊢ ( ( 𝐹 ∈ Grp ∧ ( 𝐴 , 𝐶 ) ∈ ( Base ‘ 𝐹 ) ∧ ( 𝐴 , 𝐷 ) ∈ ( Base ‘ 𝐹 ) ) → ( ( 𝐴 , 𝐶 ) 𝑆 ( 𝐴 , 𝐷 ) ) ∈ ( Base ‘ 𝐹 ) )
39	37 20 22 38	syl3anc	⊢ ( 𝜑 → ( ( 𝐴 , 𝐶 ) 𝑆 ( 𝐴 , 𝐷 ) ) ∈ ( Base ‘ 𝐹 ) )
40	1 2 3 12	ipcl	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) → ( 𝐵 , 𝐷 ) ∈ ( Base ‘ 𝐹 ) )
41	7 9 11 40	syl3anc	⊢ ( 𝜑 → ( 𝐵 , 𝐷 ) ∈ ( Base ‘ 𝐹 ) )
42	12 6 5 18 39 24 41	ablsubsub	⊢ ( 𝜑 → ( ( ( 𝐴 , 𝐶 ) 𝑆 ( 𝐴 , 𝐷 ) ) 𝑆 ( ( 𝐵 , 𝐶 ) 𝑆 ( 𝐵 , 𝐷 ) ) ) = ( ( ( ( 𝐴 , 𝐶 ) 𝑆 ( 𝐴 , 𝐷 ) ) 𝑆 ( 𝐵 , 𝐶 ) ) + ( 𝐵 , 𝐷 ) ) )
43	30 35 42	3eqtrd	⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) , ( 𝐶 − 𝐷 ) ) = ( ( ( ( 𝐴 , 𝐶 ) 𝑆 ( 𝐴 , 𝐷 ) ) 𝑆 ( 𝐵 , 𝐶 ) ) + ( 𝐵 , 𝐷 ) ) )
44	12 6	ringacl	⊢ ( ( 𝐹 ∈ Ring ∧ ( 𝐴 , 𝐷 ) ∈ ( Base ‘ 𝐹 ) ∧ ( 𝐵 , 𝐶 ) ∈ ( Base ‘ 𝐹 ) ) → ( ( 𝐴 , 𝐷 ) + ( 𝐵 , 𝐶 ) ) ∈ ( Base ‘ 𝐹 ) )
45	16 22 24 44	syl3anc	⊢ ( 𝜑 → ( ( 𝐴 , 𝐷 ) + ( 𝐵 , 𝐶 ) ) ∈ ( Base ‘ 𝐹 ) )
46	12 6 5	abladdsub	⊢ ( ( 𝐹 ∈ Abel ∧ ( ( 𝐴 , 𝐶 ) ∈ ( Base ‘ 𝐹 ) ∧ ( 𝐵 , 𝐷 ) ∈ ( Base ‘ 𝐹 ) ∧ ( ( 𝐴 , 𝐷 ) + ( 𝐵 , 𝐶 ) ) ∈ ( Base ‘ 𝐹 ) ) ) → ( ( ( 𝐴 , 𝐶 ) + ( 𝐵 , 𝐷 ) ) 𝑆 ( ( 𝐴 , 𝐷 ) + ( 𝐵 , 𝐶 ) ) ) = ( ( ( 𝐴 , 𝐶 ) 𝑆 ( ( 𝐴 , 𝐷 ) + ( 𝐵 , 𝐶 ) ) ) + ( 𝐵 , 𝐷 ) ) )
47	18 20 41 45 46	syl13anc	⊢ ( 𝜑 → ( ( ( 𝐴 , 𝐶 ) + ( 𝐵 , 𝐷 ) ) 𝑆 ( ( 𝐴 , 𝐷 ) + ( 𝐵 , 𝐶 ) ) ) = ( ( ( 𝐴 , 𝐶 ) 𝑆 ( ( 𝐴 , 𝐷 ) + ( 𝐵 , 𝐶 ) ) ) + ( 𝐵 , 𝐷 ) ) )
48	26 43 47	3eqtr4d	⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) , ( 𝐶 − 𝐷 ) ) = ( ( ( 𝐴 , 𝐶 ) + ( 𝐵 , 𝐷 ) ) 𝑆 ( ( 𝐴 , 𝐷 ) + ( 𝐵 , 𝐶 ) ) ) )