Metamath Proof Explorer

Theorem isprimroot2

Description: Alternative way of creating primitive roots. (Contributed by metakunt, 14-Jul-2025)

Ref Expression
Hypotheses isprimroot2.1 
|- ( ph -> R e. CMnd )
isprimroot2.2 
|- ( ph -> K e. NN )
isprimroot2.3 
|- ( ph -> M e. ( Base ` R ) )
isprimroot2.4 
|- ( ph -> ( ( od ` R ) ` M ) = K )
Assertion isprimroot2 
|- ( ph -> M e. ( R PrimRoots K ) )

Proof

Step Hyp Ref Expression
1 isprimroot2.1 
 |-  ( ph -> R e. CMnd )
2 isprimroot2.2 
 |-  ( ph -> K e. NN )
3 isprimroot2.3 
 |-  ( ph -> M e. ( Base ` R ) )
4 isprimroot2.4 
 |-  ( ph -> ( ( od ` R ) ` M ) = K )
5 4 eqcomd 
 |-  ( ph -> K = ( ( od ` R ) ` M ) )
6 5 oveq1d 
 |-  ( ph -> ( K ( .g ` R ) M ) = ( ( ( od ` R ) ` M ) ( .g ` R ) M ) )
7 eqid 
 |-  ( Base ` R ) = ( Base ` R )
8 eqid 
 |-  ( od ` R ) = ( od ` R )
9 eqid 
 |-  ( .g ` R ) = ( .g ` R )
10 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
11 7 8 9 10 odid 
 |-  ( M e. ( Base ` R ) -> ( ( ( od ` R ) ` M ) ( .g ` R ) M ) = ( 0g ` R ) )
12 3 11 syl 
 |-  ( ph -> ( ( ( od ` R ) ` M ) ( .g ` R ) M ) = ( 0g ` R ) )
13 6 12 eqtrd 
 |-  ( ph -> ( K ( .g ` R ) M ) = ( 0g ` R ) )
14 4 ad2antrr 
 |-  ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` R ) M ) = ( 0g ` R ) ) -> ( ( od ` R ) ` M ) = K )
15 14 eqcomd 
 |-  ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` R ) M ) = ( 0g ` R ) ) -> K = ( ( od ` R ) ` M ) )
16 1 cmnmndd 
 |-  ( ph -> R e. Mnd )
17 16 adantr 
 |-  ( ( ph /\ l e. NN0 ) -> R e. Mnd )
18 3 adantr 
 |-  ( ( ph /\ l e. NN0 ) -> M e. ( Base ` R ) )
19 simpr 
 |-  ( ( ph /\ l e. NN0 ) -> l e. NN0 )
20 7 8 9 10 oddvdsnn0 
 |-  ( ( R e. Mnd /\ M e. ( Base ` R ) /\ l e. NN0 ) -> ( ( ( od ` R ) ` M ) || l <-> ( l ( .g ` R ) M ) = ( 0g ` R ) ) )
21 17 18 19 20 syl3anc 
 |-  ( ( ph /\ l e. NN0 ) -> ( ( ( od ` R ) ` M ) || l <-> ( l ( .g ` R ) M ) = ( 0g ` R ) ) )
22 21 bicomd 
 |-  ( ( ph /\ l e. NN0 ) -> ( ( l ( .g ` R ) M ) = ( 0g ` R ) <-> ( ( od ` R ) ` M ) || l ) )
23 22 biimpd 
 |-  ( ( ph /\ l e. NN0 ) -> ( ( l ( .g ` R ) M ) = ( 0g ` R ) -> ( ( od ` R ) ` M ) || l ) )
24 23 imp 
 |-  ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` R ) M ) = ( 0g ` R ) ) -> ( ( od ` R ) ` M ) || l )
25 15 24 eqbrtrd 
 |-  ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` R ) M ) = ( 0g ` R ) ) -> K || l )
26 25 ex 
 |-  ( ( ph /\ l e. NN0 ) -> ( ( l ( .g ` R ) M ) = ( 0g ` R ) -> K || l ) )
27 26 ralrimiva 
 |-  ( ph -> A. l e. NN0 ( ( l ( .g ` R ) M ) = ( 0g ` R ) -> K || l ) )
28 3 13 27 3jca 
 |-  ( ph -> ( M e. ( Base ` R ) /\ ( K ( .g ` R ) M ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) M ) = ( 0g ` R ) -> K || l ) ) )
29 2 nnnn0d 
 |-  ( ph -> K e. NN0 )
30 1 29 9 isprimroot 
 |-  ( ph -> ( M e. ( R PrimRoots K ) <-> ( M e. ( Base ` R ) /\ ( K ( .g ` R ) M ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) M ) = ( 0g ` R ) -> K || l ) ) ) )
31 28 30 mpbird 
 |-  ( ph -> M e. ( R PrimRoots K ) )