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 ‘ 𝐹 ) ) )