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 → , : ( 𝑉 × 𝑉 ) ⟶ 𝐾 )