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

Metamath Proof Explorer

Theorem phlipf

Description: The inner product operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015)

Ref Expression
Hypotheses ipffn.1 ⊢ 𝑉 = ( Base ‘ 𝑊 )
ipffn.2 ⊢ , = ( ·if ‘ 𝑊 )
phlipf.s ⊢ 𝑆 = ( Scalar ‘ 𝑊 )
phlipf.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
Assertion phlipf ( 𝑊 ∈ PreHil → , : ( 𝑉 × 𝑉 ) ⟶ 𝐾 )

Proof

Step Hyp Ref Expression
1 ipffn.1 ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 ipffn.2 ⊢ , = ( ·if ‘ 𝑊 )
3 phlipf.s ⊢ 𝑆 = ( Scalar ‘ 𝑊 )
4 phlipf.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
5 eqid ⊢ ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝑊 )
6 3 5 1 4 ipcl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ∈ 𝐾 )
7 6 3expb ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ∈ 𝐾 )
8 7 ralrimivva ⊢ ( 𝑊 ∈ PreHil → ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ∈ 𝐾 )
9 1 5 2 ipffval ⊢ , = ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) )
10 9 fmpo ⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ∈ 𝐾 ↔ , : ( 𝑉 × 𝑉 ) ⟶ 𝐾 )
11 8 10 sylib ⊢ ( 𝑊 ∈ PreHil → , : ( 𝑉 × 𝑉 ) ⟶ 𝐾 )