Theorem lmodvsassd

Description: In a module, scalar multiplication is a semigroup action. (Contributed by SN, 24-Sep-2026)

	Ref	Expression
Hypotheses	lmodvsassd.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lmodvsassd.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	lmodvsassd.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
	lmodvsassd.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	lmodvsassd.t	⊢ × = ( .r ‘ 𝐹 )
	lmodvsassd.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lmodvsassd.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐾 )
	lmodvsassd.r	⊢ ( 𝜑 → 𝑅 ∈ 𝐾 )
	lmodvsassd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion	lmodvsassd	⊢ ( 𝜑 → ( ( 𝑄 × 𝑅 ) · 𝑋 ) = ( 𝑄 · ( 𝑅 · 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lmodvsassd.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lmodvsassd.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3		lmodvsassd.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
4		lmodvsassd.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
5		lmodvsassd.t	⊢ × = ( .r ‘ 𝐹 )
6		lmodvsassd.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
7		lmodvsassd.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐾 )
8		lmodvsassd.r	⊢ ( 𝜑 → 𝑅 ∈ 𝐾 )
9		lmodvsassd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
10	1 2 3 4 5	lmodvsass	⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝑄 × 𝑅 ) · 𝑋 ) = ( 𝑄 · ( 𝑅 · 𝑋 ) ) )
11	6 7 8 9 10	syl13anc	⊢ ( 𝜑 → ( ( 𝑄 × 𝑅 ) · 𝑋 ) = ( 𝑄 · ( 𝑅 · 𝑋 ) ) )