Definition df-assa 19312

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 = { w e. ( LMod i^i Ring ) | [. (Scalar ` w ) / f ]. ( f e. CRing /\ 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 19309	. 2 class AssAlg
2		vf	. . . . . . 7 setvar f
3	2	cv 1482	. . . . . 6 class f
4		ccrg 18548	. . . . . 6 class CRing
5	3, 4	wcel 1990	. . . . 5 wff f e. CRing
6		vr	. . . . . . . . . . . . . . 15 setvar r
7	6	cv 1482	. . . . . . . . . . . . . 14 class r
8		vx	. . . . . . . . . . . . . . 15 setvar x
9	8	cv 1482	. . . . . . . . . . . . . 14 class x
10		vs	. . . . . . . . . . . . . . 15 setvar s
11	10	cv 1482	. . . . . . . . . . . . . 14 class s
12	7, 9, 11	co 6650	. . . . . . . . . . . . 13 class ( r s x )
13		vy	. . . . . . . . . . . . . 14 setvar y
14	13	cv 1482	. . . . . . . . . . . . 13 class y
15		vt	. . . . . . . . . . . . . 14 setvar t
16	15	cv 1482	. . . . . . . . . . . . 13 class t
17	12, 14, 16	co 6650	. . . . . . . . . . . 12 class ( ( r s x ) t y )
18	9, 14, 16	co 6650	. . . . . . . . . . . . 13 class ( x t y )
19	7, 18, 11	co 6650	. . . . . . . . . . . 12 class ( r s ( x t y ) )
20	17, 19	wceq 1483	. . . . . . . . . . 11 wff ( ( r s x ) t y ) = ( r s ( x t y ) )
21	7, 14, 11	co 6650	. . . . . . . . . . . . 13 class ( r s y )
22	9, 21, 16	co 6650	. . . . . . . . . . . 12 class ( x t ( r s y ) )
23	22, 19	wceq 1483	. . . . . . . . . . 11 wff ( x t ( r s y ) ) = ( r s ( x t y ) )
24	20, 23	wa 384	. . . . . . . . . 10 wff ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) )
25		vw	. . . . . . . . . . . 12 setvar w
26	25	cv 1482	. . . . . . . . . . 11 class w
27		cmulr 15942	. . . . . . . . . . 11 class .r
28	26, 27	cfv 5888	. . . . . . . . . 10 class ( .r ` w )
29	24, 15, 28	wsbc 3435	. . . . . . . . 9 wff [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) )
30		cvsca 15945	. . . . . . . . . 10 class .s
31	26, 30	cfv 5888	. . . . . . . . 9 class ( .s ` w )
32	29, 10, 31	wsbc 3435	. . . . . . . 8 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 ) ) )
33		cbs 15857	. . . . . . . . 9 class Base
34	26, 33	cfv 5888	. . . . . . . 8 class ( Base ` w )
35	32, 13, 34	wral 2912	. . . . . . 7 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 ) ) )
36	35, 8, 34	wral 2912	. . . . . 6 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 ) ) )
37	3, 33	cfv 5888	. . . . . 6 class ( Base ` f )
38	36, 6, 37	wral 2912	. . . . 5 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 ) ) )
39	5, 38	wa 384	. . . 4 wff ( f e. CRing /\ 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		csca 15944	. . . . 5 class Scalar
41	26, 40	cfv 5888	. . . 4 class (Scalar ` w )
42	39, 2, 41	wsbc 3435	. . 3 wff [. (Scalar ` w ) / f ]. ( f e. CRing /\ 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 ) ) ) )
43		clmod 18863	. . . 4 class LMod
44		crg 18547	. . . 4 class Ring
45	43, 44	cin 3573	. . 3 class ( LMod i^i Ring )
46	42, 25, 45	crab 2916	. 2 class { w e. ( LMod i^i Ring ) | [. (Scalar ` w ) / f ]. ( f e. CRing /\ 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 ) ) ) ) }
47	1, 46	wceq 1483	1 wff AssAlg = { w e. ( LMod i^i Ring ) | [. (Scalar ` w ) / f ]. ( f e. CRing /\ 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  19315