Metamath Proof Explorer

Theorem dvreslem

Description: Lemma for dvres . (Contributed by Mario Carneiro, 8-Aug-2014) (Revised by Mario Carneiro, 28-Dec-2016) Commute the consequent and shorten proof. (Revised by Peter Mazsa, 2-Oct-2022)

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 )
Assertion dvreslem 
|- ( ph -> ( x ( S _D ( F |` B ) ) y <-> ( x e. ( ( int ` T ) ` B ) /\ x ( S _D F ) 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 difss 
 |-  ( ( A i^i B ) \ { x } ) C_ ( A i^i B )
10 inss2 
 |-  ( A i^i B ) C_ B
11 9 10 sstri 
 |-  ( ( A i^i B ) \ { x } ) C_ B
12 simpr 
 |-  ( ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) /\ z e. ( ( A i^i B ) \ { x } ) ) -> z e. ( ( A i^i B ) \ { x } ) )
13 11 12 sseldi 
 |-  ( ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) /\ z e. ( ( A i^i B ) \ { x } ) ) -> z e. B )
14 13 fvresd 
 |-  ( ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) /\ z e. ( ( A i^i B ) \ { x } ) ) -> ( ( F |` B ) ` z ) = ( F ` z ) )
15 1 cnfldtop 
 |-  K e. Top
16 cnex 
 |-  CC e. _V
17 ssexg 
 |-  ( ( S C_ CC /\ CC e. _V ) -> S e. _V )
18 4 16 17 sylancl 
 |-  ( ph -> S e. _V )
19 resttop 
 |-  ( ( K e. Top /\ S e. _V ) -> ( K |`t S ) e. Top )
20 15 18 19 sylancr 
 |-  ( ph -> ( K |`t S ) e. Top )
21 2 20 eqeltrid 
 |-  ( ph -> T e. Top )
22 inss1 
 |-  ( A i^i B ) C_ A
23 22 6 sstrid 
 |-  ( ph -> ( A i^i B ) C_ S )
24 1 cnfldtopon 
 |-  K e. ( TopOn ` CC )
25 resttopon 
 |-  ( ( K e. ( TopOn ` CC ) /\ S C_ CC ) -> ( K |`t S ) e. ( TopOn ` S ) )
26 24 4 25 sylancr 
 |-  ( ph -> ( K |`t S ) e. ( TopOn ` S ) )
27 2 26 eqeltrid 
 |-  ( ph -> T e. ( TopOn ` S ) )
28 toponuni 
 |-  ( T e. ( TopOn ` S ) -> S = U. T )
29 27 28 syl 
 |-  ( ph -> S = U. T )
30 23 29 sseqtrd 
 |-  ( ph -> ( A i^i B ) C_ U. T )
31 eqid 
 |-  U. T = U. T
32 31 ntrss2 
 |-  ( ( T e. Top /\ ( A i^i B ) C_ U. T ) -> ( ( int ` T ) ` ( A i^i B ) ) C_ ( A i^i B ) )
33 21 30 32 syl2anc 
 |-  ( ph -> ( ( int ` T ) ` ( A i^i B ) ) C_ ( A i^i B ) )
34 33 10 sstrdi 
 |-  ( ph -> ( ( int ` T ) ` ( A i^i B ) ) C_ B )
35 34 sselda 
 |-  ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) -> x e. B )
36 35 fvresd 
 |-  ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) -> ( ( F |` B ) ` x ) = ( F ` x ) )
37 36 adantr 
 |-  ( ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) /\ z e. ( ( A i^i B ) \ { x } ) ) -> ( ( F |` B ) ` x ) = ( F ` x ) )
38 14 37 oveq12d 
 |-  ( ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) /\ z e. ( ( A i^i B ) \ { x } ) ) -> ( ( ( F |` B ) ` z ) - ( ( F |` B ) ` x ) ) = ( ( F ` z ) - ( F ` x ) ) )
39 38 oveq1d 
 |-  ( ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) /\ z e. ( ( A i^i B ) \ { x } ) ) -> ( ( ( ( F |` B ) ` z ) - ( ( F |` B ) ` x ) ) / ( z - x ) ) = ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) )
40 39 mpteq2dva 
 |-  ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) -> ( 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 ) ) ) )
41 3 reseq1i 
 |-  ( G |` ( ( A i^i B ) \ { x } ) ) = ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) |` ( ( A i^i B ) \ { x } ) )
42 ssdif 
 |-  ( ( A i^i B ) C_ A -> ( ( A i^i B ) \ { x } ) C_ ( A \ { x } ) )
