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	⊢ 𝐹 = ( 𝑚 ∈ ( 𝑅 PrimRoots 𝐾 ) ↦ ( 𝐸 ( .g ‘ 𝑅 ) 𝑚 ) )
	primrootscoprf.2	⊢ ( 𝜑 → 𝑅 ∈ CMnd )
	primrootscoprf.3	⊢ ( 𝜑 → 𝐾 ∈ ℕ )
	primrootscoprf.4	⊢ ( 𝜑 → 𝐸 ∈ ℕ )
	primrootscoprf.5	⊢ ( 𝜑 → ( 𝐸 gcd 𝐾 ) = 1 )
Assertion	primrootscoprf	⊢ ( 𝜑 → 𝐹 : ( 𝑅 PrimRoots 𝐾 ) ⟶ ( 𝑅 PrimRoots 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		primrootscoprf.1	⊢ 𝐹 = ( 𝑚 ∈ ( 𝑅 PrimRoots 𝐾 ) ↦ ( 𝐸 ( .g ‘ 𝑅 ) 𝑚 ) )
2		primrootscoprf.2	⊢ ( 𝜑 → 𝑅 ∈ CMnd )
3		primrootscoprf.3	⊢ ( 𝜑 → 𝐾 ∈ ℕ )
4		primrootscoprf.4	⊢ ( 𝜑 → 𝐸 ∈ ℕ )
5		primrootscoprf.5	⊢ ( 𝜑 → ( 𝐸 gcd 𝐾 ) = 1 )
6	2	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → 𝑅 ∈ CMnd )
7	3	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → 𝐾 ∈ ℕ )
8	4	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → 𝐸 ∈ ℕ )
9	5	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → ( 𝐸 gcd 𝐾 ) = 1 )
10		simpr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → 𝑚 ∈ ( 𝑅 PrimRoots 𝐾 ) )
11		eqid	⊢ { 𝑦 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑥 ∈ ( Base ‘ 𝑅 ) ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = ( 0g ‘ 𝑅 ) } = { 𝑦 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑥 ∈ ( Base ‘ 𝑅 ) ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = ( 0g ‘ 𝑅 ) }
12	6 7 8 9 10 11	primrootscoprmpow	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → ( 𝐸 ( .g ‘ 𝑅 ) 𝑚 ) ∈ ( 𝑅 PrimRoots 𝐾 ) )
13	12 1	fmptd	⊢ ( 𝜑 → 𝐹 : ( 𝑅 PrimRoots 𝐾 ) ⟶ ( 𝑅 PrimRoots 𝐾 ) )