Metamath Proof Explorer

Theorem isprimroot

Description: The value of a primitive root. (Contributed by metakunt, 25-Apr-2025)

Ref Expression
Hypotheses isprimroot.1 
|- ( ph -> R e. CMnd )
isprimroot.2 
|- ( ph -> K e. NN0 )
isprimroot.3 
|- .^ = ( .g ` R )
Assertion isprimroot 
|- ( ph -> ( M e. ( R PrimRoots K ) <-> ( M e. ( Base ` R ) /\ ( K .^ M ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l .^ M ) = ( 0g ` R ) -> K || l ) ) ) )

Proof

Step Hyp Ref Expression
1 isprimroot.1 
 |-  ( ph -> R e. CMnd )
2 isprimroot.2 
 |-  ( ph -> K e. NN0 )
3 isprimroot.3 
 |-  .^ = ( .g ` R )
4 df-primroots 
 |-  PrimRoots = ( r e. CMnd , k e. NN0 |-> [_ ( Base ` r ) / b ]_ { x e. b | ( ( k ( .g ` r ) x ) = ( 0g ` r ) /\ A. l e. NN0 ( ( l ( .g ` r ) x ) = ( 0g ` r ) -> k || l ) ) } )
5 4 a1i 
 |-  ( ph -> PrimRoots = ( r e. CMnd , k e. NN0 |-> [_ ( Base ` r ) / b ]_ { x e. b | ( ( k ( .g ` r ) x ) = ( 0g ` r ) /\ A. l e. NN0 ( ( l ( .g ` r ) x ) = ( 0g ` r ) -> k || l ) ) } ) )
6 simprl 
 |-  ( ( ph /\ ( r = R /\ k = K ) ) -> r = R )
7 6 fveq2d 
 |-  ( ( ph /\ ( r = R /\ k = K ) ) -> ( Base ` r ) = ( Base ` R ) )
8 simplrl 
 |-  ( ( ( ph /\ ( r = R /\ k = K ) ) /\ x e. b ) -> r = R )
9 8 fveq2d 
 |-  ( ( ( ph /\ ( r = R /\ k = K ) ) /\ x e. b ) -> ( .g ` r ) = ( .g ` R ) )
10 simplrr 
 |-  ( ( ( ph /\ ( r = R /\ k = K ) ) /\ x e. b ) -> k = K )
11 eqidd 
 |-  ( ( ( ph /\ ( r = R /\ k = K ) ) /\ x e. b ) -> x = x )
12 9 10 11 oveq123d 
 |-  ( ( ( ph /\ ( r = R /\ k = K ) ) /\ x e. b ) -> ( k ( .g ` r ) x ) = ( K ( .g ` R ) x ) )
13 8 fveq2d 
 |-  ( ( ( ph /\ ( r = R /\ k = K ) ) /\ x e. b ) -> ( 0g ` r ) = ( 0g ` R ) )
