Theorem mnringaddgd

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

	Ref	Expression
Hypotheses	mnringaddgd.1	|- F = ( R MndRing M )
	mnringaddgd.2	|- A = ( Base ` M )
	mnringaddgd.3	|- V = ( R freeLMod A )
	mnringaddgd.4	|- ( ph -> R e. U )
	mnringaddgd.5	|- ( ph -> M e. W )
Assertion	mnringaddgd	|- ( ph -> ( +g ` V ) = ( +g ` F ) )

Proof

Step	Hyp	Ref	Expression
1		mnringaddgd.1	|- F = ( R MndRing M )
2		mnringaddgd.2	|- A = ( Base ` M )
3		mnringaddgd.3	|- V = ( R freeLMod A )
4		mnringaddgd.4	|- ( ph -> R e. U )
5		mnringaddgd.5	|- ( ph -> M e. W )
6		df-plusg	|- +g = Slot 2
7		2nn	|- 2 e. NN
8		2re	|- 2 e. RR
9		2lt3	|- 2 < 3
10	8 9	ltneii	|- 2 =/= 3
11		mulrndx	|- ( .r ` ndx ) = 3
12	10 11	neeqtrri	|- 2 =/= ( .r ` ndx )
13	1 6 7 12 2 3 4 5	mnringnmulrd	|- ( ph -> ( +g ` V ) = ( +g ` F ) )