Theorem mnringaddgd

Description: The additive operation of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024) (Proof shortened by AV, 1-Nov-2024)

	Ref	Expression
Hypotheses	mnringaddgd.1	No typesetting found for |- F = ( R MndRing M ) with typecode |-
	mnringaddgd.2	$$⊢A={\mathrm{Base}}_M$$
	mnringaddgd.3	$$⊢V=R\mathrm{freeLMod}A$$
	mnringaddgd.4	$$⊢\phi \to R\in U$$
	mnringaddgd.5	$$⊢\phi \to M\in W$$
Assertion	mnringaddgd	$$⊢\phi \to {+}_V={+}_F$$

Proof

Step	Hyp	Ref	Expression
1		mnringaddgd.1	Could not format F = ( R MndRing M ) : No typesetting found for |- F = ( R MndRing M ) with typecode |-
2		mnringaddgd.2	$$⊢A={\mathrm{Base}}_M$$
3		mnringaddgd.3	$$⊢V=R\mathrm{freeLMod}A$$
4		mnringaddgd.4	$$⊢\phi \to R\in U$$
5		mnringaddgd.5	$$⊢\phi \to M\in W$$
6		plusgid	$$⊢{+}_{𝑔}=\mathrm{Slot}{+}_{\mathrm{ndx}}$$
7		plusgndxnmulrndx	$$⊢{+}_{\mathrm{ndx}}\ne {\cdot }_{\mathrm{ndx}}$$
8	1 6 7 2 3 4 5	mnringnmulrd	$$⊢\phi \to {+}_V={+}_F$$