Theorem lmodvsassd

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

	Ref	Expression
Hypotheses	lmodvsassd.v	|- V = ( Base ` W )
	lmodvsassd.f	|- F = ( Scalar ` W )
	lmodvsassd.s	|- .x. = ( .s ` W )
	lmodvsassd.k	|- K = ( Base ` F )
	lmodvsassd.t	|- .X. = ( .r ` F )
	lmodvsassd.w	|- ( ph -> W e. LMod )
	lmodvsassd.q	|- ( ph -> Q e. K )
	lmodvsassd.r	|- ( ph -> R e. K )
	lmodvsassd.x	|- ( ph -> X e. V )
Assertion	lmodvsassd	|- ( ph -> ( ( Q .X. R ) .x. X ) = ( Q .x. ( R .x. X ) ) )

Proof

Step	Hyp	Ref	Expression
1		lmodvsassd.v	|- V = ( Base ` W )
2		lmodvsassd.f	|- F = ( Scalar ` W )
3		lmodvsassd.s	|- .x. = ( .s ` W )
4		lmodvsassd.k	|- K = ( Base ` F )
5		lmodvsassd.t	|- .X. = ( .r ` F )
6		lmodvsassd.w	|- ( ph -> W e. LMod )
7		lmodvsassd.q	|- ( ph -> Q e. K )
8		lmodvsassd.r	|- ( ph -> R e. K )
9		lmodvsassd.x	|- ( ph -> X e. V )
10	1 2 3 4 5	lmodvsass	|- ( ( W e. LMod /\ ( Q e. K /\ R e. K /\ X e. V ) ) -> ( ( Q .X. R ) .x. X ) = ( Q .x. ( R .x. X ) ) )
11	6 7 8 9 10	syl13anc	|- ( ph -> ( ( Q .X. R ) .x. X ) = ( Q .x. ( R .x. X ) ) )