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 e. ( R PrimRoots K ) |-> ( I ( .g ` R ) m ) )
primrootscoprbij2.2 
|- ( ph -> R e. CMnd )
primrootscoprbij2.3 
|- ( ph -> K e. NN )
primrootscoprbij2.4 
|- ( ph -> I e. NN )
primrootscoprbij2.5 
|- ( ph -> ( I gcd K ) = 1 )
Assertion primrootscoprbij2 
|- ( ph -> F : ( R PrimRoots K ) -1-1-onto-> ( R PrimRoots K ) )

Proof

Step Hyp Ref Expression
1 primrootscoprbij2.1 
 |-  F = ( m e. ( R PrimRoots K ) |-> ( I ( .g ` R ) m ) )
2 primrootscoprbij2.2 
 |-  ( ph -> R e. CMnd )
3 primrootscoprbij2.3 
 |-  ( ph -> K e. NN )
4 primrootscoprbij2.4 
 |-  ( ph -> I e. NN )
5 primrootscoprbij2.5 
 |-  ( ph -> ( I gcd K ) = 1 )
6 2 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. NN ) /\ y e. ZZ ) /\ ( I gcd K ) = ( ( I x. x ) + ( K x. y ) ) ) -> R e. CMnd )
7 3 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. NN ) /\ y e. ZZ ) /\ ( I gcd K ) = ( ( I x. x ) + ( K x. y ) ) ) -> K e. NN )
8 4 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. NN ) /\ y e. ZZ ) /\ ( I gcd K ) = ( ( I x. x ) + ( K x. y ) ) ) -> I e. NN )
9 simpllr 
 |-  ( ( ( ( ph /\ x e. NN ) /\ y e. ZZ ) /\ ( I gcd K ) = ( ( I x. x ) + ( K x. y ) ) ) -> x e. NN )
10 simplr 
 |-  ( ( ( ( ph /\ x e. NN ) /\ y e. ZZ ) /\ ( I gcd K ) = ( ( I x. x ) + ( K x. y ) ) ) -> y e. ZZ )
11 5 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. NN ) /\ y e. ZZ ) /\ ( I gcd K ) = ( ( I x. x ) + ( K x. y ) ) ) -> ( I gcd K ) = 1 )
12 simpr 
 |-  ( ( ( ( ph /\ x e. NN ) /\ y e. ZZ ) /\ ( I gcd K ) = ( ( I x. x ) + ( K x. y ) ) ) -> ( I gcd K ) = ( ( I x. x ) + ( K x. y ) ) )
13 11 12 eqtr3d 
 |-  ( ( ( ( ph /\ x e. NN ) /\ y e. ZZ ) /\ ( I gcd K ) = ( ( I x. x ) + ( K x. y ) ) ) -> 1 = ( ( I x. x ) + ( K x. y ) ) )
14 eqid 
 |-  { w e. ( Base ` R ) | E. z e. ( Base ` R ) ( z ( +g ` R ) w ) = ( 0g ` R ) } = { w e. ( Base ` R ) | E. z e. ( Base ` R ) ( z ( +g ` R ) w ) = ( 0g ` R ) }
15 1 6 7 8 9 10 13 14 primrootscoprbij 
 |-  ( ( ( ( ph /\ x e. NN ) /\ y e. ZZ ) /\ ( I gcd K ) = ( ( I x. x ) + ( K x. y ) ) ) -> F : ( R PrimRoots K ) -1-1-onto-> ( R PrimRoots K ) )
16 4 3 jca 
 |-  ( ph -> ( I e. NN /\ K e. NN ) )
17 posbezout 
 |-  ( ( I e. NN /\ K e. NN ) -> E. x e. NN E. y e. ZZ ( I gcd K ) = ( ( I x. x ) + ( K x. y ) ) )
18 16 17 syl 
 |-  ( ph -> E. x e. NN E. y e. ZZ ( I gcd K ) = ( ( I x. x ) + ( K x. y ) ) )
19 15 18 r19.29vva 
 |-  ( ph -> F : ( R PrimRoots K ) -1-1-onto-> ( R PrimRoots K ) )