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={\mathrm{mulGrp}}_R$$
	srg1expzeq1.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	srg1expzeq1.1	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	srg1expzeq1	$$⊢\left(R\in \mathrm{SRing}\wedge N\in {\mathbb{N}}_0\right)\to N\underset{\dot{}}{·}\underset{\dot{}}{1}=\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		srg1expzeq1.g	$$⊢G={\mathrm{mulGrp}}_R$$
2		srg1expzeq1.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
3		srg1expzeq1.1	$$⊢\underset{\dot{}}{1}=1_R$$
4	1	srgmgp	$$⊢R\in \mathrm{SRing}\to G\in \mathrm{Mnd}$$
5		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
6	1 3	ringidval	$$⊢\underset{\dot{}}{1}=0_G$$
7	5 2 6	mulgnn0z	$$⊢\left(G\in \mathrm{Mnd}\wedge N\in {\mathbb{N}}_0\right)\to N\underset{\dot{}}{·}\underset{\dot{}}{1}=\underset{\dot{}}{1}$$
8	4 7	sylan	$$⊢\left(R\in \mathrm{SRing}\wedge N\in {\mathbb{N}}_0\right)\to N\underset{\dot{}}{·}\underset{\dot{}}{1}=\underset{\dot{}}{1}$$