Theorem mnring0g2d

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

	Ref	Expression
Hypotheses	mnring0g2d.1	|- F = ( R MndRing M )
	mnring0g2d.2	|- .0. = ( 0g ` R )
	mnring0g2d.3	|- A = ( Base ` M )
	mnring0g2d.4	|- ( ph -> R e. Ring )
	mnring0g2d.5	|- ( ph -> M e. W )
Assertion	mnring0g2d	|- ( ph -> ( A X. { .0. } ) = ( 0g ` F ) )

Proof

Step	Hyp	Ref	Expression
1		mnring0g2d.1	|- F = ( R MndRing M )
2		mnring0g2d.2	|- .0. = ( 0g ` R )
3		mnring0g2d.3	|- A = ( Base ` M )
4		mnring0g2d.4	|- ( ph -> R e. Ring )
5		mnring0g2d.5	|- ( ph -> M e. W )
6	3	fvexi	|- A e. _V
7		eqid	|- ( R freeLMod A ) = ( R freeLMod A )
8	7 2	frlm0	|- ( ( R e. Ring /\ A e. _V ) -> ( A X. { .0. } ) = ( 0g ` ( R freeLMod A ) ) )
9	4 6 8	sylancl	|- ( ph -> ( A X. { .0. } ) = ( 0g ` ( R freeLMod A ) ) )
10	1 3 7 4 5	mnring0gd	|- ( ph -> ( 0g ` ( R freeLMod A ) ) = ( 0g ` F ) )
11	9 10	eqtrd	|- ( ph -> ( A X. { .0. } ) = ( 0g ` F ) )