Theorem mnringmulrd

Description: The ring product of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024)

	Ref	Expression
Hypotheses	mnringmulrd.1	$$⊢F=R\mathrm{MndRing}M$$
	mnringmulrd.2	$$⊢B={\mathrm{Base}}_F$$
	mnringmulrd.3	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	mnringmulrd.4	$$⊢\underset{\dot{}}{0}=0_R$$
	mnringmulrd.5	$$⊢A={\mathrm{Base}}_M$$
	mnringmulrd.6	$$⊢\underset{\dot{}}{+}={+}_M$$
	mnringmulrd.7	$$⊢\phi \to R\in U$$
	mnringmulrd.8	$$⊢\phi \to M\in W$$
Assertion	mnringmulrd	$$⊢\phi \to \left(x\in B,y\in B⟼{\sum }_F\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)={\cdot }_F$$

Proof

Step	Hyp	Ref	Expression
1		mnringmulrd.1	$$⊢F=R\mathrm{MndRing}M$$
2		mnringmulrd.2	$$⊢B={\mathrm{Base}}_F$$
3		mnringmulrd.3	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		mnringmulrd.4	$$⊢\underset{\dot{}}{0}=0_R$$
5		mnringmulrd.5	$$⊢A={\mathrm{Base}}_M$$
6		mnringmulrd.6	$$⊢\underset{\dot{}}{+}={+}_M$$
7		mnringmulrd.7	$$⊢\phi \to R\in U$$
8		mnringmulrd.8	$$⊢\phi \to M\in W$$
9		eqid	$$⊢R\mathrm{freeLMod}A=R\mathrm{freeLMod}A$$
10	1 2 5 9 7 8	mnringbaserd	$$⊢\phi \to B={\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)}$$
11	5	fvexi	$$⊢A\in \mathrm{V}$$
12	11 11	mpoex	$$⊢\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)\in \mathrm{V}$$
13	12	a1i	$$⊢\phi \to \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)\in \mathrm{V}$$
14	1	ovexi	$$⊢F\in \mathrm{V}$$
15	14	a1i	$$⊢\phi \to F\in \mathrm{V}$$
16		ovex	$$⊢R\mathrm{freeLMod}A\in \mathrm{V}$$
17	16	a1i	$$⊢\phi \to R\mathrm{freeLMod}A\in \mathrm{V}$$
18	2 10	eqtr3id	$$⊢\phi \to {\mathrm{Base}}_F={\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)}$$
19	1 5 9 7 8	mnringaddgd	$$⊢\phi \to {+}_{\left(R\mathrm{freeLMod}A\right)}={+}_F$$
20	19	eqcomd	$$⊢\phi \to {+}_F={+}_{\left(R\mathrm{freeLMod}A\right)}$$
21	13 15 17 18 20	gsumpropd	$$⊢\phi \to {\sum }_F\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)={\sum }_{R\mathrm{freeLMod}A}\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)$$
22	10 10 21	mpoeq123dv	$$⊢\phi \to \left(x\in B,y\in B⟼{\sum }_F\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)=\left(x\in {\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)},y\in {\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)}⟼{\sum }_{R\mathrm{freeLMod}A}\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)$$
23		fvex	$$⊢{\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)}\in \mathrm{V}$$
24	23 23	mpoex	$$⊢\left(x\in {\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)},y\in {\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)}⟼{\sum }_{R\mathrm{freeLMod}A}\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}$$
25		mulridx	$$⊢{\cdot }_{𝑟}=\mathrm{Slot}{\cdot }_{\mathrm{ndx}}$$
26	25	setsid	$$⊢\left(R\mathrm{freeLMod}A\in \mathrm{V}\wedge \left(x\in {\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)},y\in {\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)}⟼{\sum }_{R\mathrm{freeLMod}A}\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}\right)\to \left(x\in {\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)},y\in {\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)}⟼{\sum }_{R\mathrm{freeLMod}A}\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)={\cdot }_{\left(\left(R\mathrm{freeLMod}A\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)},y\in {\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)}⟼{\sum }_{R\mathrm{freeLMod}A}\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)}$$
27	16 24 26	mp2an	$$⊢\left(x\in {\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)},y\in {\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)}⟼{\sum }_{R\mathrm{freeLMod}A}\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)={\cdot }_{\left(\left(R\mathrm{freeLMod}A\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)},y\in {\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)}⟼{\sum }_{R\mathrm{freeLMod}A}\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)}$$
28		eqid	$$⊢{\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)}={\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)}$$
29	1 3 4 5 6 9 28 7 8	mnringvald	$$⊢\phi \to F=\left(R\mathrm{freeLMod}A\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)},y\in {\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)}⟼{\sum }_{R\mathrm{freeLMod}A}\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)⟩$$
30	29	fveq2d	$$⊢\phi \to {\cdot }_F={\cdot }_{\left(\left(R\mathrm{freeLMod}A\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)},y\in {\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)}⟼{\sum }_{R\mathrm{freeLMod}A}\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)}$$
31	27 30	eqtr4id	$$⊢\phi \to \left(x\in {\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)},y\in {\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)}⟼{\sum }_{R\mathrm{freeLMod}A}\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)={\cdot }_F$$
32	22 31	eqtrd	$$⊢\phi \to \left(x\in B,y\in B⟼{\sum }_F\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)={\cdot }_F$$