14 12 13 eqeq12d 
 |-  ( ( ( ph /\ ( r = R /\ k = K ) ) /\ x e. b ) -> ( ( k ( .g ` r ) x ) = ( 0g ` r ) <-> ( K ( .g ` R ) x ) = ( 0g ` R ) ) )
15 6 fveq2d 
 |-  ( ( ph /\ ( r = R /\ k = K ) ) -> ( .g ` r ) = ( .g ` R ) )
16 15 oveqdr 
 |-  ( ( ( ph /\ ( r = R /\ k = K ) ) /\ x e. b ) -> ( l ( .g ` r ) x ) = ( l ( .g ` R ) x ) )
17 16 13 eqeq12d 
 |-  ( ( ( ph /\ ( r = R /\ k = K ) ) /\ x e. b ) -> ( ( l ( .g ` r ) x ) = ( 0g ` r ) <-> ( l ( .g ` R ) x ) = ( 0g ` R ) ) )
18 10 breq1d 
 |-  ( ( ( ph /\ ( r = R /\ k = K ) ) /\ x e. b ) -> ( k || l <-> K || l ) )
19 17 18 imbi12d 
 |-  ( ( ( ph /\ ( r = R /\ k = K ) ) /\ x e. b ) -> ( ( ( l ( .g ` r ) x ) = ( 0g ` r ) -> k || l ) <-> ( ( l ( .g ` R ) x ) = ( 0g ` R ) -> K || l ) ) )
20 19 ralbidv 
 |-  ( ( ( ph /\ ( r = R /\ k = K ) ) /\ x e. b ) -> ( A. l e. NN0 ( ( l ( .g ` r ) x ) = ( 0g ` r ) -> k || l ) <-> A. l e. NN0 ( ( l ( .g ` R ) x ) = ( 0g ` R ) -> K || l ) ) )
21 14 20 anbi12d 
 |-  ( ( ( ph /\ ( r = R /\ k = K ) ) /\ x e. b ) -> ( ( ( k ( .g ` r ) x ) = ( 0g ` r ) /\ A. l e. NN0 ( ( l ( .g ` r ) x ) = ( 0g ` r ) -> k || l ) ) <-> ( ( K ( .g ` R ) x ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) x ) = ( 0g ` R ) -> K || l ) ) ) )
22 21 rabbidva 
 |-  ( ( ph /\ ( r = R /\ k = K ) ) -> { x e. b | ( ( k ( .g ` r ) x ) = ( 0g ` r ) /\ A. l e. NN0 ( ( l ( .g ` r ) x ) = ( 0g ` r ) -> k || l ) ) } = { x e. b | ( ( K ( .g ` R ) x ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) x ) = ( 0g ` R ) -> K || l ) ) } )
23 7 22 csbeq12dv 
 |-  ( ( ph /\ ( r = R /\ k = K ) ) -> [_ ( Base ` r ) / b ]_ { x e. b | ( ( k ( .g ` r ) x ) = ( 0g ` r ) /\ A. l e. NN0 ( ( l ( .g ` r ) x ) = ( 0g ` r ) -> k || l ) ) } = [_ ( Base ` R ) / b ]_ { x e. b | ( ( K ( .g ` R ) x ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) x ) = ( 0g ` R ) -> K || l ) ) } )
24 eqid 
 |-  { x e. ( Base ` R ) | ( ( K ( .g ` R ) x ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) x ) = ( 0g ` R ) -> K || l ) ) } = { x e. ( Base ` R ) | ( ( K ( .g ` R ) x ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) x ) = ( 0g ` R ) -> K || l ) ) }
25 fvexd 
 |-  ( ph -> ( Base ` R ) e. _V )
26 24 25 rabexd 
 |-  ( ph -> { x e. ( Base ` R ) | ( ( K ( .g ` R ) x ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) x ) = ( 0g ` R ) -> K || l ) ) } e. _V )
27 simpr 
 |-  ( ( ph /\ b = ( Base ` R ) ) -> b = ( Base ` R ) )
28 27 rabeqdv 
 |-  ( ( ph /\ b = ( Base ` R ) ) -> { x e. b | ( ( K ( .g ` R ) x ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) x ) = ( 0g ` R ) -> K || l ) ) } = { x e. ( Base ` R ) | ( ( K ( .g ` R ) x ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) x ) = ( 0g ` R ) -> K || l ) ) } )
29 25 28 csbied 
 |-  ( ph -> [_ ( Base ` R ) / b ]_ { x e. b | ( ( K ( .g ` R ) x ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) x ) = ( 0g ` R ) -> K || l ) ) } = { x e. ( Base ` R ) | ( ( K ( .g ` R ) x ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) x ) = ( 0g ` R ) -> K || l ) ) } )
30 29 eleq1d 
 |-  ( ph -> ( [_ ( Base ` R ) / b ]_ { x e. b | ( ( K ( .g ` R ) x ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) x ) = ( 0g ` R ) -> K || l ) ) } e. _V <-> { x e. ( Base ` R ) | ( ( K ( .g ` R ) x ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) x ) = ( 0g ` R ) -> K || l ) ) } e. _V ) )
31 26 30 mpbird 
 |-  ( ph -> [_ ( Base ` R ) / b ]_ { x e. b | ( ( K ( .g ` R ) x ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) x ) = ( 0g ` R ) -> K || l ) ) } e. _V )
32 5 23 1 2 31 ovmpod 
 |-  ( ph -> ( R PrimRoots K ) = [_ ( Base ` R ) / b ]_ { x e. b | ( ( K ( .g ` R ) x ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) x ) = ( 0g ` R ) -> K || l ) ) } )
33 32 29 eqtrd 
 |-  ( ph -> ( R PrimRoots K ) = { x e. ( Base ` R ) | ( ( K ( .g ` R ) x ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) x ) = ( 0g ` R ) -> K || l ) ) } )
34 33 eleq2d 
 |-  ( ph -> ( M e. ( R PrimRoots K ) <-> M e. { x e. ( Base ` R ) | ( ( K ( .g ` R ) x ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) x ) = ( 0g ` R ) -> K || l ) ) } ) )
35 oveq2 
 |-  ( x = M -> ( K ( .g ` R ) x ) = ( K ( .g ` R ) M ) )
