Mathbox for Rohan Ridenour < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mnring Structured version   Visualization version   GIF version

Definition df-mnring 40844
 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
StepHypRef Expression
1 cmnring 40843 . 2 class MndRing
2 vr . . 3 setvar 𝑟
3 vm . . 3 setvar 𝑚
4 cvv 3480 . . 3 class V
5 vv . . . 4 setvar 𝑣
62cv 1537 . . . . 5 class 𝑟
73cv 1537 . . . . . 6 class 𝑚
8 cbs 16483 . . . . . 6 class Base
97, 8cfv 6343 . . . . 5 class (Base‘𝑚)
10 cfrlm 20492 . . . . 5 class freeLMod
116, 9, 10co 7149 . . . 4 class (𝑟 freeLMod (Base‘𝑚))
125cv 1537 . . . . 5 class 𝑣
13 cnx 16480 . . . . . . 7 class ndx
14 cmulr 16566 . . . . . . 7 class .r
1513, 14cfv 6343 . . . . . 6 class (.r‘ndx)
16 vx . . . . . . 7 setvar 𝑥
17 vy . . . . . . 7 setvar 𝑦
1812, 8cfv 6343 . . . . . . 7 class (Base‘𝑣)
19 va . . . . . . . . 9 setvar 𝑎
20 vb . . . . . . . . 9 setvar 𝑏
21 vi . . . . . . . . . 10 setvar 𝑖
2221cv 1537 . . . . . . . . . . . 12 class 𝑖
2319cv 1537 . . . . . . . . . . . . 13 class 𝑎
2420cv 1537 . . . . . . . . . . . . 13 class 𝑏
25 cplusg 16565 . . . . . . . . . . . . . 14 class +g
267, 25cfv 6343 . . . . . . . . . . . . 13 class (+g𝑚)
2723, 24, 26co 7149 . . . . . . . . . . . 12 class (𝑎(+g𝑚)𝑏)
2822, 27wceq 1538 . . . . . . . . . . 11 wff 𝑖 = (𝑎(+g𝑚)𝑏)
2916cv 1537 . . . . . . . . . . . . 13 class 𝑥
3023, 29cfv 6343 . . . . . . . . . . . 12 class (𝑥𝑎)
3117cv 1537 . . . . . . . . . . . . 13 class 𝑦
3224, 31cfv 6343 . . . . . . . . . . . 12 class (𝑦𝑏)
336, 14cfv 6343 . . . . . . . . . . . 12 class (.r𝑟)
3430, 32, 33co 7149 . . . . . . . . . . 11 class ((𝑥𝑎)(.r𝑟)(𝑦𝑏))
35 c0g 16713 . . . . . . . . . . . 12 class 0g
366, 35cfv 6343 . . . . . . . . . . 11 class (0g𝑟)
3728, 34, 36cif 4450 . . . . . . . . . 10 class if(𝑖 = (𝑎(+g𝑚)𝑏), ((𝑥𝑎)(.r𝑟)(𝑦𝑏)), (0g𝑟))
3821, 9, 37cmpt 5132 . . . . . . . . 9 class (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g𝑚)𝑏), ((𝑥𝑎)(.r𝑟)(𝑦𝑏)), (0g𝑟)))
3919, 20, 9, 9, 38cmpo 7151 . . . . . . . 8 class (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g𝑚)𝑏), ((𝑥𝑎)(.r𝑟)(𝑦𝑏)), (0g𝑟))))
40 cgsu 16714 . . . . . . . 8 class Σg
4112, 39, 40co 7149 . . . . . . 7 class (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g𝑚)𝑏), ((𝑥𝑎)(.r𝑟)(𝑦𝑏)), (0g𝑟)))))
4216, 17, 18, 18, 41cmpo 7151 . . . . . 6 class (𝑥 ∈ (Base‘𝑣), 𝑦 ∈ (Base‘𝑣) ↦ (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g𝑚)𝑏), ((𝑥𝑎)(.r𝑟)(𝑦𝑏)), (0g𝑟))))))
4315, 42cop 4556 . . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ (Base‘𝑣), 𝑦 ∈ (Base‘𝑣) ↦ (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g𝑚)𝑏), ((𝑥𝑎)(.r𝑟)(𝑦𝑏)), (0g𝑟))))))⟩
44 csts 16481 . . . . 5 class sSet
4512, 43, 44co 7149 . . . 4 class (𝑣 sSet ⟨(.r‘ndx), (𝑥 ∈ (Base‘𝑣), 𝑦 ∈ (Base‘𝑣) ↦ (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g𝑚)𝑏), ((𝑥𝑎)(.r𝑟)(𝑦𝑏)), (0g𝑟))))))⟩)
465, 11, 45csb 3866 . . 3 class (𝑟 freeLMod (Base‘𝑚)) / 𝑣(𝑣 sSet ⟨(.r‘ndx), (𝑥 ∈ (Base‘𝑣), 𝑦 ∈ (Base‘𝑣) ↦ (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g𝑚)𝑏), ((𝑥𝑎)(.r𝑟)(𝑦𝑏)), (0g𝑟))))))⟩)
472, 3, 4, 4, 46cmpo 7151 . 2 class (𝑟 ∈ V, 𝑚 ∈ V ↦ (𝑟 freeLMod (Base‘𝑚)) / 𝑣(𝑣 sSet ⟨(.r‘ndx), (𝑥 ∈ (Base‘𝑣), 𝑦 ∈ (Base‘𝑣) ↦ (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g𝑚)𝑏), ((𝑥𝑎)(.r𝑟)(𝑦𝑏)), (0g𝑟))))))⟩))
481, 47wceq 1538 1 wff MndRing = (𝑟 ∈ V, 𝑚 ∈ V ↦ (𝑟 freeLMod (Base‘𝑚)) / 𝑣(𝑣 sSet ⟨(.r‘ndx), (𝑥 ∈ (Base‘𝑣), 𝑦 ∈ (Base‘𝑣) ↦ (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g𝑚)𝑏), ((𝑥𝑎)(.r𝑟)(𝑦𝑏)), (0g𝑟))))))⟩))
 Colors of variables: wff setvar class This definition is referenced by:  mnringvald  40845
 Copyright terms: Public domain W3C validator