Theorem primrootscoprf

Description: Coprime powers of primitive roots are primitive roots, as a function. (Contributed by metakunt, 26-Apr-2025)

	Ref	Expression
Hypotheses	primrootscoprf.1	|- F = ( m e. ( R PrimRoots K ) |-> ( E ( .g ` R ) m ) )
	primrootscoprf.2	|- ( ph -> R e. CMnd )
	primrootscoprf.3	|- ( ph -> K e. NN )
	primrootscoprf.4	|- ( ph -> E e. NN )
	primrootscoprf.5	|- ( ph -> ( E gcd K ) = 1 )
Assertion	primrootscoprf	|- ( ph -> F : ( R PrimRoots K ) --> ( R PrimRoots K ) )

Proof

Step	Hyp	Ref	Expression
1		primrootscoprf.1	|- F = ( m e. ( R PrimRoots K ) |-> ( E ( .g ` R ) m ) )
2		primrootscoprf.2	|- ( ph -> R e. CMnd )
3		primrootscoprf.3	|- ( ph -> K e. NN )
4		primrootscoprf.4	|- ( ph -> E e. NN )
5		primrootscoprf.5	|- ( ph -> ( E gcd K ) = 1 )
6	2	adantr	|- ( ( ph /\ m e. ( R PrimRoots K ) ) -> R e. CMnd )
7	3	adantr	|- ( ( ph /\ m e. ( R PrimRoots K ) ) -> K e. NN )
8	4	adantr	|- ( ( ph /\ m e. ( R PrimRoots K ) ) -> E e. NN )
9	5	adantr	|- ( ( ph /\ m e. ( R PrimRoots K ) ) -> ( E gcd K ) = 1 )
10		simpr	|- ( ( ph /\ m e. ( R PrimRoots K ) ) -> m e. ( R PrimRoots K ) )
11		eqid	|- { y e. ( Base ` R ) | E. x e. ( Base ` R ) ( x ( +g ` R ) y ) = ( 0g ` R ) } = { y e. ( Base ` R ) | E. x e. ( Base ` R ) ( x ( +g ` R ) y ) = ( 0g ` R ) }
12	6 7 8 9 10 11	primrootscoprmpow	|- ( ( ph /\ m e. ( R PrimRoots K ) ) -> ( E ( .g ` R ) m ) e. ( R PrimRoots K ) )
13	12 1	fmptd	|- ( ph -> F : ( R PrimRoots K ) --> ( R PrimRoots K ) )