Theorem mnringvald

Description: Value of the monoid ring function. (Contributed by Rohan Ridenour, 14-May-2024)

	Ref	Expression
Hypotheses	mnringvald.1	No typesetting found for |- F = ( R MndRing M ) with typecode |-
	mnringvald.2	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	mnringvald.3	$$⊢\underset{\dot{}}{0}=0_R$$
	mnringvald.4	$$⊢A={\mathrm{Base}}_M$$
	mnringvald.5	$$⊢\underset{\dot{}}{+}={+}_M$$
	mnringvald.6	$$⊢V=R\mathrm{freeLMod}A$$
	mnringvald.7	$$⊢B={\mathrm{Base}}_V$$
	mnringvald.8	$$⊢\phi \to R\in U$$
	mnringvald.9	$$⊢\phi \to M\in W$$
Assertion	mnringvald	$$⊢\phi \to F=V\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼{\sum }_V\left(a\in A,b\in A⟼\left(i\in A⟼if\left(i=a\underset{\dot{}}{+}b,x\left(a\right)\underset{\dot{}}{·}y\left(b\right),\underset{\dot{}}{0}\right)\right)\right)\right)⟩$$

Proof

Step	Hyp	Ref	Expression
1		mnringvald.1	Could not format F = ( R MndRing M ) : No typesetting found for |- F = ( R MndRing M ) with typecode |-
2		mnringvald.2	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		mnringvald.3	$$⊢\underset{\dot{}}{0}=0_R$$
4		mnringvald.4	$$⊢A={\mathrm{Base}}_M$$
5		mnringvald.5	$$⊢\underset{\dot{}}{+}={+}_M$$
6		mnringvald.6	$$⊢V=R\mathrm{freeLMod}A$$
7		mnringvald.7	$$⊢B={\mathrm{Base}}_V$$
8		mnringvald.8	$$⊢\phi \to R\in U$$
9		mnringvald.9	$$⊢\phi \to M\in W$$
10	8	elexd	$$⊢\phi \to R\in \mathrm{V}$$
11	9	elexd	$$⊢\phi \to M\in \mathrm{V}$$
12		nfv	$$⊢Ⅎv\left(r=R\wedge m=M\right)$$
13		nfcvd	$$⊢\left(r=R\wedge m=M\right)\to \underset{\_}{Ⅎ}v\left(V\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼{\sum }_V\left(a\in A,b\in A⟼\left(i\in A⟼if\left(i=a\underset{\dot{}}{+}b,x\left(a\right)\underset{\dot{}}{·}y\left(b\right),\underset{\dot{}}{0}\right)\right)\right)\right)⟩\right)$$
14		ovexd	$$⊢\left(r=R\wedge m=M\right)\to r\mathrm{freeLMod}{\mathrm{Base}}_m\in \mathrm{V}$$
15		simpr	$$⊢\left(\left(r=R\wedge m=M\right)\wedge v=r\mathrm{freeLMod}{\mathrm{Base}}_m\right)\to v=r\mathrm{freeLMod}{\mathrm{Base}}_m$$
16		simpll	$$⊢\left(\left(r=R\wedge m=M\right)\wedge v=r\mathrm{freeLMod}{\mathrm{Base}}_m\right)\to r=R$$
17		fveq2	$$⊢m=M\to {\mathrm{Base}}_m={\mathrm{Base}}_M$$
18	17 4	eqtr4di	$$⊢m=M\to {\mathrm{Base}}_m=A$$
19	18	ad2antlr	$$⊢\left(\left(r=R\wedge m=M\right)\wedge v=r\mathrm{freeLMod}{\mathrm{Base}}_m\right)\to {\mathrm{Base}}_m=A$$
20	16 19	oveq12d	$$⊢\left(\left(r=R\wedge m=M\right)\wedge v=r\mathrm{freeLMod}{\mathrm{Base}}_m\right)\to r\mathrm{freeLMod}{\mathrm{Base}}_m=R\mathrm{freeLMod}A$$
21	15 20	eqtrd	$$⊢\left(\left(r=R\wedge m=M\right)\wedge v=r\mathrm{freeLMod}{\mathrm{Base}}_m\right)\to v=R\mathrm{freeLMod}A$$
22	21 6	eqtr4di	$$⊢\left(\left(r=R\wedge m=M\right)\wedge v=r\mathrm{freeLMod}{\mathrm{Base}}_m\right)\to v=V$$
23	22	fveq2d	$$⊢\left(\left(r=R\wedge m=M\right)\wedge v=r\mathrm{freeLMod}{\mathrm{Base}}_m\right)\to {\mathrm{Base}}_v={\mathrm{Base}}_V$$
24	23 7	eqtr4di	$$⊢\left(\left(r=R\wedge m=M\right)\wedge v=r\mathrm{freeLMod}{\mathrm{Base}}_m\right)\to {\mathrm{Base}}_v=B$$
25		fveq2	$$⊢m=M\to {+}_m={+}_M$$
26	25 5	eqtr4di	$$⊢m=M\to {+}_m=\underset{\dot{}}{+}$$
27	26	oveqd	$$⊢m=M\to a{+}_{m}b=a\underset{\dot{}}{+}b$$
28	27	ad2antlr	$$⊢\left(\left(r=R\wedge m=M\right)\wedge v=r\mathrm{freeLMod}{\mathrm{Base}}_m\right)\to a{+}_{m}b=a\underset{\dot{}}{+}b$$
29	28	eqeq2d	$$⊢\left(\left(r=R\wedge m=M\right)\wedge v=r\mathrm{freeLMod}{\mathrm{Base}}_m\right)\to \left(i=a{+}_{m}b\leftrightarrow i=a\underset{\dot{}}{+}b\right)$$
30		fveq2	$$⊢r=R\to {\cdot }_r={\cdot }_R$$
31	30 2	eqtr4di	$$⊢r=R\to {\cdot }_r=\underset{\dot{}}{·}$$
32	31	oveqd	$$⊢r=R\to x\left(a\right){\cdot }_{r}y\left(b\right)=x\left(a\right)\underset{\dot{}}{·}y\left(b\right)$$
33	32	ad2antrr	$$⊢\left(\left(r=R\wedge m=M\right)\wedge v=r\mathrm{freeLMod}{\mathrm{Base}}_m\right)\to x\left(a\right){\cdot }_{r}y\left(b\right)=x\left(a\right)\underset{\dot{}}{·}y\left(b\right)$$
34		fveq2	$$⊢r=R\to 0_r=0_R$$
35	34 3	eqtr4di	$$⊢r=R\to 0_r=\underset{\dot{}}{0}$$
36	35	ad2antrr	$$⊢\left(\left(r=R\wedge m=M\right)\wedge v=r\mathrm{freeLMod}{\mathrm{Base}}_m\right)\to 0_r=\underset{\dot{}}{0}$$
37	29 33 36	ifbieq12d	$$⊢\left(\left(r=R\wedge m=M\right)\wedge v=r\mathrm{freeLMod}{\mathrm{Base}}_m\right)\to if\left(i=a{+}_{m}b,x\left(a\right){\cdot }_{r}y\left(b\right),0_r\right)=if\left(i=a\underset{\dot{}}{+}b,x\left(a\right)\underset{\dot{}}{·}y\left(b\right),\underset{\dot{}}{0}\right)$$
38	19 37	mpteq12dv	$$⊢\left(\left(r=R\wedge m=M\right)\wedge v=r\mathrm{freeLMod}{\mathrm{Base}}_m\right)\to \left(i\in {\mathrm{Base}}_m⟼if\left(i=a{+}_{m}b,x\left(a\right){\cdot }_{r}y\left(b\right),0_r\right)\right)=\left(i\in A⟼if\left(i=a\underset{\dot{}}{+}b,x\left(a\right)\underset{\dot{}}{·}y\left(b\right),\underset{\dot{}}{0}\right)\right)$$
39	19 19 38	mpoeq123dv	$$⊢\left(\left(r=R\wedge m=M\right)\wedge v=r\mathrm{freeLMod}{\mathrm{Base}}_m\right)\to \left(a\in {\mathrm{Base}}_m,b\in {\mathrm{Base}}_m⟼\left(i\in {\mathrm{Base}}_m⟼if\left(i=a{+}_{m}b,x\left(a\right){\cdot }_{r}y\left(b\right),0_r\right)\right)\right)=\left(a\in A,b\in A⟼\left(i\in A⟼if\left(i=a\underset{\dot{}}{+}b,x\left(a\right)\underset{\dot{}}{·}y\left(b\right),\underset{\dot{}}{0}\right)\right)\right)$$
40	22 39	oveq12d	$$⊢\left(\left(r=R\wedge m=M\right)\wedge v=r\mathrm{freeLMod}{\mathrm{Base}}_m\right)\to {\sum }_v\left(a\in {\mathrm{Base}}_m,b\in {\mathrm{Base}}_m⟼\left(i\in {\mathrm{Base}}_m⟼if\left(i=a{+}_{m}b,x\left(a\right){\cdot }_{r}y\left(b\right),0_r\right)\right)\right)={\sum }_V\left(a\in A,b\in A⟼\left(i\in A⟼if\left(i=a\underset{\dot{}}{+}b,x\left(a\right)\underset{\dot{}}{·}y\left(b\right),\underset{\dot{}}{0}\right)\right)\right)$$
41	24 24 40	mpoeq123dv	$$⊢\left(\left(r=R\wedge m=M\right)\wedge v=r\mathrm{freeLMod}{\mathrm{Base}}_m\right)\to \left(x\in {\mathrm{Base}}_v,y\in {\mathrm{Base}}_v⟼{\sum }_v\left(a\in {\mathrm{Base}}_m,b\in {\mathrm{Base}}_m⟼\left(i\in {\mathrm{Base}}_m⟼if\left(i=a{+}_{m}b,x\left(a\right){\cdot }_{r}y\left(b\right),0_r\right)\right)\right)\right)=\left(x\in B,y\in B⟼{\sum }_V\left(a\in A,b\in A⟼\left(i\in A⟼if\left(i=a\underset{\dot{}}{+}b,x\left(a\right)\underset{\dot{}}{·}y\left(b\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
42	41	opeq2d	$$⊢\left(\left(r=R\wedge m=M\right)\wedge v=r\mathrm{freeLMod}{\mathrm{Base}}_m\right)\to ⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_v,y\in {\mathrm{Base}}_v⟼{\sum }_v\left(a\in {\mathrm{Base}}_m,b\in {\mathrm{Base}}_m⟼\left(i\in {\mathrm{Base}}_m⟼if\left(i=a{+}_{m}b,x\left(a\right){\cdot }_{r}y\left(b\right),0_r\right)\right)\right)\right)⟩=⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼{\sum }_V\left(a\in A,b\in A⟼\left(i\in A⟼if\left(i=a\underset{\dot{}}{+}b,x\left(a\right)\underset{\dot{}}{·}y\left(b\right),\underset{\dot{}}{0}\right)\right)\right)\right)⟩$$
43	22 42	oveq12d	$$⊢\left(\left(r=R\wedge m=M\right)\wedge v=r\mathrm{freeLMod}{\mathrm{Base}}_m\right)\to v\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_v,y\in {\mathrm{Base}}_v⟼{\sum }_v\left(a\in {\mathrm{Base}}_m,b\in {\mathrm{Base}}_m⟼\left(i\in {\mathrm{Base}}_m⟼if\left(i=a{+}_{m}b,x\left(a\right){\cdot }_{r}y\left(b\right),0_r\right)\right)\right)\right)⟩=V\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼{\sum }_V\left(a\in A,b\in A⟼\left(i\in A⟼if\left(i=a\underset{\dot{}}{+}b,x\left(a\right)\underset{\dot{}}{·}y\left(b\right),\underset{\dot{}}{0}\right)\right)\right)\right)⟩$$
44	12 13 14 43	csbiedf	$$⊢\left(r=R\wedge m=M\right)\to ⦋\left(r\mathrm{freeLMod}{\mathrm{Base}}_m\right)/v⦌\left(v\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_v,y\in {\mathrm{Base}}_v⟼{\sum }_v\left(a\in {\mathrm{Base}}_m,b\in {\mathrm{Base}}_m⟼\left(i\in {\mathrm{Base}}_m⟼if\left(i=a{+}_{m}b,x\left(a\right){\cdot }_{r}y\left(b\right),0_r\right)\right)\right)\right)⟩\right)=V\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼{\sum }_V\left(a\in A,b\in A⟼\left(i\in A⟼if\left(i=a\underset{\dot{}}{+}b,x\left(a\right)\underset{\dot{}}{·}y\left(b\right),\underset{\dot{}}{0}\right)\right)\right)\right)⟩$$
45		df-mnring	Could not format 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 ) ) ) ) ) ) >. ) ) : No typesetting found for |- 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 ) ) ) ) ) ) >. ) ) with typecode |-
46		ovex	$$⊢V\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼{\sum }_V\left(a\in A,b\in A⟼\left(i\in A⟼if\left(i=a\underset{\dot{}}{+}b,x\left(a\right)\underset{\dot{}}{·}y\left(b\right),\underset{\dot{}}{0}\right)\right)\right)\right)⟩\in \mathrm{V}$$
47	44 45 46	ovmpoa	Could not format ( ( R e. _V /\ M e. _V ) -> ( R MndRing M ) = ( V sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> ( V gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) ) >. ) ) : No typesetting found for |- ( ( R e. _V /\ M e. _V ) -> ( R MndRing M ) = ( V sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> ( V gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) ) >. ) ) with typecode |-
48	10 11 47	syl2anc	Could not format ( ph -> ( R MndRing M ) = ( V sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> ( V gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) ) >. ) ) : No typesetting found for |- ( ph -> ( R MndRing M ) = ( V sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> ( V gsum ( a e. A , b e. A |-> ( i e. A |-> if ( i = ( a .+ b ) , ( ( x ` a ) .x. ( y ` b ) ) , .0. ) ) ) ) ) >. ) ) with typecode |-
49	1 48	syl5eq	$$⊢\phi \to F=V\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼{\sum }_V\left(a\in A,b\in A⟼\left(i\in A⟼if\left(i=a\underset{\dot{}}{+}b,x\left(a\right)\underset{\dot{}}{·}y\left(b\right),\underset{\dot{}}{0}\right)\right)\right)\right)⟩$$