Metamath Proof Explorer

Theorem ipdi

Description: Distributive law for inner product (left-distributivity). (Contributed by NM, 20-Nov-2007) (Revised by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses phlsrng.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
phllmhm.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
phllmhm.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
ipdir.g ⊢ + = ( +g ‘ 𝑊 )
ipdir.p ⊢ ⨣ = ( +g ‘ 𝐹 )
Assertion ipdi ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐴 , ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 , 𝐵 ) ⨣ ( 𝐴 , 𝐶 ) ) )

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 simpl ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝑊 ∈ PreHil )
7 simpr2 ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐵 ∈ 𝑉 )
8 simpr3 ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐶 ∈ 𝑉 )
9 simpr1 ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐴 ∈ 𝑉 )
10 1 2 3 4 5 ipdir ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ) → ( ( 𝐵 + 𝐶 ) , 𝐴 ) = ( ( 𝐵 , 𝐴 ) ⨣ ( 𝐶 , 𝐴 ) ) )
11 6 7 8 9 10 syl13anc ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐵 + 𝐶 ) , 𝐴 ) = ( ( 𝐵 , 𝐴 ) ⨣ ( 𝐶 , 𝐴 ) ) )
12 11 fveq2d ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( *𝑟 ‘ 𝐹 ) ‘ ( ( 𝐵 + 𝐶 ) , 𝐴 ) ) = ( ( *𝑟 ‘ 𝐹 ) ‘ ( ( 𝐵 , 𝐴 ) ⨣ ( 𝐶 , 𝐴 ) ) ) )
13 1 phlsrng ⊢ ( 𝑊 ∈ PreHil → 𝐹 ∈ *-Ring )
14 13 adantr ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐹 ∈ *-Ring )
15 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
16 1 2 3 15 ipcl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐵 , 𝐴 ) ∈ ( Base ‘ 𝐹 ) )
17 6 7 9 16 syl3anc ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐵 , 𝐴 ) ∈ ( Base ‘ 𝐹 ) )
18 1 2 3 15 ipcl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐶 , 𝐴 ) ∈ ( Base ‘ 𝐹 ) )
19 6 8 9 18 syl3anc ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐶 , 𝐴 ) ∈ ( Base ‘ 𝐹 ) )
20 eqid ⊢ ( *𝑟 ‘ 𝐹 ) = ( *𝑟 ‘ 𝐹 )
21 20 15 5 srngadd ⊢ ( ( 𝐹 ∈ *-Ring ∧ ( 𝐵 , 𝐴 ) ∈ ( Base ‘ 𝐹 ) ∧ ( 𝐶 , 𝐴 ) ∈ ( Base ‘ 𝐹 ) ) → ( ( *𝑟 ‘ 𝐹 ) ‘ ( ( 𝐵 , 𝐴 ) ⨣ ( 𝐶 , 𝐴 ) ) ) = ( ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝐵 , 𝐴 ) ) ⨣ ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝐶 , 𝐴 ) ) ) )
22 14 17 19 21 syl3anc ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( *𝑟 ‘ 𝐹 ) ‘ ( ( 𝐵 , 𝐴 ) ⨣ ( 𝐶 , 𝐴 ) ) ) = ( ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝐵 , 𝐴 ) ) ⨣ ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝐶 , 𝐴 ) ) ) )
23 12 22 eqtrd ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( *𝑟 ‘ 𝐹 ) ‘ ( ( 𝐵 + 𝐶 ) , 𝐴 ) ) = ( ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝐵 , 𝐴 ) ) ⨣ ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝐶 , 𝐴 ) ) ) )
24 phllmod ⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
25 24 adantr ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝑊 ∈ LMod )
26 3 4 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐵 + 𝐶 ) ∈ 𝑉 )
27 25 7 8 26 syl3anc ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐵 + 𝐶 ) ∈ 𝑉 )
28 1 2 3 20 ipcj ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐵 + 𝐶 ) ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( ( *𝑟 ‘ 𝐹 ) ‘ ( ( 𝐵 + 𝐶 ) , 𝐴 ) ) = ( 𝐴 , ( 𝐵 + 𝐶 ) ) )
29 6 27 9 28 syl3anc ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( *𝑟 ‘ 𝐹 ) ‘ ( ( 𝐵 + 𝐶 ) , 𝐴 ) ) = ( 𝐴 , ( 𝐵 + 𝐶 ) ) )
30 1 2 3 20 ipcj ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝐵 , 𝐴 ) ) = ( 𝐴 , 𝐵 ) )
31 6 7 9 30 syl3anc ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝐵 , 𝐴 ) ) = ( 𝐴 , 𝐵 ) )
32 1 2 3 20 ipcj ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝐶 , 𝐴 ) ) = ( 𝐴 , 𝐶 ) )
33 6 8 9 32 syl3anc ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝐶 , 𝐴 ) ) = ( 𝐴 , 𝐶 ) )
34 31 33 oveq12d ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝐵 , 𝐴 ) ) ⨣ ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝐶 , 𝐴 ) ) ) = ( ( 𝐴 , 𝐵 ) ⨣ ( 𝐴 , 𝐶 ) ) )
35 23 29 34 3eqtr3d ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐴 , ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 , 𝐵 ) ⨣ ( 𝐴 , 𝐶 ) ) )