Theorem mnring0gd

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

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

Proof

Step	Hyp	Ref	Expression
1		mnring0gd.1	|- F = ( R MndRing M )
2		mnring0gd.2	|- A = ( Base ` M )
3		mnring0gd.3	|- V = ( R freeLMod A )
4		mnring0gd.4	|- ( ph -> R e. U )
5		mnring0gd.5	|- ( ph -> M e. W )
6		eqidd	|- ( ph -> ( Base ` V ) = ( Base ` V ) )
7		eqid	|- ( Base ` V ) = ( Base ` V )
8	1 2 3 7 4 5	mnringbased	|- ( ph -> ( Base ` V ) = ( Base ` F ) )
9	1 2 3 4 5	mnringaddgd	|- ( ph -> ( +g ` V ) = ( +g ` F ) )
10	9	oveqdr	|- ( ( ph /\ ( x e. ( Base ` V ) /\ y e. ( Base ` V ) ) ) -> ( x ( +g ` V ) y ) = ( x ( +g ` F ) y ) )
11	6 8 10	grpidpropd	|- ( ph -> ( 0g ` V ) = ( 0g ` F ) )