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 ⊢ 𝐵 = ( Base ‘ 𝑊 )
scaffval.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
scaffval.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
scaffval.a ⊢ ∙ = ( ·sf ‘ 𝑊 )
Assertion scaffn ∙ Fn ( 𝐾 × 𝐵 )

Proof

Step Hyp Ref Expression
1 scaffval.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 scaffval.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3 scaffval.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
4 scaffval.a ⊢ ∙ = ( ·sf ‘ 𝑊 )
5 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
6 1 2 3 4 5 scaffval ⊢ ∙ = ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) )
7 ovex ⊢ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ V
8 6 7 fnmpoi ⊢ ∙ Fn ( 𝐾 × 𝐵 )