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

Metamath Proof Explorer

Theorem phllmhm

Description: The inner product of a pre-Hilbert space is linear in its left argument. (Contributed by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses phlsrng.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
phllmhm.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
phllmhm.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
phllmhm.g ⊢ 𝐺 = ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐴 ) )
Assertion phllmhm ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ) → 𝐺 ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 phlsrng.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 phllmhm.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
3 phllmhm.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
4 phllmhm.g ⊢ 𝐺 = ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐴 ) )
5 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
6 eqid ⊢ ( *𝑟 ‘ 𝐹 ) = ( *𝑟 ‘ 𝐹 )
7 eqid ⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐹 )
8 3 1 2 5 6 7 isphl ⊢ ( 𝑊 ∈ PreHil ↔ ( 𝑊 ∈ LVec ∧ 𝐹 ∈ *-Ring ∧ ∀ 𝑦 ∈ 𝑉 ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝑦 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑦 , 𝑦 ) = ( 0g ‘ 𝐹 ) → 𝑦 = ( 0g ‘ 𝑊 ) ) ∧ ∀ 𝑥 ∈ 𝑉 ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝑦 , 𝑥 ) ) = ( 𝑥 , 𝑦 ) ) ) )
9 8 simp3bi ⊢ ( 𝑊 ∈ PreHil → ∀ 𝑦 ∈ 𝑉 ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝑦 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑦 , 𝑦 ) = ( 0g ‘ 𝐹 ) → 𝑦 = ( 0g ‘ 𝑊 ) ) ∧ ∀ 𝑥 ∈ 𝑉 ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝑦 , 𝑥 ) ) = ( 𝑥 , 𝑦 ) ) )
10 simp1 ⊢ ( ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝑦 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑦 , 𝑦 ) = ( 0g ‘ 𝐹 ) → 𝑦 = ( 0g ‘ 𝑊 ) ) ∧ ∀ 𝑥 ∈ 𝑉 ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝑦 , 𝑥 ) ) = ( 𝑥 , 𝑦 ) ) → ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝑦 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) )
11 10 ralimi ⊢ ( ∀ 𝑦 ∈ 𝑉 ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝑦 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑦 , 𝑦 ) = ( 0g ‘ 𝐹 ) → 𝑦 = ( 0g ‘ 𝑊 ) ) ∧ ∀ 𝑥 ∈ 𝑉 ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝑦 , 𝑥 ) ) = ( 𝑥 , 𝑦 ) ) → ∀ 𝑦 ∈ 𝑉 ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝑦 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) )
12 9 11 syl ⊢ ( 𝑊 ∈ PreHil → ∀ 𝑦 ∈ 𝑉 ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝑦 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) )
13 oveq2 ⊢ ( 𝑦 = 𝐴 → ( 𝑥 , 𝑦 ) = ( 𝑥 , 𝐴 ) )
14 13 mpteq2dv ⊢ ( 𝑦 = 𝐴 → ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝑦 ) ) = ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐴 ) ) )
15 14 4 eqtr4di ⊢ ( 𝑦 = 𝐴 → ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝑦 ) ) = 𝐺 )
16 15 eleq1d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝑦 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ↔ 𝐺 ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ) )
17 16 rspccva ⊢ ( ( ∀ 𝑦 ∈ 𝑉 ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝑦 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ 𝐴 ∈ 𝑉 ) → 𝐺 ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) )
18 12 17 sylan ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ) → 𝐺 ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) )