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	$⊢ G = {mulGrp}_{R}$
		srg1expzeq1.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
		srg1expzeq1.1	$⊢ \underset{˙}{1} = 1_{R}$
	Assertion	srg1expzeq1	$⊢ (R \in SRing \land N \in ℕ_{0}) \to N \underset{˙}{\cdot} \underset{˙}{1} = \underset{˙}{1}$

Proof

Step	Hyp	Ref	Expression
1		srg1expzeq1.g	$⊢ G = {mulGrp}_{R}$
2		srg1expzeq1.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		srg1expzeq1.1	$⊢ \underset{˙}{1} = 1_{R}$
4	1	srgmgp	$⊢ R \in SRing \to G \in Mnd$
5		eqid	$⊢ {Base}_{G} = {Base}_{G}$
6	1 3	ringidval	$⊢ \underset{˙}{1} = 0_{G}$
7	5 2 6	mulgnn0z	$⊢ (G \in Mnd \land N \in ℕ_{0}) \to N \underset{˙}{\cdot} \underset{˙}{1} = \underset{˙}{1}$
8	4 7	sylan	$⊢ (R \in SRing \land N \in ℕ_{0}) \to N \underset{˙}{\cdot} \underset{˙}{1} = \underset{˙}{1}$