Theorem srg1expzeq1

Description: The exponentiation (by a nonnegative integer) of the multiplicative identity of a semiring, analogous to mulgnn0z . (Contributed by AV, 25-Nov-2019)

	Ref	Expression
Hypotheses	srg1expzeq1.g	|- G = ( mulGrp ` R )
	srg1expzeq1.t	|- .x. = ( .g ` G )
	srg1expzeq1.1	|- .1. = ( 1r ` R )
Assertion	srg1expzeq1	|- ( ( R e. SRing /\ N e. NN0 ) -> ( N .x. .1. ) = .1. )

Proof

Step	Hyp	Ref	Expression
1		srg1expzeq1.g	|- G = ( mulGrp ` R )
2		srg1expzeq1.t	|- .x. = ( .g ` G )
3		srg1expzeq1.1	|- .1. = ( 1r ` R )
4	1	srgmgp	|- ( R e. SRing -> G e. Mnd )
5		eqid	|- ( Base ` G ) = ( Base ` G )
6	1 3	ringidval	|- .1. = ( 0g ` G )
7	5 2 6	mulgnn0z	|- ( ( G e. Mnd /\ N e. NN0 ) -> ( N .x. .1. ) = .1. )
8	4 7	sylan	|- ( ( R e. SRing /\ N e. NN0 ) -> ( N .x. .1. ) = .1. )