Metamath Proof Explorer

Theorem dvres2lem

Description: Lemma for dvres2 . (Contributed by Mario Carneiro, 9-Feb-2015) (Revised by Mario Carneiro, 28-Dec-2016)

Ref Expression
Hypotheses dvres.k 
|- K = ( TopOpen ` CCfld )
dvres.t 
|- T = ( K |`t S )
dvres.g 
|- G = ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) )
dvres.s 
|- ( ph -> S C_ CC )
dvres.f 
|- ( ph -> F : A --> CC )
dvres.a 
|- ( ph -> A C_ S )
dvres.b 
|- ( ph -> B C_ S )
dvres.y 
|- ( ph -> y e. CC )
dvres2lem.d 
|- ( ph -> x ( S _D F ) y )
dvres2lem.x 
|- ( ph -> x e. B )
Assertion dvres2lem 
|- ( ph -> x ( B _D ( F |` B ) ) y )

Proof

Step Hyp Ref Expression
1 dvres.k 
 |-  K = ( TopOpen ` CCfld )
2 dvres.t 
 |-  T = ( K |`t S )
3 dvres.g 
 |-  G = ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) )
4 dvres.s 
 |-  ( ph -> S C_ CC )
5 dvres.f 
 |-  ( ph -> F : A --> CC )
6 dvres.a 
 |-  ( ph -> A C_ S )
7 dvres.b 
 |-  ( ph -> B C_ S )
8 dvres.y 
 |-  ( ph -> y e. CC )
9 dvres2lem.d 
 |-  ( ph -> x ( S _D F ) y )
10 dvres2lem.x 
 |-  ( ph -> x e. B )
11 1 cnfldtop 
 |-  K e. Top
12 cnex 
 |-  CC e. _V
13 ssexg 
 |-  ( ( S C_ CC /\ CC e. _V ) -> S e. _V )
14 4 12 13 sylancl 
 |-  ( ph -> S e. _V )
15 resttop 
 |-  ( ( K e. Top /\ S e. _V ) -> ( K |`t S ) e. Top )
16 11 14 15 sylancr 
 |-  ( ph -> ( K |`t S ) e. Top )
17 2 16 eqeltrid 
 |-  ( ph -> T e. Top )
18 inss1 
 |-  ( A i^i B ) C_ A
19 18 6 sstrid 
 |-  ( ph -> ( A i^i B ) C_ S )
20 1 cnfldtopon 
 |-  K e. ( TopOn ` CC )
21 resttopon 
 |-  ( ( K e. ( TopOn ` CC ) /\ S C_ CC ) -> ( K |`t S ) e. ( TopOn ` S ) )
22 20 4 21 sylancr 
 |-  ( ph -> ( K |`t S ) e. ( TopOn ` S ) )
23 2 22 eqeltrid 
 |-  ( ph -> T e. ( TopOn ` S ) )
24 toponuni 
 |-  ( T e. ( TopOn ` S ) -> S = U. T )
25 23 24 syl 
 |-  ( ph -> S = U. T )
26 19 25 sseqtrd 
 |-  ( ph -> ( A i^i B ) C_ U. T )
27 difssd 
 |-  ( ph -> ( U. T \ B ) C_ U. T )
28 26 27 unssd 
 |-  ( ph -> ( ( A i^i B ) u. ( U. T \ B ) ) C_ U. T )
29 inundif 
 |-  ( ( A i^i B ) u. ( A \ B ) ) = A
30 6 25 sseqtrd 
 |-  ( ph -> A C_ U. T )
31 ssdif 
 |-  ( A C_ U. T -> ( A \ B ) C_ ( U. T \ B ) )
32 unss2 
 |-  ( ( A \ B ) C_ ( U. T \ B ) -> ( ( A i^i B ) u. ( A \ B ) ) C_ ( ( A i^i B ) u. ( U. T \ B ) ) )
33 30 31 32 3syl 
 |-  ( ph -> ( ( A i^i B ) u. ( A \ B ) ) C_ ( ( A i^i B ) u. ( U. T \ B ) ) )
34 29 33 eqsstrrid 
 |-  ( ph -> A C_ ( ( A i^i B ) u. ( U. T \ B ) ) )
35 eqid 
 |-  U. T = U. T
36 35 ntrss 
 |-  ( ( T e. Top /\ ( ( A i^i B ) u. ( U. T \ B ) ) C_ U. T /\ A C_ ( ( A i^i B ) u. ( U. T \ B ) ) ) -> ( ( int ` T ) ` A ) C_ ( ( int ` T ) ` ( ( A i^i B ) u. ( U. T \ B ) ) ) )
37 17 28 34 36 syl3anc 
 |-  ( ph -> ( ( int ` T ) ` A ) C_ ( ( int ` T ) ` ( ( A i^i B ) u. ( U. T \ B ) ) ) )
38 2 1 3 4 5 6 eldv 
 |-  ( ph -> ( x ( S _D F ) y <-> ( x e. ( ( int ` T ) ` A ) /\ y e. ( G limCC x ) ) ) )
39 9 38 mpbid 
 |-  ( ph -> ( x e. ( ( int ` T ) ` A ) /\ y e. ( G limCC x ) ) )
40 39 simpld 
 |-  ( ph -> x e. ( ( int ` T ) ` A ) )
41 37 40 sseldd 
 |-  ( ph -> x e. ( ( int ` T ) ` ( ( A i^i B ) u. ( U. T \ B ) ) ) )
42 41 10 elind 
 |-  ( ph -> x e. ( ( ( int ` T ) ` ( ( A i^i B ) u. ( U. T \ B ) ) ) i^i B ) )
43 7 25 sseqtrd 
 |-  ( ph -> B C_ U. T )
44 inss2 
 |-  ( A i^i B ) C_ B
45 44 a1i 
 |-  ( ph -> ( A i^i B ) C_ B )
46 eqid 
 |-  ( T |`t B ) = ( T |`t B )
47 35 46 restntr 
 |-  ( ( T e. Top /\ B C_ U. T /\ ( A i^i B ) C_ B ) -> ( ( int ` ( T |`t B ) ) ` ( A i^i B ) ) = ( ( ( int ` T ) ` ( ( A i^i B ) u. ( U. T \ B ) ) ) i^i B ) )
48 17 43 45 47 syl3anc 
 |-  ( ph -> ( ( int ` ( T |`t B ) ) ` ( A i^i B ) ) = ( ( ( int ` T ) ` ( ( A i^i B ) u. ( U. T \ B ) ) ) i^i B ) )
49 2 oveq1i 
 |-  ( T |`t B ) = ( ( K |`t S ) |`t B )
50 11 a1i 
 |-  ( ph -> K e. Top )
51 restabs 
 |-  ( ( K e. Top /\ B C_ S /\ S e. _V ) -> ( ( K |`t S ) |`t B ) = ( K |`t B ) )
52 50 7 14 51 syl3anc 
 |-  ( ph -> ( ( K |`t S ) |`t B ) = ( K |`t B ) )
53 49 52 eqtrid 
 |-  ( ph -> ( T |`t B ) = ( K |`t B ) )
54 53 fveq2d 
 |-  ( ph -> ( int ` ( T |`t B ) ) = ( int ` ( K |`t B ) ) )
