Theorem lmodvsassd

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

	Ref	Expression
Hypotheses	lmodvsassd.v	$$⊢V={\mathrm{Base}}_W$$
	lmodvsassd.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	lmodvsassd.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	lmodvsassd.k	$$⊢K={\mathrm{Base}}_F$$
	lmodvsassd.t	$$⊢\underset{\dot{}}{\times }={\cdot }_F$$
	lmodvsassd.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lmodvsassd.q	$$⊢\phi \to Q\in K$$
	lmodvsassd.r	$$⊢\phi \to R\in K$$
	lmodvsassd.x	$$⊢\phi \to X\in V$$
Assertion	lmodvsassd	$$⊢\phi \to \left(Q\underset{\dot{}}{\times }R\right)\underset{\dot{}}{·}X=Q\underset{\dot{}}{·}\left(R\underset{\dot{}}{·}X\right)$$

Proof

Step	Hyp	Ref	Expression
1		lmodvsassd.v	$$⊢V={\mathrm{Base}}_W$$
2		lmodvsassd.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
3		lmodvsassd.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
4		lmodvsassd.k	$$⊢K={\mathrm{Base}}_F$$
5		lmodvsassd.t	$$⊢\underset{\dot{}}{\times }={\cdot }_F$$
6		lmodvsassd.w	$$⊢\phi \to W\in \mathrm{LMod}$$
7		lmodvsassd.q	$$⊢\phi \to Q\in K$$
8		lmodvsassd.r	$$⊢\phi \to R\in K$$
9		lmodvsassd.x	$$⊢\phi \to X\in V$$
10	1 2 3 4 5	lmodvsass	$$⊢\left(W\in \mathrm{LMod}\wedge \left(Q\in K\wedge R\in K\wedge X\in V\right)\right)\to \left(Q\underset{\dot{}}{\times }R\right)\underset{\dot{}}{·}X=Q\underset{\dot{}}{·}\left(R\underset{\dot{}}{·}X\right)$$
11	6 7 8 9 10	syl13anc	$$⊢\phi \to \left(Q\underset{\dot{}}{\times }R\right)\underset{\dot{}}{·}X=Q\underset{\dot{}}{·}\left(R\underset{\dot{}}{·}X\right)$$