Theorem primrootsunit

Description: Primitive roots have left inverses. (Contributed by metakunt, 25-Apr-2025)

	Ref	Expression
Hypotheses	primrootsunit.1	$$⊢\phi \to R\in \mathrm{CMnd}$$
	primrootsunit.2	$$⊢\phi \to K\in \mathbb{N}$$
	primrootsunit.3	$$⊢U=\left\{a\in {\mathrm{Base}}_R|\exists i\in {\mathrm{Base}}_{R}i{+}_{R}a=0_R\right\}$$
Assertion	primrootsunit	$$⊢\phi \to \left(R\mathrm{PrimRoots}K=\left(R{\upharpoonright }_{𝑠}U\right)\mathrm{PrimRoots}K\wedge R{\upharpoonright }_{𝑠}U\in \mathrm{Abel}\right)$$

Proof

Step	Hyp	Ref	Expression
1		primrootsunit.1	$$⊢\phi \to R\in \mathrm{CMnd}$$
2		primrootsunit.2	$$⊢\phi \to K\in \mathbb{N}$$
3		primrootsunit.3	$$⊢U=\left\{a\in {\mathrm{Base}}_R|\exists i\in {\mathrm{Base}}_{R}i{+}_{R}a=0_R\right\}$$
4		nfv	$$⊢Ⅎji{+}_{R}a=0_R$$
5		nfv	$$⊢Ⅎij{+}_{R}a=0_R$$
6		oveq1	$$⊢i=j\to i{+}_{R}a=j{+}_{R}a$$
7	6	eqeq1d	$$⊢i=j\to \left(i{+}_{R}a=0_R\leftrightarrow j{+}_{R}a=0_R\right)$$
8	4 5 7	cbvrexw	$$⊢\exists i\in {\mathrm{Base}}_{R}i{+}_{R}a=0_R\leftrightarrow \exists j\in {\mathrm{Base}}_{R}j{+}_{R}a=0_R$$
9	8	rabbii	$$⊢\left\{a\in {\mathrm{Base}}_R|\exists i\in {\mathrm{Base}}_{R}i{+}_{R}a=0_R\right\}=\left\{a\in {\mathrm{Base}}_R|\exists j\in {\mathrm{Base}}_{R}j{+}_{R}a=0_R\right\}$$
10	3 9	eqtri	$$⊢U=\left\{a\in {\mathrm{Base}}_R|\exists j\in {\mathrm{Base}}_{R}j{+}_{R}a=0_R\right\}$$
11	1 2 10	primrootsunit1	$$⊢\phi \to \left(R\mathrm{PrimRoots}K=\left(R{\upharpoonright }_{𝑠}U\right)\mathrm{PrimRoots}K\wedge R{\upharpoonright }_{𝑠}U\in \mathrm{Abel}\right)$$