Metamath Proof Explorer

Theorem ipass

Description: Associative law for inner product. Equation I2 of Ponnusamy p. 363. (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.f ⊢ 𝐾 = ( Base ‘ 𝐹 )
ipass.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
ipass.p ⊢ × = ( .r ‘ 𝐹 )
Assertion ipass ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 · 𝐵 ) , 𝐶 ) = ( 𝐴 × ( 𝐵 , 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 phlsrng.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 phllmhm.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
3 phllmhm.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
4 ipdir.f ⊢ 𝐾 = ( Base ‘ 𝐹 )
5 ipass.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
6 ipass.p ⊢ × = ( .r ‘ 𝐹 )
7 eqid ⊢ ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) = ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) )
8 1 2 3 7 phllmhm ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐶 ∈ 𝑉 ) → ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) )
9 8 3ad2antr3 ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) )
10 simpr1 ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐴 ∈ 𝐾 )
11 simpr2 ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐵 ∈ 𝑉 )
12 rlmvsca ⊢ ( .r ‘ 𝐹 ) = ( ·𝑠 ‘ ( ringLMod ‘ 𝐹 ) )
13 6 12 eqtri ⊢ × = ( ·𝑠 ‘ ( ringLMod ‘ 𝐹 ) )
14 1 4 3 5 13 lmhmlin ⊢ ( ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ ( 𝐴 · 𝐵 ) ) = ( 𝐴 × ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ 𝐵 ) ) )
15 9 10 11 14 syl3anc ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ ( 𝐴 · 𝐵 ) ) = ( 𝐴 × ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ 𝐵 ) ) )
16 phllmod ⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
17 16 adantr ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝑊 ∈ LMod )
18 3 1 5 4 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 · 𝐵 ) ∈ 𝑉 )
19 17 10 11 18 syl3anc ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐴 · 𝐵 ) ∈ 𝑉 )
20 oveq1 ⊢ ( 𝑥 = ( 𝐴 · 𝐵 ) → ( 𝑥 , 𝐶 ) = ( ( 𝐴 · 𝐵 ) , 𝐶 ) )
21 ovex ⊢ ( 𝑥 , 𝐶 ) ∈ V
22 20 7 21 fvmpt3i ⊢ ( ( 𝐴 · 𝐵 ) ∈ 𝑉 → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ ( 𝐴 · 𝐵 ) ) = ( ( 𝐴 · 𝐵 ) , 𝐶 ) )
23 19 22 syl ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ ( 𝐴 · 𝐵 ) ) = ( ( 𝐴 · 𝐵 ) , 𝐶 ) )
24 oveq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 , 𝐶 ) = ( 𝐵 , 𝐶 ) )
25 24 7 21 fvmpt3i ⊢ ( 𝐵 ∈ 𝑉 → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ 𝐵 ) = ( 𝐵 , 𝐶 ) )
26 11 25 syl ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ 𝐵 ) = ( 𝐵 , 𝐶 ) )
27 26 oveq2d ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐴 × ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ 𝐵 ) ) = ( 𝐴 × ( 𝐵 , 𝐶 ) ) )
28 15 23 27 3eqtr3d ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 · 𝐵 ) , 𝐶 ) = ( 𝐴 × ( 𝐵 , 𝐶 ) ) )