# Metamath Proof Explorer

## 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 ${setvar}{r}$
2 cvv ${class}\mathrm{V}$
3 vm ${setvar}{m}$
4 1 cv ${setvar}{r}$
5 cfrlm ${class}\mathrm{freeLMod}$
6 cbs ${class}\mathrm{Base}$
7 3 cv ${setvar}{m}$
8 7 6 cfv ${class}{\mathrm{Base}}_{{m}}$
9 4 8 5 co ${class}\left({r}\mathrm{freeLMod}{\mathrm{Base}}_{{m}}\right)$
10 vv ${setvar}{v}$
11 10 cv ${setvar}{v}$
12 csts ${class}\mathrm{sSet}$
13 cmulr ${class}{\cdot }_{𝑟}$
14 cnx ${class}\mathrm{ndx}$
15 14 13 cfv ${class}{\cdot }_{\mathrm{ndx}}$
16 vx ${setvar}{x}$
17 11 6 cfv ${class}{\mathrm{Base}}_{{v}}$
18 vy ${setvar}{y}$
19 cgsu ${class}{\Sigma }_{𝑔}$
20 va ${setvar}{a}$
21 vb ${setvar}{b}$
22 vi ${setvar}{i}$
23 22 cv ${setvar}{i}$
24 20 cv ${setvar}{a}$
25 cplusg ${class}{+}_{𝑔}$
26 7 25 cfv ${class}{+}_{{m}}$
27 21 cv ${setvar}{b}$
28 24 27 26 co ${class}\left({a}{+}_{{m}}{b}\right)$
29 23 28 wceq ${wff}{i}={a}{+}_{{m}}{b}$
30 16 cv ${setvar}{x}$
31 24 30 cfv ${class}{x}\left({a}\right)$
32 4 13 cfv ${class}{\cdot }_{{r}}$
33 18 cv ${setvar}{y}$
34 27 33 cfv ${class}{y}\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 ${class}if\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
46 1 3 2 2 45 cmpo
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