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|[˙Baseg/v]˙[˙+g/a]˙[˙⋅g/s]˙[˙Scalar⁡g/f]˙[˙Basef/k]˙[˙+f/p]˙[˙⋅f/t]˙f∈SRing∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w∧0fsw=0g

Detailed syntax breakdown

Step Hyp Ref Expression
0 cslmd classSLMod
1 vg setvarg
2 ccmn classCMnd
3 cbs classBase
4 1 cv setvarg
5 4 3 cfv classBaseg
6 vv setvarv
7 cplusg class+𝑔
8 4 7 cfv class+g
9 va setvara
10 cvsca class⋅𝑠
11 4 10 cfv class⋅g
12 vs setvars
13 csca classScalar
14 4 13 cfv classScalar⁡g
15 vf setvarf
16 15 cv setvarf
17 16 3 cfv classBasef
18 vk setvark
19 16 7 cfv class+f
20 vp setvarp
21 cmulr class⋅𝑟
22 16 21 cfv class⋅f
23 vt setvart
24 csrg classSRing
25 16 24 wcel wfff∈SRing
26 vq setvarq
27 18 cv setvark
28 vr setvarr
29 vx setvarx
30 6 cv setvarv
31 vw setvarw
32 28 cv setvarr
33 12 cv setvars
34 31 cv setvarw
35 32 34 33 co classrsw
36 35 30 wcel wffrsw∈v
37 9 cv setvara
38 29 cv setvarx
39 34 38 37 co classwax
40 32 39 33 co classrswax
41 32 38 33 co classrsx
42 35 41 37 co classrswarsx
43 40 42 wceq wffrswax=rswarsx
44 26 cv setvarq
45 20 cv setvarp
46 44 32 45 co classqpr
47 46 34 33 co classqprsw
48 44 34 33 co classqsw
49 48 35 37 co classqswarsw
50 47 49 wceq wffqprsw=qswarsw
51 36 43 50 w3a wffrsw∈v∧rswax=rswarsx∧qprsw=qswarsw
52 23 cv setvart
53 44 32 52 co classqtr
54 53 34 33 co classqtrsw
55 44 35 33 co classqsrsw
56 54 55 wceq wffqtrsw=qsrsw
57 cur class1r
58 16 57 cfv class1f
59 58 34 33 co class1fsw
60 59 34 wceq wff1fsw=w
61 c0g class0𝑔
62 16 61 cfv class0f
63 62 34 33 co class0fsw
64 4 61 cfv class0g
65 63 64 wceq wff0fsw=0g
66 56 60 65 w3a wffqtrsw=qsrsw∧1fsw=w∧0fsw=0g
67 51 66 wa wffrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w∧0fsw=0g
68 67 31 30 wral wff∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w∧0fsw=0g
69 68 29 30 wral wff∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w∧0fsw=0g
70 69 28 27 wral wff∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w∧0fsw=0g
71 70 26 27 wral wff∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w∧0fsw=0g
72 25 71 wa wfff∈SRing∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w∧0fsw=0g
73 72 23 22 wsbc wff[˙⋅f/t]˙f∈SRing∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w∧0fsw=0g
74 73 20 19 wsbc wff[˙+f/p]˙[˙⋅f/t]˙f∈SRing∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w∧0fsw=0g
75 74 18 17 wsbc wff[˙Basef/k]˙[˙+f/p]˙[˙⋅f/t]˙f∈SRing∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w∧0fsw=0g
76 75 15 14 wsbc wff[˙Scalar⁡g/f]˙[˙Basef/k]˙[˙+f/p]˙[˙⋅f/t]˙f∈SRing∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w∧0fsw=0g
77 76 12 11 wsbc wff[˙⋅g/s]˙[˙Scalar⁡g/f]˙[˙Basef/k]˙[˙+f/p]˙[˙⋅f/t]˙f∈SRing∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w∧0fsw=0g
78 77 9 8 wsbc wff[˙+g/a]˙[˙⋅g/s]˙[˙Scalar⁡g/f]˙[˙Basef/k]˙[˙+f/p]˙[˙⋅f/t]˙f∈SRing∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w∧0fsw=0g
79 78 6 5 wsbc wff[˙Baseg/v]˙[˙+g/a]˙[˙⋅g/s]˙[˙Scalar⁡g/f]˙[˙Basef/k]˙[˙+f/p]˙[˙⋅f/t]˙f∈SRing∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w∧0fsw=0g
80 79 1 2 crab classg∈CMnd|[˙Baseg/v]˙[˙+g/a]˙[˙⋅g/s]˙[˙Scalar⁡g/f]˙[˙Basef/k]˙[˙+f/p]˙[˙⋅f/t]˙f∈SRing∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w∧0fsw=0g
81 0 80 wceq wffSLMod=g∈CMnd|[˙Baseg/v]˙[˙+g/a]˙[˙⋅g/s]˙[˙Scalar⁡g/f]˙[˙Basef/k]˙[˙+f/p]˙[˙⋅f/t]˙f∈SRing∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w∧0fsw=0g