Definition df-mnring 45169

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

Assertion

Ref	Expression
df-mnring	⊢ MndRing = (𝑟 ∈ V, 𝑚 ∈ V ↦ ⦋(𝑟 freeLMod (Base‘𝑚)) / 𝑣⦌(𝑣 sSet ⟨(.r‘ndx), (𝑥 ∈ (Base‘𝑣), 𝑦 ∈ (Base‘𝑣) ↦ (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟))))))⟩))

Distinct variable group:   𝑚,𝑟,𝑣,𝑥,𝑦,𝑖,𝑎,𝑏

Detailed syntax breakdown of Definition df-mnring

Step	Hyp	Ref	Expression
1		cmnring 45168	. 2 class MndRing
2		vr	. . 3 setvar 𝑟
3		vm	. . 3 setvar 𝑚
4		cvv 3451	. . 3 class V
5		vv	. . . 4 setvar 𝑣
6	2	cv 1569	. . . . 5 class 𝑟
7	3	cv 1569	. . . . . 6 class 𝑚
8		cbs 17367	. . . . . 6 class Base
9	7, 8	cfv 6531	. . . . 5 class (Base‘𝑚)
10		cfrlm 22032	. . . . 5 class freeLMod
11	6, 9, 10	co 7412	. . . 4 class (𝑟 freeLMod (Base‘𝑚))
12	5	cv 1569	. . . . 5 class 𝑣
13		cnx 17351	. . . . . . 7 class ndx
14		cmulr 17409	. . . . . . 7 class .r
15	13, 14	cfv 6531	. . . . . 6 class (.r‘ndx)
16		vx	. . . . . . 7 setvar 𝑥
17		vy	. . . . . . 7 setvar 𝑦
18	12, 8	cfv 6531	. . . . . . 7 class (Base‘𝑣)
19		va	. . . . . . . . 9 setvar 𝑎
20		vb	. . . . . . . . 9 setvar 𝑏
21		vi	. . . . . . . . . 10 setvar 𝑖
22	21	cv 1569	. . . . . . . . . . . 12 class 𝑖
23	19	cv 1569	. . . . . . . . . . . . 13 class 𝑎
24	20	cv 1569	. . . . . . . . . . . . 13 class 𝑏
25		cplusg 17408	. . . . . . . . . . . . . 14 class +g
26	7, 25	cfv 6531	. . . . . . . . . . . . 13 class (+g‘𝑚)
27	23, 24, 26	co 7412	. . . . . . . . . . . 12 class (𝑎(+g‘𝑚)𝑏)
28	22, 27	wceq 1570	. . . . . . . . . . 11 wff 𝑖 = (𝑎(+g‘𝑚)𝑏)
29	16	cv 1569	. . . . . . . . . . . . 13 class 𝑥
30	23, 29	cfv 6531	. . . . . . . . . . . 12 class (𝑥‘𝑎)
31	17	cv 1569	. . . . . . . . . . . . 13 class 𝑦
32	24, 31	cfv 6531	. . . . . . . . . . . 12 class (𝑦‘𝑏)
33	6, 14	cfv 6531	. . . . . . . . . . . 12 class (.r‘𝑟)
34	30, 32, 33	co 7412	. . . . . . . . . . 11 class ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏))
35		c0g 17590	. . . . . . . . . . . 12 class 0g
36	6, 35	cfv 6531	. . . . . . . . . . 11 class (0g‘𝑟)
37	28, 34, 36	cif 4482	. . . . . . . . . 10 class if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟))
38	21, 9, 37	cmpt 5186	. . . . . . . . 9 class (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟)))
39	19, 20, 9, 9, 38	cmpo 7414	. . . . . . . 8 class (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟))))
40		cgsu 17591	. . . . . . . 8 class Σg
41	12, 39, 40	co 7412	. . . . . . 7 class (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟)))))
42	16, 17, 18, 18, 41	cmpo 7414	. . . . . 6 class (𝑥 ∈ (Base‘𝑣), 𝑦 ∈ (Base‘𝑣) ↦ (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟))))))
43	15, 42	cop 4590	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ (Base‘𝑣), 𝑦 ∈ (Base‘𝑣) ↦ (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟))))))⟩
44		csts 17321	. . . . 5 class sSet
45	12, 43, 44	co 7412	. . . 4 class (𝑣 sSet ⟨(.r‘ndx), (𝑥 ∈ (Base‘𝑣), 𝑦 ∈ (Base‘𝑣) ↦ (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟))))))⟩)
46	5, 11, 45	csb 3847	. . 3 class ⦋(𝑟 freeLMod (Base‘𝑚)) / 𝑣⦌(𝑣 sSet ⟨(.r‘ndx), (𝑥 ∈ (Base‘𝑣), 𝑦 ∈ (Base‘𝑣) ↦ (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟))))))⟩)
47	2, 3, 4, 4, 46	cmpo 7414	. 2 class (𝑟 ∈ V, 𝑚 ∈ V ↦ ⦋(𝑟 freeLMod (Base‘𝑚)) / 𝑣⦌(𝑣 sSet ⟨(.r‘ndx), (𝑥 ∈ (Base‘𝑣), 𝑦 ∈ (Base‘𝑣) ↦ (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟))))))⟩))
48	1, 47	wceq 1570	1 wff MndRing = (𝑟 ∈ V, 𝑚 ∈ V ↦ ⦋(𝑟 freeLMod (Base‘𝑚)) / 𝑣⦌(𝑣 sSet ⟨(.r‘ndx), (𝑥 ∈ (Base‘𝑣), 𝑦 ∈ (Base‘𝑣) ↦ (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟))))))⟩))

This definition is used by:  mnringvald  45170