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

Metamath Proof Explorer

Theorem ipdir

Description: Distributive law for inner product (right-distributivity). Equation I3 of Ponnusamy p. 362. (Contributed by NM, 25-Aug-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 ipdir ( ( 𝑊 ∈ 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 eqid ⊢ ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) = ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) )
7 1 2 3 6 phllmhm ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐶 ∈ 𝑉 ) → ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) )
8 7 3ad2antr3 ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) )
9 lmghm ⊢ ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) → ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ∈ ( 𝑊 GrpHom ( ringLMod ‘ 𝐹 ) ) )
10 8 9 syl ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ∈ ( 𝑊 GrpHom ( ringLMod ‘ 𝐹 ) ) )
11 simpr1 ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐴 ∈ 𝑉 )
12 simpr2 ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐵 ∈ 𝑉 )
13 rlmplusg ⊢ ( +g ‘ 𝐹 ) = ( +g ‘ ( ringLMod ‘ 𝐹 ) )
14 5 13 eqtri ⊢ ⨣ = ( +g ‘ ( ringLMod ‘ 𝐹 ) )
15 3 4 14 ghmlin ⊢ ( ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ∈ ( 𝑊 GrpHom ( ringLMod ‘ 𝐹 ) ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ 𝐴 ) ⨣ ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ 𝐵 ) ) )
16 10 11 12 15 syl3anc ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ 𝐴 ) ⨣ ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ 𝐵 ) ) )
17 phllmod ⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
18 3 4 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 + 𝐵 ) ∈ 𝑉 )
19 17 18 syl3an1 ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 + 𝐵 ) ∈ 𝑉 )
20 19 3adant3r3 ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐴 + 𝐵 ) ∈ 𝑉 )
21 oveq1 ⊢ ( 𝑥 = ( 𝐴 + 𝐵 ) → ( 𝑥 , 𝐶 ) = ( ( 𝐴 + 𝐵 ) , 𝐶 ) )
22 ovex ⊢ ( 𝑥 , 𝐶 ) ∈ V
23 21 6 22 fvmpt3i ⊢ ( ( 𝐴 + 𝐵 ) ∈ 𝑉 → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ ( 𝐴 + 𝐵 ) ) = ( ( 𝐴 + 𝐵 ) , 𝐶 ) )
24 20 23 syl ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ ( 𝐴 + 𝐵 ) ) = ( ( 𝐴 + 𝐵 ) , 𝐶 ) )
25 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 , 𝐶 ) = ( 𝐴 , 𝐶 ) )
26 25 6 22 fvmpt3i ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ 𝐴 ) = ( 𝐴 , 𝐶 ) )
27 11 26 syl ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ 𝐴 ) = ( 𝐴 , 𝐶 ) )
28 oveq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 , 𝐶 ) = ( 𝐵 , 𝐶 ) )
29 28 6 22 fvmpt3i ⊢ ( 𝐵 ∈ 𝑉 → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ 𝐵 ) = ( 𝐵 , 𝐶 ) )
30 12 29 syl ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ 𝐵 ) = ( 𝐵 , 𝐶 ) )
31 27 30 oveq12d ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ 𝐴 ) ⨣ ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ 𝐵 ) ) = ( ( 𝐴 , 𝐶 ) ⨣ ( 𝐵 , 𝐶 ) ) )
32 16 24 31 3eqtr3d ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 + 𝐵 ) , 𝐶 ) = ( ( 𝐴 , 𝐶 ) ⨣ ( 𝐵 , 𝐶 ) ) )