Theorem ipcl

Description: Closure of the inner product operation in a pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypotheses	phlsrng.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	phllmhm.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
	phllmhm.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	ipcl.f	⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion	ipcl	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 , 𝐵 ) ∈ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		phlsrng.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		phllmhm.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
3		phllmhm.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
4		ipcl.f	⊢ 𝐾 = ( Base ‘ 𝐹 )
5		eqid	⊢ ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐵 ) ) = ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐵 ) )
6	1 2 3 5	phllmhm	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐵 ∈ 𝑉 ) → ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐵 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) )
7		rlmbas	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ ( ringLMod ‘ 𝐹 ) )
8	4 7	eqtri	⊢ 𝐾 = ( Base ‘ ( ringLMod ‘ 𝐹 ) )
9	3 8	lmhmf	⊢ ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐵 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) → ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐵 ) ) : 𝑉 ⟶ 𝐾 )
10	6 9	syl	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐵 ∈ 𝑉 ) → ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐵 ) ) : 𝑉 ⟶ 𝐾 )
11	5	fmpt	⊢ ( ∀ 𝑥 ∈ 𝑉 ( 𝑥 , 𝐵 ) ∈ 𝐾 ↔ ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐵 ) ) : 𝑉 ⟶ 𝐾 )
12	10 11	sylibr	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐵 ∈ 𝑉 ) → ∀ 𝑥 ∈ 𝑉 ( 𝑥 , 𝐵 ) ∈ 𝐾 )
13		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 , 𝐵 ) = ( 𝐴 , 𝐵 ) )
14	13	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 , 𝐵 ) ∈ 𝐾 ↔ ( 𝐴 , 𝐵 ) ∈ 𝐾 ) )
15	14	rspccva	⊢ ( ( ∀ 𝑥 ∈ 𝑉 ( 𝑥 , 𝐵 ) ∈ 𝐾 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 , 𝐵 ) ∈ 𝐾 )
16	12 15	stoic3	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 , 𝐵 ) ∈ 𝐾 )
17	16	3com23	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 , 𝐵 ) ∈ 𝐾 )