Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-slmd Structured version   Unicode version

Definition df-slmd 28355
Description: Define the class of all (left) modules over semirings, i.e. semimodules, which are generalizations of left modules. A semimodule is a commutative monoid (=vectors) together with a semiring (=scalars) and a left scalar product connecting them.  ( 0 [,] +oo ) for example is not a full fledged left module, but is a semimodule. Definition of [Golan] p. 149. (Contributed by Thierry Arnoux, 21-Mar-2018.)
Assertion
Ref Expression
df-slmd  |- SLMod  =  {
g  e. CMnd  |  [. ( Base `  g )  / 
v ]. [. ( +g  `  g )  /  a ]. [. ( .s `  g )  /  s ]. [. (Scalar `  g
)  /  f ]. [. ( Base `  f
)  /  k ]. [. ( +g  `  f
)  /  p ]. [. ( .r `  f
)  /  t ]. ( f  e. SRing  /\  A. q  e.  k  A. r  e.  k  A. x  e.  v  A. w  e.  v  (
( ( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  ( ( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  (
( 1r `  f
) s w )  =  w  /\  (
( 0g `  f
) s w )  =  ( 0g `  g ) ) ) ) }
Distinct variable group:    f, a, g, k, p, q, r, s, t, v, w, x

Detailed syntax breakdown of Definition df-slmd
StepHypRef Expression
1 cslmd 28354 . 2  class SLMod
2 vf . . . . . . . . . . . . 13  setvar  f
32cv 1436 . . . . . . . . . . . 12  class  f
4 csrg 17674 . . . . . . . . . . . 12  class SRing
53, 4wcel 1870 . . . . . . . . . . 11  wff  f  e. SRing
6 vr . . . . . . . . . . . . . . . . . . . 20  setvar  r
76cv 1436 . . . . . . . . . . . . . . . . . . 19  class  r
8 vw . . . . . . . . . . . . . . . . . . . 20  setvar  w
98cv 1436 . . . . . . . . . . . . . . . . . . 19  class  w
10 vs . . . . . . . . . . . . . . . . . . . 20  setvar  s
1110cv 1436 . . . . . . . . . . . . . . . . . . 19  class  s
127, 9, 11co 6305 . . . . . . . . . . . . . . . . . 18  class  ( r s w )
13 vv . . . . . . . . . . . . . . . . . . 19  setvar  v
1413cv 1436 . . . . . . . . . . . . . . . . . 18  class  v
1512, 14wcel 1870 . . . . . . . . . . . . . . . . 17  wff  ( r s w )  e.  v
16 vx . . . . . . . . . . . . . . . . . . . . 21  setvar  x
1716cv 1436 . . . . . . . . . . . . . . . . . . . 20  class  x
18 va . . . . . . . . . . . . . . . . . . . . 21  setvar  a
1918cv 1436 . . . . . . . . . . . . . . . . . . . 20  class  a
209, 17, 19co 6305 . . . . . . . . . . . . . . . . . . 19  class  ( w a x )
217, 20, 11co 6305 . . . . . . . . . . . . . . . . . 18  class  ( r s ( w a x ) )
227, 17, 11co 6305 . . . . . . . . . . . . . . . . . . 19  class  ( r s x )
2312, 22, 19co 6305 . . . . . . . . . . . . . . . . . 18  class  ( ( r s w ) a ( r s x ) )
2421, 23wceq 1437 . . . . . . . . . . . . . . . . 17  wff  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )
25 vq . . . . . . . . . . . . . . . . . . . . 21  setvar  q
2625cv 1436 . . . . . . . . . . . . . . . . . . . 20  class  q
27 vp . . . . . . . . . . . . . . . . . . . . 21  setvar  p
2827cv 1436 . . . . . . . . . . . . . . . . . . . 20  class  p
2926, 7, 28co 6305 . . . . . . . . . . . . . . . . . . 19  class  ( q p r )
3029, 9, 11co 6305 . . . . . . . . . . . . . . . . . 18  class  ( ( q p r ) s w )
3126, 9, 11co 6305 . . . . . . . . . . . . . . . . . . 19  class  ( q s w )
3231, 12, 19co 6305 . . . . . . . . . . . . . . . . . 18  class  ( ( q s w ) a ( r s w ) )
3330, 32wceq 1437 . . . . . . . . . . . . . . . . 17  wff  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) )
3415, 24, 33w3a 982 . . . . . . . . . . . . . . . 16  wff  ( ( r s w )  e.  v  /\  (
r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  (
( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )
35 vt . . . . . . . . . . . . . . . . . . . . 21  setvar  t
3635cv 1436 . . . . . . . . . . . . . . . . . . . 20  class  t
3726, 7, 36co 6305 . . . . . . . . . . . . . . . . . . 19  class  ( q t r )
3837, 9, 11co 6305 . . . . . . . . . . . . . . . . . 18  class  ( ( q t r ) s w )
3926, 12, 11co 6305 . . . . . . . . . . . . . . . . . 18  class  ( q s ( r s w ) )
4038, 39wceq 1437 . . . . . . . . . . . . . . . . 17  wff  ( ( q t r ) s w )  =  ( q s ( r s w ) )
41 cur 17670 . . . . . . . . . . . . . . . . . . . 20  class  1r
423, 41cfv 5601 . . . . . . . . . . . . . . . . . . 19  class  ( 1r
`  f )
4342, 9, 11co 6305 . . . . . . . . . . . . . . . . . 18  class  ( ( 1r `  f ) s w )
4443, 9wceq 1437 . . . . . . . . . . . . . . . . 17  wff  ( ( 1r `  f ) s w )  =  w
45 c0g 15297 . . . . . . . . . . . . . . . . . . . 20  class  0g
463, 45cfv 5601 . . . . . . . . . . . . . . . . . . 19  class  ( 0g
`  f )
4746, 9, 11co 6305 . . . . . . . . . . . . . . . . . 18  class  ( ( 0g `  f ) s w )
48 vg . . . . . . . . . . . . . . . . . . . 20  setvar  g
4948cv 1436 . . . . . . . . . . . . . . . . . . 19  class  g
5049, 45cfv 5601 . . . . . . . . . . . . . . . . . 18  class  ( 0g
`  g )
5147, 50wceq 1437 . . . . . . . . . . . . . . . . 17  wff  ( ( 0g `  f ) s w )  =  ( 0g `  g
)
5240, 44, 51w3a 982 . . . . . . . . . . . . . . . 16  wff  ( ( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  (
( 1r `  f
) s w )  =  w  /\  (
( 0g `  f
) s w )  =  ( 0g `  g ) )
5334, 52wa 370 . . . . . . . . . . . . . . 15  wff  ( ( ( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  ( ( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  ( ( 1r `  f ) s w )  =  w  /\  ( ( 0g `  f ) s w )  =  ( 0g `  g
) ) )
5453, 8, 14wral 2782 . . . . . . . . . . . . . 14  wff  A. w  e.  v  ( (
( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  ( ( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  ( ( 1r `  f ) s w )  =  w  /\  ( ( 0g `  f ) s w )  =  ( 0g `  g
) ) )
5554, 16, 14wral 2782 . . . . . . . . . . . . 13  wff  A. x  e.  v  A. w  e.  v  ( (
( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  ( ( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  ( ( 1r `  f ) s w )  =  w  /\  ( ( 0g `  f ) s w )  =  ( 0g `  g
) ) )
56 vk . . . . . . . . . . . . . 14  setvar  k
5756cv 1436 . . . . . . . . . . . . 13  class  k
5855, 6, 57wral 2782 . . . . . . . . . . . 12  wff  A. r  e.  k  A. x  e.  v  A. w  e.  v  ( (
( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  ( ( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  ( ( 1r `  f ) s w )  =  w  /\  ( ( 0g `  f ) s w )  =  ( 0g `  g
) ) )
5958, 25, 57wral 2782 . . . . . . . . . . 11  wff  A. q  e.  k  A. r  e.  k  A. x  e.  v  A. w  e.  v  ( (
( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  ( ( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  ( ( 1r `  f ) s w )  =  w  /\  ( ( 0g `  f ) s w )  =  ( 0g `  g
) ) )
605, 59wa 370 . . . . . . . . . 10  wff  ( f  e. SRing  /\  A. q  e.  k  A. r  e.  k  A. x  e.  v  A. w  e.  v  ( (
( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  ( ( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  ( ( 1r `  f ) s w )  =  w  /\  ( ( 0g `  f ) s w )  =  ( 0g `  g
) ) ) )
61 cmulr 15153 . . . . . . . . . . 11  class  .r
623, 61cfv 5601 . . . . . . . . . 10  class  ( .r
`  f )
6360, 35, 62wsbc 3305 . . . . . . . . 9  wff  [. ( .r `  f )  / 
t ]. ( f  e. SRing  /\  A. q  e.  k 
A. r  e.  k 
A. x  e.  v 
A. w  e.  v  ( ( ( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  (
( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  ( ( 1r `  f ) s w )  =  w  /\  ( ( 0g `  f ) s w )  =  ( 0g
`  g ) ) ) )
64 cplusg 15152 . . . . . . . . . 10  class  +g
653, 64cfv 5601 . . . . . . . . 9  class  ( +g  `  f )
6663, 27, 65wsbc 3305 . . . . . . . 8  wff  [. ( +g  `  f )  /  p ]. [. ( .r
`  f )  / 
t ]. ( f  e. SRing  /\  A. q  e.  k 
A. r  e.  k 
A. x  e.  v 
A. w  e.  v  ( ( ( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  (
( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  ( ( 1r `  f ) s w )  =  w  /\  ( ( 0g `  f ) s w )  =  ( 0g
`  g ) ) ) )
67 cbs 15084 . . . . . . . . 9  class  Base
683, 67cfv 5601 . . . . . . . 8  class  ( Base `  f )
6966, 56, 68wsbc 3305 . . . . . . 7  wff  [. ( Base `  f )  / 
k ]. [. ( +g  `  f )  /  p ]. [. ( .r `  f )  /  t ]. ( f  e. SRing  /\  A. q  e.  k  A. r  e.  k  A. x  e.  v  A. w  e.  v  (
( ( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  ( ( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  (
( 1r `  f
) s w )  =  w  /\  (
( 0g `  f
) s w )  =  ( 0g `  g ) ) ) )
70 csca 15155 . . . . . . . 8  class Scalar
7149, 70cfv 5601 . . . . . . 7  class  (Scalar `  g )
7269, 2, 71wsbc 3305 . . . . . 6  wff  [. (Scalar `  g )  /  f ]. [. ( Base `  f
)  /  k ]. [. ( +g  `  f
)  /  p ]. [. ( .r `  f
)  /  t ]. ( f  e. SRing  /\  A. q  e.  k  A. r  e.  k  A. x  e.  v  A. w  e.  v  (
( ( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  ( ( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  (
( 1r `  f
) s w )  =  w  /\  (
( 0g `  f
) s w )  =  ( 0g `  g ) ) ) )
73 cvsca 15156 . . . . . . 7  class  .s
7449, 73cfv 5601 . . . . . 6  class  ( .s
`  g )
7572, 10, 74wsbc 3305 . . . . 5  wff  [. ( .s `  g )  / 
s ]. [. (Scalar `  g )  /  f ]. [. ( Base `  f
)  /  k ]. [. ( +g  `  f
)  /  p ]. [. ( .r `  f
)  /  t ]. ( f  e. SRing  /\  A. q  e.  k  A. r  e.  k  A. x  e.  v  A. w  e.  v  (
( ( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  ( ( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  (
( 1r `  f
) s w )  =  w  /\  (
( 0g `  f
) s w )  =  ( 0g `  g ) ) ) )
7649, 64cfv 5601 . . . . 5  class  ( +g  `  g )
7775, 18, 76wsbc 3305 . . . 4  wff  [. ( +g  `  g )  / 
a ]. [. ( .s
`  g )  / 
s ]. [. (Scalar `  g )  /  f ]. [. ( Base `  f
)  /  k ]. [. ( +g  `  f
)  /  p ]. [. ( .r `  f
)  /  t ]. ( f  e. SRing  /\  A. q  e.  k  A. r  e.  k  A. x  e.  v  A. w  e.  v  (
( ( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  ( ( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  (
( 1r `  f
) s w )  =  w  /\  (
( 0g `  f
) s w )  =  ( 0g `  g ) ) ) )
7849, 67cfv 5601 . . . 4  class  ( Base `  g )
7977, 13, 78wsbc 3305 . . 3  wff  [. ( Base `  g )  / 
v ]. [. ( +g  `  g )  /  a ]. [. ( .s `  g )  /  s ]. [. (Scalar `  g
)  /  f ]. [. ( Base `  f
)  /  k ]. [. ( +g  `  f
)  /  p ]. [. ( .r `  f
)  /  t ]. ( f  e. SRing  /\  A. q  e.  k  A. r  e.  k  A. x  e.  v  A. w  e.  v  (
( ( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  ( ( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  (
( 1r `  f
) s w )  =  w  /\  (
( 0g `  f
) s w )  =  ( 0g `  g ) ) ) )
80 ccmn 17365 . . 3  class CMnd
8179, 48, 80crab 2786 . 2  class  { g  e. CMnd  |  [. ( Base `  g )  / 
v ]. [. ( +g  `  g )  /  a ]. [. ( .s `  g )  /  s ]. [. (Scalar `  g
)  /  f ]. [. ( Base `  f
)  /  k ]. [. ( +g  `  f
)  /  p ]. [. ( .r `  f
)  /  t ]. ( f  e. SRing  /\  A. q  e.  k  A. r  e.  k  A. x  e.  v  A. w  e.  v  (
( ( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  ( ( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  (
( 1r `  f
) s w )  =  w  /\  (
( 0g `  f
) s w )  =  ( 0g `  g ) ) ) ) }
821, 81wceq 1437 1  wff SLMod  =  {
g  e. CMnd  |  [. ( Base `  g )  / 
v ]. [. ( +g  `  g )  /  a ]. [. ( .s `  g )  /  s ]. [. (Scalar `  g
)  /  f ]. [. ( Base `  f
)  /  k ]. [. ( +g  `  f
)  /  p ]. [. ( .r `  f
)  /  t ]. ( f  e. SRing  /\  A. q  e.  k  A. r  e.  k  A. x  e.  v  A. w  e.  v  (
( ( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  ( ( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  (
( 1r `  f
) s w )  =  w  /\  (
( 0g `  f
) s w )  =  ( 0g `  g ) ) ) ) }
Colors of variables: wff setvar class
This definition is referenced by:  isslmd  28356
  Copyright terms: Public domain W3C validator