Definition df-mnring

Description: Define the monoid ring function. This takes a monoid M and a ring R and produces a free left module over R with a product extending the monoid function on M . (Contributed by Rohan Ridenour, 13-May-2024)

	Ref	Expression
Assertion	df-mnring	Could not format assertion : No typesetting found for |- MndRing = ( r e. _V , m e. _V |-> [_ ( r freeLMod ( Base ` m ) ) / v ]_ ( v sSet <. ( .r ` ndx ) , ( x e. ( Base ` v ) , y e. ( Base ` v ) |-> ( v gsum ( a e. ( Base ` m ) , b e. ( Base ` m ) |-> ( i e. ( Base ` m ) |-> if ( i = ( a ( +g ` m ) b ) , ( ( x ` a ) ( .r ` r ) ( y ` b ) ) , ( 0g ` r ) ) ) ) ) ) >. ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmnring	Could not format MndRing : No typesetting found for class MndRing with typecode class
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3		vm	$$setvarm$$
4	1	cv	$$setvarr$$
5		cfrlm	$$class\mathrm{freeLMod}$$
6		cbs	$$class\mathrm{Base}$$
7	3	cv	$$setvarm$$
8	7 6	cfv	$$class{\mathrm{Base}}_m$$
9	4 8 5	co	$$class\left(r\mathrm{freeLMod}{\mathrm{Base}}_m\right)$$
10		vv	$$setvarv$$
11	10	cv	$$setvarv$$
12		csts	$$class\mathrm{sSet}$$
13		cmulr	$$class{\cdot }_{𝑟}$$
14		cnx	$$class\mathrm{ndx}$$
15	14 13	cfv	$$class{\cdot }_{\mathrm{ndx}}$$
16		vx	$$setvarx$$
17	11 6	cfv	$$class{\mathrm{Base}}_v$$
18		vy	$$setvary$$
19		cgsu	$$class{\Sigma }_{𝑔}$$
20		va	$$setvara$$
21		vb	$$setvarb$$
22		vi	$$setvari$$
23	22	cv	$$setvari$$
24	20	cv	$$setvara$$
25		cplusg	$$class{+}_{𝑔}$$
26	7 25	cfv	$$class{+}_m$$
27	21	cv	$$setvarb$$
28	24 27 26	co	$$class\left(a{+}_{m}b\right)$$
29	23 28	wceq	$$wffi=a{+}_{m}b$$
30	16	cv	$$setvarx$$
31	24 30	cfv	$$classx\left(a\right)$$
32	4 13	cfv	$$class{\cdot }_r$$
33	18	cv	$$setvary$$
34	27 33	cfv	$$classy\left(b\right)$$
35	31 34 32	co	$$class\left(x\left(a\right){\cdot }_{r}y\left(b\right)\right)$$
36		c0g	$$class{0}_{𝑔}$$
37	4 36	cfv	$$class{0}_r$$
38	29 35 37	cif	$$classif\left(i=a{+}_{m}b,x\left(a\right){\cdot }_{r}y\left(b\right),0_r\right)$$
39	22 8 38	cmpt	$$class\left(i\in {\mathrm{Base}}_m⟼if\left(i=a{+}_{m}b,x\left(a\right){\cdot }_{r}y\left(b\right),0_r\right)\right)$$
40	20 21 8 8 39	cmpo	$$class\left(a\in {\mathrm{Base}}_m,b\in {\mathrm{Base}}_m⟼\left(i\in {\mathrm{Base}}_m⟼if\left(i=a{+}_{m}b,x\left(a\right){\cdot }_{r}y\left(b\right),0_r\right)\right)\right)$$
41	11 40 19	co	$$class\left({\sum }_v,\left(a\in {\mathrm{Base}}_m,b\in {\mathrm{Base}}_m⟼\left(i\in {\mathrm{Base}}_m⟼if\left(i=a{+}_{m}b,x\left(a\right){\cdot }_{r}y\left(b\right),0_r\right)\right)\right)\right)$$
42	16 18 17 17 41	cmpo	$$class\left(x\in {\mathrm{Base}}_v,y\in {\mathrm{Base}}_v⟼{\sum }_v\left(a\in {\mathrm{Base}}_m,b\in {\mathrm{Base}}_m⟼\left(i\in {\mathrm{Base}}_m⟼if\left(i=a{+}_{m}b,x\left(a\right){\cdot }_{r}y\left(b\right),0_r\right)\right)\right)\right)$$
43	15 42	cop	$$class⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_v,y\in {\mathrm{Base}}_v⟼{\sum }_v\left(a\in {\mathrm{Base}}_m,b\in {\mathrm{Base}}_m⟼\left(i\in {\mathrm{Base}}_m⟼if\left(i=a{+}_{m}b,x\left(a\right){\cdot }_{r}y\left(b\right),0_r\right)\right)\right)\right)⟩$$
44	11 43 12	co	$$class\left(v\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_v,y\in {\mathrm{Base}}_v⟼{\sum }_v\left(a\in {\mathrm{Base}}_m,b\in {\mathrm{Base}}_m⟼\left(i\in {\mathrm{Base}}_m⟼if\left(i=a{+}_{m}b,x\left(a\right){\cdot }_{r}y\left(b\right),0_r\right)\right)\right)\right)⟩\right)$$
45	10 9 44	csb	$$class⦋\left(r\mathrm{freeLMod}{\mathrm{Base}}_m\right)/v⦌\left(v\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_v,y\in {\mathrm{Base}}_v⟼{\sum }_v\left(a\in {\mathrm{Base}}_m,b\in {\mathrm{Base}}_m⟼\left(i\in {\mathrm{Base}}_m⟼if\left(i=a{+}_{m}b,x\left(a\right){\cdot }_{r}y\left(b\right),0_r\right)\right)\right)\right)⟩\right)$$
46	1 3 2 2 45	cmpo	$$class\left(r\in \mathrm{V},m\in \mathrm{V}⟼⦋\left(r\mathrm{freeLMod}{\mathrm{Base}}_m\right)/v⦌\left(v\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_v,y\in {\mathrm{Base}}_v⟼{\sum }_v\left(a\in {\mathrm{Base}}_m,b\in {\mathrm{Base}}_m⟼\left(i\in {\mathrm{Base}}_m⟼if\left(i=a{+}_{m}b,x\left(a\right){\cdot }_{r}y\left(b\right),0_r\right)\right)\right)\right)⟩\right)\right)$$
47	0 46	wceq	Could not format MndRing = ( r e. _V , m e. _V |-> [_ ( r freeLMod ( Base ` m ) ) / v ]_ ( v sSet <. ( .r ` ndx ) , ( x e. ( Base ` v ) , y e. ( Base ` v ) |-> ( v gsum ( a e. ( Base ` m ) , b e. ( Base ` m ) |-> ( i e. ( Base ` m ) |-> if ( i = ( a ( +g ` m ) b ) , ( ( x ` a ) ( .r ` r ) ( y ` b ) ) , ( 0g ` r ) ) ) ) ) ) >. ) ) : No typesetting found for wff MndRing = ( r e. _V , m e. _V |-> [_ ( r freeLMod ( Base ` m ) ) / v ]_ ( v sSet <. ( .r ` ndx ) , ( x e. ( Base ` v ) , y e. ( Base ` v ) |-> ( v gsum ( a e. ( Base ` m ) , b e. ( Base ` m ) |-> ( i e. ( Base ` m ) |-> if ( i = ( a ( +g ` m ) b ) , ( ( x ` a ) ( .r ` r ) ( y ` b ) ) , ( 0g ` r ) ) ) ) ) ) >. ) ) with typecode wff