Metamath Proof Explorer


Theorem dvnres

Description: Multiple derivative version of dvres3a . (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Assertion dvnres
|- ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) /\ N e. NN0 ) /\ dom ( ( CC Dn F ) ` N ) = dom F ) -> ( ( S Dn ( F |` S ) ) ` N ) = ( ( ( CC Dn F ) ` N ) |` S ) )

Proof

Step Hyp Ref Expression
1 fveq2
 |-  ( x = 0 -> ( ( CC Dn F ) ` x ) = ( ( CC Dn F ) ` 0 ) )
2 1 dmeqd
 |-  ( x = 0 -> dom ( ( CC Dn F ) ` x ) = dom ( ( CC Dn F ) ` 0 ) )
3 2 eqeq1d
 |-  ( x = 0 -> ( dom ( ( CC Dn F ) ` x ) = dom F <-> dom ( ( CC Dn F ) ` 0 ) = dom F ) )
4 fveq2
 |-  ( x = 0 -> ( ( S Dn ( F |` S ) ) ` x ) = ( ( S Dn ( F |` S ) ) ` 0 ) )
5 1 reseq1d
 |-  ( x = 0 -> ( ( ( CC Dn F ) ` x ) |` S ) = ( ( ( CC Dn F ) ` 0 ) |` S ) )
6 4 5 eqeq12d
 |-  ( x = 0 -> ( ( ( S Dn ( F |` S ) ) ` x ) = ( ( ( CC Dn F ) ` x ) |` S ) <-> ( ( S Dn ( F |` S ) ) ` 0 ) = ( ( ( CC Dn F ) ` 0 ) |` S ) ) )
7 3 6 imbi12d
 |-  ( x = 0 -> ( ( dom ( ( CC Dn F ) ` x ) = dom F -> ( ( S Dn ( F |` S ) ) ` x ) = ( ( ( CC Dn F ) ` x ) |` S ) ) <-> ( dom ( ( CC Dn F ) ` 0 ) = dom F -> ( ( S Dn ( F |` S ) ) ` 0 ) = ( ( ( CC Dn F ) ` 0 ) |` S ) ) ) )
8 7 imbi2d
 |-  ( x = 0 -> ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) -> ( dom ( ( CC Dn F ) ` x ) = dom F -> ( ( S Dn ( F |` S ) ) ` x ) = ( ( ( CC Dn F ) ` x ) |` S ) ) ) <-> ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) -> ( dom ( ( CC Dn F ) ` 0 ) = dom F -> ( ( S Dn ( F |` S ) ) ` 0 ) = ( ( ( CC Dn F ) ` 0 ) |` S ) ) ) ) )
9 fveq2
 |-  ( x = n -> ( ( CC Dn F ) ` x ) = ( ( CC Dn F ) ` n ) )
10 9 dmeqd
 |-  ( x = n -> dom ( ( CC Dn F ) ` x ) = dom ( ( CC Dn F ) ` n ) )
11 10 eqeq1d
 |-  ( x = n -> ( dom ( ( CC Dn F ) ` x ) = dom F <-> dom ( ( CC Dn F ) ` n ) = dom F ) )
12 fveq2
 |-  ( x = n -> ( ( S Dn ( F |` S ) ) ` x ) = ( ( S Dn ( F |` S ) ) ` n ) )
13 9 reseq1d
 |-  ( x = n -> ( ( ( CC Dn F ) ` x ) |` S ) = ( ( ( CC Dn F ) ` n ) |` S ) )
14 12 13 eqeq12d
 |-  ( x = n -> ( ( ( S Dn ( F |` S ) ) ` x ) = ( ( ( CC Dn F ) ` x ) |` S ) <-> ( ( S Dn ( F |` S ) ) ` n ) = ( ( ( CC Dn F ) ` n ) |` S ) ) )
15 11 14 imbi12d
 |-  ( x = n -> ( ( dom ( ( CC Dn F ) ` x ) = dom F -> ( ( S Dn ( F |` S ) ) ` x ) = ( ( ( CC Dn F ) ` x ) |` S ) ) <-> ( dom ( ( CC Dn F ) ` n ) = dom F -> ( ( S Dn ( F |` S ) ) ` n ) = ( ( ( CC Dn F ) ` n ) |` S ) ) ) )
16 15 imbi2d
 |-  ( x = n -> ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) -> ( dom ( ( CC Dn F ) ` x ) = dom F -> ( ( S Dn ( F |` S ) ) ` x ) = ( ( ( CC Dn F ) ` x ) |` S ) ) ) <-> ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) -> ( dom ( ( CC Dn F ) ` n ) = dom F -> ( ( S Dn ( F |` S ) ) ` n ) = ( ( ( CC Dn F ) ` n ) |` S ) ) ) ) )
17 fveq2
 |-  ( x = ( n + 1 ) -> ( ( CC Dn F ) ` x ) = ( ( CC Dn F ) ` ( n + 1 ) ) )
18 17 dmeqd
 |-  ( x = ( n + 1 ) -> dom ( ( CC Dn F ) ` x ) = dom ( ( CC Dn F ) ` ( n + 1 ) ) )
19 18 eqeq1d
 |-  ( x = ( n + 1 ) -> ( dom ( ( CC Dn F ) ` x ) = dom F <-> dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) )
