assaass

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

	Ref	Expression
Hypotheses	isassa.v	$⊢ V = {Base}_{W}$
	isassa.f	$⊢ F = Scalar (W)$
	isassa.b	$⊢ B = {Base}_{F}$
	isassa.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	isassa.t	$⊢ \underset{˙}{\times} = \cdot_{W}$
Assertion	assaass	$⊢ (W \in AssAlg \land (A \in B \land X \in V \land Y \in V)) \to (A \underset{˙}{\cdot} X) \underset{˙}{\times} Y = A \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$

Step	Hyp	Ref	Expression
1		isassa.v	$⊢ V = {Base}_{W}$
2		isassa.f	$⊢ F = Scalar (W)$
3		isassa.b	$⊢ B = {Base}_{F}$
4		isassa.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
5		isassa.t	$⊢ \underset{˙}{\times} = \cdot_{W}$
6	1 2 3 4 5	assalem	$⊢ (W \in AssAlg \land (A \in B \land X \in V \land Y \in V)) \to ((A \underset{˙}{\cdot} X) \underset{˙}{\times} Y = A \underset{˙}{\cdot} (X \underset{˙}{\times} Y) \land X \underset{˙}{\times} (A \underset{˙}{\cdot} Y) = A \underset{˙}{\cdot} (X \underset{˙}{\times} Y))$
7	6	simpld	$⊢ (W \in AssAlg \land (A \in B \land X \in V \land Y \in V)) \to (A \underset{˙}{\cdot} X) \underset{˙}{\times} Y = A \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$

Metamath Proof Explorer