ringm1expp1

Description: Ring exponentiation of minus one: Adding one to the exponent is the same as taking the additive inverse. (Contributed by Thierry Arnoux, 15-Feb-2026)

	Ref	Expression
Hypotheses	ringm1expp1.1	$⊢ \underset{˙}{1} = 1_{R}$
	ringm1expp1.2	$⊢ N = {inv}_{g} (R)$
	ringm1expp1.3	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{R}}$
	ringm1expp1.4	$⊢ φ \to R \in Ring$
	ringm1expp1.5	$⊢ φ \to K \in ℕ_{0}$
Assertion	ringm1expp1	$⊢ φ \to (K + 1) \underset{˙}{\times} N (\underset{˙}{1}) = N (K \underset{˙}{\times} N (\underset{˙}{1}))$

Proof

Step	Hyp	Ref	Expression
1		ringm1expp1.1	$⊢ \underset{˙}{1} = 1_{R}$
2		ringm1expp1.2	$⊢ N = {inv}_{g} (R)$
3		ringm1expp1.3	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{R}}$
4		ringm1expp1.4	$⊢ φ \to R \in Ring$
5		ringm1expp1.5	$⊢ φ \to K \in ℕ_{0}$
6		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
7	6	ringmgp	$⊢ R \in Ring \to {mulGrp}_{R} \in Mnd$
8	4 7	syl	$⊢ φ \to {mulGrp}_{R} \in Mnd$
9		eqid	$⊢ {Base}_{R} = {Base}_{R}$
10	4	ringgrpd	$⊢ φ \to R \in Grp$
11	9 1 4	ringidcld	$⊢ φ \to \underset{˙}{1} \in {Base}_{R}$
12	9 2 10 11	grpinvcld	$⊢ φ \to N (\underset{˙}{1}) \in {Base}_{R}$
13	6 9	mgpbas	$⊢ {Base}_{R} = {Base}_{{mulGrp}_{R}}$
14		eqid	$⊢ \cdot_{R} = \cdot_{R}$
15	6 14	mgpplusg	$⊢ \cdot_{R} = +_{{mulGrp}_{R}}$
16	13 3 15	mulgnn0p1	$⊢ ({mulGrp}_{R} \in Mnd \land K \in ℕ_{0} \land N (\underset{˙}{1}) \in {Base}_{R}) \to (K + 1) \underset{˙}{\times} N (\underset{˙}{1}) = (K \underset{˙}{\times} N (\underset{˙}{1})) \cdot_{R} N (\underset{˙}{1})$
17	8 5 12 16	syl3anc	$⊢ φ \to (K + 1) \underset{˙}{\times} N (\underset{˙}{1}) = (K \underset{˙}{\times} N (\underset{˙}{1})) \cdot_{R} N (\underset{˙}{1})$
18	13 3 8 5 12	mulgnn0cld	$⊢ φ \to K \underset{˙}{\times} N (\underset{˙}{1}) \in {Base}_{R}$
19	9 14 1 2 4 18	ringnegr	$⊢ φ \to (K \underset{˙}{\times} N (\underset{˙}{1})) \cdot_{R} N (\underset{˙}{1}) = N (K \underset{˙}{\times} N (\underset{˙}{1}))$
20	17 19	eqtrd	$⊢ φ \to (K + 1) \underset{˙}{\times} N (\underset{˙}{1}) = N (K \underset{˙}{\times} N (\underset{˙}{1}))$

Metamath Proof Explorer

Theorem ringm1expp1

Proof