Metamath Proof Explorer

Definition df-slmd

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)

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cslmd 
 |-  SLMod
1 vg 
 |-  g
2 ccmn 
 |-  CMnd
3 cbs 
 |-  Base
4 1 cv 
 |-  g
5 4 3 cfv 
 |-  ( Base ` g )
6 vv 
 |-  v
7 cplusg 
 |-  +g
8 4 7 cfv 
 |-  ( +g ` g )
9 va 
 |-  a
10 cvsca 
 |-  .s
11 4 10 cfv 
 |-  ( .s ` g )
12 vs 
 |-  s
13 csca 
 |-  Scalar
14 4 13 cfv 
 |-  ( Scalar ` g )
15 vf 
 |-  f
16 15 cv 
 |-  f
17 16 3 cfv 
 |-  ( Base ` f )
18 vk 
 |-  k
19 16 7 cfv 
 |-  ( +g ` f )
20 vp 
 |-  p
21 cmulr 
 |-  .r
22 16 21 cfv 
 |-  ( .r ` f )
23 vt 
 |-  t
24 csrg 
 |-  SRing
25 16 24 wcel 
 |-  f e. SRing
26 vq 
 |-  q
27 18 cv 
 |-  k
28 vr 
 |-  r
29 vx 
 |-  x
30 6 cv 
 |-  v
31 vw 
 |-  w
32 28 cv 
 |-  r
33 12 cv 
 |-  s
34 31 cv 
 |-  w
35 32 34 33 co 
 |-  ( r s w )
36 35 30 wcel 
 |-  ( r s w ) e. v
37 9 cv 
 |-  a
38 29 cv 
 |-  x
39 34 38 37 co 
 |-  ( w a x )
40 32 39 33 co 
 |-  ( r s ( w a x ) )
41 32 38 33 co 
 |-  ( r s x )
42 35 41 37 co 
 |-  ( ( r s w ) a ( r s x ) )
43 40 42 wceq 
 |-  ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) )
44 26 cv 
 |-  q
45 20 cv 
 |-  p
46 44 32 45 co 
 |-  ( q p r )
47 46 34 33 co 
 |-  ( ( q p r ) s w )
48 44 34 33 co 
 |-  ( q s w )
49 48 35 37 co 
 |-  ( ( q s w ) a ( r s w ) )
50 47 49 wceq 
 |-  ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) )
51 36 43 50 w3a 
 |-  ( ( 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 ) ) )
52 23 cv 
 |-  t
53 44 32 52 co 
 |-  ( q t r )
54 53 34 33 co 
 |-  ( ( q t r ) s w )
55 44 35 33 co 
 |-  ( q s ( r s w ) )
56 54 55 wceq 
 |-  ( ( q t r ) s w ) = ( q s ( r s w ) )
57 cur 
 |-  1r
58 16 57 cfv 
 |-  ( 1r ` f )
59 58 34 33 co 
 |-  ( ( 1r ` f ) s w )
60 59 34 wceq 
 |-  ( ( 1r ` f ) s w ) = w
61 c0g 
 |-  0g
62 16 61 cfv 
 |-  ( 0g ` f )
63 62 34 33 co 
 |-  ( ( 0g ` f ) s w )
64 4 61 cfv 
 |-  ( 0g ` g )
65 63 64 wceq 
 |-  ( ( 0g ` f ) s w ) = ( 0g ` g )
66 56 60 65 w3a 
 |-  ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) )
67 51 66 wa 
 |-  ( ( ( 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 ) ) )
68 67 31 30 wral 
 |-  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 ) ) )
69 68 29 30 wral 
 |-  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 69 28 27 wral 
 |-  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 ) ) )
71 70 26 27 wral 
 |-  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 ) ) )
72 25 71 wa 
 |-  ( 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 72 23 22 wsbc 
 |-  [. ( .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 ) ) ) )
74 73 20 19 wsbc 
 |-  [. ( +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 ) ) ) )
75 74 18 17 wsbc 
 |-  [. ( 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 ) ) ) )
76 75 15 14 wsbc 
 |-  [. ( 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 ) ) ) )
77 76 12 11 wsbc 
 |-  [. ( .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 ) ) ) )
78 77 9 8 wsbc 
 |-  [. ( +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 ) ) ) )
79 78 6 5 wsbc 
 |-  [. ( 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 79 1 2 crab 
 |-  { 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 ) ) ) ) }
81 0 80 wceq 
 |-  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 ) ) ) ) }