assa2ass2

Description: Left- and right-associative property of an associative algebra. Notice that the scalars are not commuted! (Contributed by Zhi Wang, 11-Sep-2025)

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

Proof

Step	Hyp	Ref	Expression
1		assa2ass.v	$⊢ V = {Base}_{W}$
2		assa2ass.f	$⊢ F = Scalar (W)$
3		assa2ass.b	$⊢ B = {Base}_{F}$
4		assa2ass.m	$⊢ \underset{˙}{*} = \cdot_{F}$
5		assa2ass.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
6		assa2ass.t	$⊢ \underset{˙}{\times} = \cdot_{W}$
7		simp1	$⊢ (W \in AssAlg \land (A \in B \land C \in B) \land (X \in V \land Y \in V)) \to W \in AssAlg$
8		simpl	$⊢ (A \in B \land C \in B) \to A \in B$
9	8	3ad2ant2	$⊢ (W \in AssAlg \land (A \in B \land C \in B) \land (X \in V \land Y \in V)) \to A \in B$
10		simpl	$⊢ (X \in V \land Y \in V) \to X \in V$
11	10	3ad2ant3	$⊢ (W \in AssAlg \land (A \in B \land C \in B) \land (X \in V \land Y \in V)) \to X \in V$
12		assalmod	$⊢ W \in AssAlg \to W \in LMod$
13	12	3ad2ant1	$⊢ (W \in AssAlg \land (A \in B \land C \in B) \land (X \in V \land Y \in V)) \to W \in LMod$
14		simpr	$⊢ (A \in B \land C \in B) \to C \in B$
15	14	3ad2ant2	$⊢ (W \in AssAlg \land (A \in B \land C \in B) \land (X \in V \land Y \in V)) \to C \in B$
16		simpr	$⊢ (X \in V \land Y \in V) \to Y \in V$
17	16	3ad2ant3	$⊢ (W \in AssAlg \land (A \in B \land C \in B) \land (X \in V \land Y \in V)) \to Y \in V$
18	1 2 5 3 13 15 17	lmodvscld	$⊢ (W \in AssAlg \land (A \in B \land C \in B) \land (X \in V \land Y \in V)) \to C \underset{˙}{\cdot} Y \in V$
19	1 2 3 5 6	assaass	$⊢ (W \in AssAlg \land (A \in B \land X \in V \land C \underset{˙}{\cdot} Y \in V)) \to (A \underset{˙}{\cdot} X) \underset{˙}{\times} (C \underset{˙}{\cdot} Y) = A \underset{˙}{\cdot} (X \underset{˙}{\times} (C \underset{˙}{\cdot} Y))$
20	7 9 11 18 19	syl13anc	$⊢ (W \in AssAlg \land (A \in B \land C \in B) \land (X \in V \land Y \in V)) \to (A \underset{˙}{\cdot} X) \underset{˙}{\times} (C \underset{˙}{\cdot} Y) = A \underset{˙}{\cdot} (X \underset{˙}{\times} (C \underset{˙}{\cdot} Y))$
21	1 2 3 5 6	assaassr	$⊢ (W \in AssAlg \land (A \in B \land X \in V \land C \underset{˙}{\cdot} Y \in V)) \to X \underset{˙}{\times} (A \underset{˙}{\cdot} (C \underset{˙}{\cdot} Y)) = A \underset{˙}{\cdot} (X \underset{˙}{\times} (C \underset{˙}{\cdot} Y))$
22	21	eqcomd	$⊢ (W \in AssAlg \land (A \in B \land X \in V \land C \underset{˙}{\cdot} Y \in V)) \to A \underset{˙}{\cdot} (X \underset{˙}{\times} (C \underset{˙}{\cdot} Y)) = X \underset{˙}{\times} (A \underset{˙}{\cdot} (C \underset{˙}{\cdot} Y))$
23	7 9 11 18 22	syl13anc	$⊢ (W \in AssAlg \land (A \in B \land C \in B) \land (X \in V \land Y \in V)) \to A \underset{˙}{\cdot} (X \underset{˙}{\times} (C \underset{˙}{\cdot} Y)) = X \underset{˙}{\times} (A \underset{˙}{\cdot} (C \underset{˙}{\cdot} Y))$
24	1 2 5 3 4	lmodvsass	$⊢ (W \in LMod \land (A \in B \land C \in B \land Y \in V)) \to (A \underset{˙}{*} C) \underset{˙}{\cdot} Y = A \underset{˙}{\cdot} (C \underset{˙}{\cdot} Y)$
25	24	eqcomd	$⊢ (W \in LMod \land (A \in B \land C \in B \land Y \in V)) \to A \underset{˙}{\cdot} (C \underset{˙}{\cdot} Y) = (A \underset{˙}{*} C) \underset{˙}{\cdot} Y$
26	25	oveq2d	$⊢ (W \in LMod \land (A \in B \land C \in B \land Y \in V)) \to X \underset{˙}{\times} (A \underset{˙}{\cdot} (C \underset{˙}{\cdot} Y)) = X \underset{˙}{\times} ((A \underset{˙}{*} C) \underset{˙}{\cdot} Y)$
27	13 9 15 17 26	syl13anc	$⊢ (W \in AssAlg \land (A \in B \land C \in B) \land (X \in V \land Y \in V)) \to X \underset{˙}{\times} (A \underset{˙}{\cdot} (C \underset{˙}{\cdot} Y)) = X \underset{˙}{\times} ((A \underset{˙}{*} C) \underset{˙}{\cdot} Y)$
28	2	assasca	$⊢ W \in AssAlg \to F \in Ring$
29	28	adantr	$⊢ (W \in AssAlg \land (A \in B \land C \in B)) \to F \in Ring$
30	8	adantl	$⊢ (W \in AssAlg \land (A \in B \land C \in B)) \to A \in B$
31	14	adantl	$⊢ (W \in AssAlg \land (A \in B \land C \in B)) \to C \in B$
32	3 4 29 30 31	ringcld	$⊢ (W \in AssAlg \land (A \in B \land C \in B)) \to A \underset{˙}{*} C \in B$
33	32	3adant3	$⊢ (W \in AssAlg \land (A \in B \land C \in B) \land (X \in V \land Y \in V)) \to A \underset{˙}{*} C \in B$
34	1 2 3 5 6	assaassr	$⊢ (W \in AssAlg \land (A \underset{˙}{} C \in B \land X \in V \land Y \in V)) \to X \underset{˙}{\times} ((A \underset{˙}{} C) \underset{˙}{\cdot} Y) = (A \underset{˙}{*} C) \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$
35	7 33 11 17 34	syl13anc	$⊢ (W \in AssAlg \land (A \in B \land C \in B) \land (X \in V \land Y \in V)) \to X \underset{˙}{\times} ((A \underset{˙}{} C) \underset{˙}{\cdot} Y) = (A \underset{˙}{} C) \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$
36	27 35	eqtrd	$⊢ (W \in AssAlg \land (A \in B \land C \in B) \land (X \in V \land Y \in V)) \to X \underset{˙}{\times} (A \underset{˙}{\cdot} (C \underset{˙}{\cdot} Y)) = (A \underset{˙}{*} C) \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$
37	20 23 36	3eqtrd	$⊢ (W \in AssAlg \land (A \in B \land C \in B) \land (X \in V \land Y \in V)) \to (A \underset{˙}{\cdot} X) \underset{˙}{\times} (C \underset{˙}{\cdot} Y) = (A \underset{˙}{*} C) \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$

Metamath Proof Explorer

Theorem assa2ass2

Proof