Metamath Proof Explorer

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 ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
phllmhm.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
phllmhm.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
ipdir.g ⊢ + = ( +g ‘ 𝑊 )
ipdir.p ⊢ ⨣ = ( +g ‘ 𝐹 )
ip2di.1 ⊢ ( 𝜑 → 𝑊 ∈ PreHil )
ip2di.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
ip2di.3 ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
ip2di.4 ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
ip2di.5 ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
Assertion ip2di ( 𝜑 → ( ( 𝐴 + 𝐵 ) , ( 𝐶 + 𝐷 ) ) = ( ( ( 𝐴 , 𝐶 ) ⨣ ( 𝐵 , 𝐷 ) ) ⨣ ( ( 𝐴 , 𝐷 ) ⨣ ( 𝐵 , 𝐶 ) ) ) )

Proof

Step Hyp Ref Expression
1 phlsrng.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 phllmhm.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
3 phllmhm.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
4 ipdir.g ⊢ + = ( +g ‘ 𝑊 )
5 ipdir.p ⊢ ⨣ = ( +g ‘ 𝐹 )
6 ip2di.1 ⊢ ( 𝜑 → 𝑊 ∈ PreHil )
7 ip2di.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
8 ip2di.3 ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
9 ip2di.4 ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
10 ip2di.5 ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
11 phllmod ⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
12 6 11 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
13 3 4 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) → ( 𝐶 + 𝐷 ) ∈ 𝑉 )
14 12 9 10 13 syl3anc ⊢ ( 𝜑 → ( 𝐶 + 𝐷 ) ∈ 𝑉 )
15 1 2 3 4 5 ipdir ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐶 + 𝐷 ) ∈ 𝑉 ) ) → ( ( 𝐴 + 𝐵 ) , ( 𝐶 + 𝐷 ) ) = ( ( 𝐴 , ( 𝐶 + 𝐷 ) ) ⨣ ( 𝐵 , ( 𝐶 + 𝐷 ) ) ) )
16 6 7 8 14 15 syl13anc ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) , ( 𝐶 + 𝐷 ) ) = ( ( 𝐴 , ( 𝐶 + 𝐷 ) ) ⨣ ( 𝐵 , ( 𝐶 + 𝐷 ) ) ) )
17 1 2 3 4 5 ipdi ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( 𝐴 , ( 𝐶 + 𝐷 ) ) = ( ( 𝐴 , 𝐶 ) ⨣ ( 𝐴 , 𝐷 ) ) )
18 6 7 9 10 17 syl13anc ⊢ ( 𝜑 → ( 𝐴 , ( 𝐶 + 𝐷 ) ) = ( ( 𝐴 , 𝐶 ) ⨣ ( 𝐴 , 𝐷 ) ) )
19 1 2 3 4 5 ipdi ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( 𝐵 , ( 𝐶 + 𝐷 ) ) = ( ( 𝐵 , 𝐶 ) ⨣ ( 𝐵 , 𝐷 ) ) )
20 6 8 9 10 19 syl13anc ⊢ ( 𝜑 → ( 𝐵 , ( 𝐶 + 𝐷 ) ) = ( ( 𝐵 , 𝐶 ) ⨣ ( 𝐵 , 𝐷 ) ) )
21 1 phlsrng ⊢ ( 𝑊 ∈ PreHil → 𝐹 ∈ *-Ring )
22 srngring ⊢ ( 𝐹 ∈ *-Ring → 𝐹 ∈ Ring )
23 ringcmn ⊢ ( 𝐹 ∈ Ring → 𝐹 ∈ CMnd )
24 6 21 22 23 4syl ⊢ ( 𝜑 → 𝐹 ∈ CMnd )
25 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
26 1 2 3 25 ipcl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐵 , 𝐶 ) ∈ ( Base ‘ 𝐹 ) )
27 6 8 9 26 syl3anc ⊢ ( 𝜑 → ( 𝐵 , 𝐶 ) ∈ ( Base ‘ 𝐹 ) )
28 1 2 3 25 ipcl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) → ( 𝐵 , 𝐷 ) ∈ ( Base ‘ 𝐹 ) )
29 6 8 10 28 syl3anc ⊢ ( 𝜑 → ( 𝐵 , 𝐷 ) ∈ ( Base ‘ 𝐹 ) )
30 25 5 cmncom ⊢ ( ( 𝐹 ∈ CMnd ∧ ( 𝐵 , 𝐶 ) ∈ ( Base ‘ 𝐹 ) ∧ ( 𝐵 , 𝐷 ) ∈ ( Base ‘ 𝐹 ) ) → ( ( 𝐵 , 𝐶 ) ⨣ ( 𝐵 , 𝐷 ) ) = ( ( 𝐵 , 𝐷 ) ⨣ ( 𝐵 , 𝐶 ) ) )
31 24 27 29 30 syl3anc ⊢ ( 𝜑 → ( ( 𝐵 , 𝐶 ) ⨣ ( 𝐵 , 𝐷 ) ) = ( ( 𝐵 , 𝐷 ) ⨣ ( 𝐵 , 𝐶 ) ) )
32 20 31 eqtrd ⊢ ( 𝜑 → ( 𝐵 , ( 𝐶 + 𝐷 ) ) = ( ( 𝐵 , 𝐷 ) ⨣ ( 𝐵 , 𝐶 ) ) )
33 18 32 oveq12d ⊢ ( 𝜑 → ( ( 𝐴 , ( 𝐶 + 𝐷 ) ) ⨣ ( 𝐵 , ( 𝐶 + 𝐷 ) ) ) = ( ( ( 𝐴 , 𝐶 ) ⨣ ( 𝐴 , 𝐷 ) ) ⨣ ( ( 𝐵 , 𝐷 ) ⨣ ( 𝐵 , 𝐶 ) ) ) )
34 1 2 3 25 ipcl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐴 , 𝐶 ) ∈ ( Base ‘ 𝐹 ) )
35 6 7 9 34 syl3anc ⊢ ( 𝜑 → ( 𝐴 , 𝐶 ) ∈ ( Base ‘ 𝐹 ) )
36 1 2 3 25 ipcl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) → ( 𝐴 , 𝐷 ) ∈ ( Base ‘ 𝐹 ) )
37 6 7 10 36 syl3anc ⊢ ( 𝜑 → ( 𝐴 , 𝐷 ) ∈ ( Base ‘ 𝐹 ) )
38 25 5 cmn4 ⊢ ( ( 𝐹 ∈ CMnd ∧ ( ( 𝐴 , 𝐶 ) ∈ ( Base ‘ 𝐹 ) ∧ ( 𝐴 , 𝐷 ) ∈ ( Base ‘ 𝐹 ) ) ∧ ( ( 𝐵 , 𝐷 ) ∈ ( Base ‘ 𝐹 ) ∧ ( 𝐵 , 𝐶 ) ∈ ( Base ‘ 𝐹 ) ) ) → ( ( ( 𝐴 , 𝐶 ) ⨣ ( 𝐴 , 𝐷 ) ) ⨣ ( ( 𝐵 , 𝐷 ) ⨣ ( 𝐵 , 𝐶 ) ) ) = ( ( ( 𝐴 , 𝐶 ) ⨣ ( 𝐵 , 𝐷 ) ) ⨣ ( ( 𝐴 , 𝐷 ) ⨣ ( 𝐵 , 𝐶 ) ) ) )
39 24 35 37 29 27 38 syl122anc ⊢ ( 𝜑 → ( ( ( 𝐴 , 𝐶 ) ⨣ ( 𝐴 , 𝐷 ) ) ⨣ ( ( 𝐵 , 𝐷 ) ⨣ ( 𝐵 , 𝐶 ) ) ) = ( ( ( 𝐴 , 𝐶 ) ⨣ ( 𝐵 , 𝐷 ) ) ⨣ ( ( 𝐴 , 𝐷 ) ⨣ ( 𝐵 , 𝐶 ) ) ) )
40 16 33 39 3eqtrd ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) , ( 𝐶 + 𝐷 ) ) = ( ( ( 𝐴 , 𝐶 ) ⨣ ( 𝐵 , 𝐷 ) ) ⨣ ( ( 𝐴 , 𝐷 ) ⨣ ( 𝐵 , 𝐶 ) ) ) )