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	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
	srg1expzeq1.t	⊢ · = ( .g ‘ 𝐺 )
	srg1expzeq1.1	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	srg1expzeq1	⊢ ( ( 𝑅 ∈ SRing ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 · 1 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		srg1expzeq1.g	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
2		srg1expzeq1.t	⊢ · = ( .g ‘ 𝐺 )
3		srg1expzeq1.1	⊢ 1 = ( 1r ‘ 𝑅 )
4	1	srgmgp	⊢ ( 𝑅 ∈ SRing → 𝐺 ∈ Mnd )
5		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
6	1 3	ringidval	⊢ 1 = ( 0g ‘ 𝐺 )
7	5 2 6	mulgnn0z	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 · 1 ) = 1 )
8	4 7	sylan	⊢ ( ( 𝑅 ∈ SRing ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 · 1 ) = 1 )