This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrrid 
 |-  ( ( ( 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 ) )