20 fveq2
 |-  ( x = ( n + 1 ) -> ( ( S Dn ( F |` S ) ) ` x ) = ( ( S Dn ( F |` S ) ) ` ( n + 1 ) ) )
21 17 reseq1d
 |-  ( x = ( n + 1 ) -> ( ( ( CC Dn F ) ` x ) |` S ) = ( ( ( CC Dn F ) ` ( n + 1 ) ) |` S ) )
22 20 21 eqeq12d
 |-  ( x = ( n + 1 ) -> ( ( ( S Dn ( F |` S ) ) ` x ) = ( ( ( CC Dn F ) ` x ) |` S ) <-> ( ( S Dn ( F |` S ) ) ` ( n + 1 ) ) = ( ( ( CC Dn F ) ` ( n + 1 ) ) |` S ) ) )
23 19 22 imbi12d
 |-  ( x = ( n + 1 ) -> ( ( dom ( ( CC Dn F ) ` x ) = dom F -> ( ( S Dn ( F |` S ) ) ` x ) = ( ( ( CC Dn F ) ` x ) |` S ) ) <-> ( dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F -> ( ( S Dn ( F |` S ) ) ` ( n + 1 ) ) = ( ( ( CC Dn F ) ` ( n + 1 ) ) |` S ) ) ) )
24 23 imbi2d
 |-  ( x = ( n + 1 ) -> ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) -> ( dom ( ( CC Dn F ) ` x ) = dom F -> ( ( S Dn ( F |` S ) ) ` x ) = ( ( ( CC Dn F ) ` x ) |` S ) ) ) <-> ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) -> ( dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F -> ( ( S Dn ( F |` S ) ) ` ( n + 1 ) ) = ( ( ( CC Dn F ) ` ( n + 1 ) ) |` S ) ) ) ) )
25 fveq2
 |-  ( x = N -> ( ( CC Dn F ) ` x ) = ( ( CC Dn F ) ` N ) )
26 25 dmeqd
 |-  ( x = N -> dom ( ( CC Dn F ) ` x ) = dom ( ( CC Dn F ) ` N ) )
27 26 eqeq1d
 |-  ( x = N -> ( dom ( ( CC Dn F ) ` x ) = dom F <-> dom ( ( CC Dn F ) ` N ) = dom F ) )
28 fveq2
 |-  ( x = N -> ( ( S Dn ( F |` S ) ) ` x ) = ( ( S Dn ( F |` S ) ) ` N ) )
29 25 reseq1d
 |-  ( x = N -> ( ( ( CC Dn F ) ` x ) |` S ) = ( ( ( CC Dn F ) ` N ) |` S ) )
30 28 29 eqeq12d
 |-  ( x = N -> ( ( ( S Dn ( F |` S ) ) ` x ) = ( ( ( CC Dn F ) ` x ) |` S ) <-> ( ( S Dn ( F |` S ) ) ` N ) = ( ( ( CC Dn F ) ` N ) |` S ) ) )
31 27 30 imbi12d
 |-  ( x = N -> ( ( dom ( ( CC Dn F ) ` x ) = dom F -> ( ( S Dn ( F |` S ) ) ` x ) = ( ( ( CC Dn F ) ` x ) |` S ) ) <-> ( dom ( ( CC Dn F ) ` N ) = dom F -> ( ( S Dn ( F |` S ) ) ` N ) = ( ( ( CC Dn F ) ` N ) |` S ) ) ) )
32 31 imbi2d
 |-  ( x = N -> ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) -> ( dom ( ( CC Dn F ) ` x ) = dom F -> ( ( S Dn ( F |` S ) ) ` x ) = ( ( ( CC Dn F ) ` x ) |` S ) ) ) <-> ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) -> ( dom ( ( CC Dn F ) ` N ) = dom F -> ( ( S Dn ( F |` S ) ) ` N ) = ( ( ( CC Dn F ) ` N ) |` S ) ) ) ) )
33 recnprss
 |-  ( S e. { RR , CC } -> S C_ CC )
34 33 adantr
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) -> S C_ CC )
35 pmresg
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) -> ( F |` S ) e. ( CC ^pm S ) )
36 dvn0
 |-  ( ( S C_ CC /\ ( F |` S ) e. ( CC ^pm S ) ) -> ( ( S Dn ( F |` S ) ) ` 0 ) = ( F |` S ) )
37 34 35 36 syl2anc
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) -> ( ( S Dn ( F |` S ) ) ` 0 ) = ( F |` S ) )
38 ssidd
 |-  ( S e. { RR , CC } -> CC C_ CC )
39 dvn0
 |-  ( ( CC C_ CC /\ F e. ( CC ^pm CC ) ) -> ( ( CC Dn F ) ` 0 ) = F )
40 38 39 sylan
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) -> ( ( CC Dn F ) ` 0 ) = F )
41 40 reseq1d
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) -> ( ( ( CC Dn F ) ` 0 ) |` S ) = ( F |` S ) )
42 37 41 eqtr4d
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) -> ( ( S Dn ( F |` S ) ) ` 0 ) = ( ( ( CC Dn F ) ` 0 ) |` S ) )
43 42 a1d
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) -> ( dom ( ( CC Dn F ) ` 0 ) = dom F -> ( ( S Dn ( F |` S ) ) ` 0 ) = ( ( ( CC Dn F ) ` 0 ) |` S ) ) )
44 cnelprrecn
 |-  CC e. { RR , CC }
45 simplr
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> F e. ( CC ^pm CC ) )
46 simprl
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> n e. NN0 )
47 dvnbss
 |-  ( ( CC e. { RR , CC } /\ F e. ( CC ^pm CC ) /\ n e. NN0 ) -> dom ( ( CC Dn F ) ` n ) C_ dom F )
48 44 45 46 47 mp3an2i
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> dom ( ( CC Dn F ) ` n ) C_ dom F )
49 simprr
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F )
50 ssidd
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> CC C_ CC )
51 dvnp1
 |-  ( ( CC C_ CC /\ F e. ( CC ^pm CC ) /\ n e. NN0 ) -> ( ( CC Dn F ) ` ( n + 1 ) ) = ( CC _D ( ( CC Dn F ) ` n ) ) )
52 50 45 46 51 syl3anc
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> ( ( CC Dn F ) ` ( n + 1 ) ) = ( CC _D ( ( CC Dn F ) ` n ) ) )
53 52 dmeqd
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom ( CC _D ( ( CC Dn F ) ` n ) ) )
54 49 53 eqtr3d
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> dom F = dom ( CC _D ( ( CC Dn F ) ` n ) ) )
55 dvnf
 |-  ( ( CC e. { RR , CC } /\ F e. ( CC ^pm CC ) /\ n e. NN0 ) -> ( ( CC Dn F ) ` n ) : dom ( ( CC Dn F ) ` n ) --> CC )
56 44 45 46 55 mp3an2i
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> ( ( CC Dn F ) ` n ) : dom ( ( CC Dn F ) ` n ) --> CC )
57 cnex
 |-  CC e. _V
58 57 57 elpm2
 |-  ( F e. ( CC ^pm CC ) <-> ( F : dom F --> CC /\ dom F C_ CC ) )
59 58 simprbi
 |-  ( F e. ( CC ^pm CC ) -> dom F C_ CC )
60 45 59 syl
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> dom F C_ CC )
61 48 60 sstrd
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> dom ( ( CC Dn F ) ` n ) C_ CC )
62 50 56 61 dvbss
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> dom ( CC _D ( ( CC Dn F ) ` n ) ) C_ dom ( ( CC Dn F ) ` n ) )
63 54 62 eqsstrd
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> dom F C_ dom ( ( CC Dn F ) ` n ) )
64 48 63 eqssd
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> dom ( ( CC Dn F ) ` n ) = dom F )
65 64 expr
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ n e. NN0 ) -> ( dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F -> dom ( ( CC Dn F ) ` n ) = dom F ) )
66 65 imim1d
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ n e. NN0 ) -> ( ( dom ( ( CC Dn F ) ` n ) = dom F -> ( ( S Dn ( F |` S ) ) ` n ) = ( ( ( CC Dn F ) ` n ) |` S ) ) -> ( dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F -> ( ( S Dn ( F |` S ) ) ` n ) = ( ( ( CC Dn F ) ` n ) |` S ) ) ) )
67 oveq2
 |-  ( ( ( S Dn ( F |` S ) ) ` n ) = ( ( ( CC Dn F ) ` n ) |` S ) -> ( S _D ( ( S Dn ( F |` S ) ) ` n ) ) = ( S _D ( ( ( CC Dn F ) ` n ) |` S ) ) )
68 34 adantr
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> S C_ CC )
69 35 adantr
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> ( F |` S ) e. ( CC ^pm S ) )
70 dvnp1
 |-  ( ( S C_ CC /\ ( F |` S ) e. ( CC ^pm S ) /\ n e. NN0 ) -> ( ( S Dn ( F |` S ) ) ` ( n + 1 ) ) = ( S _D ( ( S Dn ( F |` S ) ) ` n ) ) )
71 68 69 46 70 syl3anc
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> ( ( S Dn ( F |` S ) ) ` ( n + 1 ) ) = ( S _D ( ( S Dn ( F |` S ) ) ` n ) ) )
72 52 reseq1d
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> ( ( ( CC Dn F ) ` ( n + 1 ) ) |` S ) = ( ( CC _D ( ( CC Dn F ) ` n ) ) |` S ) )
73 simpll
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> S e. { RR , CC } )
74 eqid
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
75 74 cnfldtop
 |-  ( TopOpen ` CCfld ) e. Top
