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

Definition df-assa 17308
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
StepHypRef Expression
1 casa 17305 . 2  class AssAlg
2 vf . . . . . . 7  setvar  f
32cv 1363 . . . . . 6  class  f
4 ccrg 16580 . . . . . 6  class  CRing
53, 4wcel 1757 . . . . 5  wff  f  e. 
CRing
6 vr . . . . . . . . . . . . . . 15  setvar  r
76cv 1363 . . . . . . . . . . . . . 14  class  r
8 vx . . . . . . . . . . . . . . 15  setvar  x
98cv 1363 . . . . . . . . . . . . . 14  class  x
10 vs . . . . . . . . . . . . . . 15  setvar  s
1110cv 1363 . . . . . . . . . . . . . 14  class  s
127, 9, 11co 6082 . . . . . . . . . . . . 13  class  ( r s x )
13 vy . . . . . . . . . . . . . 14  setvar  y
1413cv 1363 . . . . . . . . . . . . 13  class  y
15 vt . . . . . . . . . . . . . 14  setvar  t
1615cv 1363 . . . . . . . . . . . . 13  class  t
1712, 14, 16co 6082 . . . . . . . . . . . 12  class  ( ( r s x ) t y )
189, 14, 16co 6082 . . . . . . . . . . . . 13  class  ( x t y )
197, 18, 11co 6082 . . . . . . . . . . . 12  class  ( r s ( x t y ) )
2017, 19wceq 1364 . . . . . . . . . . 11  wff  ( ( r s x ) t y )  =  ( r s ( x t y ) )
217, 14, 11co 6082 . . . . . . . . . . . . 13  class  ( r s y )
229, 21, 16co 6082 . . . . . . . . . . . 12  class  ( x t ( r s y ) )
2322, 19wceq 1364 . . . . . . . . . . 11  wff  ( x t ( r s y ) )  =  ( r s ( x t y ) )
2420, 23wa 369 . . . . . . . . . 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
2625cv 1363 . . . . . . . . . . 11  class  w
27 cmulr 14224 . . . . . . . . . . 11  class  .r
2826, 27cfv 5408 . . . . . . . . . 10  class  ( .r
`  w )
2924, 15, 28wsbc 3177 . . . . . . . . 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 14227 . . . . . . . . . 10  class  .s
3126, 30cfv 5408 . . . . . . . . 9  class  ( .s
`  w )
3229, 10, 31wsbc 3177 . . . . . . . 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 14159 . . . . . . . . 9  class  Base
3426, 33cfv 5408 . . . . . . . 8  class  ( Base `  w )
3532, 13, 34wral 2707 . . . . . . 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 2707 . . . . . 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 5408 . . . . . 6  class  ( Base `  f )
3836, 6, 37wral 2707 . . . . 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 369 . . . 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 14226 . . . . 5  class Scalar
4126, 40cfv 5408 . . . 4  class  (Scalar `  w )
4239, 2, 41wsbc 3177 . . 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 16874 . . . 4  class  LMod
44 crg 16579 . . . 4  class  Ring
4543, 44cin 3317 . . 3  class  ( LMod 
i^i  Ring )
4642, 25, 45crab 2711 . 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 1364 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 setvar class
This definition is referenced by:  isassa  17311
  Copyright terms: Public domain W3C validator