Theorem primrootscoprbij2

Description: A bijection between coprime powers of primitive roots and primitive roots. (Contributed by metakunt, 26-Apr-2025)

	Ref	Expression
Hypotheses	primrootscoprbij2.1	⊢ 𝐹 = ( 𝑚 ∈ ( 𝑅 PrimRoots 𝐾 ) ↦ ( 𝐼 ( .g ‘ 𝑅 ) 𝑚 ) )
	primrootscoprbij2.2	⊢ ( 𝜑 → 𝑅 ∈ CMnd )
	primrootscoprbij2.3	⊢ ( 𝜑 → 𝐾 ∈ ℕ )
	primrootscoprbij2.4	⊢ ( 𝜑 → 𝐼 ∈ ℕ )
	primrootscoprbij2.5	⊢ ( 𝜑 → ( 𝐼 gcd 𝐾 ) = 1 )
Assertion	primrootscoprbij2	⊢ ( 𝜑 → 𝐹 : ( 𝑅 PrimRoots 𝐾 ) –1-1-onto→ ( 𝑅 PrimRoots 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		primrootscoprbij2.1	⊢ 𝐹 = ( 𝑚 ∈ ( 𝑅 PrimRoots 𝐾 ) ↦ ( 𝐼 ( .g ‘ 𝑅 ) 𝑚 ) )
2		primrootscoprbij2.2	⊢ ( 𝜑 → 𝑅 ∈ CMnd )
3		primrootscoprbij2.3	⊢ ( 𝜑 → 𝐾 ∈ ℕ )
4		primrootscoprbij2.4	⊢ ( 𝜑 → 𝐼 ∈ ℕ )
5		primrootscoprbij2.5	⊢ ( 𝜑 → ( 𝐼 gcd 𝐾 ) = 1 )
6	2	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝐼 gcd 𝐾 ) = ( ( 𝐼 · 𝑥 ) + ( 𝐾 · 𝑦 ) ) ) → 𝑅 ∈ CMnd )
7	3	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝐼 gcd 𝐾 ) = ( ( 𝐼 · 𝑥 ) + ( 𝐾 · 𝑦 ) ) ) → 𝐾 ∈ ℕ )
8	4	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝐼 gcd 𝐾 ) = ( ( 𝐼 · 𝑥 ) + ( 𝐾 · 𝑦 ) ) ) → 𝐼 ∈ ℕ )
9		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝐼 gcd 𝐾 ) = ( ( 𝐼 · 𝑥 ) + ( 𝐾 · 𝑦 ) ) ) → 𝑥 ∈ ℕ )
10		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝐼 gcd 𝐾 ) = ( ( 𝐼 · 𝑥 ) + ( 𝐾 · 𝑦 ) ) ) → 𝑦 ∈ ℤ )
11	5	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝐼 gcd 𝐾 ) = ( ( 𝐼 · 𝑥 ) + ( 𝐾 · 𝑦 ) ) ) → ( 𝐼 gcd 𝐾 ) = 1 )
12		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝐼 gcd 𝐾 ) = ( ( 𝐼 · 𝑥 ) + ( 𝐾 · 𝑦 ) ) ) → ( 𝐼 gcd 𝐾 ) = ( ( 𝐼 · 𝑥 ) + ( 𝐾 · 𝑦 ) ) )
13	11 12	eqtr3d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝐼 gcd 𝐾 ) = ( ( 𝐼 · 𝑥 ) + ( 𝐾 · 𝑦 ) ) ) → 1 = ( ( 𝐼 · 𝑥 ) + ( 𝐾 · 𝑦 ) ) )
14		eqid	⊢ { 𝑤 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑧 ( +g ‘ 𝑅 ) 𝑤 ) = ( 0g ‘ 𝑅 ) } = { 𝑤 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑧 ( +g ‘ 𝑅 ) 𝑤 ) = ( 0g ‘ 𝑅 ) }
15	1 6 7 8 9 10 13 14	primrootscoprbij	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝐼 gcd 𝐾 ) = ( ( 𝐼 · 𝑥 ) + ( 𝐾 · 𝑦 ) ) ) → 𝐹 : ( 𝑅 PrimRoots 𝐾 ) –1-1-onto→ ( 𝑅 PrimRoots 𝐾 ) )
16	4 3	jca	⊢ ( 𝜑 → ( 𝐼 ∈ ℕ ∧ 𝐾 ∈ ℕ ) )
17		posbezout	⊢ ( ( 𝐼 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℤ ( 𝐼 gcd 𝐾 ) = ( ( 𝐼 · 𝑥 ) + ( 𝐾 · 𝑦 ) ) )
18	16 17	syl	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℤ ( 𝐼 gcd 𝐾 ) = ( ( 𝐼 · 𝑥 ) + ( 𝐾 · 𝑦 ) ) )
19	15 18	r19.29vva	⊢ ( 𝜑 → 𝐹 : ( 𝑅 PrimRoots 𝐾 ) –1-1-onto→ ( 𝑅 PrimRoots 𝐾 ) )