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 ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
dvres.t ⊢ 𝑇 = ( 𝐾 ↾t 𝑆 )
dvres.g ⊢ 𝐺 = ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) )
dvres.s ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
dvres.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
dvres.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
dvres.b ⊢ ( 𝜑 → 𝐵 ⊆ 𝑆 )
dvres.y ⊢ ( 𝜑 → 𝑦 ∈ ℂ )
dvres2lem.d ⊢ ( 𝜑 → 𝑥 ( 𝑆 D 𝐹 ) 𝑦 )
dvres2lem.x ⊢ ( 𝜑 → 𝑥 ∈ 𝐵 )
Assertion dvres2lem ( 𝜑 → 𝑥 ( 𝐵 D ( 𝐹 ↾ 𝐵 ) ) 𝑦 )

Proof

Step Hyp Ref Expression
1 dvres.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
2 dvres.t ⊢ 𝑇 = ( 𝐾 ↾t 𝑆 )
3 dvres.g ⊢ 𝐺 = ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) )
4 dvres.s ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
5 dvres.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
6 dvres.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
7 dvres.b ⊢ ( 𝜑 → 𝐵 ⊆ 𝑆 )
8 dvres.y ⊢ ( 𝜑 → 𝑦 ∈ ℂ )
9 dvres2lem.d ⊢ ( 𝜑 → 𝑥 ( 𝑆 D 𝐹 ) 𝑦 )
10 dvres2lem.x ⊢ ( 𝜑 → 𝑥 ∈ 𝐵 )
11 1 cnfldtop ⊢ 𝐾 ∈ Top
12 cnex ⊢ ℂ ∈ V
13 ssexg ⊢ ( ( 𝑆 ⊆ ℂ ∧ ℂ ∈ V ) → 𝑆 ∈ V )
14 4 12 13 sylancl ⊢ ( 𝜑 → 𝑆 ∈ V )
15 resttop ⊢ ( ( 𝐾 ∈ Top ∧ 𝑆 ∈ V ) → ( 𝐾 ↾t 𝑆 ) ∈ Top )
16 11 14 15 sylancr ⊢ ( 𝜑 → ( 𝐾 ↾t 𝑆 ) ∈ Top )
17 2 16 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ Top )
18 inss1 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
19 18 6 sstrid ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ⊆ 𝑆 )
20 1 cnfldtopon ⊢ 𝐾 ∈ ( TopOn ‘ ℂ )
21 resttopon ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( 𝐾 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
22 20 4 21 sylancr ⊢ ( 𝜑 → ( 𝐾 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
23 2 22 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ( TopOn ‘ 𝑆 ) )
24 toponuni ⊢ ( 𝑇 ∈ ( TopOn ‘ 𝑆 ) → 𝑆 = ∪ 𝑇 )
25 23 24 syl ⊢ ( 𝜑 → 𝑆 = ∪ 𝑇 )
26 19 25 sseqtrd ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ⊆ ∪ 𝑇 )
27 difssd ⊢ ( 𝜑 → ( ∪ 𝑇 ∖ 𝐵 ) ⊆ ∪ 𝑇 )
28 26 27 unssd ⊢ ( 𝜑 → ( ( 𝐴 ∩ 𝐵 ) ∪ ( ∪ 𝑇 ∖ 𝐵 ) ) ⊆ ∪ 𝑇 )
29 inundif ⊢ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴
30 6 25 sseqtrd ⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝑇 )
31 ssdif ⊢ ( 𝐴 ⊆ ∪ 𝑇 → ( 𝐴 ∖ 𝐵 ) ⊆ ( ∪ 𝑇 ∖ 𝐵 ) )
32 unss2 ⊢ ( ( 𝐴 ∖ 𝐵 ) ⊆ ( ∪ 𝑇 ∖ 𝐵 ) → ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ⊆ ( ( 𝐴 ∩ 𝐵 ) ∪ ( ∪ 𝑇 ∖ 𝐵 ) ) )
33 30 31 32 3syl ⊢ ( 𝜑 → ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ⊆ ( ( 𝐴 ∩ 𝐵 ) ∪ ( ∪ 𝑇 ∖ 𝐵 ) ) )
34 29 33 eqsstrrid ⊢ ( 𝜑 → 𝐴 ⊆ ( ( 𝐴 ∩ 𝐵 ) ∪ ( ∪ 𝑇 ∖ 𝐵 ) ) )
35 eqid ⊢ ∪ 𝑇 = ∪ 𝑇
36 35 ntrss ⊢ ( ( 𝑇 ∈ Top ∧ ( ( 𝐴 ∩ 𝐵 ) ∪ ( ∪ 𝑇 ∖ 𝐵 ) ) ⊆ ∪ 𝑇 ∧ 𝐴 ⊆ ( ( 𝐴 ∩ 𝐵 ) ∪ ( ∪ 𝑇 ∖ 𝐵 ) ) ) → ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ⊆ ( ( int ‘ 𝑇 ) ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( ∪ 𝑇 ∖ 𝐵 ) ) ) )
37 17 28 34 36 syl3anc ⊢ ( 𝜑 → ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ⊆ ( ( int ‘ 𝑇 ) ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( ∪ 𝑇 ∖ 𝐵 ) ) ) )
38 2 1 3 4 5 6 eldv ⊢ ( 𝜑 → ( 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ↔ ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( 𝐺 limℂ 𝑥 ) ) ) )
39 9 38 mpbid ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( 𝐺 limℂ 𝑥 ) ) )
40 39 simpld ⊢ ( 𝜑 → 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) )
41 37 40 sseldd ⊢ ( 𝜑 → 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( ∪ 𝑇 ∖ 𝐵 ) ) ) )
42 41 10 elind ⊢ ( 𝜑 → 𝑥 ∈ ( ( ( int ‘ 𝑇 ) ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( ∪ 𝑇 ∖ 𝐵 ) ) ) ∩ 𝐵 ) )
43 7 25 sseqtrd ⊢ ( 𝜑 → 𝐵 ⊆ ∪ 𝑇 )
44 inss2 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
45 44 a1i ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 )
46 eqid ⊢ ( 𝑇 ↾t 𝐵 ) = ( 𝑇 ↾t 𝐵 )
47 35 46 restntr ⊢ ( ( 𝑇 ∈ Top ∧ 𝐵 ⊆ ∪ 𝑇 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ) → ( ( int ‘ ( 𝑇 ↾t 𝐵 ) ) ‘ ( 𝐴 ∩ 𝐵 ) ) = ( ( ( int ‘ 𝑇 ) ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( ∪ 𝑇 ∖ 𝐵 ) ) ) ∩ 𝐵 ) )
48 17 43 45 47 syl3anc ⊢ ( 𝜑 → ( ( int ‘ ( 𝑇 ↾t 𝐵 ) ) ‘ ( 𝐴 ∩ 𝐵 ) ) = ( ( ( int ‘ 𝑇 ) ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( ∪ 𝑇 ∖ 𝐵 ) ) ) ∩ 𝐵 ) )
49 2 oveq1i ⊢ ( 𝑇 ↾t 𝐵 ) = ( ( 𝐾 ↾t 𝑆 ) ↾t 𝐵 )
50 11 a1i ⊢ ( 𝜑 → 𝐾 ∈ Top )
51 restabs ⊢ ( ( 𝐾 ∈ Top ∧ 𝐵 ⊆ 𝑆 ∧ 𝑆 ∈ V ) → ( ( 𝐾 ↾t 𝑆 ) ↾t 𝐵 ) = ( 𝐾 ↾t 𝐵 ) )
52 50 7 14 51 syl3anc ⊢ ( 𝜑 → ( ( 𝐾 ↾t 𝑆 ) ↾t 𝐵 ) = ( 𝐾 ↾t 𝐵 ) )
53 49 52 syl5eq ⊢ ( 𝜑 → ( 𝑇 ↾t 𝐵 ) = ( 𝐾 ↾t 𝐵 ) )
54 53 fveq2d ⊢ ( 𝜑 → ( int ‘ ( 𝑇 ↾t 𝐵 ) ) = ( int ‘ ( 𝐾 ↾t 𝐵 ) ) )
55 54 fveq1d ⊢ ( 𝜑 → ( ( int ‘ ( 𝑇 ↾t 𝐵 ) ) ‘ ( 𝐴 ∩ 𝐵 ) ) = ( ( int ‘ ( 𝐾 ↾t 𝐵 ) ) ‘ ( 𝐴 ∩ 𝐵 ) ) )
56 48 55 eqtr3d ⊢ ( 𝜑 → ( ( ( int ‘ 𝑇 ) ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( ∪ 𝑇 ∖ 𝐵 ) ) ) ∩ 𝐵 ) = ( ( int ‘ ( 𝐾 ↾t 𝐵 ) ) ‘ ( 𝐴 ∩ 𝐵 ) ) )
57 42 56 eleqtrd ⊢ ( 𝜑 → 𝑥 ∈ ( ( int ‘ ( 𝐾 ↾t 𝐵 ) ) ‘ ( 𝐴 ∩ 𝐵 ) ) )
58 limcresi ⊢ ( 𝐺 limℂ 𝑥 ) ⊆ ( ( 𝐺 ↾ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ) limℂ 𝑥 )
59 39 simprd ⊢ ( 𝜑 → 𝑦 ∈ ( 𝐺 limℂ 𝑥 ) )
60 58 59 sselid ⊢ ( 𝜑 → 𝑦 ∈ ( ( 𝐺 ↾ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ) limℂ 𝑥 ) )
61 difss ⊢ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ⊆ ( 𝐴 ∩ 𝐵 )
62 61 44 sstri ⊢ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ⊆ 𝐵
63 62 sseli ⊢ ( 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) → 𝑧 ∈ 𝐵 )
64 fvres ⊢ ( 𝑧 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
65 10 fvresd ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
66 64 65 oveqan12rd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑧 ) − ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) )
67 66 oveq1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑧 ) − ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) = ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) )
68 63 67 sylan2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ) → ( ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑧 ) − ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) = ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) )
69 68 mpteq2dva ⊢ ( 𝜑 → ( 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ↦ ( ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑧 ) − ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) = ( 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) )
70 3 reseq1i ⊢ ( 𝐺 ↾ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ) = ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) ↾ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) )
71 ssdif ⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 → ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ⊆ ( 𝐴 ∖ { 𝑥 } ) )
72 resmpt ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ⊆ ( 𝐴 ∖ { 𝑥 } ) → ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) ↾ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ) = ( 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) )
73 18 71 72 mp2b ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) ↾ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ) = ( 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) )
74 70 73 eqtri ⊢ ( 𝐺 ↾ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ) = ( 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) )
75 69 74 eqtr4di ⊢ ( 𝜑 → ( 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ↦ ( ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑧 ) − ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) = ( 𝐺 ↾ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ) )
76 75 oveq1d ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ↦ ( ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑧 ) − ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) = ( ( 𝐺 ↾ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ) limℂ 𝑥 ) )
77 60 76 eleqtrrd ⊢ ( 𝜑 → 𝑦 ∈ ( ( 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ↦ ( ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑧 ) − ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) )
78 eqid ⊢ ( 𝐾 ↾t 𝐵 ) = ( 𝐾 ↾t 𝐵 )
79 eqid ⊢ ( 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ↦ ( ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑧 ) − ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) = ( 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ↦ ( ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑧 ) − ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) )
80 7 4 sstrd ⊢ ( 𝜑 → 𝐵 ⊆ ℂ )
81 fresin ⊢ ( 𝐹 : 𝐴 ⟶ ℂ → ( 𝐹 ↾ 𝐵 ) : ( 𝐴 ∩ 𝐵 ) ⟶ ℂ )
82 5 81 syl ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) : ( 𝐴 ∩ 𝐵 ) ⟶ ℂ )
83 78 1 79 80 82 45 eldv ⊢ ( 𝜑 → ( 𝑥 ( 𝐵 D ( 𝐹 ↾ 𝐵 ) ) 𝑦 ↔ ( 𝑥 ∈ ( ( int ‘ ( 𝐾 ↾t 𝐵 ) ) ‘ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ↦ ( ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑧 ) − ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ) )
84 57 77 83 mpbir2and ⊢ ( 𝜑 → 𝑥 ( 𝐵 D ( 𝐹 ↾ 𝐵 ) ) 𝑦 )