43 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 ) ) ) )
44 22 42 43 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 ) ) )
45 41 44 eqtri 
 |-  ( G |` ( ( A i^i B ) \ { x } ) ) = ( z e. ( ( A i^i B ) \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) )
46 40 45 eqtr4di 
 |-  ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) -> ( z e. ( ( A i^i B ) \ { x } ) |-> ( ( ( ( F |` B ) ` z ) - ( ( F |` B ) ` x ) ) / ( z - x ) ) ) = ( G |` ( ( A i^i B ) \ { x } ) ) )
47 46 oveq1d 
 |-  ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) -> ( ( 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 ) )
48 5 adantr 
 |-  ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) -> F : A --> CC )
49 6 4 sstrd 
 |-  ( ph -> A C_ CC )
50 49 adantr 
 |-  ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) -> A C_ CC )
51 33 22 sstrdi 
 |-  ( ph -> ( ( int ` T ) ` ( A i^i B ) ) C_ A )
52 51 sselda 
 |-  ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) -> x e. A )
53 48 50 52 dvlem 
 |-  ( ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) /\ z e. ( A \ { x } ) ) -> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) e. CC )
54 53 3 fmptd 
 |-  ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) -> G : ( A \ { x } ) --> CC )
55 22 42 mp1i 
 |-  ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) -> ( ( A i^i B ) \ { x } ) C_ ( A \ { x } ) )
56 difss 
 |-  ( A \ { x } ) C_ A
57 56 50 sstrid 
 |-  ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) -> ( A \ { x } ) C_ CC )
58 eqid 
 |-  ( K |`t ( ( A \ { x } ) u. { x } ) ) = ( K |`t ( ( A \ { x } ) u. { x } ) )
59 difssd 
 |-  ( ph -> ( U. T \ A ) C_ U. T )
60 30 59 unssd 
 |-  ( ph -> ( ( A i^i B ) u. ( U. T \ A ) ) C_ U. T )
61 ssun1 
 |-  ( A i^i B ) C_ ( ( A i^i B ) u. ( U. T \ A ) )
62 61 a1i 
 |-  ( ph -> ( A i^i B ) C_ ( ( A i^i B ) u. ( U. T \ A ) ) )
63 31 ntrss 
 |-  ( ( T e. Top /\ ( ( A i^i B ) u. ( U. T \ A ) ) C_ U. T /\ ( A i^i B ) C_ ( ( A i^i B ) u. ( U. T \ A ) ) ) -> ( ( int ` T ) ` ( A i^i B ) ) C_ ( ( int ` T ) ` ( ( A i^i B ) u. ( U. T \ A ) ) ) )
64 21 60 62 63 syl3anc 
 |-  ( ph -> ( ( int ` T ) ` ( A i^i B ) ) C_ ( ( int ` T ) ` ( ( A i^i B ) u. ( U. T \ A ) ) ) )
65 64 51 ssind 
 |-  ( ph -> ( ( int ` T ) ` ( A i^i B ) ) C_ ( ( ( int ` T ) ` ( ( A i^i B ) u. ( U. T \ A ) ) ) i^i A ) )
66 6 29 sseqtrd 
 |-  ( ph -> A C_ U. T )
67 22 a1i 
 |-  ( ph -> ( A i^i B ) C_ A )
68 eqid 
 |-  ( T |`t A ) = ( T |`t A )
69 31 68 restntr 
 |-  ( ( T e. Top /\ A C_ U. T /\ ( A i^i B ) C_ A ) -> ( ( int ` ( T |`t A ) ) ` ( A i^i B ) ) = ( ( ( int ` T ) ` ( ( A i^i B ) u. ( U. T \ A ) ) ) i^i A ) )
70 21 66 67 69 syl3anc 
 |-  ( ph -> ( ( int ` ( T |`t A ) ) ` ( A i^i B ) ) = ( ( ( int ` T ) ` ( ( A i^i B ) u. ( U. T \ A ) ) ) i^i A ) )
71 2 oveq1i 
 |-  ( T |`t A ) = ( ( K |`t S ) |`t A )
72 15 a1i 
 |-  ( ph -> K e. Top )
73 restabs 
 |-  ( ( K e. Top /\ A C_ S /\ S e. _V ) -> ( ( K |`t S ) |`t A ) = ( K |`t A ) )
74 72 6 18 73 syl3anc 
 |-  ( ph -> ( ( K |`t S ) |`t A ) = ( K |`t A ) )
75 71 74 syl5eq 
 |-  ( ph -> ( T |`t A ) = ( K |`t A ) )
76 75 fveq2d 
 |-  ( ph -> ( int ` ( T |`t A ) ) = ( int ` ( K |`t A ) ) )
77 76 fveq1d 
 |-  ( ph -> ( ( int ` ( T |`t A ) ) ` ( A i^i B ) ) = ( ( int ` ( K |`t A ) ) ` ( A i^i B ) ) )
78 70 77 eqtr3d 
 |-  ( ph -> ( ( ( int ` T ) ` ( ( A i^i B ) u. ( U. T \ A ) ) ) i^i A ) = ( ( int ` ( K |`t A ) ) ` ( A i^i B ) ) )
79 65 78 sseqtrd 
 |-  ( ph -> ( ( int ` T ) ` ( A i^i B ) ) C_ ( ( int ` ( K |`t A ) ) ` ( A i^i B ) ) )
80 79 sselda 
 |-  ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) -> x e. ( ( int ` ( K |`t A ) ) ` ( A i^i B ) ) )
81 undif1 
 |-  ( ( A \ { x } ) u. { x } ) = ( A u. { x } )
82 33 sselda 
 |-  ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) -> x e. ( A i^i B ) )
83 82 snssd 
 |-  ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) -> { x } C_ ( A i^i B ) )
84 83 22 sstrdi 
 |-  ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) -> { x } C_ A )
85 ssequn2 
 |-  ( { x } C_ A <-> ( A u. { x } ) = A )
86 84 85 sylib 
 |-  ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) -> ( A u. { x } ) = A )