76 unicntop
 |-  CC = U. ( TopOpen ` CCfld )
77 76 ntrss2
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ dom ( ( CC Dn F ) ` n ) C_ CC ) -> ( ( int ` ( TopOpen ` CCfld ) ) ` dom ( ( CC Dn F ) ` n ) ) C_ dom ( ( CC Dn F ) ` n ) )
78 75 61 77 sylancr
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> ( ( int ` ( TopOpen ` CCfld ) ) ` dom ( ( CC Dn F ) ` n ) ) C_ dom ( ( CC Dn F ) ` n ) )
79 74 cnfldtopon
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
80 79 toponrestid
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
81 50 56 61 80 74 dvbssntr
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> dom ( CC _D ( ( CC Dn F ) ` n ) ) C_ ( ( int ` ( TopOpen ` CCfld ) ) ` dom ( ( CC Dn F ) ` n ) ) )
82 54 81 eqsstrd
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> dom F C_ ( ( int ` ( TopOpen ` CCfld ) ) ` dom ( ( CC Dn F ) ` n ) ) )
83 48 82 sstrd
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> dom ( ( CC Dn F ) ` n ) C_ ( ( int ` ( TopOpen ` CCfld ) ) ` dom ( ( CC Dn F ) ` n ) ) )
84 78 83 eqssd
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> ( ( int ` ( TopOpen ` CCfld ) ) ` dom ( ( CC Dn F ) ` n ) ) = dom ( ( CC Dn F ) ` n ) )
85 76 isopn3
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ dom ( ( CC Dn F ) ` n ) C_ CC ) -> ( dom ( ( CC Dn F ) ` n ) e. ( TopOpen ` CCfld ) <-> ( ( int ` ( TopOpen ` CCfld ) ) ` dom ( ( CC Dn F ) ` n ) ) = dom ( ( CC Dn F ) ` n ) ) )
86 75 61 85 sylancr
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> ( dom ( ( CC Dn F ) ` n ) e. ( TopOpen ` CCfld ) <-> ( ( int ` ( TopOpen ` CCfld ) ) ` dom ( ( CC Dn F ) ` n ) ) = dom ( ( CC Dn F ) ` n ) ) )
87 84 86 mpbird
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> dom ( ( CC Dn F ) ` n ) e. ( TopOpen ` CCfld ) )
88 64 54 eqtr2d
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> dom ( CC _D ( ( CC Dn F ) ` n ) ) = dom ( ( CC Dn F ) ` n ) )
89 74 dvres3a
 |-  ( ( ( S e. { RR , CC } /\ ( ( CC Dn F ) ` n ) : dom ( ( CC Dn F ) ` n ) --> CC ) /\ ( dom ( ( CC Dn F ) ` n ) e. ( TopOpen ` CCfld ) /\ dom ( CC _D ( ( CC Dn F ) ` n ) ) = dom ( ( CC Dn F ) ` n ) ) ) -> ( S _D ( ( ( CC Dn F ) ` n ) |` S ) ) = ( ( CC _D ( ( CC Dn F ) ` n ) ) |` S ) )
90 73 56 87 88 89 syl22anc
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> ( S _D ( ( ( CC Dn F ) ` n ) |` S ) ) = ( ( CC _D ( ( CC Dn F ) ` n ) ) |` S ) )
91 72 90 eqtr4d
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> ( ( ( CC Dn F ) ` ( n + 1 ) ) |` S ) = ( S _D ( ( ( CC Dn F ) ` n ) |` S ) ) )
92 71 91 eqeq12d
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> ( ( ( S Dn ( F |` S ) ) ` ( n + 1 ) ) = ( ( ( CC Dn F ) ` ( n + 1 ) ) |` S ) <-> ( S _D ( ( S Dn ( F |` S ) ) ` n ) ) = ( S _D ( ( ( CC Dn F ) ` n ) |` S ) ) ) )
93 67 92 syl5ibr
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) /\ ( n e. NN0 /\ dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F ) ) -> ( ( ( S Dn ( F |` S ) ) ` n ) = ( ( ( CC Dn F ) ` n ) |` S ) -> ( ( S Dn ( F |` S ) ) ` ( n + 1 ) ) = ( ( ( CC Dn F ) ` ( n + 1 ) ) |` S ) ) )
94 66 93 animpimp2impd
 |-  ( n e. NN0 -> ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) -> ( dom ( ( CC Dn F ) ` n ) = dom F -> ( ( S Dn ( F |` S ) ) ` n ) = ( ( ( CC Dn F ) ` n ) |` S ) ) ) -> ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) -> ( dom ( ( CC Dn F ) ` ( n + 1 ) ) = dom F -> ( ( S Dn ( F |` S ) ) ` ( n + 1 ) ) = ( ( ( CC Dn F ) ` ( n + 1 ) ) |` S ) ) ) ) )
95 8 16 24 32 43 94 nn0ind
 |-  ( N e. NN0 -> ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) -> ( dom ( ( CC Dn F ) ` N ) = dom F -> ( ( S Dn ( F |` S ) ) ` N ) = ( ( ( CC Dn F ) ` N ) |` S ) ) ) )
96 95 com12
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) -> ( N e. NN0 -> ( dom ( ( CC Dn F ) ` N ) = dom F -> ( ( S Dn ( F |` S ) ) ` N ) = ( ( ( CC Dn F ) ` N ) |` S ) ) ) )
97 96 3impia
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) /\ N e. NN0 ) -> ( dom ( ( CC Dn F ) ` N ) = dom F -> ( ( S Dn ( F |` S ) ) ` N ) = ( ( ( CC Dn F ) ` N ) |` S ) ) )
98 97 imp
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) /\ N e. NN0 ) /\ dom ( ( CC Dn F ) ` N ) = dom F ) -> ( ( S Dn ( F |` S ) ) ` N ) = ( ( ( CC Dn F ) ` N ) |` S ) )