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	$$⊢\underset{\dot{}}{1}=1_R$$
	ringm1expp1.2	$$⊢N={inv}_g\left(R\right)$$
	ringm1expp1.3	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_R}$$
	ringm1expp1.4	$$⊢\phi \to R\in \mathrm{Ring}$$
	ringm1expp1.5	$$⊢\phi \to K\in {\mathbb{N}}_0$$
Assertion	ringm1expp1	$$⊢\phi \to \left(K+1\right)\underset{\dot{}}{\times }N\left(\underset{\dot{}}{1}\right)=N\left(K\underset{\dot{}}{\times }N\left(\underset{\dot{}}{1}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ringm1expp1.1	$$⊢\underset{\dot{}}{1}=1_R$$
2		ringm1expp1.2	$$⊢N={inv}_g\left(R\right)$$
3		ringm1expp1.3	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_R}$$
4		ringm1expp1.4	$$⊢\phi \to R\in \mathrm{Ring}$$
5		ringm1expp1.5	$$⊢\phi \to K\in {\mathbb{N}}_0$$
6		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
7	6	ringmgp	$$⊢R\in \mathrm{Ring}\to {\mathrm{mulGrp}}_R\in \mathrm{Mnd}$$
8	4 7	syl	$$⊢\phi \to {\mathrm{mulGrp}}_R\in \mathrm{Mnd}$$
9		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
10	4	ringgrpd	$$⊢\phi \to R\in \mathrm{Grp}$$
11	9 1 4	ringidcld	$$⊢\phi \to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
12	9 2 10 11	grpinvcld	$$⊢\phi \to N\left(\underset{\dot{}}{1}\right)\in {\mathrm{Base}}_R$$
13	6 9	mgpbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
14		eqid	$$⊢{\cdot }_R={\cdot }_R$$
15	6 14	mgpplusg	$$⊢{\cdot }_R={+}_{{\mathrm{mulGrp}}_R}$$
16	13 3 15	mulgnn0p1	$$⊢\left({\mathrm{mulGrp}}_R\in \mathrm{Mnd}\wedge K\in {\mathbb{N}}_0\wedge N\left(\underset{\dot{}}{1}\right)\in {\mathrm{Base}}_R\right)\to \left(K+1\right)\underset{\dot{}}{\times }N\left(\underset{\dot{}}{1}\right)=\left(K\underset{\dot{}}{\times }N\left(\underset{\dot{}}{1}\right)\right){\cdot }_{R}N\left(\underset{\dot{}}{1}\right)$$
17	8 5 12 16	syl3anc	$$⊢\phi \to \left(K+1\right)\underset{\dot{}}{\times }N\left(\underset{\dot{}}{1}\right)=\left(K\underset{\dot{}}{\times }N\left(\underset{\dot{}}{1}\right)\right){\cdot }_{R}N\left(\underset{\dot{}}{1}\right)$$
18	13 3 8 5 12	mulgnn0cld	$$⊢\phi \to K\underset{\dot{}}{\times }N\left(\underset{\dot{}}{1}\right)\in {\mathrm{Base}}_R$$
19	9 14 1 2 4 18	ringnegr	$$⊢\phi \to \left(K\underset{\dot{}}{\times }N\left(\underset{\dot{}}{1}\right)\right){\cdot }_{R}N\left(\underset{\dot{}}{1}\right)=N\left(K\underset{\dot{}}{\times }N\left(\underset{\dot{}}{1}\right)\right)$$
20	17 19	eqtrd	$$⊢\phi \to \left(K+1\right)\underset{\dot{}}{\times }N\left(\underset{\dot{}}{1}\right)=N\left(K\underset{\dot{}}{\times }N\left(\underset{\dot{}}{1}\right)\right)$$