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

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 ⊢ V = Base W
ipffn.2 ⊢ , ˙ = ⋅ if ⁡ W
Assertion ipffn ⊢ , ˙ Fn V × V

Proof

Step Hyp Ref Expression
1 ipffn.1 ⊢ V = Base W
2 ipffn.2 ⊢ , ˙ = ⋅ if ⁡ W
3 eqid ⊢ ⋅ 𝑖 ⁡ W = ⋅ 𝑖 ⁡ W
4 1 3 2 ipffval ⊢ , ˙ = x ∈ V , y ∈ V ⟼ x ⋅ 𝑖 ⁡ W y
5 ovex ⊢ x ⋅ 𝑖 ⁡ W y ∈ V
6 4 5 fnmpoi ⊢ , ˙ Fn V × V