Metamath Proof Explorer


Theorem ipffn

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

Ref Expression
Hypotheses ipffn.1 𝑉 = ( Base ‘ 𝑊 )
ipffn.2 , = ( ·if𝑊 )
Assertion ipffn , Fn ( 𝑉 × 𝑉 )

Proof

Step Hyp Ref Expression
1 ipffn.1 𝑉 = ( Base ‘ 𝑊 )
2 ipffn.2 , = ( ·if𝑊 )
3 eqid ( ·𝑖𝑊 ) = ( ·𝑖𝑊 )
4 1 3 2 ipffval , = ( 𝑥𝑉 , 𝑦𝑉 ↦ ( 𝑥 ( ·𝑖𝑊 ) 𝑦 ) )
5 ovex ( 𝑥 ( ·𝑖𝑊 ) 𝑦 ) ∈ V
6 4 5 fnmpoi , Fn ( 𝑉 × 𝑉 )