Theorem mnringnmulrd

Description: Components of a monoid ring other than its ring product match its underlying free module. (Contributed by Rohan Ridenour, 14-May-2024) (Revised by AV, 1-Nov-2024)

	Ref	Expression
Hypotheses	mnringnmulrd.1	No typesetting found for |- F = ( R MndRing M ) with typecode |-
	mnringnmulrd.2	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
	mnringnmulrd.4	$$⊢E\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
	mnringnmulrd.5	$$⊢A={\mathrm{Base}}_M$$
	mnringnmulrd.6	$$⊢V=R\mathrm{freeLMod}A$$
	mnringnmulrd.7	$$⊢\phi \to R\in U$$
	mnringnmulrd.8	$$⊢\phi \to M\in W$$
Assertion	mnringnmulrd	$$⊢\phi \to E\left(V\right)=E\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		mnringnmulrd.1	Could not format F = ( R MndRing M ) : No typesetting found for |- F = ( R MndRing M ) with typecode |-
2		mnringnmulrd.2	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
3		mnringnmulrd.4	$$⊢E\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
4		mnringnmulrd.5	$$⊢A={\mathrm{Base}}_M$$
5		mnringnmulrd.6	$$⊢V=R\mathrm{freeLMod}A$$
6		mnringnmulrd.7	$$⊢\phi \to R\in U$$
7		mnringnmulrd.8	$$⊢\phi \to M\in W$$
8	2 3	setsnid	$$⊢E\left(V\right)=E\left(V\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_V,y\in {\mathrm{Base}}_V⟼{\sum }_V\left(a\in A,b\in A⟼\left(i\in A⟼if\left(i=a{+}_{M}b,x\left(a\right){\cdot }_{R}y\left(b\right),0_R\right)\right)\right)\right)⟩\right)$$
9		eqid	$$⊢{\cdot }_R={\cdot }_R$$
10		eqid	$$⊢0_R=0_R$$
11		eqid	$$⊢{+}_M={+}_M$$
12		eqid	$$⊢{\mathrm{Base}}_V={\mathrm{Base}}_V$$
13	1 9 10 4 11 5 12 6 7	mnringvald	$$⊢\phi \to F=V\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_V,y\in {\mathrm{Base}}_V⟼{\sum }_V\left(a\in A,b\in A⟼\left(i\in A⟼if\left(i=a{+}_{M}b,x\left(a\right){\cdot }_{R}y\left(b\right),0_R\right)\right)\right)\right)⟩$$
14	13	fveq2d	$$⊢\phi \to E\left(F\right)=E\left(V\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_V,y\in {\mathrm{Base}}_V⟼{\sum }_V\left(a\in A,b\in A⟼\left(i\in A⟼if\left(i=a{+}_{M}b,x\left(a\right){\cdot }_{R}y\left(b\right),0_R\right)\right)\right)\right)⟩\right)$$
15	8 14	eqtr4id	$$⊢\phi \to E\left(V\right)=E\left(F\right)$$