87 81 86 syl5eq 
 |-  ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) -> ( ( A \ { x } ) u. { x } ) = A )
88 87 oveq2d 
 |-  ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) -> ( K |`t ( ( A \ { x } ) u. { x } ) ) = ( K |`t A ) )
89 88 fveq2d 
 |-  ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) -> ( int ` ( K |`t ( ( A \ { x } ) u. { x } ) ) ) = ( int ` ( K |`t A ) ) )
90 undif1 
 |-  ( ( ( A i^i B ) \ { x } ) u. { x } ) = ( ( A i^i B ) u. { x } )
91 ssequn2 
 |-  ( { x } C_ ( A i^i B ) <-> ( ( A i^i B ) u. { x } ) = ( A i^i B ) )
92 83 91 sylib 
 |-  ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) -> ( ( A i^i B ) u. { x } ) = ( A i^i B ) )
93 90 92 syl5eq 
 |-  ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) -> ( ( ( A i^i B ) \ { x } ) u. { x } ) = ( A i^i B ) )
94 89 93 fveq12d 
 |-  ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) -> ( ( int ` ( K |`t ( ( A \ { x } ) u. { x } ) ) ) ` ( ( ( A i^i B ) \ { x } ) u. { x } ) ) = ( ( int ` ( K |`t A ) ) ` ( A i^i B ) ) )
95 80 94 eleqtrrd 
 |-  ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) -> x e. ( ( int ` ( K |`t ( ( A \ { x } ) u. { x } ) ) ) ` ( ( ( A i^i B ) \ { x } ) u. { x } ) ) )
96 54 55 57 1 58 95 limcres 
 |-  ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) -> ( ( G |` ( ( A i^i B ) \ { x } ) ) limCC x ) = ( G limCC x ) )
