Metamath Proof Explorer

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	$⊢ F = (m \in (R PrimRoots K) ⟼ I \cdot_{R} m)$
		primrootscoprbij2.2	$⊢ φ \to R \in CMnd$
		primrootscoprbij2.3	$⊢ φ \to K \in ℕ$
		primrootscoprbij2.4	$⊢ φ \to I \in ℕ$
		primrootscoprbij2.5	$⊢ φ \to I \gcd K = 1$
	Assertion	primrootscoprbij2	$⊢ φ \to F : R PrimRoots K \underset{1-1 onto}{⟶} R PrimRoots K$

Proof

Step	Hyp	Ref	Expression
1		primrootscoprbij2.1	$⊢ F = (m \in (R PrimRoots K) ⟼ I \cdot_{R} m)$
2		primrootscoprbij2.2	$⊢ φ \to R \in CMnd$
3		primrootscoprbij2.3	$⊢ φ \to K \in ℕ$
4		primrootscoprbij2.4	$⊢ φ \to I \in ℕ$
5		primrootscoprbij2.5	$⊢ φ \to I \gcd K = 1$
6	2	ad3antrrr	$⊢ (((φ \land x \in ℕ) \land y \in ℤ) \land I \gcd K = I x + K y) \to R \in CMnd$
7	3	ad3antrrr	$⊢ (((φ \land x \in ℕ) \land y \in ℤ) \land I \gcd K = I x + K y) \to K \in ℕ$
8	4	ad3antrrr	$⊢ (((φ \land x \in ℕ) \land y \in ℤ) \land I \gcd K = I x + K y) \to I \in ℕ$
9		simpllr	$⊢ (((φ \land x \in ℕ) \land y \in ℤ) \land I \gcd K = I x + K y) \to x \in ℕ$
10		simplr	$⊢ (((φ \land x \in ℕ) \land y \in ℤ) \land I \gcd K = I x + K y) \to y \in ℤ$
11	5	ad3antrrr	$⊢ (((φ \land x \in ℕ) \land y \in ℤ) \land I \gcd K = I x + K y) \to I \gcd K = 1$
12		simpr	$⊢ (((φ \land x \in ℕ) \land y \in ℤ) \land I \gcd K = I x + K y) \to I \gcd K = I x + K y$
13	11 12	eqtr3d	$⊢ (((φ \land x \in ℕ) \land y \in ℤ) \land I \gcd K = I x + K y) \to 1 = I x + K y$
14		eqid	$⊢ \{w \in {Base}_{R} \| \exists z \in {Base}_{R} z +_{R} w = 0_{R}\} = \{w \in {Base}_{R} \| \exists z \in {Base}_{R} z +_{R} w = 0_{R}\}$
15	1 6 7 8 9 10 13 14	primrootscoprbij	$⊢ (((φ \land x \in ℕ) \land y \in ℤ) \land I \gcd K = I x + K y) \to F : R PrimRoots K \underset{1-1 onto}{⟶} R PrimRoots K$
16	4 3	jca	$⊢ φ \to (I \in ℕ \land K \in ℕ)$
17		posbezout	$⊢ (I \in ℕ \land K \in ℕ) \to \exists x \in ℕ \exists y \in ℤ I \gcd K = I x + K y$
18	16 17	syl	$⊢ φ \to \exists x \in ℕ \exists y \in ℤ I \gcd K = I x + K y$
19	15 18	r19.29vva	$⊢ φ \to F : R PrimRoots K \underset{1-1 onto}{⟶} R PrimRoots K$