Definition df-assa 21873

Description: Definition of an associative algebra. An associative algebra is a set equipped with a left-module structure on a ring, coupled with a multiplicative internal operation on the vectors of the module that is associative and distributive for the additive structure of the left-module (so giving the vectors a ring structure) and that is also bilinear under the scalar product. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by SN, 2-Mar-2025.)

Assertion

Ref	Expression
df-assa	⊢ AssAlg = {𝑤 ∈ (LMod ∩ Ring) ∣ [(Scalar‘𝑤) / 𝑓]∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))}

Distinct variable group:   𝑓,𝑟,𝑠,𝑡,𝑤,𝑥,𝑦

Detailed syntax breakdown of Definition df-assa

Step	Hyp	Ref	Expression
1		casa 21870	. 2 class AssAlg
2		vr	. . . . . . . . . . . . . 14 setvar 𝑟
3	2	cv 1539	. . . . . . . . . . . . 13 class 𝑟
4		vx	. . . . . . . . . . . . . 14 setvar 𝑥
5	4	cv 1539	. . . . . . . . . . . . 13 class 𝑥
6		vs	. . . . . . . . . . . . . 14 setvar 𝑠
7	6	cv 1539	. . . . . . . . . . . . 13 class 𝑠
8	3, 5, 7	co 7431	. . . . . . . . . . . 12 class (𝑟𝑠𝑥)
9		vy	. . . . . . . . . . . . 13 setvar 𝑦
10	9	cv 1539	. . . . . . . . . . . 12 class 𝑦
11		vt	. . . . . . . . . . . . 13 setvar 𝑡
12	11	cv 1539	. . . . . . . . . . . 12 class 𝑡
13	8, 10, 12	co 7431	. . . . . . . . . . 11 class ((𝑟𝑠𝑥)𝑡𝑦)
14	5, 10, 12	co 7431	. . . . . . . . . . . 12 class (𝑥𝑡𝑦)
15	3, 14, 7	co 7431	. . . . . . . . . . 11 class (𝑟𝑠(𝑥𝑡𝑦))
16	13, 15	wceq 1540	. . . . . . . . . 10 wff ((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦))
17	3, 10, 7	co 7431	. . . . . . . . . . . 12 class (𝑟𝑠𝑦)
18	5, 17, 12	co 7431	. . . . . . . . . . 11 class (𝑥𝑡(𝑟𝑠𝑦))
19	18, 15	wceq 1540	. . . . . . . . . 10 wff (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))
20	16, 19	wa 395	. . . . . . . . 9 wff (((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))
21		vw	. . . . . . . . . . 11 setvar 𝑤
22	21	cv 1539	. . . . . . . . . 10 class 𝑤
23		cmulr 17298	. . . . . . . . . 10 class .r
24	22, 23	cfv 6561	. . . . . . . . 9 class (.r‘𝑤)
25	20, 11, 24	wsbc 3788	. . . . . . . 8 wff [(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))
26		cvsca 17301	. . . . . . . . 9 class ·𝑠
27	22, 26	cfv 6561	. . . . . . . 8 class ( ·𝑠 ‘𝑤)
28	25, 6, 27	wsbc 3788	. . . . . . 7 wff [( ·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))
29		cbs 17247	. . . . . . . 8 class Base
30	22, 29	cfv 6561	. . . . . . 7 class (Base‘𝑤)
31	28, 9, 30	wral 3061	. . . . . 6 wff ∀𝑦 ∈ (Base‘𝑤)[( ·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))
32	31, 4, 30	wral 3061	. . . . 5 wff ∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))
33		vf	. . . . . . 7 setvar 𝑓
34	33	cv 1539	. . . . . 6 class 𝑓
35	34, 29	cfv 6561	. . . . 5 class (Base‘𝑓)
36	32, 2, 35	wral 3061	. . . 4 wff ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))
37		csca 17300	. . . . 5 class Scalar
38	22, 37	cfv 6561	. . . 4 class (Scalar‘𝑤)
39	36, 33, 38	wsbc 3788	. . 3 wff [(Scalar‘𝑤) / 𝑓]∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))
40		clmod 20858	. . . 4 class LMod
41		crg 20230	. . . 4 class Ring
42	40, 41	cin 3950	. . 3 class (LMod ∩ Ring)
43	39, 21, 42	crab 3436	. 2 class {𝑤 ∈ (LMod ∩ Ring) ∣ [(Scalar‘𝑤) / 𝑓]∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))}
44	1, 43	wceq 1540	1 wff AssAlg = {𝑤 ∈ (LMod ∩ Ring) ∣ [(Scalar‘𝑤) / 𝑓]∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))}

This definition is referenced by:  isassa  21876