Definition df-assa 21259

Description: Definition of an associative algebra. An associative algebra is a set equipped with a left-module structure on a (commutative) 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.)

Assertion

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

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

Detailed syntax breakdown of Definition df-assa

Step	Hyp	Ref	Expression
1		casa 21256	. 2 class AssAlg
2		vf	. . . . . . 7 setvar 𝑓
3	2	cv 1540	. . . . . 6 class 𝑓
4		ccrg 19965	. . . . . 6 class CRing
5	3, 4	wcel 2106	. . . . 5 wff 𝑓 ∈ CRing
6		vr	. . . . . . . . . . . . . . 15 setvar 𝑟
7	6	cv 1540	. . . . . . . . . . . . . 14 class 𝑟
8		vx	. . . . . . . . . . . . . . 15 setvar 𝑥
9	8	cv 1540	. . . . . . . . . . . . . 14 class 𝑥
10		vs	. . . . . . . . . . . . . . 15 setvar 𝑠
11	10	cv 1540	. . . . . . . . . . . . . 14 class 𝑠
12	7, 9, 11	co 7357	. . . . . . . . . . . . 13 class (𝑟𝑠𝑥)
13		vy	. . . . . . . . . . . . . 14 setvar 𝑦
14	13	cv 1540	. . . . . . . . . . . . 13 class 𝑦
15		vt	. . . . . . . . . . . . . 14 setvar 𝑡
16	15	cv 1540	. . . . . . . . . . . . 13 class 𝑡
17	12, 14, 16	co 7357	. . . . . . . . . . . 12 class ((𝑟𝑠𝑥)𝑡𝑦)
18	9, 14, 16	co 7357	. . . . . . . . . . . . 13 class (𝑥𝑡𝑦)
19	7, 18, 11	co 7357	. . . . . . . . . . . 12 class (𝑟𝑠(𝑥𝑡𝑦))
20	17, 19	wceq 1541	. . . . . . . . . . 11 wff ((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦))
21	7, 14, 11	co 7357	. . . . . . . . . . . . 13 class (𝑟𝑠𝑦)
22	9, 21, 16	co 7357	. . . . . . . . . . . 12 class (𝑥𝑡(𝑟𝑠𝑦))
23	22, 19	wceq 1541	. . . . . . . . . . 11 wff (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))
24	20, 23	wa 396	. . . . . . . . . 10 wff (((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))
25		vw	. . . . . . . . . . . 12 setvar 𝑤
26	25	cv 1540	. . . . . . . . . . 11 class 𝑤
27		cmulr 17134	. . . . . . . . . . 11 class .r
28	26, 27	cfv 6496	. . . . . . . . . 10 class (.r‘𝑤)
29	24, 15, 28	wsbc 3739	. . . . . . . . 9 wff [(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))
30		cvsca 17137	. . . . . . . . . 10 class ·𝑠
31	26, 30	cfv 6496	. . . . . . . . 9 class ( ·𝑠 ‘𝑤)
32	29, 10, 31	wsbc 3739	. . . . . . . 8 wff [( ·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))
33		cbs 17083	. . . . . . . . 9 class Base
34	26, 33	cfv 6496	. . . . . . . 8 class (Base‘𝑤)
35	32, 13, 34	wral 3064	. . . . . . 7 wff ∀𝑦 ∈ (Base‘𝑤)[( ·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))
36	35, 8, 34	wral 3064	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))
37	3, 33	cfv 6496	. . . . . 6 class (Base‘𝑓)
38	36, 6, 37	wral 3064	. . . . 5 wff ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))
39	5, 38	wa 396	. . . 4 wff (𝑓 ∈ CRing ∧ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))))
40		csca 17136	. . . . 5 class Scalar
41	26, 40	cfv 6496	. . . 4 class (Scalar‘𝑤)
42	39, 2, 41	wsbc 3739	. . 3 wff [(Scalar‘𝑤) / 𝑓](𝑓 ∈ CRing ∧ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))))
43		clmod 20322	. . . 4 class LMod
44		crg 19964	. . . 4 class Ring
45	43, 44	cin 3909	. . 3 class (LMod ∩ Ring)
46	42, 25, 45	crab 3407	. 2 class {𝑤 ∈ (LMod ∩ Ring) ∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ CRing ∧ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))))}
47	1, 46	wceq 1541	1 wff AssAlg = {𝑤 ∈ (LMod ∩ Ring) ∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ CRing ∧ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠 ‘𝑤) / 𝑠][(.r‘𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))))}

This definition is referenced by:  isassa  21262