Users' Mathboxes 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 42579
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 42578 . 2 class MndRing
2 vr . . 3 setvar π‘Ÿ
3 vm . . 3 setvar π‘š
4 cvv 3447 . . 3 class V
5 vv . . . 4 setvar 𝑣
62cv 1541 . . . . 5 class π‘Ÿ
73cv 1541 . . . . . 6 class π‘š
8 cbs 17091 . . . . . 6 class Base
97, 8cfv 6500 . . . . 5 class (Baseβ€˜π‘š)
10 cfrlm 21175 . . . . 5 class freeLMod
116, 9, 10co 7361 . . . 4 class (π‘Ÿ freeLMod (Baseβ€˜π‘š))
125cv 1541 . . . . 5 class 𝑣
13 cnx 17073 . . . . . . 7 class ndx
14 cmulr 17142 . . . . . . 7 class .r
1513, 14cfv 6500 . . . . . 6 class (.rβ€˜ndx)
16 vx . . . . . . 7 setvar π‘₯
17 vy . . . . . . 7 setvar 𝑦
1812, 8cfv 6500 . . . . . . 7 class (Baseβ€˜π‘£)
19 va . . . . . . . . 9 setvar π‘Ž
20 vb . . . . . . . . 9 setvar 𝑏
21 vi . . . . . . . . . 10 setvar 𝑖
2221cv 1541 . . . . . . . . . . . 12 class 𝑖
2319cv 1541 . . . . . . . . . . . . 13 class π‘Ž
2420cv 1541 . . . . . . . . . . . . 13 class 𝑏
25 cplusg 17141 . . . . . . . . . . . . . 14 class +g
267, 25cfv 6500 . . . . . . . . . . . . 13 class (+gβ€˜π‘š)
2723, 24, 26co 7361 . . . . . . . . . . . 12 class (π‘Ž(+gβ€˜π‘š)𝑏)
2822, 27wceq 1542 . . . . . . . . . . 11 wff 𝑖 = (π‘Ž(+gβ€˜π‘š)𝑏)
2916cv 1541 . . . . . . . . . . . . 13 class π‘₯
3023, 29cfv 6500 . . . . . . . . . . . 12 class (π‘₯β€˜π‘Ž)
3117cv 1541 . . . . . . . . . . . . 13 class 𝑦
3224, 31cfv 6500 . . . . . . . . . . . 12 class (π‘¦β€˜π‘)
336, 14cfv 6500 . . . . . . . . . . . 12 class (.rβ€˜π‘Ÿ)
3430, 32, 33co 7361 . . . . . . . . . . 11 class ((π‘₯β€˜π‘Ž)(.rβ€˜π‘Ÿ)(π‘¦β€˜π‘))
35 c0g 17329 . . . . . . . . . . . 12 class 0g
366, 35cfv 6500 . . . . . . . . . . 11 class (0gβ€˜π‘Ÿ)
3728, 34, 36cif 4490 . . . . . . . . . 10 class if(𝑖 = (π‘Ž(+gβ€˜π‘š)𝑏), ((π‘₯β€˜π‘Ž)(.rβ€˜π‘Ÿ)(π‘¦β€˜π‘)), (0gβ€˜π‘Ÿ))
3821, 9, 37cmpt 5192 . . . . . . . . 9 class (𝑖 ∈ (Baseβ€˜π‘š) ↦ if(𝑖 = (π‘Ž(+gβ€˜π‘š)𝑏), ((π‘₯β€˜π‘Ž)(.rβ€˜π‘Ÿ)(π‘¦β€˜π‘)), (0gβ€˜π‘Ÿ)))
3919, 20, 9, 9, 38cmpo 7363 . . . . . . . 8 class (π‘Ž ∈ (Baseβ€˜π‘š), 𝑏 ∈ (Baseβ€˜π‘š) ↦ (𝑖 ∈ (Baseβ€˜π‘š) ↦ if(𝑖 = (π‘Ž(+gβ€˜π‘š)𝑏), ((π‘₯β€˜π‘Ž)(.rβ€˜π‘Ÿ)(π‘¦β€˜π‘)), (0gβ€˜π‘Ÿ))))
40 cgsu 17330 . . . . . . . 8 class Ξ£g
4112, 39, 40co 7361 . . . . . . 7 class (𝑣 Ξ£g (π‘Ž ∈ (Baseβ€˜π‘š), 𝑏 ∈ (Baseβ€˜π‘š) ↦ (𝑖 ∈ (Baseβ€˜π‘š) ↦ if(𝑖 = (π‘Ž(+gβ€˜π‘š)𝑏), ((π‘₯β€˜π‘Ž)(.rβ€˜π‘Ÿ)(π‘¦β€˜π‘)), (0gβ€˜π‘Ÿ)))))
4216, 17, 18, 18, 41cmpo 7363 . . . . . 6 class (π‘₯ ∈ (Baseβ€˜π‘£), 𝑦 ∈ (Baseβ€˜π‘£) ↦ (𝑣 Ξ£g (π‘Ž ∈ (Baseβ€˜π‘š), 𝑏 ∈ (Baseβ€˜π‘š) ↦ (𝑖 ∈ (Baseβ€˜π‘š) ↦ if(𝑖 = (π‘Ž(+gβ€˜π‘š)𝑏), ((π‘₯β€˜π‘Ž)(.rβ€˜π‘Ÿ)(π‘¦β€˜π‘)), (0gβ€˜π‘Ÿ))))))
4315, 42cop 4596 . . . . 5 class ⟨(.rβ€˜ndx), (π‘₯ ∈ (Baseβ€˜π‘£), 𝑦 ∈ (Baseβ€˜π‘£) ↦ (𝑣 Ξ£g (π‘Ž ∈ (Baseβ€˜π‘š), 𝑏 ∈ (Baseβ€˜π‘š) ↦ (𝑖 ∈ (Baseβ€˜π‘š) ↦ if(𝑖 = (π‘Ž(+gβ€˜π‘š)𝑏), ((π‘₯β€˜π‘Ž)(.rβ€˜π‘Ÿ)(π‘¦β€˜π‘)), (0gβ€˜π‘Ÿ))))))⟩
44 csts 17043 . . . . 5 class sSet
4512, 43, 44co 7361 . . . 4 class (𝑣 sSet ⟨(.rβ€˜ndx), (π‘₯ ∈ (Baseβ€˜π‘£), 𝑦 ∈ (Baseβ€˜π‘£) ↦ (𝑣 Ξ£g (π‘Ž ∈ (Baseβ€˜π‘š), 𝑏 ∈ (Baseβ€˜π‘š) ↦ (𝑖 ∈ (Baseβ€˜π‘š) ↦ if(𝑖 = (π‘Ž(+gβ€˜π‘š)𝑏), ((π‘₯β€˜π‘Ž)(.rβ€˜π‘Ÿ)(π‘¦β€˜π‘)), (0gβ€˜π‘Ÿ))))))⟩)
465, 11, 45csb 3859 . . 3 class ⦋(π‘Ÿ freeLMod (Baseβ€˜π‘š)) / π‘£β¦Œ(𝑣 sSet ⟨(.rβ€˜ndx), (π‘₯ ∈ (Baseβ€˜π‘£), 𝑦 ∈ (Baseβ€˜π‘£) ↦ (𝑣 Ξ£g (π‘Ž ∈ (Baseβ€˜π‘š), 𝑏 ∈ (Baseβ€˜π‘š) ↦ (𝑖 ∈ (Baseβ€˜π‘š) ↦ if(𝑖 = (π‘Ž(+gβ€˜π‘š)𝑏), ((π‘₯β€˜π‘Ž)(.rβ€˜π‘Ÿ)(π‘¦β€˜π‘)), (0gβ€˜π‘Ÿ))))))⟩)
472, 3, 4, 4, 46cmpo 7363 . 2 class (π‘Ÿ ∈ V, π‘š ∈ V ↦ ⦋(π‘Ÿ freeLMod (Baseβ€˜π‘š)) / π‘£β¦Œ(𝑣 sSet ⟨(.rβ€˜ndx), (π‘₯ ∈ (Baseβ€˜π‘£), 𝑦 ∈ (Baseβ€˜π‘£) ↦ (𝑣 Ξ£g (π‘Ž ∈ (Baseβ€˜π‘š), 𝑏 ∈ (Baseβ€˜π‘š) ↦ (𝑖 ∈ (Baseβ€˜π‘š) ↦ if(𝑖 = (π‘Ž(+gβ€˜π‘š)𝑏), ((π‘₯β€˜π‘Ž)(.rβ€˜π‘Ÿ)(π‘¦β€˜π‘)), (0gβ€˜π‘Ÿ))))))⟩))
481, 47wceq 1542 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  42580
  Copyright terms: Public domain W3C validator