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 CMnd | [˙Base g / v]˙ [˙+ g / a]˙ [˙ g / s]˙ [˙ Scalar g / f]˙ [˙Base f / k]˙ [˙+ f / p]˙ [˙ f / t]˙ f SRing q k r k x v w v r s w 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 1 f s w = w 0 f s w = 0 g

Detailed syntax breakdown

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