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	$$⊢\mathrm{SLMod}=\left\{g\in \mathrm{CMnd}|\underset{\dot{}}{[}{\mathrm{Base}}_g/v\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_g/a\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_g/s\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Scalar}\left(g\right)/f\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{SRing}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\wedge 0_{f}sw=0_g\right)\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cslmd	$$class\mathrm{SLMod}$$
1		vg	$$setvarg$$
2		ccmn	$$class\mathrm{CMnd}$$
3		cbs	$$class\mathrm{Base}$$
4	1	cv	$$setvarg$$
5	4 3	cfv	$$class{\mathrm{Base}}_g$$
6		vv	$$setvarv$$
7		cplusg	$$class{+}_{𝑔}$$
8	4 7	cfv	$$class{+}_g$$
9		va	$$setvara$$
10		cvsca	$$class{\cdot }_{𝑠}$$
11	4 10	cfv	$$class{\cdot }_g$$
12		vs	$$setvars$$
13		csca	$$class\mathrm{Scalar}$$
14	4 13	cfv	$$class\mathrm{Scalar}\left(g\right)$$
15		vf	$$setvarf$$
16	15	cv	$$setvarf$$
17	16 3	cfv	$$class{\mathrm{Base}}_f$$
18		vk	$$setvark$$
19	16 7	cfv	$$class{+}_f$$
20		vp	$$setvarp$$
21		cmulr	$$class{\cdot }_{𝑟}$$
22	16 21	cfv	$$class{\cdot }_f$$
23		vt	$$setvart$$
24		csrg	$$class\mathrm{SRing}$$
25	16 24	wcel	$$wfff\in \mathrm{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	$$class\left(rsw\right)$$
36	35 30	wcel	$$wffrsw\in v$$
37	9	cv	$$setvara$$
38	29	cv	$$setvarx$$
39	34 38 37	co	$$class\left(wax\right)$$
40	32 39 33	co	$$class\left(rs\left(wax\right)\right)$$
41	32 38 33	co	$$class\left(rsx\right)$$
42	35 41 37	co	$$class\left(\left(rsw\right)a\left(rsx\right)\right)$$
43	40 42	wceq	$$wffrs\left(wax\right)=\left(rsw\right)a\left(rsx\right)$$
44	26	cv	$$setvarq$$
45	20	cv	$$setvarp$$
46	44 32 45	co	$$class\left(qpr\right)$$
47	46 34 33	co	$$class\left(\left(qpr\right)sw\right)$$
48	44 34 33	co	$$class\left(qsw\right)$$
49	48 35 37	co	$$class\left(\left(qsw\right)a\left(rsw\right)\right)$$
50	47 49	wceq	$$wff\left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)$$
51	36 43 50	w3a	$$wff\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)$$
52	23	cv	$$setvart$$
53	44 32 52	co	$$class\left(qtr\right)$$
54	53 34 33	co	$$class\left(\left(qtr\right)sw\right)$$
55	44 35 33	co	$$class\left(qs\left(rsw\right)\right)$$
56	54 55	wceq	$$wff\left(qtr\right)sw=qs\left(rsw\right)$$
57		cur	$$class{1}_r$$
58	16 57	cfv	$$class{1}_f$$
59	58 34 33	co	$$class\left(1_{f}sw\right)$$
60	59 34	wceq	$$wff{1}_{f}sw=w$$
61		c0g	$$class{0}_{𝑔}$$
62	16 61	cfv	$$class{0}_f$$
63	62 34 33	co	$$class\left(0_{f}sw\right)$$
64	4 61	cfv	$$class{0}_g$$
65	63 64	wceq	$$wff{0}_{f}sw=0_g$$
66	56 60 65	w3a	$$wff\left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\wedge 0_{f}sw=0_g\right)$$
67	51 66	wa	$$wff\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\wedge 0_{f}sw=0_g\right)\right)$$
68	67 31 30	wral	$$wff\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\wedge 0_{f}sw=0_g\right)\right)$$
69	68 29 30	wral	$$wff\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\wedge 0_{f}sw=0_g\right)\right)$$
70	69 28 27	wral	$$wff\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\wedge 0_{f}sw=0_g\right)\right)$$
71	70 26 27	wral	$$wff\forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\wedge 0_{f}sw=0_g\right)\right)$$
72	25 71	wa	$$wff\left(f\in \mathrm{SRing}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\wedge 0_{f}sw=0_g\right)\right)\right)$$
73	72 23 22	wsbc	$$wff\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{SRing}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\wedge 0_{f}sw=0_g\right)\right)\right)$$
74	73 20 19	wsbc	$$wff\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{SRing}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\wedge 0_{f}sw=0_g\right)\right)\right)$$
75	74 18 17	wsbc	$$wff\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{SRing}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\wedge 0_{f}sw=0_g\right)\right)\right)$$
76	75 15 14	wsbc	$$wff\underset{\dot{}}{[}\mathrm{Scalar}\left(g\right)/f\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{SRing}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\wedge 0_{f}sw=0_g\right)\right)\right)$$
77	76 12 11	wsbc	$$wff\underset{\dot{}}{[}{\cdot }_g/s\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Scalar}\left(g\right)/f\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{SRing}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\wedge 0_{f}sw=0_g\right)\right)\right)$$
78	77 9 8	wsbc	$$wff\underset{\dot{}}{[}{+}_g/a\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_g/s\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Scalar}\left(g\right)/f\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{SRing}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\wedge 0_{f}sw=0_g\right)\right)\right)$$
79	78 6 5	wsbc	$$wff\underset{\dot{}}{[}{\mathrm{Base}}_g/v\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_g/a\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_g/s\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Scalar}\left(g\right)/f\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{SRing}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\wedge 0_{f}sw=0_g\right)\right)\right)$$
80	79 1 2	crab	$$class\left\{g\in \mathrm{CMnd}|\underset{\dot{}}{[}{\mathrm{Base}}_g/v\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_g/a\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_g/s\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Scalar}\left(g\right)/f\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{SRing}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\wedge 0_{f}sw=0_g\right)\right)\right)\right\}$$
81	0 80	wceq	$$wff\mathrm{SLMod}=\left\{g\in \mathrm{CMnd}|\underset{\dot{}}{[}{\mathrm{Base}}_g/v\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_g/a\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_g/s\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Scalar}\left(g\right)/f\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{SRing}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\wedge 0_{f}sw=0_g\right)\right)\right)\right\}$$