Metamath Proof Explorer

Theorem aks6d1c6isolem3

Description: The preimage of a map sending a primitive root to its powers of zero is equal to the set of integers that divide R . (Contributed by metakunt, 15-May-2025)

Ref Expression
Hypotheses aks6d1c6isolem1.1 
|- ( ph -> R e. CMnd )
aks6d1c6isolem1.2 
|- ( ph -> K e. NN )
aks6d1c6isolem1.3 
|- U = { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) }
aks6d1c6isolem1.4 
|- F = ( x e. ZZ |-> ( x ( .g ` ( R |`s U ) ) M ) )
aks6d1c6isolem1.5 
|- ( ph -> M e. ( R PrimRoots K ) )
aks6d1c6isolem3.1 
|- S = ( RSpan ` ZZring )
Assertion aks6d1c6isolem3 
|- ( ph -> ( S ` { K } ) = ( `' F " { ( 0g ` ( R |`s U ) ) } ) )

Proof

Step Hyp Ref Expression
1 aks6d1c6isolem1.1 
 |-  ( ph -> R e. CMnd )
2 aks6d1c6isolem1.2 
 |-  ( ph -> K e. NN )
3 aks6d1c6isolem1.3 
 |-  U = { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) }
4 aks6d1c6isolem1.4 
 |-  F = ( x e. ZZ |-> ( x ( .g ` ( R |`s U ) ) M ) )
5 aks6d1c6isolem1.5 
 |-  ( ph -> M e. ( R PrimRoots K ) )
6 aks6d1c6isolem3.1 
 |-  S = ( RSpan ` ZZring )
7 zringring 
 |-  ZZring e. Ring
8 7 a1i 
 |-  ( ph -> ZZring e. Ring )
9 2 nnzd 
 |-  ( ph -> K e. ZZ )
10 zringbas 
 |-  ZZ = ( Base ` ZZring )
11 dvdsrzring 
 |-  || = ( ||r ` ZZring )
12 10 6 11 rspsn 
 |-  ( ( ZZring e. Ring /\ K e. ZZ ) -> ( S ` { K } ) = { z | K || z } )
13 8 9 12 syl2anc 
 |-  ( ph -> ( S ` { K } ) = { z | K || z } )
14 ovexd 
 |-  ( ( ph /\ x e. ZZ ) -> ( x ( .g ` ( R |`s U ) ) M ) e. _V )
15 14 4 fmptd 
 |-  ( ph -> F : ZZ --> _V )
16 15 ffnd 
 |-  ( ph -> F Fn ZZ )
17 fniniseg2 
 |-  ( F Fn ZZ -> ( `' F " { ( 0g ` ( R |`s U ) ) } ) = { z e. ZZ | ( F ` z ) = ( 0g ` ( R |`s U ) ) } )
18 16 17 syl 
 |-  ( ph -> ( `' F " { ( 0g ` ( R |`s U ) ) } ) = { z e. ZZ | ( F ` z ) = ( 0g ` ( R |`s U ) ) } )
19 4 a1i 
 |-  ( ( ph /\ z e. ZZ ) -> F = ( x e. ZZ |-> ( x ( .g ` ( R |`s U ) ) M ) ) )
20 simpr 
 |-  ( ( ( ph /\ z e. ZZ ) /\ x = z ) -> x = z )
21 20 oveq1d 
 |-  ( ( ( ph /\ z e. ZZ ) /\ x = z ) -> ( x ( .g ` ( R |`s U ) ) M ) = ( z ( .g ` ( R |`s U ) ) M ) )
22 simpr 
 |-  ( ( ph /\ z e. ZZ ) -> z e. ZZ )
23 ovexd 
 |-  ( ( ph /\ z e. ZZ ) -> ( z ( .g ` ( R |`s U ) ) M ) e. _V )
24 19 21 22 23 fvmptd 
 |-  ( ( ph /\ z e. ZZ ) -> ( F ` z ) = ( z ( .g ` ( R |`s U ) ) M ) )
25 24 eqeq1d 
 |-  ( ( ph /\ z e. ZZ ) -> ( ( F ` z ) = ( 0g ` ( R |`s U ) ) <-> ( z ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) ) )
26 1 adantr 
 |-  ( ( ph /\ z e. ZZ ) -> R e. CMnd )
27 2 adantr 
 |-  ( ( ph /\ z e. ZZ ) -> K e. NN )
28 5 adantr 
 |-  ( ( ph /\ z e. ZZ ) -> M e. ( R PrimRoots K ) )
29 26 27 28 3 22 primrootspoweq0 
 |-  ( ( ph /\ z e. ZZ ) -> ( ( z ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) <-> K || z ) )
30 25 29 bitrd 
 |-  ( ( ph /\ z e. ZZ ) -> ( ( F ` z ) = ( 0g ` ( R |`s U ) ) <-> K || z ) )
31 30 rabbidva 
 |-  ( ph -> { z e. ZZ | ( F ` z ) = ( 0g ` ( R |`s U ) ) } = { z e. ZZ | K || z } )
32 df-rab 
 |-  { z e. ZZ | K || z } = { z | ( z e. ZZ /\ K || z ) }
33 32 a1i 
 |-  ( ph -> { z e. ZZ | K || z } = { z | ( z e. ZZ /\ K || z ) } )
34 simpr 
 |-  ( ( z e. ZZ /\ K || z ) -> K || z )
35 dvdszrcl 
 |-  ( K || z -> ( K e. ZZ /\ z e. ZZ ) )
36 35 simprd 
 |-  ( K || z -> z e. ZZ )
37 36 ancri 
 |-  ( K || z -> ( z e. ZZ /\ K || z ) )
38 34 37 impbii 
 |-  ( ( z e. ZZ /\ K || z ) <-> K || z )
39 38 a1i 
 |-  ( ph -> ( ( z e. ZZ /\ K || z ) <-> K || z ) )
40 39 abbidv 
 |-  ( ph -> { z | ( z e. ZZ /\ K || z ) } = { z | K || z } )
41 33 40 eqtrd 
 |-  ( ph -> { z e. ZZ | K || z } = { z | K || z } )
42 31 41 eqtrd 
 |-  ( ph -> { z e. ZZ | ( F ` z ) = ( 0g ` ( R |`s U ) ) } = { z | K || z } )
43 18 42 eqtr2d 
 |-  ( ph -> { z | K || z } = ( `' F " { ( 0g ` ( R |`s U ) ) } ) )
44 13 43 eqtrd 
 |-  ( ph -> ( S ` { K } ) = ( `' F " { ( 0g ` ( R |`s U ) ) } ) )