36 35 eqeq1d 
 |-  ( x = M -> ( ( K ( .g ` R ) x ) = ( 0g ` R ) <-> ( K ( .g ` R ) M ) = ( 0g ` R ) ) )
37 oveq2 
 |-  ( x = M -> ( l ( .g ` R ) x ) = ( l ( .g ` R ) M ) )
38 37 eqeq1d 
 |-  ( x = M -> ( ( l ( .g ` R ) x ) = ( 0g ` R ) <-> ( l ( .g ` R ) M ) = ( 0g ` R ) ) )
39 38 imbi1d 
 |-  ( x = M -> ( ( ( l ( .g ` R ) x ) = ( 0g ` R ) -> K || l ) <-> ( ( l ( .g ` R ) M ) = ( 0g ` R ) -> K || l ) ) )
40 39 ralbidv 
 |-  ( x = M -> ( A. l e. NN0 ( ( l ( .g ` R ) x ) = ( 0g ` R ) -> K || l ) <-> A. l e. NN0 ( ( l ( .g ` R ) M ) = ( 0g ` R ) -> K || l ) ) )
41 36 40 anbi12d 
 |-  ( x = M -> ( ( ( K ( .g ` R ) x ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) x ) = ( 0g ` R ) -> K || l ) ) <-> ( ( K ( .g ` R ) M ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) M ) = ( 0g ` R ) -> K || l ) ) ) )
42 41 elrab 
 |-  ( M e. { x e. ( Base ` R ) | ( ( K ( .g ` R ) x ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) x ) = ( 0g ` R ) -> K || l ) ) } <-> ( M e. ( Base ` R ) /\ ( ( K ( .g ` R ) M ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) M ) = ( 0g ` R ) -> K || l ) ) ) )
43 42 a1i 
 |-  ( ph -> ( M e. { x e. ( Base ` R ) | ( ( K ( .g ` R ) x ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) x ) = ( 0g ` R ) -> K || l ) ) } <-> ( M e. ( Base ` R ) /\ ( ( K ( .g ` R ) M ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) M ) = ( 0g ` R ) -> K || l ) ) ) ) )
44 3anass 
 |-  ( ( M e. ( Base ` R ) /\ ( K ( .g ` R ) M ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) M ) = ( 0g ` R ) -> K || l ) ) <-> ( M e. ( Base ` R ) /\ ( ( K ( .g ` R ) M ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) M ) = ( 0g ` R ) -> K || l ) ) ) )
45 44 bicomi 
 |-  ( ( M e. ( Base ` R ) /\ ( ( K ( .g ` R ) M ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) M ) = ( 0g ` R ) -> K || l ) ) ) <-> ( M e. ( Base ` R ) /\ ( K ( .g ` R ) M ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) M ) = ( 0g ` R ) -> K || l ) ) )
46 45 a1i 
 |-  ( ph -> ( ( M e. ( Base ` R ) /\ ( ( K ( .g ` R ) M ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) M ) = ( 0g ` R ) -> K || l ) ) ) <-> ( M e. ( Base ` R ) /\ ( K ( .g ` R ) M ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) M ) = ( 0g ` R ) -> K || l ) ) ) )
47 biidd 
 |-  ( ph -> ( M e. ( Base ` R ) <-> M e. ( Base ` R ) ) )
48 3 eqcomi 
 |-  ( .g ` R ) = .^
49 48 a1i 
 |-  ( ph -> ( .g ` R ) = .^ )
50 49 oveqd 
 |-  ( ph -> ( K ( .g ` R ) M ) = ( K .^ M ) )
51 50 eqeq1d 
 |-  ( ph -> ( ( K ( .g ` R ) M ) = ( 0g ` R ) <-> ( K .^ M ) = ( 0g ` R ) ) )
52 49 oveqd 
 |-  ( ph -> ( l ( .g ` R ) M ) = ( l .^ M ) )
53 52 eqeq1d 
 |-  ( ph -> ( ( l ( .g ` R ) M ) = ( 0g ` R ) <-> ( l .^ M ) = ( 0g ` R ) ) )
54 53 imbi1d 
 |-  ( ph -> ( ( ( l ( .g ` R ) M ) = ( 0g ` R ) -> K || l ) <-> ( ( l .^ M ) = ( 0g ` R ) -> K || l ) ) )
55 54 ralbidv 
 |-  ( ph -> ( A. l e. NN0 ( ( l ( .g ` R ) M ) = ( 0g ` R ) -> K || l ) <-> A. l e. NN0 ( ( l .^ M ) = ( 0g ` R ) -> K || l ) ) )
56 47 51 55 3anbi123d 
 |-  ( ph -> ( ( M e. ( Base ` R ) /\ ( K ( .g ` R ) M ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) M ) = ( 0g ` R ) -> K || l ) ) <-> ( M e. ( Base ` R ) /\ ( K .^ M ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l .^ M ) = ( 0g ` R ) -> K || l ) ) ) )
57 46 56 bitrd 
 |-  ( ph -> ( ( M e. ( Base ` R ) /\ ( ( K ( .g ` R ) M ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) M ) = ( 0g ` R ) -> K || l ) ) ) <-> ( M e. ( Base ` R ) /\ ( K .^ M ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l .^ M ) = ( 0g ` R ) -> K || l ) ) ) )
58 43 57 bitrd 
 |-  ( ph -> ( M e. { x e. ( Base ` R ) | ( ( K ( .g ` R ) x ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) x ) = ( 0g ` R ) -> K || l ) ) } <-> ( M e. ( Base ` R ) /\ ( K .^ M ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l .^ M ) = ( 0g ` R ) -> K || l ) ) ) )
59 34 58 bitrd 
 |-  ( ph -> ( M e. ( R PrimRoots K ) <-> ( M e. ( Base ` R ) /\ ( K .^ M ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l .^ M ) = ( 0g ` R ) -> K || l ) ) ) )