Metamath Proof Explorer

Definition df-assa

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)

Ref Expression
Assertion 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 ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 casa 
 |-  AssAlg
1 vw 
 |-  w
2 clmod 
 |-  LMod
3 crg 
 |-  Ring
4 2 3 cin 
 |-  ( LMod i^i Ring )
5 csca 
 |-  Scalar
6 1 cv 
 |-  w
7 6 5 cfv 
 |-  ( Scalar ` w )
8 vf 
 |-  f
9 vr 
 |-  r
10 cbs 
 |-  Base
11 8 cv 
 |-  f
12 11 10 cfv 
 |-  ( Base ` f )
13 vx 
 |-  x
14 6 10 cfv 
 |-  ( Base ` w )
15 vy 
 |-  y
16 cvsca 
 |-  .s
17 6 16 cfv 
 |-  ( .s ` w )
18 vs 
 |-  s
19 cmulr 
 |-  .r
20 6 19 cfv 
 |-  ( .r ` w )
21 vt 
 |-  t
22 9 cv 
 |-  r
23 18 cv 
 |-  s
24 13 cv 
 |-  x
25 22 24 23 co 
 |-  ( r s x )
26 21 cv 
 |-  t
27 15 cv 
 |-  y
28 25 27 26 co 
 |-  ( ( r s x ) t y )
29 24 27 26 co 
 |-  ( x t y )
30 22 29 23 co 
 |-  ( r s ( x t y ) )
31 28 30 wceq 
 |-  ( ( r s x ) t y ) = ( r s ( x t y ) )
32 22 27 23 co 
 |-  ( r s y )
33 24 32 26 co 
 |-  ( x t ( r s y ) )
34 33 30 wceq 
 |-  ( x t ( r s y ) ) = ( r s ( x t y ) )
35 31 34 wa 
 |-  ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) )
36 35 21 20 wsbc 
 |-  [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) )
37 36 18 17 wsbc 
 |-  [. ( .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 ) ) )
38 37 15 14 wral 
 |-  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 38 13 14 wral 
 |-  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 39 9 12 wral 
 |-  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 ) ) )
41 40 8 7 wsbc 
 |-  [. ( 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 ) ) )
42 41 1 4 crab 
 |-  { 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 ) ) ) }
43 0 42 wceq 
 |-  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 ) ) ) }