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={\mathrm{Base}}_W$$
	assaassd.2	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	assaassd.3	$$⊢B={\mathrm{Base}}_F$$
	assaassd.4	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	assaassd.5	$$⊢\underset{\dot{}}{\times }={\cdot }_W$$
	assaassd.6	$$⊢\phi \to W\in \mathrm{AssAlg}$$
	assaassd.7	$$⊢\phi \to A\in B$$
	assaassd.8	$$⊢\phi \to X\in V$$
	assaassd.9	$$⊢\phi \to Y\in V$$
Assertion	assaassrd	$$⊢\phi \to X\underset{\dot{}}{\times }\left(A\underset{\dot{}}{·}Y\right)=A\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		assaassd.1	$$⊢V={\mathrm{Base}}_W$$
2		assaassd.2	$$⊢F=\mathrm{Scalar}\left(W\right)$$
3		assaassd.3	$$⊢B={\mathrm{Base}}_F$$
4		assaassd.4	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
5		assaassd.5	$$⊢\underset{\dot{}}{\times }={\cdot }_W$$
6		assaassd.6	$$⊢\phi \to W\in \mathrm{AssAlg}$$
7		assaassd.7	$$⊢\phi \to A\in B$$
8		assaassd.8	$$⊢\phi \to X\in V$$
9		assaassd.9	$$⊢\phi \to Y\in V$$
10	1 2 3 4 5	assaassr	$$⊢\left(W\in \mathrm{AssAlg}\wedge \left(A\in B\wedge X\in V\wedge Y\in V\right)\right)\to X\underset{\dot{}}{\times }\left(A\underset{\dot{}}{·}Y\right)=A\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)$$
11	6 7 8 9 10	syl13anc	$$⊢\phi \to X\underset{\dot{}}{\times }\left(A\underset{\dot{}}{·}Y\right)=A\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)$$