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)

	Ref	Expression
Hypotheses	mnringnmulrd.1	No typesetting found for |- F = ( R MndRing M ) with typecode |-
	mnringnmulrd.2	$$⊢E=\mathrm{Slot}N$$
	mnringnmulrd.3	$$⊢N\in \mathbb{N}$$
	mnringnmulrd.4	$$⊢N\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}N$$
3		mnringnmulrd.3	$$⊢N\in \mathbb{N}$$
4		mnringnmulrd.4	$$⊢N\ne {\cdot }_{\mathrm{ndx}}$$
5		mnringnmulrd.5	$$⊢A={\mathrm{Base}}_M$$
6		mnringnmulrd.6	$$⊢V=R\mathrm{freeLMod}A$$
7		mnringnmulrd.7	$$⊢\phi \to R\in U$$
8		mnringnmulrd.8	$$⊢\phi \to M\in W$$
9	2 3	ndxid	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
10	2 3	ndxarg	$$⊢E\left(\mathrm{ndx}\right)=N$$
11	10 4	eqnetri	$$⊢E\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
12	9 11	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)$$
13		eqid	$$⊢{\cdot }_R={\cdot }_R$$
14		eqid	$$⊢0_R=0_R$$
15		eqid	$$⊢{+}_M={+}_M$$
16		eqid	$$⊢{\mathrm{Base}}_V={\mathrm{Base}}_V$$
17	1 13 14 5 15 6 16 7 8	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)⟩$$
18	17	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)$$
19	12 18	eqtr4id	$$⊢\phi \to E\left(V\right)=E\left(F\right)$$