55 54 fveq1d 
 |-  ( ph -> ( ( int ` ( T |`t B ) ) ` ( A i^i B ) ) = ( ( int ` ( K |`t B ) ) ` ( A i^i B ) ) )
56 48 55 eqtr3d 
 |-  ( ph -> ( ( ( int ` T ) ` ( ( A i^i B ) u. ( U. T \ B ) ) ) i^i B ) = ( ( int ` ( K |`t B ) ) ` ( A i^i B ) ) )
57 42 56 eleqtrd 
 |-  ( ph -> x e. ( ( int ` ( K |`t B ) ) ` ( A i^i B ) ) )
58 limcresi 
 |-  ( G limCC x ) C_ ( ( G |` ( ( A i^i B ) \ { x } ) ) limCC x )
59 39 simprd 
 |-  ( ph -> y e. ( G limCC x ) )
60 58 59 sselid 
 |-  ( ph -> y e. ( ( G |` ( ( A i^i B ) \ { x } ) ) limCC x ) )
61 difss 
 |-  ( ( A i^i B ) \ { x } ) C_ ( A i^i B )
62 61 44 sstri 
 |-  ( ( A i^i B ) \ { x } ) C_ B
63 62 sseli 
 |-  ( z e. ( ( A i^i B ) \ { x } ) -> z e. B )
