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

Metamath Proof Explorer

Theorem lmodscaf

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 lmodscaf ( 𝑊 ∈ LMod → ∙ : ( 𝐾 × 𝐵 ) ⟶ 𝐵 )

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 5 3 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝐵 )
7 6 3expb ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝐵 )
8 7 ralrimivva ⊢ ( 𝑊 ∈ LMod → ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝐵 )
9 1 2 3 4 5 scaffval ⊢ ∙ = ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) )
10 9 fmpo ⊢ ( ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝐵 ↔ ∙ : ( 𝐾 × 𝐵 ) ⟶ 𝐵 )
11 8 10 sylib ⊢ ( 𝑊 ∈ LMod → ∙ : ( 𝐾 × 𝐵 ) ⟶ 𝐵 )