Definition df-assa 14982

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 = { w e. ( LMod i^i Ring ) | [. (Scalar ` w ) / f ]. A. r e. ( Base ` f ) A. x e. ( Base ` w ) A. y e. ( Base ` w ) [. ( .s ` w ) / s ]. [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) ) }

Distinct variable group:   f, r, s, t, w, x, y

Detailed syntax breakdown of Definition df-assa

Step	Hyp	Ref	Expression
1		casa 14979	. 2 class AssAlg
2		vr	. . . . . . . . . . . . . 14 setvar r
3	2	cv 1401	. . . . . . . . . . . . 13 class r
4		vx	. . . . . . . . . . . . . 14 setvar x
5	4	cv 1401	. . . . . . . . . . . . 13 class x
6		vs	. . . . . . . . . . . . . 14 setvar s
7	6	cv 1401	. . . . . . . . . . . . 13 class s
8	3, 5, 7	co 6079	. . . . . . . . . . . 12 class ( r s x )
9		vy	. . . . . . . . . . . . 13 setvar y
10	9	cv 1401	. . . . . . . . . . . 12 class y
11		vt	. . . . . . . . . . . . 13 setvar t
12	11	cv 1401	. . . . . . . . . . . 12 class t
13	8, 10, 12	co 6079	. . . . . . . . . . 11 class ( ( r s x ) t y )
14	5, 10, 12	co 6079	. . . . . . . . . . . 12 class ( x t y )
15	3, 14, 7	co 6079	. . . . . . . . . . 11 class ( r s ( x t y ) )
16	13, 15	wceq 1402	. . . . . . . . . 10 wff ( ( r s x ) t y ) = ( r s ( x t y ) )
17	3, 10, 7	co 6079	. . . . . . . . . . . 12 class ( r s y )
18	5, 17, 12	co 6079	. . . . . . . . . . 11 class ( x t ( r s y ) )
19	18, 15	wceq 1402	. . . . . . . . . 10 wff ( x t ( r s y ) ) = ( r s ( x t y ) )
20	16, 19	wa 104	. . . . . . . . 9 wff ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) )
21		vw	. . . . . . . . . . 11 setvar w
22	21	cv 1401	. . . . . . . . . 10 class w
23		cmulr 13415	. . . . . . . . . 10 class .r
24	22, 23	cfv 5375	. . . . . . . . 9 class ( .r ` w )
25	20, 11, 24	wsbc 3051	. . . . . . . 8 wff [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) )
26		cvsca 13418	. . . . . . . . 9 class .s
27	22, 26	cfv 5375	. . . . . . . 8 class ( .s ` w )
28	25, 6, 27	wsbc 3051	. . . . . . 7 wff [. ( .s ` w ) / s ]. [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) )
29		cbs 13335	. . . . . . . 8 class Base
30	22, 29	cfv 5375	. . . . . . 7 class ( Base ` w )
31	28, 9, 30	wral 2528	. . . . . 6 wff A. y e. ( Base ` w ) [. ( .s ` w ) / s ]. [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) )
32	31, 4, 30	wral 2528	. . . . 5 wff A. x e. ( Base ` w ) A. y e. ( Base ` w ) [. ( .s ` w ) / s ]. [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) )
33		vf	. . . . . . 7 setvar f
34	33	cv 1401	. . . . . 6 class f
35	34, 29	cfv 5375	. . . . 5 class ( Base ` f )
36	32, 2, 35	wral 2528	. . . 4 wff A. r e. ( Base ` f ) A. x e. ( Base ` w ) A. y e. ( Base ` w ) [. ( .s ` w ) / s ]. [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) )
37		csca 13417	. . . . 5 class Scalar
38	22, 37	cfv 5375	. . . 4 class (Scalar ` w )
39	36, 33, 38	wsbc 3051	. . 3 wff [. (Scalar ` w ) / f ]. A. r e. ( Base ` f ) A. x e. ( Base ` w ) A. y e. ( Base ` w ) [. ( .s ` w ) / s ]. [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) )
40		clmod 14606	. . . 4 class LMod
41		crg 14283	. . . 4 class Ring
42	40, 41	cin 3219	. . 3 class ( LMod i^i Ring )
43	39, 21, 42	crab 2532	. 2 class { w e. ( LMod i^i Ring ) | [. (Scalar ` w ) / f ]. A. r e. ( Base ` f ) A. x e. ( Base ` w ) A. y e. ( Base ` w ) [. ( .s ` w ) / s ]. [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) ) }
44	1, 43	wceq 1402	1 wff AssAlg = { w e. ( LMod i^i Ring ) | [. (Scalar ` w ) / f ]. A. r e. ( Base ` f ) A. x e. ( Base ` w ) A. y e. ( Base ` w ) [. ( .s ` w ) / s ]. [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) ) }

This definition is referenced by:  isassa  14985