Theorem 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	⊢ 1 = ( 1r ‘ 𝑅 )
	ringm1expp1.2	⊢ 𝑁 = ( invg ‘ 𝑅 )
	ringm1expp1.3	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
	ringm1expp1.4	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	ringm1expp1.5	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
Assertion	ringm1expp1	⊢ ( 𝜑 → ( ( 𝐾 + 1 ) ↑ ( 𝑁 ‘ 1 ) ) = ( 𝑁 ‘ ( 𝐾 ↑ ( 𝑁 ‘ 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ringm1expp1.1	⊢ 1 = ( 1r ‘ 𝑅 )
2		ringm1expp1.2	⊢ 𝑁 = ( invg ‘ 𝑅 )
3		ringm1expp1.3	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
4		ringm1expp1.4	⊢ ( 𝜑 → 𝑅 ∈ Ring )
5		ringm1expp1.5	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
6		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
7	6	ringmgp	⊢ ( 𝑅 ∈ Ring → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
8	4 7	syl	⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
9		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10	4	ringgrpd	⊢ ( 𝜑 → 𝑅 ∈ Grp )
11	9 1 4	ringidcld	⊢ ( 𝜑 → 1 ∈ ( Base ‘ 𝑅 ) )
12	9 2 10 11	grpinvcld	⊢ ( 𝜑 → ( 𝑁 ‘ 1 ) ∈ ( Base ‘ 𝑅 ) )
13	6 9	mgpbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
14		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
15	6 14	mgpplusg	⊢ ( .r ‘ 𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
16	13 3 15	mulgnn0p1	⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ 𝐾 ∈ ℕ0 ∧ ( 𝑁 ‘ 1 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐾 + 1 ) ↑ ( 𝑁 ‘ 1 ) ) = ( ( 𝐾 ↑ ( 𝑁 ‘ 1 ) ) ( .r ‘ 𝑅 ) ( 𝑁 ‘ 1 ) ) )
17	8 5 12 16	syl3anc	⊢ ( 𝜑 → ( ( 𝐾 + 1 ) ↑ ( 𝑁 ‘ 1 ) ) = ( ( 𝐾 ↑ ( 𝑁 ‘ 1 ) ) ( .r ‘ 𝑅 ) ( 𝑁 ‘ 1 ) ) )
18	13 3 8 5 12	mulgnn0cld	⊢ ( 𝜑 → ( 𝐾 ↑ ( 𝑁 ‘ 1 ) ) ∈ ( Base ‘ 𝑅 ) )
19	9 14 1 2 4 18	ringnegr	⊢ ( 𝜑 → ( ( 𝐾 ↑ ( 𝑁 ‘ 1 ) ) ( .r ‘ 𝑅 ) ( 𝑁 ‘ 1 ) ) = ( 𝑁 ‘ ( 𝐾 ↑ ( 𝑁 ‘ 1 ) ) ) )
20	17 19	eqtrd	⊢ ( 𝜑 → ( ( 𝐾 + 1 ) ↑ ( 𝑁 ‘ 1 ) ) = ( 𝑁 ‘ ( 𝐾 ↑ ( 𝑁 ‘ 1 ) ) ) )