This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )