Metamath Proof Explorer

Theorem aks6d1c1p6

Description: If a polynomials F is introspective to E , then so are its powers. (Contributed by metakunt, 30-Apr-2025)

Ref Expression
Hypotheses aks6d1c1.1 
|- .~ = { <. e , f >. | ( e e. NN /\ f e. B /\ A. y e. ( V PrimRoots R ) ( e .^ ( ( O ` f ) ` y ) ) = ( ( O ` f ) ` ( e .^ y ) ) ) }
aks6d1c1.2 
|- S = ( Poly1 ` K )
aks6d1c1.3 
|- B = ( Base ` S )
aks6d1c1.4 
|- X = ( var1 ` K )
aks6d1c1.5 
|- W = ( mulGrp ` S )
aks6d1c1.6 
|- V = ( mulGrp ` K )
aks6d1c1.7 
|- .^ = ( .g ` V )
aks6d1c1.8 
|- C = ( algSc ` S )
aks6d1c1.9 
|- D = ( .g ` W )
aks6d1c1.10 
|- P = ( chr ` K )
aks6d1c1.11 
|- O = ( eval1 ` K )
aks6d1c1.12 
|- .+ = ( +g ` S )
aks6d1c1.13 
|- ( ph -> K e. Field )
aks6d1c1.14 
|- ( ph -> P e. Prime )
aks6d1c1.15 
|- ( ph -> R e. NN )
aks6d1c1.16 
|- ( ph -> N e. NN )
aks6d1c1.17 
|- ( ph -> P || N )
aks6d1c1.18 
|- ( ph -> ( N gcd R ) = 1 )
aks6d1c1p6.1 
|- ( ph -> E .~ F )
aks6d1c1p6.2 
|- ( ph -> L e. NN0 )
Assertion aks6d1c1p6 
|- ( ph -> E .~ ( L D F ) )

Proof

Step Hyp Ref Expression
1 aks6d1c1.1 
 |-  .~ = { <. e , f >. | ( e e. NN /\ f e. B /\ A. y e. ( V PrimRoots R ) ( e .^ ( ( O ` f ) ` y ) ) = ( ( O ` f ) ` ( e .^ y ) ) ) }
2 aks6d1c1.2 
 |-  S = ( Poly1 ` K )
3 aks6d1c1.3 
 |-  B = ( Base ` S )
4 aks6d1c1.4 
 |-  X = ( var1 ` K )
5 aks6d1c1.5 
 |-  W = ( mulGrp ` S )
6 aks6d1c1.6 
 |-  V = ( mulGrp ` K )
7 aks6d1c1.7 
 |-  .^ = ( .g ` V )
8 aks6d1c1.8 
 |-  C = ( algSc ` S )
9 aks6d1c1.9 
 |-  D = ( .g ` W )
10 aks6d1c1.10 
 |-  P = ( chr ` K )
11 aks6d1c1.11 
 |-  O = ( eval1 ` K )
12 aks6d1c1.12 
 |-  .+ = ( +g ` S )
13 aks6d1c1.13 
 |-  ( ph -> K e. Field )
14 aks6d1c1.14 
 |-  ( ph -> P e. Prime )
15 aks6d1c1.15 
 |-  ( ph -> R e. NN )
16 aks6d1c1.16 
 |-  ( ph -> N e. NN )
17 aks6d1c1.17 
 |-  ( ph -> P || N )
18 aks6d1c1.18 
 |-  ( ph -> ( N gcd R ) = 1 )
19 aks6d1c1p6.1 
 |-  ( ph -> E .~ F )
20 aks6d1c1p6.2 
 |-  ( ph -> L e. NN0 )
21 oveq1 
 |-  ( h = 0 -> ( h D F ) = ( 0 D F ) )
22 21 breq2d 
 |-  ( h = 0 -> ( E .~ ( h D F ) <-> E .~ ( 0 D F ) ) )
23 oveq1 
 |-  ( h = i -> ( h D F ) = ( i D F ) )
24 23 breq2d 
 |-  ( h = i -> ( E .~ ( h D F ) <-> E .~ ( i D F ) ) )
25 oveq1 
 |-  ( h = ( i + 1 ) -> ( h D F ) = ( ( i + 1 ) D F ) )
26 25 breq2d 
 |-  ( h = ( i + 1 ) -> ( E .~ ( h D F ) <-> E .~ ( ( i + 1 ) D F ) ) )
27 oveq1 
 |-  ( h = L -> ( h D F ) = ( L D F ) )
28 27 breq2d 
 |-  ( h = L -> ( E .~ ( h D F ) <-> E .~ ( L D F ) ) )
29 1 19 aks6d1c1p1rcl 
 |-  ( ph -> ( E e. NN /\ F e. B ) )
30 29 simprd 
 |-  ( ph -> F e. B )
31 30 3 eleqtrdi 
 |-  ( ph -> F e. ( Base ` S ) )
32 eqid 
 |-  ( Base ` S ) = ( Base ` S )
33 5 32 mgpbas 
 |-  ( Base ` S ) = ( Base ` W )
34 31 33 eleqtrdi 
 |-  ( ph -> F e. ( Base ` W ) )
35 eqid 
 |-  ( Base ` W ) = ( Base ` W )
36 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
37 35 36 9 mulg0 
 |-  ( F e. ( Base ` W ) -> ( 0 D F ) = ( 0g ` W ) )
38 34 37 syl 
 |-  ( ph -> ( 0 D F ) = ( 0g ` W ) )
39 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
40 5 39 ringidval 
 |-  ( 1r ` S ) = ( 0g ` W )
41 40 eqcomi 
 |-  ( 0g ` W ) = ( 1r ` S )
42 38 41 eqtrdi 
 |-  ( ph -> ( 0 D F ) = ( 1r ` S ) )
43 42 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( 0 D F ) = ( 1r ` S ) )
44 43 fveq2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( O ` ( 0 D F ) ) = ( O ` ( 1r ` S ) ) )
45 44 fveq1d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` ( 0 D F ) ) ` y ) = ( ( O ` ( 1r ` S ) ) ` y ) )
46 45 oveq2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( E .^ ( ( O ` ( 0 D F ) ) ` y ) ) = ( E .^ ( ( O ` ( 1r ` S ) ) ` y ) ) )
47 13 fldcrngd 
 |-  ( ph -> K e. CRing )
48 crngring 
 |-  ( K e. CRing -> K e. Ring )
49 47 48 syl 
 |-  ( ph -> K e. Ring )
50 eqid 
 |-  ( 1r ` K ) = ( 1r ` K )
51 2 8 50 39 ply1scl1 
 |-  ( K e. Ring -> ( C ` ( 1r ` K ) ) = ( 1r ` S ) )
52 49 51 syl 
 |-  ( ph -> ( C ` ( 1r ` K ) ) = ( 1r ` S ) )
53 52 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( C ` ( 1r ` K ) ) = ( 1r ` S ) )
54 53 eqcomd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( 1r ` S ) = ( C ` ( 1r ` K ) ) )
55 54 fveq2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( O ` ( 1r ` S ) ) = ( O ` ( C ` ( 1r ` K ) ) ) )
56 55 fveq1d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` ( 1r ` S ) ) ` y ) = ( ( O ` ( C ` ( 1r ` K ) ) ) ` y ) )
57 56 oveq2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( E .^ ( ( O ` ( 1r ` S ) ) ` y ) ) = ( E .^ ( ( O ` ( C ` ( 1r ` K ) ) ) ` y ) ) )
58 eqid 
 |-  ( Base ` K ) = ( Base ` K )
59 47 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> K e. CRing )
60 58 50 ringidcl 
 |-  ( K e. Ring -> ( 1r ` K ) e. ( Base ` K ) )
61 49 60 syl 
 |-  ( ph -> ( 1r ` K ) e. ( Base ` K ) )
62 61 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( 1r ` K ) e. ( Base ` K ) )
63 6 crngmgp 
 |-  ( K e. CRing -> V e. CMnd )
64 47 63 syl 
 |-  ( ph -> V e. CMnd )
65 15 nnnn0d 
 |-  ( ph -> R e. NN0 )
66 eqid 
 |-  ( .g ` V ) = ( .g ` V )
67 64 65 66 isprimroot 
 |-  ( ph -> ( y e. ( V PrimRoots R ) <-> ( y e. ( Base ` V ) /\ ( R ( .g ` V ) y ) = ( 0g ` V ) /\ A. z e. NN0 ( ( z ( .g ` V ) y ) = ( 0g ` V ) -> R || z ) ) ) )
68 67 biimpd 
 |-  ( ph -> ( y e. ( V PrimRoots R ) -> ( y e. ( Base ` V ) /\ ( R ( .g ` V ) y ) = ( 0g ` V ) /\ A. z e. NN0 ( ( z ( .g ` V ) y ) = ( 0g ` V ) -> R || z ) ) ) )
69 68 imp 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( y e. ( Base ` V ) /\ ( R ( .g ` V ) y ) = ( 0g ` V ) /\ A. z e. NN0 ( ( z ( .g ` V ) y ) = ( 0g ` V ) -> R || z ) ) )
70 69 simp1d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> y e. ( Base ` V ) )
71 6 58 mgpbas 
 |-  ( Base ` K ) = ( Base ` V )
72 71 eqcomi 
 |-  ( Base ` V ) = ( Base ` K )
73 70 72 eleqtrdi 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> y e. ( Base ` K ) )
74 11 2 58 8 3 59 62 73 evl1scad 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( C ` ( 1r ` K ) ) e. B /\ ( ( O ` ( C ` ( 1r ` K ) ) ) ` y ) = ( 1r ` K ) ) )
75 74 simprd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` ( C ` ( 1r ` K ) ) ) ` y ) = ( 1r ` K ) )
76 75 oveq2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( E .^ ( ( O ` ( C ` ( 1r ` K ) ) ) ` y ) ) = ( E .^ ( 1r ` K ) ) )
77 64 cmnmndd 
 |-  ( ph -> V e. Mnd )
78 29 simpld 
 |-  ( ph -> E e. NN )
79 78 nnnn0d 
 |-  ( ph -> E e. NN0 )
80 eqid 
 |-  ( Base ` V ) = ( Base ` V )
81 6 50 ringidval 
 |-  ( 1r ` K ) = ( 0g ` V )
82 80 7 81 mulgnn0z 
 |-  ( ( V e. Mnd /\ E e. NN0 ) -> ( E .^ ( 1r ` K ) ) = ( 1r ` K ) )
83 77 79 82 syl2anc 
 |-  ( ph -> ( E .^ ( 1r ` K ) ) = ( 1r ` K ) )
84 83 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( E .^ ( 1r ` K ) ) = ( 1r ` K ) )
85 77 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> V e. Mnd )
86 79 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> E e. NN0 )
87 71 7 mulgnn0cl 
 |-  ( ( V e. Mnd /\ E e. NN0 /\ y e. ( Base ` K ) ) -> ( E .^ y ) e. ( Base ` K ) )
88 85 86 73 87 syl3anc 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( E .^ y ) e. ( Base ` K ) )
89 11 2 58 8 3 59 62 88 evl1scad 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( C ` ( 1r ` K ) ) e. B /\ ( ( O ` ( C ` ( 1r ` K ) ) ) ` ( E .^ y ) ) = ( 1r ` K ) ) )
90 89 simprd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` ( C ` ( 1r ` K ) ) ) ` ( E .^ y ) ) = ( 1r ` K ) )
91 90 eqcomd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( 1r ` K ) = ( ( O ` ( C ` ( 1r ` K ) ) ) ` ( E .^ y ) ) )
92 76 84 91 3eqtrd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( E .^ ( ( O ` ( C ` ( 1r ` K ) ) ) ` y ) ) = ( ( O ` ( C ` ( 1r ` K ) ) ) ` ( E .^ y ) ) )
93 53 fveq2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( O ` ( C ` ( 1r ` K ) ) ) = ( O ` ( 1r ` S ) ) )
94 93 fveq1d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` ( C ` ( 1r ` K ) ) ) ` ( E .^ y ) ) = ( ( O ` ( 1r ` S ) ) ` ( E .^ y ) ) )
95 57 92 94 3eqtrd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( E .^ ( ( O ` ( 1r ` S ) ) ` y ) ) = ( ( O ` ( 1r ` S ) ) ` ( E .^ y ) ) )
96 43 eqcomd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( 1r ` S ) = ( 0 D F ) )
97 96 fveq2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( O ` ( 1r ` S ) ) = ( O ` ( 0 D F ) ) )
98 97 fveq1d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` ( 1r ` S ) ) ` ( E .^ y ) ) = ( ( O ` ( 0 D F ) ) ` ( E .^ y ) ) )
99 46 95 98 3eqtrd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( E .^ ( ( O ` ( 0 D F ) ) ` y ) ) = ( ( O ` ( 0 D F ) ) ` ( E .^ y ) ) )
100 99 ralrimiva 
 |-  ( ph -> A. y e. ( V PrimRoots R ) ( E .^ ( ( O ` ( 0 D F ) ) ` y ) ) = ( ( O ` ( 0 D F ) ) ` ( E .^ y ) ) )
101 2 ply1ring 
 |-  ( K e. Ring -> S e. Ring )
102 49 101 syl 
 |-  ( ph -> S e. Ring )
103 32 39 ringidcl 
 |-  ( S e. Ring -> ( 1r ` S ) e. ( Base ` S ) )
104 102 103 syl 
 |-  ( ph -> ( 1r ` S ) e. ( Base ` S ) )
105 42 eqcomd 
 |-  ( ph -> ( 1r ` S ) = ( 0 D F ) )
106 3 a1i 
 |-  ( ph -> B = ( Base ` S ) )
107 106 eqcomd 
 |-  ( ph -> ( Base ` S ) = B )
108 105 107 eleq12d 
 |-  ( ph -> ( ( 1r ` S ) e. ( Base ` S ) <-> ( 0 D F ) e. B ) )
109 104 108 mpbid 
 |-  ( ph -> ( 0 D F ) e. B )
110 1 109 78 aks6d1c1p1 
 |-  ( ph -> ( E .~ ( 0 D F ) <-> A. y e. ( V PrimRoots R ) ( E .^ ( ( O ` ( 0 D F ) ) ` y ) ) = ( ( O ` ( 0 D F ) ) ` ( E .^ y ) ) ) )
111 100 110 mpbird 
 |-  ( ph -> E .~ ( 0 D F ) )
112 13 ad2antrr 
 |-  ( ( ( ph /\ i e. NN0 ) /\ E .~ ( i D F ) ) -> K e. Field )
113 14 ad2antrr 
 |-  ( ( ( ph /\ i e. NN0 ) /\ E .~ ( i D F ) ) -> P e. Prime )
114 15 ad2antrr 
 |-  ( ( ( ph /\ i e. NN0 ) /\ E .~ ( i D F ) ) -> R e. NN )
115 18 ad2antrr 
 |-  ( ( ( ph /\ i e. NN0 ) /\ E .~ ( i D F ) ) -> ( N gcd R ) = 1 )
116 17 ad2antrr 
 |-  ( ( ( ph /\ i e. NN0 ) /\ E .~ ( i D F ) ) -> P || N )
117 simpr 
 |-  ( ( ( ph /\ i e. NN0 ) /\ E .~ ( i D F ) ) -> E .~ ( i D F ) )
118 19 ad2antrr 
 |-  ( ( ( ph /\ i e. NN0 ) /\ E .~ ( i D F ) ) -> E .~ F )
119 1 2 3 4 5 6 7 8 9 10 11 12 112 113 114 115 116 117 118 aks6d1c1p4 
 |-  ( ( ( ph /\ i e. NN0 ) /\ E .~ ( i D F ) ) -> E .~ ( ( i D F ) ( +g ` W ) F ) )
120 5 ringmgp 
 |-  ( S e. Ring -> W e. Mnd )
121 102 120 syl 
 |-  ( ph -> W e. Mnd )
122 121 adantr 
 |-  ( ( ph /\ i e. NN0 ) -> W e. Mnd )
123 122 adantr 
 |-  ( ( ( ph /\ i e. NN0 ) /\ E .~ ( i D F ) ) -> W e. Mnd )
124 simplr 
 |-  ( ( ( ph /\ i e. NN0 ) /\ E .~ ( i D F ) ) -> i e. NN0 )
125 33 a1i 
 |-  ( ph -> ( Base ` S ) = ( Base ` W ) )
126 106 125 eqtrd 
 |-  ( ph -> B = ( Base ` W ) )
127 126 eleq2d 
 |-  ( ph -> ( F e. B <-> F e. ( Base ` W ) ) )
128 30 127 mpbid 
 |-  ( ph -> F e. ( Base ` W ) )
129 128 adantr 
 |-  ( ( ph /\ i e. NN0 ) -> F e. ( Base ` W ) )
130 129 adantr 
 |-  ( ( ( ph /\ i e. NN0 ) /\ E .~ ( i D F ) ) -> F e. ( Base ` W ) )
131 eqid 
 |-  ( +g ` W ) = ( +g ` W )
132 35 9 131 mulgnn0p1 
 |-  ( ( W e. Mnd /\ i e. NN0 /\ F e. ( Base ` W ) ) -> ( ( i + 1 ) D F ) = ( ( i D F ) ( +g ` W ) F ) )
133 123 124 130 132 syl3anc 
 |-  ( ( ( ph /\ i e. NN0 ) /\ E .~ ( i D F ) ) -> ( ( i + 1 ) D F ) = ( ( i D F ) ( +g ` W ) F ) )
134 119 133 breqtrrd 
 |-  ( ( ( ph /\ i e. NN0 ) /\ E .~ ( i D F ) ) -> E .~ ( ( i + 1 ) D F ) )
135 22 24 26 28 111 134 nn0indd 
 |-  ( ( ph /\ L e. NN0 ) -> E .~ ( L D F ) )
136 20 135 mpdan 
 |-  ( ph -> E .~ ( L D F ) )