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