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