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	⊢ MndRing = ( 𝑟 ∈ V , 𝑚 ∈ V ↦ ⦋ ( 𝑟 freeLMod ( Base ‘ 𝑚 ) ) / 𝑣 ⦌ ( 𝑣 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑣 ) , 𝑦 ∈ ( Base ‘ 𝑣 ) ↦ ( 𝑣 Σg ( 𝑎 ∈ ( Base ‘ 𝑚 ) , 𝑏 ∈ ( Base ‘ 𝑚 ) ↦ ( 𝑖 ∈ ( Base ‘ 𝑚 ) ↦ if ( 𝑖 = ( 𝑎 ( +g ‘ 𝑚 ) 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) ( .r ‘ 𝑟 ) ( 𝑦 ‘ 𝑏 ) ) , ( 0g ‘ 𝑟 ) ) ) ) ) ) ⟩ ) )

Detailed syntax breakdown

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