Step |
Hyp |
Ref |
Expression |
1 |
|
fveq2 |
|- ( x = 0 -> ( ( CC Dn F ) ` x ) = ( ( CC Dn F ) ` 0 ) ) |
2 |
1
|
eleq1d |
|- ( x = 0 -> ( ( ( CC Dn F ) ` x ) e. ( Poly ` S ) <-> ( ( CC Dn F ) ` 0 ) e. ( Poly ` S ) ) ) |
3 |
2
|
imbi2d |
|- ( x = 0 -> ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( CC Dn F ) ` x ) e. ( Poly ` S ) ) <-> ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( CC Dn F ) ` 0 ) e. ( Poly ` S ) ) ) ) |
4 |
|
fveq2 |
|- ( x = n -> ( ( CC Dn F ) ` x ) = ( ( CC Dn F ) ` n ) ) |
5 |
4
|
eleq1d |
|- ( x = n -> ( ( ( CC Dn F ) ` x ) e. ( Poly ` S ) <-> ( ( CC Dn F ) ` n ) e. ( Poly ` S ) ) ) |
6 |
5
|
imbi2d |
|- ( x = n -> ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( CC Dn F ) ` x ) e. ( Poly ` S ) ) <-> ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( CC Dn F ) ` n ) e. ( Poly ` S ) ) ) ) |
7 |
|
fveq2 |
|- ( x = ( n + 1 ) -> ( ( CC Dn F ) ` x ) = ( ( CC Dn F ) ` ( n + 1 ) ) ) |
8 |
7
|
eleq1d |
|- ( x = ( n + 1 ) -> ( ( ( CC Dn F ) ` x ) e. ( Poly ` S ) <-> ( ( CC Dn F ) ` ( n + 1 ) ) e. ( Poly ` S ) ) ) |
9 |
8
|
imbi2d |
|- ( x = ( n + 1 ) -> ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( CC Dn F ) ` x ) e. ( Poly ` S ) ) <-> ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( CC Dn F ) ` ( n + 1 ) ) e. ( Poly ` S ) ) ) ) |
10 |
|
fveq2 |
|- ( x = N -> ( ( CC Dn F ) ` x ) = ( ( CC Dn F ) ` N ) ) |
11 |
10
|
eleq1d |
|- ( x = N -> ( ( ( CC Dn F ) ` x ) e. ( Poly ` S ) <-> ( ( CC Dn F ) ` N ) e. ( Poly ` S ) ) ) |
12 |
11
|
imbi2d |
|- ( x = N -> ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( CC Dn F ) ` x ) e. ( Poly ` S ) ) <-> ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( CC Dn F ) ` N ) e. ( Poly ` S ) ) ) ) |
13 |
|
ssid |
|- CC C_ CC |
14 |
|
cnex |
|- CC e. _V |
15 |
|
plyf |
|- ( F e. ( Poly ` S ) -> F : CC --> CC ) |
16 |
15
|
adantl |
|- ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> F : CC --> CC ) |
17 |
|
fpmg |
|- ( ( CC e. _V /\ CC e. _V /\ F : CC --> CC ) -> F e. ( CC ^pm CC ) ) |
18 |
14 14 16 17
|
mp3an12i |
|- ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> F e. ( CC ^pm CC ) ) |
19 |
|
dvn0 |
|- ( ( CC C_ CC /\ F e. ( CC ^pm CC ) ) -> ( ( CC Dn F ) ` 0 ) = F ) |
20 |
13 18 19
|
sylancr |
|- ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( CC Dn F ) ` 0 ) = F ) |
21 |
|
simpr |
|- ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> F e. ( Poly ` S ) ) |
22 |
20 21
|
eqeltrd |
|- ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( CC Dn F ) ` 0 ) e. ( Poly ` S ) ) |
23 |
|
dvply2g |
|- ( ( S e. ( SubRing ` CCfld ) /\ ( ( CC Dn F ) ` n ) e. ( Poly ` S ) ) -> ( CC _D ( ( CC Dn F ) ` n ) ) e. ( Poly ` S ) ) |
24 |
23
|
ex |
|- ( S e. ( SubRing ` CCfld ) -> ( ( ( CC Dn F ) ` n ) e. ( Poly ` S ) -> ( CC _D ( ( CC Dn F ) ` n ) ) e. ( Poly ` S ) ) ) |
25 |
24
|
ad2antrr |
|- ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> ( ( ( CC Dn F ) ` n ) e. ( Poly ` S ) -> ( CC _D ( ( CC Dn F ) ` n ) ) e. ( Poly ` S ) ) ) |
26 |
|
dvnp1 |
|- ( ( CC C_ CC /\ F e. ( CC ^pm CC ) /\ n e. NN0 ) -> ( ( CC Dn F ) ` ( n + 1 ) ) = ( CC _D ( ( CC Dn F ) ` n ) ) ) |
27 |
13 26
|
mp3an1 |
|- ( ( F e. ( CC ^pm CC ) /\ n e. NN0 ) -> ( ( CC Dn F ) ` ( n + 1 ) ) = ( CC _D ( ( CC Dn F ) ` n ) ) ) |
28 |
18 27
|
sylan |
|- ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> ( ( CC Dn F ) ` ( n + 1 ) ) = ( CC _D ( ( CC Dn F ) ` n ) ) ) |
29 |
28
|
eleq1d |
|- ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> ( ( ( CC Dn F ) ` ( n + 1 ) ) e. ( Poly ` S ) <-> ( CC _D ( ( CC Dn F ) ` n ) ) e. ( Poly ` S ) ) ) |
30 |
25 29
|
sylibrd |
|- ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> ( ( ( CC Dn F ) ` n ) e. ( Poly ` S ) -> ( ( CC Dn F ) ` ( n + 1 ) ) e. ( Poly ` S ) ) ) |
31 |
30
|
expcom |
|- ( n e. NN0 -> ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( ( CC Dn F ) ` n ) e. ( Poly ` S ) -> ( ( CC Dn F ) ` ( n + 1 ) ) e. ( Poly ` S ) ) ) ) |
32 |
31
|
a2d |
|- ( n e. NN0 -> ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( CC Dn F ) ` n ) e. ( Poly ` S ) ) -> ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( CC Dn F ) ` ( n + 1 ) ) e. ( Poly ` S ) ) ) ) |
33 |
3 6 9 12 22 32
|
nn0ind |
|- ( N e. NN0 -> ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( CC Dn F ) ` N ) e. ( Poly ` S ) ) ) |
34 |
33
|
impcom |
|- ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ N e. NN0 ) -> ( ( CC Dn F ) ` N ) e. ( Poly ` S ) ) |
35 |
34
|
3impa |
|- ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) /\ N e. NN0 ) -> ( ( CC Dn F ) ` N ) e. ( Poly ` S ) ) |