64 fvres 
 |-  ( z e. B -> ( ( F |` B ) ` z ) = ( F ` z ) )
65 10 fvresd 
 |-  ( ph -> ( ( F |` B ) ` x ) = ( F ` x ) )
66 64 65 oveqan12rd 
 |-  ( ( ph /\ z e. B ) -> ( ( ( F |` B ) ` z ) - ( ( F |` B ) ` x ) ) = ( ( F ` z ) - ( F ` x ) ) )
67 66 oveq1d 
 |-  ( ( ph /\ z e. B ) -> ( ( ( ( F |` B ) ` z ) - ( ( F |` B ) ` x ) ) / ( z - x ) ) = ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) )
68 63 67 sylan2 
 |-  ( ( ph /\ z e. ( ( A i^i B ) \ { x } ) ) -> ( ( ( ( F |` B ) ` z ) - ( ( F |` B ) ` x ) ) / ( z - x ) ) = ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) )
69 68 mpteq2dva 
 |-  ( ph -> ( z e. ( ( A i^i B ) \ { x } ) |-> ( ( ( ( F |` B ) ` z ) - ( ( F |` B ) ` x ) ) / ( z - x ) ) ) = ( z e. ( ( A i^i B ) \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) )
70 3 reseq1i 
 |-  ( G |` ( ( A i^i B ) \ { x } ) ) = ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) |` ( ( A i^i B ) \ { x } ) )
71 ssdif 
 |-  ( ( A i^i B ) C_ A -> ( ( A i^i B ) \ { x } ) C_ ( A \ { x } ) )
72 resmpt 
 |-  ( ( ( A i^i B ) \ { x } ) C_ ( A \ { x } ) -> ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) |` ( ( A i^i B ) \ { x } ) ) = ( z e. ( ( A i^i B ) \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) )
73 18 71 72 mp2b 
 |-  ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) |` ( ( A i^i B ) \ { x } ) ) = ( z e. ( ( A i^i B ) \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) )
74 70 73 eqtri 
 |-  ( G |` ( ( A i^i B ) \ { x } ) ) = ( z e. ( ( A i^i B ) \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) )
75 69 74 eqtr4di 
 |-  ( ph -> ( z e. ( ( A i^i B ) \ { x } ) |-> ( ( ( ( F |` B ) ` z ) - ( ( F |` B ) ` x ) ) / ( z - x ) ) ) = ( G |` ( ( A i^i B ) \ { x } ) ) )
76 75 oveq1d 
 |-  ( ph -> ( ( z e. ( ( A i^i B ) \ { x } ) |-> ( ( ( ( F |` B ) ` z ) - ( ( F |` B ) ` x ) ) / ( z - x ) ) ) limCC x ) = ( ( G |` ( ( A i^i B ) \ { x } ) ) limCC x ) )
77 60 76 eleqtrrd 
 |-  ( ph -> y e. ( ( z e. ( ( A i^i B ) \ { x } ) |-> ( ( ( ( F |` B ) ` z ) - ( ( F |` B ) ` x ) ) / ( z - x ) ) ) limCC x ) )
78 eqid 
 |-  ( K |`t B ) = ( K |`t B )
79 eqid 
 |-  ( z e. ( ( A i^i B ) \ { x } ) |-> ( ( ( ( F |` B ) ` z ) - ( ( F |` B ) ` x ) ) / ( z - x ) ) ) = ( z e. ( ( A i^i B ) \ { x } ) |-> ( ( ( ( F |` B ) ` z ) - ( ( F |` B ) ` x ) ) / ( z - x ) ) )
80 7 4 sstrd 
 |-  ( ph -> B C_ CC )
81 fresin 
 |-  ( F : A --> CC -> ( F |` B ) : ( A i^i B ) --> CC )
82 5 81 syl 
 |-  ( ph -> ( F |` B ) : ( A i^i B ) --> CC )
83 78 1 79 80 82 45 eldv 
 |-  ( ph -> ( x ( B _D ( F |` B ) ) y <-> ( x e. ( ( int ` ( K |`t B ) ) ` ( A i^i B ) ) /\ y e. ( ( z e. ( ( A i^i B ) \ { x } ) |-> ( ( ( ( F |` B ) ` z ) - ( ( F |` B ) ` x ) ) / ( z - x ) ) ) limCC x ) ) ) )
84 57 77 83 mpbir2and 
 |-  ( ph -> x ( B _D ( F |` B ) ) y )