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

Metamath Proof Explorer

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 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 , 𝐵 ) ∈ 𝐾 )