assa2ass

Description: Left- and right-associative property of an associative algebra. Notice that the scalars are commuted! (Contributed by AV, 14-Aug-2019) (Proof shortened 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	assa2ass	$⊢ (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) = (C \underset{˙}{*} A) \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		simpr	$⊢ (A \in B \land C \in B) \to C \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 C \in B$
10		assalmod	$⊢ W \in AssAlg \to W \in LMod$
11		simpl	$⊢ (A \in B \land C \in B) \to A \in B$
12		simpl	$⊢ (X \in V \land Y \in V) \to X \in V$
13	1 2 5 3	lmodvscl	$⊢ (W \in LMod \land A \in B \land X \in V) \to A \underset{˙}{\cdot} X \in V$
14	10 11 12 13	syl3an	$⊢ (W \in AssAlg \land (A \in B \land C \in B) \land (X \in V \land Y \in V)) \to A \underset{˙}{\cdot} X \in V$
15		simpr	$⊢ (X \in V \land Y \in V) \to Y \in V$
16	15	3ad2ant3	$⊢ (W \in AssAlg \land (A \in B \land C \in B) \land (X \in V \land Y \in V)) \to Y \in V$
17	1 2 3 5 6	assaassr	$⊢ (W \in AssAlg \land (C \in B \land A \underset{˙}{\cdot} X \in V \land Y \in V)) \to (A \underset{˙}{\cdot} X) \underset{˙}{\times} (C \underset{˙}{\cdot} Y) = C \underset{˙}{\cdot} ((A \underset{˙}{\cdot} X) \underset{˙}{\times} Y)$
18	7 9 14 16 17	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) = C \underset{˙}{\cdot} ((A \underset{˙}{\cdot} X) \underset{˙}{\times} Y)$
19	1 2 3 5 6	assaass	$⊢ (W \in AssAlg \land (C \in B \land A \underset{˙}{\cdot} X \in V \land Y \in V)) \to (C \underset{˙}{\cdot} (A \underset{˙}{\cdot} X)) \underset{˙}{\times} Y = C \underset{˙}{\cdot} ((A \underset{˙}{\cdot} X) \underset{˙}{\times} Y)$
20	19	eqcomd	$⊢ (W \in AssAlg \land (C \in B \land A \underset{˙}{\cdot} X \in V \land Y \in V)) \to C \underset{˙}{\cdot} ((A \underset{˙}{\cdot} X) \underset{˙}{\times} Y) = (C \underset{˙}{\cdot} (A \underset{˙}{\cdot} X)) \underset{˙}{\times} Y$
21	7 9 14 16 20	syl13anc	$⊢ (W \in AssAlg \land (A \in B \land C \in B) \land (X \in V \land Y \in V)) \to C \underset{˙}{\cdot} ((A \underset{˙}{\cdot} X) \underset{˙}{\times} Y) = (C \underset{˙}{\cdot} (A \underset{˙}{\cdot} X)) \underset{˙}{\times} Y$
22	10	3ad2ant1	$⊢ (W \in AssAlg \land (A \in B \land C \in B) \land (X \in V \land Y \in V)) \to W \in LMod$
23	11	3ad2ant2	$⊢ (W \in AssAlg \land (A \in B \land C \in B) \land (X \in V \land Y \in V)) \to A \in B$
24	12	3ad2ant3	$⊢ (W \in AssAlg \land (A \in B \land C \in B) \land (X \in V \land Y \in V)) \to X \in V$
25	1 2 5 3 4	lmodvsass	$⊢ (W \in LMod \land (C \in B \land A \in B \land X \in V)) \to (C \underset{˙}{*} A) \underset{˙}{\cdot} X = C \underset{˙}{\cdot} (A \underset{˙}{\cdot} X)$
26	25	eqcomd	$⊢ (W \in LMod \land (C \in B \land A \in B \land X \in V)) \to C \underset{˙}{\cdot} (A \underset{˙}{\cdot} X) = (C \underset{˙}{*} A) \underset{˙}{\cdot} X$
27	26	oveq1d	$⊢ (W \in LMod \land (C \in B \land A \in B \land X \in V)) \to (C \underset{˙}{\cdot} (A \underset{˙}{\cdot} X)) \underset{˙}{\times} Y = ((C \underset{˙}{*} A) \underset{˙}{\cdot} X) \underset{˙}{\times} Y$
28	22 9 23 24 27	syl13anc	$⊢ (W \in AssAlg \land (A \in B \land C \in B) \land (X \in V \land Y \in V)) \to (C \underset{˙}{\cdot} (A \underset{˙}{\cdot} X)) \underset{˙}{\times} Y = ((C \underset{˙}{*} A) \underset{˙}{\cdot} X) \underset{˙}{\times} Y$
29	2	assasca	$⊢ W \in AssAlg \to F \in Ring$
30	29	adantr	$⊢ (W \in AssAlg \land (A \in B \land C \in B)) \to F \in Ring$
31	8	adantl	$⊢ (W \in AssAlg \land (A \in B \land C \in B)) \to C \in B$
32	11	adantl	$⊢ (W \in AssAlg \land (A \in B \land C \in B)) \to A \in B$
33	3 4 30 31 32	ringcld	$⊢ (W \in AssAlg \land (A \in B \land C \in B)) \to C \underset{˙}{*} A \in B$
34	33	3adant3	$⊢ (W \in AssAlg \land (A \in B \land C \in B) \land (X \in V \land Y \in V)) \to C \underset{˙}{*} A \in B$
35	1 2 3 5 6	assaass	$⊢ (W \in AssAlg \land (C \underset{˙}{} A \in B \land X \in V \land Y \in V)) \to ((C \underset{˙}{} A) \underset{˙}{\cdot} X) \underset{˙}{\times} Y = (C \underset{˙}{*} A) \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$
36	7 34 24 16 35	syl13anc	$⊢ (W \in AssAlg \land (A \in B \land C \in B) \land (X \in V \land Y \in V)) \to ((C \underset{˙}{} A) \underset{˙}{\cdot} X) \underset{˙}{\times} Y = (C \underset{˙}{} A) \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$
37	28 36	eqtrd	$⊢ (W \in AssAlg \land (A \in B \land C \in B) \land (X \in V \land Y \in V)) \to (C \underset{˙}{\cdot} (A \underset{˙}{\cdot} X)) \underset{˙}{\times} Y = (C \underset{˙}{*} A) \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$
38	18 21 37	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) = (C \underset{˙}{*} A) \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$

Metamath Proof Explorer

Theorem assa2ass

Proof