Theorem assaassr

Description: Right-associative property of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014)

	Ref	Expression
Hypotheses	isassa.v	$$⊢V={\mathrm{Base}}_W$$
	isassa.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	isassa.b	$$⊢B={\mathrm{Base}}_F$$
	isassa.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	isassa.t	$$⊢\underset{\dot{}}{\times }={\cdot }_W$$
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		isassa.v	$$⊢V={\mathrm{Base}}_W$$
2		isassa.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
3		isassa.b	$$⊢B={\mathrm{Base}}_F$$
4		isassa.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
5		isassa.t	$$⊢\underset{\dot{}}{\times }={\cdot }_W$$
6	1 2 3 4 5	assalem	$$⊢\left(W\in \mathrm{AssAlg}\wedge \left(A\in B\wedge X\in V\wedge Y\in V\right)\right)\to \left(\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=A\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\wedge X\underset{\dot{}}{\times }\left(A\underset{\dot{}}{·}Y\right)=A\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\right)$$
7	6	simprd	$$⊢\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)$$