Theorem mnringnmulrdOLD

Description: Obsolete version of mnringnmulrd as of 1-Nov-2024. Components of a monoid ring other than its ring product match its underlying free module. (Contributed by Rohan Ridenour, 14-May-2024) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	mnringnmulrdOLD.1	$$⊢F=R\mathrm{MndRing}M$$
	mnringnmulrdOLD.2	$$⊢E=\mathrm{Slot}N$$
	mnringnmulrdOLD.3	$$⊢N\in \mathbb{N}$$
	mnringnmulrdOLD.4	$$⊢N\ne {\cdot }_{\mathrm{ndx}}$$
	mnringnmulrdOLD.5	$$⊢A={\mathrm{Base}}_M$$
	mnringnmulrdOLD.6	$$⊢V=R\mathrm{freeLMod}A$$
	mnringnmulrdOLD.7	$$⊢\phi \to R\in U$$
	mnringnmulrdOLD.8	$$⊢\phi \to M\in W$$
Assertion	mnringnmulrdOLD	$$⊢\phi \to E\left(V\right)=E\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		mnringnmulrdOLD.1	$$⊢F=R\mathrm{MndRing}M$$
2		mnringnmulrdOLD.2	$$⊢E=\mathrm{Slot}N$$
3		mnringnmulrdOLD.3	$$⊢N\in \mathbb{N}$$
4		mnringnmulrdOLD.4	$$⊢N\ne {\cdot }_{\mathrm{ndx}}$$
5		mnringnmulrdOLD.5	$$⊢A={\mathrm{Base}}_M$$
6		mnringnmulrdOLD.6	$$⊢V=R\mathrm{freeLMod}A$$
7		mnringnmulrdOLD.7	$$⊢\phi \to R\in U$$
8		mnringnmulrdOLD.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)$$