Theorem mnringaddgd

Description: The additive operation of a monoid ring. (Contributed by Rohan Ridenour, 14-May-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		df-plusg	$$⊢{+}_{𝑔}=\mathrm{Slot}2$$
7		2nn	$$⊢2\in \mathbb{N}$$
8		2re	$$⊢2\in ℝ$$
9		2lt3	$$⊢2<3$$
10	8 9	ltneii	$$⊢2\ne 3$$
11		mulrndx	$$⊢{\cdot }_{\mathrm{ndx}}=3$$
12	10 11	neeqtrri	$$⊢2\ne {\cdot }_{\mathrm{ndx}}$$
13	1 6 7 12 2 3 4 5	mnringnmulrd	$$⊢\phi \to {+}_V={+}_F$$