97 47 96 eqtrd 
 |-  ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) -> ( ( z e. ( ( A i^i B ) \ { x } ) |-> ( ( ( ( F |` B ) ` z ) - ( ( F |` B ) ` x ) ) / ( z - x ) ) ) limCC x ) = ( G limCC x ) )
98 97 eleq2d 
 |-  ( ( ph /\ x e. ( ( int ` T ) ` ( A i^i B ) ) ) -> ( y e. ( ( z e. ( ( A i^i B ) \ { x } ) |-> ( ( ( ( F |` B ) ` z ) - ( ( F |` B ) ` x ) ) / ( z - x ) ) ) limCC x ) <-> y e. ( G limCC x ) ) )
99 98 pm5.32da 
 |-  ( ph -> ( ( x e. ( ( int ` T ) ` ( A i^i B ) ) /\ y e. ( ( z e. ( ( A i^i B ) \ { x } ) |-> ( ( ( ( F |` B ) ` z ) - ( ( F |` B ) ` x ) ) / ( z - x ) ) ) limCC x ) ) <-> ( x e. ( ( int ` T ) ` ( A i^i B ) ) /\ y e. ( G limCC x ) ) ) )
100 7 29 sseqtrd 
 |-  ( ph -> B C_ U. T )
101 31 ntrin 
 |-  ( ( T e. Top /\ A C_ U. T /\ B C_ U. T ) -> ( ( int ` T ) ` ( A i^i B ) ) = ( ( ( int ` T ) ` A ) i^i ( ( int ` T ) ` B ) ) )
102 21 66 100 101 syl3anc 
 |-  ( ph -> ( ( int ` T ) ` ( A i^i B ) ) = ( ( ( int ` T ) ` A ) i^i ( ( int ` T ) ` B ) ) )
103 102 eleq2d 
 |-  ( ph -> ( x e. ( ( int ` T ) ` ( A i^i B ) ) <-> x e. ( ( ( int ` T ) ` A ) i^i ( ( int ` T ) ` B ) ) ) )
104 elin 
 |-  ( x e. ( ( ( int ` T ) ` A ) i^i ( ( int ` T ) ` B ) ) <-> ( x e. ( ( int ` T ) ` A ) /\ x e. ( ( int ` T ) ` B ) ) )
105 103 104 bitrdi 
 |-  ( ph -> ( x e. ( ( int ` T ) ` ( A i^i B ) ) <-> ( x e. ( ( int ` T ) ` A ) /\ x e. ( ( int ` T ) ` B ) ) ) )
106 105 anbi1d 
 |-  ( ph -> ( ( x e. ( ( int ` T ) ` ( A i^i B ) ) /\ y e. ( G limCC x ) ) <-> ( ( x e. ( ( int ` T ) ` A ) /\ x e. ( ( int ` T ) ` B ) ) /\ y e. ( G limCC x ) ) ) )
107 99 106 bitrd 
 |-  ( ph -> ( ( x e. ( ( int ` T ) ` ( A i^i B ) ) /\ y e. ( ( z e. ( ( A i^i B ) \ { x } ) |-> ( ( ( ( F |` B ) ` z ) - ( ( F |` B ) ` x ) ) / ( z - x ) ) ) limCC x ) ) <-> ( ( x e. ( ( int ` T ) ` A ) /\ x e. ( ( int ` T ) ` B ) ) /\ y e. ( G limCC x ) ) ) )
108 an32 
 |-  ( ( ( x e. ( ( int ` T ) ` A ) /\ x e. ( ( int ` T ) ` B ) ) /\ y e. ( G limCC x ) ) <-> ( ( x e. ( ( int ` T ) ` A ) /\ y e. ( G limCC x ) ) /\ x e. ( ( int ` T ) ` B ) ) )
109 107 108 bitrdi 
 |-  ( ph -> ( ( x e. ( ( int ` T ) ` ( A i^i B ) ) /\ y e. ( ( z e. ( ( A i^i B ) \ { x } ) |-> ( ( ( ( F |` B ) ` z ) - ( ( F |` B ) ` x ) ) / ( z - x ) ) ) limCC x ) ) <-> ( ( x e. ( ( int ` T ) ` A ) /\ y e. ( G limCC x ) ) /\ x e. ( ( int ` T ) ` B ) ) ) )
110 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 ) ) )
111 fresin 
 |-  ( F : A --> CC -> ( F |` B ) : ( A i^i B ) --> CC )
112 5 111 syl 
 |-  ( ph -> ( F |` B ) : ( A i^i B ) --> CC )
113 2 1 110 4 112 23 eldv 
 |-  ( ph -> ( x ( S _D ( F |` B ) ) y <-> ( x e. ( ( int ` T ) ` ( A i^i B ) ) /\ y e. ( ( z e. ( ( A i^i B ) \ { x } ) |-> ( ( ( ( F |` B ) ` z ) - ( ( F |` B ) ` x ) ) / ( z - x ) ) ) limCC x ) ) ) )
114 2 1 3 4 5 6 eldv 
 |-  ( ph -> ( x ( S _D F ) y <-> ( x e. ( ( int ` T ) ` A ) /\ y e. ( G limCC x ) ) ) )
115 114 anbi1cd 
 |-  ( ph -> ( ( x e. ( ( int ` T ) ` B ) /\ x ( S _D F ) y ) <-> ( ( x e. ( ( int ` T ) ` A ) /\ y e. ( G limCC x ) ) /\ x e. ( ( int ` T ) ` B ) ) ) )
116 109 113 115 3bitr4d 
 |-  ( ph -> ( x ( S _D ( F |` B ) ) y <-> ( x e. ( ( int ` T ) ` B ) /\ x ( S _D F ) y ) ) )