Theorem mnringmulrvald

Description: Value of multiplication in a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024)

	Ref	Expression
Hypotheses	mnringmulrvald.1	No typesetting found for |- F = ( R MndRing M ) with typecode |-
	mnringmulrvald.2	$$⊢B={\mathrm{Base}}_F$$
	mnringmulrvald.3	$$⊢\underset{\dot{}}{\bullet }={\cdot }_R$$
	mnringmulrvald.4	$$⊢\underset{\dot{}}{𝟎}=0_R$$
	mnringmulrvald.5	$$⊢A={\mathrm{Base}}_M$$
	mnringmulrvald.6	$$⊢\underset{\dot{}}{+}={+}_M$$
	mnringmulrvald.7	$$⊢\underset{\dot{}}{·}={\cdot }_F$$
	mnringmulrvald.8	$$⊢\phi \to R\in U$$
	mnringmulrvald.9	$$⊢\phi \to M\in W$$
	mnringmulrvald.10	$$⊢\phi \to X\in B$$
	mnringmulrvald.11	$$⊢\phi \to Y\in B$$
Assertion	mnringmulrvald	$$⊢\phi \to X\underset{\dot{}}{·}Y={\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{}}{\bullet }Y\left(b\right),\underset{\dot{}}{𝟎}\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mnringmulrvald.1	Could not format F = ( R MndRing M ) : No typesetting found for |- F = ( R MndRing M ) with typecode |-
2		mnringmulrvald.2	$$⊢B={\mathrm{Base}}_F$$
3		mnringmulrvald.3	$$⊢\underset{\dot{}}{\bullet }={\cdot }_R$$
4		mnringmulrvald.4	$$⊢\underset{\dot{}}{𝟎}=0_R$$
5		mnringmulrvald.5	$$⊢A={\mathrm{Base}}_M$$
6		mnringmulrvald.6	$$⊢\underset{\dot{}}{+}={+}_M$$
7		mnringmulrvald.7	$$⊢\underset{\dot{}}{·}={\cdot }_F$$
8		mnringmulrvald.8	$$⊢\phi \to R\in U$$
9		mnringmulrvald.9	$$⊢\phi \to M\in W$$
10		mnringmulrvald.10	$$⊢\phi \to X\in B$$
11		mnringmulrvald.11	$$⊢\phi \to Y\in B$$
12	1 2 3 4 5 6 8 9	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{}}{\bullet }y\left(b\right),\underset{\dot{}}{𝟎}\right)\right)\right)\right)={\cdot }_F$$
13	12 7	eqtr4di	$$⊢\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{}}{\bullet }y\left(b\right),\underset{\dot{}}{𝟎}\right)\right)\right)\right)=\underset{\dot{}}{·}$$
14	13	eqcomd	$$⊢\phi \to \underset{\dot{}}{·}=\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{}}{\bullet }y\left(b\right),\underset{\dot{}}{𝟎}\right)\right)\right)\right)$$
15		fveq1	$$⊢x=X\to x\left(a\right)=X\left(a\right)$$
16		fveq1	$$⊢y=Y\to y\left(b\right)=Y\left(b\right)$$
17	15 16	oveqan12d	$$⊢\left(x=X\wedge y=Y\right)\to x\left(a\right)\underset{\dot{}}{\bullet }y\left(b\right)=X\left(a\right)\underset{\dot{}}{\bullet }Y\left(b\right)$$
18	17	ifeq1d	$$⊢\left(x=X\wedge y=Y\right)\to if\left(i=a\underset{\dot{}}{+}b,x\left(a\right)\underset{\dot{}}{\bullet }y\left(b\right),\underset{\dot{}}{𝟎}\right)=if\left(i=a\underset{\dot{}}{+}b,X\left(a\right)\underset{\dot{}}{\bullet }Y\left(b\right),\underset{\dot{}}{𝟎}\right)$$
19	18	mpteq2dv	$$⊢\left(x=X\wedge y=Y\right)\to \left(i\in A⟼if\left(i=a\underset{\dot{}}{+}b,x\left(a\right)\underset{\dot{}}{\bullet }y\left(b\right),\underset{\dot{}}{𝟎}\right)\right)=\left(i\in A⟼if\left(i=a\underset{\dot{}}{+}b,X\left(a\right)\underset{\dot{}}{\bullet }Y\left(b\right),\underset{\dot{}}{𝟎}\right)\right)$$
20	19	mpoeq3dv	$$⊢\left(x=X\wedge y=Y\right)\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{}}{\bullet }y\left(b\right),\underset{\dot{}}{𝟎}\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{}}{\bullet }Y\left(b\right),\underset{\dot{}}{𝟎}\right)\right)\right)$$
21	20	oveq2d	$$⊢\left(x=X\wedge y=Y\right)\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{}}{\bullet }y\left(b\right),\underset{\dot{}}{𝟎}\right)\right)\right)={\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{}}{\bullet }Y\left(b\right),\underset{\dot{}}{𝟎}\right)\right)\right)$$
22	21	adantl	$$⊢\left(\phi \wedge \left(x=X\wedge y=Y\right)\right)\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{}}{\bullet }y\left(b\right),\underset{\dot{}}{𝟎}\right)\right)\right)={\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{}}{\bullet }Y\left(b\right),\underset{\dot{}}{𝟎}\right)\right)\right)$$
23		ovexd	$$⊢\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{}}{\bullet }Y\left(b\right),\underset{\dot{}}{𝟎}\right)\right)\right)\in \mathrm{V}$$
24	14 22 10 11 23	ovmpod	$$⊢\phi \to X\underset{\dot{}}{·}Y={\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{}}{\bullet }Y\left(b\right),\underset{\dot{}}{𝟎}\right)\right)\right)$$