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 ( 𝑉 × 𝑉 )