MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-assa Unicode version

Definition df-assa 16053
Description: Definition of an associative algebra. An associative algebra is a set equipped with a left-module structure on a (commutative) ring, coupled with an 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
StepHypRef Expression
1 casa 16050 . 2  class AssAlg
2 vf . . . . . . 7  set  f
32cv 1622 . . . . . 6  class  f
4 ccrg 15338 . . . . . 6  class  CRing
53, 4wcel 1684 . . . . 5  wff  f  e. 
CRing
6 vr . . . . . . . . . . . . . . 15  set  r
76cv 1622 . . . . . . . . . . . . . 14  class  r
8 vx . . . . . . . . . . . . . . 15  set  x
98cv 1622 . . . . . . . . . . . . . 14  class  x
10 vs . . . . . . . . . . . . . . 15  set  s
1110cv 1622 . . . . . . . . . . . . . 14  class  s
127, 9, 11co 5858 . . . . . . . . . . . . 13  class  ( r s x )
13 vy . . . . . . . . . . . . . 14  set  y
1413cv 1622 . . . . . . . . . . . . 13  class  y
15 vt . . . . . . . . . . . . . 14  set  t
1615cv 1622 . . . . . . . . . . . . 13  class  t
1712, 14, 16co 5858 . . . . . . . . . . . 12  class  ( ( r s x ) t y )
189, 14, 16co 5858 . . . . . . . . . . . . 13  class  ( x t y )
197, 18, 11co 5858 . . . . . . . . . . . 12  class  ( r s ( x t y ) )
2017, 19wceq 1623 . . . . . . . . . . 11  wff  ( ( r s x ) t y )  =  ( r s ( x t y ) )
217, 14, 11co 5858 . . . . . . . . . . . . 13  class  ( r s y )
229, 21, 16co 5858 . . . . . . . . . . . 12  class  ( x t ( r s y ) )
2322, 19wceq 1623 . . . . . . . . . . 11  wff  ( x t ( r s y ) )  =  ( r s ( x t y ) )
2420, 23wa 358 . . . . . . . . . 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  set  w
2625cv 1622 . . . . . . . . . . 11  class  w
27 cmulr 13209 . . . . . . . . . . 11  class  .r
2826, 27cfv 5255 . . . . . . . . . 10  class  ( .r
`  w )
2924, 15, 28wsbc 2991 . . . . . . . . 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 13212 . . . . . . . . . 10  class  .s
3126, 30cfv 5255 . . . . . . . . 9  class  ( .s
`  w )
3229, 10, 31wsbc 2991 . . . . . . . 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 13148 . . . . . . . . 9  class  Base
3426, 33cfv 5255 . . . . . . . 8  class  ( Base `  w )
3532, 13, 34wral 2543 . . . . . . 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 ) ) )
3635, 8, 34wral 2543 . . . . . 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 ) ) )
373, 33cfv 5255 . . . . . 6  class  ( Base `  f )
3836, 6, 37wral 2543 . . . . 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 ) ) )
395, 38wa 358 . . . 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 13211 . . . . 5  class Scalar
4126, 40cfv 5255 . . . 4  class  (Scalar `  w )
4239, 2, 41wsbc 2991 . . 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 15627 . . . 4  class  LMod
44 crg 15337 . . . 4  class  Ring
4543, 44cin 3151 . . 3  class  ( LMod 
i^i  Ring )
4642, 25, 45crab 2547 . 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 ) ) ) ) }
471, 46wceq 1623 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 ) ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  isassa  16056
  Copyright terms: Public domain W3C validator