Theorem assaassrd

Description: Right-associative property of an associative algebra, deduction version. (Contributed by Thierry Arnoux, 15-Feb-2026)

	Ref	Expression
Hypotheses	assaassd.1	|- V = ( Base ` W )
	assaassd.2	|- F = ( Scalar ` W )
	assaassd.3	|- B = ( Base ` F )
	assaassd.4	|- .x. = ( .s ` W )
	assaassd.5	|- .X. = ( .r ` W )
	assaassd.6	|- ( ph -> W e. AssAlg )
	assaassd.7	|- ( ph -> A e. B )
	assaassd.8	|- ( ph -> X e. V )
	assaassd.9	|- ( ph -> Y e. V )
Assertion	assaassrd	|- ( ph -> ( X .X. ( A .x. Y ) ) = ( A .x. ( X .X. Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		assaassd.1	|- V = ( Base ` W )
2		assaassd.2	|- F = ( Scalar ` W )
3		assaassd.3	|- B = ( Base ` F )
4		assaassd.4	|- .x. = ( .s ` W )
5		assaassd.5	|- .X. = ( .r ` W )
6		assaassd.6	|- ( ph -> W e. AssAlg )
7		assaassd.7	|- ( ph -> A e. B )
8		assaassd.8	|- ( ph -> X e. V )
9		assaassd.9	|- ( ph -> Y e. V )
10	1 2 3 4 5	assaassr	|- ( ( W e. AssAlg /\ ( A e. B /\ X e. V /\ Y e. V ) ) -> ( X .X. ( A .x. Y ) ) = ( A .x. ( X .X. Y ) ) )
11	6 7 8 9 10	syl13anc	|- ( ph -> ( X .X. ( A .x. Y ) ) = ( A .x. ( X .X. Y ) ) )