Theorem primrootsunit

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

	Ref	Expression
Hypotheses	primrootsunit.1	|- ( ph -> R e. CMnd )
	primrootsunit.2	|- ( ph -> K e. NN )
	primrootsunit.3	|- U = { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) }
Assertion	primrootsunit	|- ( ph -> ( ( R PrimRoots K ) = ( ( R |`s U ) PrimRoots K ) /\ ( R |`s U ) e. Abel ) )

Proof

Step	Hyp	Ref	Expression
1		primrootsunit.1	|- ( ph -> R e. CMnd )
2		primrootsunit.2	|- ( ph -> K e. NN )
3		primrootsunit.3	|- U = { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) }
4		nfv	|- F/ j ( i ( +g ` R ) a ) = ( 0g ` R )
5		nfv	|- F/ i ( j ( +g ` R ) a ) = ( 0g ` R )
6		oveq1	|- ( i = j -> ( i ( +g ` R ) a ) = ( j ( +g ` R ) a ) )
7	6	eqeq1d	|- ( i = j -> ( ( i ( +g ` R ) a ) = ( 0g ` R ) <-> ( j ( +g ` R ) a ) = ( 0g ` R ) ) )
8	4 5 7	cbvrexw	|- ( E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) <-> E. j e. ( Base ` R ) ( j ( +g ` R ) a ) = ( 0g ` R ) )
9	8	rabbii	|- { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } = { a e. ( Base ` R ) | E. j e. ( Base ` R ) ( j ( +g ` R ) a ) = ( 0g ` R ) }
10	3 9	eqtri	|- U = { a e. ( Base ` R ) | E. j e. ( Base ` R ) ( j ( +g ` R ) a ) = ( 0g ` R ) }
11	1 2 10	primrootsunit1	|- ( ph -> ( ( R PrimRoots K ) = ( ( R |`s U ) PrimRoots K ) /\ ( R |`s U ) e. Abel ) )