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

Metamath Proof Explorer

Theorem scaffn

Description: The scalar multiplication operation is a function. (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Hypotheses scaffval.b ⊢ B = Base W
scaffval.f ⊢ F = Scalar ⁡ W
scaffval.k ⊢ K = Base F
scaffval.a ⊢ ∙ ˙ = ⋅ 𝑠𝑓 ⁡ W
Assertion scaffn ⊢ ∙ ˙ Fn K × B

Proof

Step Hyp Ref Expression
1 scaffval.b ⊢ B = Base W
2 scaffval.f ⊢ F = Scalar ⁡ W
3 scaffval.k ⊢ K = Base F
4 scaffval.a ⊢ ∙ ˙ = ⋅ 𝑠𝑓 ⁡ W
5 eqid ⊢ ⋅ W = ⋅ W
6 1 2 3 4 5 scaffval ⊢ ∙ ˙ = x ∈ K , y ∈ B ⟼ x ⋅ W y
7 ovex ⊢ x ⋅ W y ∈ V
8 6 7 fnmpoi ⊢ ∙ ˙ Fn K × B