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 
|- 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 ) ) ) ) ) ) >. ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmnring 
 |-  MndRing
1 vr 
 |-  r
2 cvv 
 |-  _V
3 vm 
 |-  m
4 1 cv 
 |-  r
5 cfrlm 
 |-  freeLMod
6 cbs 
 |-  Base
7 3 cv 
 |-  m
8 7 6 cfv 
 |-  ( Base ` m )
9 4 8 5 co 
 |-  ( r freeLMod ( Base ` m ) )
10 vv 
 |-  v
11 10 cv 
 |-  v
12 csts 
 |-  sSet
13 cmulr 
 |-  .r
14 cnx 
 |-  ndx
15 14 13 cfv 
 |-  ( .r ` ndx )
16 vx 
 |-  x
17 11 6 cfv 
 |-  ( Base ` v )
18 vy 
 |-  y
19 cgsu 
 |-  gsum
20 va 
 |-  a
21 vb 
 |-  b
22 vi 
 |-  i
23 22 cv 
 |-  i
24 20 cv 
 |-  a
25 cplusg 
 |-  +g
26 7 25 cfv 
 |-  ( +g ` m )
27 21 cv 
 |-  b
28 24 27 26 co 
 |-  ( a ( +g ` m ) b )
29 23 28 wceq 
 |-  i = ( a ( +g ` m ) b )
30 16 cv 
 |-  x
31 24 30 cfv 
 |-  ( x ` a )
32 4 13 cfv 
 |-  ( .r ` r )
33 18 cv 
 |-  y
34 27 33 cfv 
 |-  ( y ` b )
35 31 34 32 co 
 |-  ( ( x ` a ) ( .r ` r ) ( y ` b ) )
36 c0g 
 |-  0g
37 4 36 cfv 
 |-  ( 0g ` r )
38 29 35 37 cif 
 |-  if ( i = ( a ( +g ` m ) b ) , ( ( x ` a ) ( .r ` r ) ( y ` b ) ) , ( 0g ` r ) )
39 22 8 38 cmpt 
 |-  ( i e. ( Base ` m ) |-> if ( i = ( a ( +g ` m ) b ) , ( ( x ` a ) ( .r ` r ) ( y ` b ) ) , ( 0g ` r ) ) )
40 20 21 8 8 39 cmpo 
 |-  ( 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 ) ) ) )
41 11 40 19 co 
 |-  ( 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 ) ) ) ) )
42 16 18 17 17 41 cmpo 
 |-  ( 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 ) ) ) ) ) )
43 15 42 cop 
 |-  <. ( .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 ) ) ) ) ) ) >.
44 11 43 12 co 
 |-  ( 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 ) ) ) ) ) ) >. )
45 10 9 44 csb 
 |-  [_ ( 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 ) ) ) ) ) ) >. )
46 1 3 2 2 45 cmpo 
 |-  ( 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 ) ) ) ) ) ) >. ) )
47 0 46 wceq 
 |-  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 ) ) ) ) ) ) >. ) )