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

Metamath Proof Explorer

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 ) ) ) )