Theorem mnringvald

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

	Ref	Expression
Hypotheses	mnringvald.1	$$⊢F=R\mathrm{MndRing}M$$
	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	$$⊢F=R\mathrm{MndRing}M$$
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	$$⊢\mathrm{MndRing}=\left(r\in \mathrm{V},m\in \mathrm{V}⟼⦋\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)\right)$$
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	$$⊢\left(R\in \mathrm{V}\wedge M\in \mathrm{V}\right)\to R\mathrm{MndRing}M=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)⟩$$
48	10 11 47	syl2anc	$$⊢\phi \to R\mathrm{MndRing}M=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)⟩$$
49	1 48	eqtrid	$$⊢\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)⟩$$