This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) , ( 𝐶 − 𝐷 ) ) = ( ( ( 𝐴 , 𝐶 ) + ( 𝐵 , 𝐷 ) ) 𝑆 ( ( 𝐴 , 𝐷 ) + ( 𝐵 , 𝐶 ) ) ) )