Metamath Proof Explorer

Theorem perfdvf

Description: The derivative is a function, whenever it is defined relative to a perfect subset of the complex numbers. (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypothesis perfdvf.1 ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
Assertion perfdvf ( ( 𝐾 ↾t 𝑆 ) ∈ Perf → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )

Proof

Step Hyp Ref Expression
1 perfdvf.1 ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
2 df-dv ⊢ D = ( 𝑠 ∈ 𝒫 ℂ , 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ↦ ∪ 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( dom 𝑓 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) )
3 2 dmmpossx ⊢ dom D ⊆ ∪ 𝑠 ∈ 𝒫 ℂ ( { 𝑠 } × ( ℂ ↑pm 𝑠 ) )
4 simpl ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D )
5 3 4 sselid ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ⟨ 𝑆 , 𝐹 ⟩ ∈ ∪ 𝑠 ∈ 𝒫 ℂ ( { 𝑠 } × ( ℂ ↑pm 𝑠 ) ) )
6 oveq2 ⊢ ( 𝑠 = 𝑆 → ( ℂ ↑pm 𝑠 ) = ( ℂ ↑pm 𝑆 ) )
7 6 opeliunxp2 ⊢ ( ⟨ 𝑆 , 𝐹 ⟩ ∈ ∪ 𝑠 ∈ 𝒫 ℂ ( { 𝑠 } × ( ℂ ↑pm 𝑠 ) ) ↔ ( 𝑆 ∈ 𝒫 ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) )
8 5 7 sylib ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ( 𝑆 ∈ 𝒫 ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) )
9 8 simprd ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
10 cnex ⊢ ℂ ∈ V
11 8 simpld ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → 𝑆 ∈ 𝒫 ℂ )
12 elpm2g ⊢ ( ( ℂ ∈ V ∧ 𝑆 ∈ 𝒫 ℂ ) → ( 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ↔ ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ 𝑆 ) ) )
13 10 11 12 sylancr ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ( 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ↔ ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ 𝑆 ) ) )
14 9 13 mpbid ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ 𝑆 ) )
15 14 simpld ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → 𝐹 : dom 𝐹 ⟶ ℂ )
16 15 adantr ⊢ ( ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) ∧ 𝑥 ∈ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ) → 𝐹 : dom 𝐹 ⟶ ℂ )
17 3 sseli ⊢ ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → ⟨ 𝑆 , 𝐹 ⟩ ∈ ∪ 𝑠 ∈ 𝒫 ℂ ( { 𝑠 } × ( ℂ ↑pm 𝑠 ) ) )
18 17 7 sylib ⊢ ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → ( 𝑆 ∈ 𝒫 ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) )
19 18 simprd ⊢ ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
20 18 simpld ⊢ ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → 𝑆 ∈ 𝒫 ℂ )
21 10 20 12 sylancr ⊢ ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → ( 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ↔ ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ 𝑆 ) ) )
22 19 21 mpbid ⊢ ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ 𝑆 ) )
23 22 simprd ⊢ ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → dom 𝐹 ⊆ 𝑆 )
24 23 adantr ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → dom 𝐹 ⊆ 𝑆 )
25 11 elpwid ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → 𝑆 ⊆ ℂ )
26 24 25 sstrd ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → dom 𝐹 ⊆ ℂ )
27 26 adantr ⊢ ( ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) ∧ 𝑥 ∈ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ) → dom 𝐹 ⊆ ℂ )
28 1 cnfldtopon ⊢ 𝐾 ∈ ( TopOn ‘ ℂ )
29 resttopon ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( 𝐾 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
30 28 25 29 sylancr ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ( 𝐾 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
31 topontop ⊢ ( ( 𝐾 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) → ( 𝐾 ↾t 𝑆 ) ∈ Top )
32 30 31 syl ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ( 𝐾 ↾t 𝑆 ) ∈ Top )
33 toponuni ⊢ ( ( 𝐾 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) → 𝑆 = ∪ ( 𝐾 ↾t 𝑆 ) )
34 30 33 syl ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → 𝑆 = ∪ ( 𝐾 ↾t 𝑆 ) )
35 24 34 sseqtrd ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → dom 𝐹 ⊆ ∪ ( 𝐾 ↾t 𝑆 ) )
36 eqid ⊢ ∪ ( 𝐾 ↾t 𝑆 ) = ∪ ( 𝐾 ↾t 𝑆 )
37 36 ntrss2 ⊢ ( ( ( 𝐾 ↾t 𝑆 ) ∈ Top ∧ dom 𝐹 ⊆ ∪ ( 𝐾 ↾t 𝑆 ) ) → ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ⊆ dom 𝐹 )
38 32 35 37 syl2anc ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ⊆ dom 𝐹 )
39 38 sselda ⊢ ( ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) ∧ 𝑥 ∈ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ) → 𝑥 ∈ dom 𝐹 )
40 16 27 39 dvlem ⊢ ( ( ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) ∧ 𝑥 ∈ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∖ { 𝑥 } ) ) → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ∈ ℂ )
41 40 fmpttd ⊢ ( ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) ∧ 𝑥 ∈ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ) → ( 𝑧 ∈ ( dom 𝐹 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) : ( dom 𝐹 ∖ { 𝑥 } ) ⟶ ℂ )
42 27 ssdifssd ⊢ ( ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) ∧ 𝑥 ∈ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ) → ( dom 𝐹 ∖ { 𝑥 } ) ⊆ ℂ )
43 36 ntrss3 ⊢ ( ( ( 𝐾 ↾t 𝑆 ) ∈ Top ∧ dom 𝐹 ⊆ ∪ ( 𝐾 ↾t 𝑆 ) ) → ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ⊆ ∪ ( 𝐾 ↾t 𝑆 ) )
44 32 35 43 syl2anc ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ⊆ ∪ ( 𝐾 ↾t 𝑆 ) )
45 44 34 sseqtrrd ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ⊆ 𝑆 )
46 restabs ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ⊆ 𝑆 ∧ 𝑆 ∈ 𝒫 ℂ ) → ( ( 𝐾 ↾t 𝑆 ) ↾t ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ) = ( 𝐾 ↾t ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ) )
47 28 45 11 46 mp3an2i ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ( ( 𝐾 ↾t 𝑆 ) ↾t ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ) = ( 𝐾 ↾t ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ) )
48 simpr ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ( 𝐾 ↾t 𝑆 ) ∈ Perf )
49 36 ntropn ⊢ ( ( ( 𝐾 ↾t 𝑆 ) ∈ Top ∧ dom 𝐹 ⊆ ∪ ( 𝐾 ↾t 𝑆 ) ) → ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ∈ ( 𝐾 ↾t 𝑆 ) )
50 32 35 49 syl2anc ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ∈ ( 𝐾 ↾t 𝑆 ) )
51 eqid ⊢ ( ( 𝐾 ↾t 𝑆 ) ↾t ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ) = ( ( 𝐾 ↾t 𝑆 ) ↾t ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) )
52 36 51 perfopn ⊢ ( ( ( 𝐾 ↾t 𝑆 ) ∈ Perf ∧ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ∈ ( 𝐾 ↾t 𝑆 ) ) → ( ( 𝐾 ↾t 𝑆 ) ↾t ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ) ∈ Perf )
53 48 50 52 syl2anc ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ( ( 𝐾 ↾t 𝑆 ) ↾t ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ) ∈ Perf )
54 47 53 eqeltrrd ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ( 𝐾 ↾t ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ) ∈ Perf )
55 1 cnfldtop ⊢ 𝐾 ∈ Top
56 45 25 sstrd ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ⊆ ℂ )
57 28 toponunii ⊢ ℂ = ∪ 𝐾
58 eqid ⊢ ( 𝐾 ↾t ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ) = ( 𝐾 ↾t ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) )
59 57 58 restperf ⊢ ( ( 𝐾 ∈ Top ∧ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ⊆ ℂ ) → ( ( 𝐾 ↾t ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ) ∈ Perf ↔ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ⊆ ( ( limPt ‘ 𝐾 ) ‘ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ) ) )
60 55 56 59 sylancr ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ( ( 𝐾 ↾t ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ) ∈ Perf ↔ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ⊆ ( ( limPt ‘ 𝐾 ) ‘ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ) ) )
61 54 60 mpbid ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ⊆ ( ( limPt ‘ 𝐾 ) ‘ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ) )
62 57 lpss3 ⊢ ( ( 𝐾 ∈ Top ∧ dom 𝐹 ⊆ ℂ ∧ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ⊆ dom 𝐹 ) → ( ( limPt ‘ 𝐾 ) ‘ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ) ⊆ ( ( limPt ‘ 𝐾 ) ‘ dom 𝐹 ) )
63 55 26 38 62 mp3an2i ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ( ( limPt ‘ 𝐾 ) ‘ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ) ⊆ ( ( limPt ‘ 𝐾 ) ‘ dom 𝐹 ) )
64 61 63 sstrd ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ⊆ ( ( limPt ‘ 𝐾 ) ‘ dom 𝐹 ) )
65 64 sselda ⊢ ( ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) ∧ 𝑥 ∈ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ) → 𝑥 ∈ ( ( limPt ‘ 𝐾 ) ‘ dom 𝐹 ) )
66 57 lpdifsn ⊢ ( ( 𝐾 ∈ Top ∧ dom 𝐹 ⊆ ℂ ) → ( 𝑥 ∈ ( ( limPt ‘ 𝐾 ) ‘ dom 𝐹 ) ↔ 𝑥 ∈ ( ( limPt ‘ 𝐾 ) ‘ ( dom 𝐹 ∖ { 𝑥 } ) ) ) )
67 55 27 66 sylancr ⊢ ( ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) ∧ 𝑥 ∈ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ) → ( 𝑥 ∈ ( ( limPt ‘ 𝐾 ) ‘ dom 𝐹 ) ↔ 𝑥 ∈ ( ( limPt ‘ 𝐾 ) ‘ ( dom 𝐹 ∖ { 𝑥 } ) ) ) )
68 65 67 mpbid ⊢ ( ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) ∧ 𝑥 ∈ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ) → 𝑥 ∈ ( ( limPt ‘ 𝐾 ) ‘ ( dom 𝐹 ∖ { 𝑥 } ) ) )
69 41 42 68 1 limcmo ⊢ ( ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) ∧ 𝑥 ∈ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ) → ∃* 𝑦 𝑦 ∈ ( ( 𝑧 ∈ ( dom 𝐹 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) )
70 69 ex ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ( 𝑥 ∈ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) → ∃* 𝑦 𝑦 ∈ ( ( 𝑧 ∈ ( dom 𝐹 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) )
71 moanimv ⊢ ( ∃* 𝑦 ( 𝑥 ∈ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ∧ 𝑦 ∈ ( ( 𝑧 ∈ ( dom 𝐹 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ↔ ( 𝑥 ∈ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) → ∃* 𝑦 𝑦 ∈ ( ( 𝑧 ∈ ( dom 𝐹 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) )
72 70 71 sylibr ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ∃* 𝑦 ( 𝑥 ∈ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ∧ 𝑦 ∈ ( ( 𝑧 ∈ ( dom 𝐹 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) )
73 eqid ⊢ ( 𝐾 ↾t 𝑆 ) = ( 𝐾 ↾t 𝑆 )
74 eqid ⊢ ( 𝑧 ∈ ( dom 𝐹 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) = ( 𝑧 ∈ ( dom 𝐹 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) )
75 73 1 74 25 15 24 eldv ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ( 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ↔ ( 𝑥 ∈ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ∧ 𝑦 ∈ ( ( 𝑧 ∈ ( dom 𝐹 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ) )
76 75 mobidv ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ( ∃* 𝑦 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ↔ ∃* 𝑦 ( 𝑥 ∈ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ dom 𝐹 ) ∧ 𝑦 ∈ ( ( 𝑧 ∈ ( dom 𝐹 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ) )
77 72 76 mpbird ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ∃* 𝑦 𝑥 ( 𝑆 D 𝐹 ) 𝑦 )
78 77 alrimiv ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ∀ 𝑥 ∃* 𝑦 𝑥 ( 𝑆 D 𝐹 ) 𝑦 )
79 reldv ⊢ Rel ( 𝑆 D 𝐹 )
80 dffun6 ⊢ ( Fun ( 𝑆 D 𝐹 ) ↔ ( Rel ( 𝑆 D 𝐹 ) ∧ ∀ 𝑥 ∃* 𝑦 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) )
81 79 80 mpbiran ⊢ ( Fun ( 𝑆 D 𝐹 ) ↔ ∀ 𝑥 ∃* 𝑦 𝑥 ( 𝑆 D 𝐹 ) 𝑦 )
82 78 81 sylibr ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → Fun ( 𝑆 D 𝐹 ) )
83 82 funfnd ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ( 𝑆 D 𝐹 ) Fn dom ( 𝑆 D 𝐹 ) )
84 vex ⊢ 𝑦 ∈ V
85 84 elrn ⊢ ( 𝑦 ∈ ran ( 𝑆 D 𝐹 ) ↔ ∃ 𝑥 𝑥 ( 𝑆 D 𝐹 ) 𝑦 )
86 25 15 24 dvcl ⊢ ( ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝑦 ∈ ℂ )
87 86 ex ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ( 𝑥 ( 𝑆 D 𝐹 ) 𝑦 → 𝑦 ∈ ℂ ) )
88 87 exlimdv ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ( ∃ 𝑥 𝑥 ( 𝑆 D 𝐹 ) 𝑦 → 𝑦 ∈ ℂ ) )
89 85 88 syl5bi ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ( 𝑦 ∈ ran ( 𝑆 D 𝐹 ) → 𝑦 ∈ ℂ ) )
90 89 ssrdv ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ran ( 𝑆 D 𝐹 ) ⊆ ℂ )
91 df-f ⊢ ( ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ ↔ ( ( 𝑆 D 𝐹 ) Fn dom ( 𝑆 D 𝐹 ) ∧ ran ( 𝑆 D 𝐹 ) ⊆ ℂ ) )
92 83 90 91 sylanbrc ⊢ ( ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D ∧ ( 𝐾 ↾t 𝑆 ) ∈ Perf ) → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
93 92 ex ⊢ ( ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → ( ( 𝐾 ↾t 𝑆 ) ∈ Perf → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ ) )
94 f0 ⊢ ∅ : ∅ ⟶ ℂ
95 df-ov ⊢ ( 𝑆 D 𝐹 ) = ( D ‘ ⟨ 𝑆 , 𝐹 ⟩ )
96 ndmfv ⊢ ( ¬ ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → ( D ‘ ⟨ 𝑆 , 𝐹 ⟩ ) = ∅ )
97 95 96 syl5eq ⊢ ( ¬ ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → ( 𝑆 D 𝐹 ) = ∅ )
98 97 dmeqd ⊢ ( ¬ ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → dom ( 𝑆 D 𝐹 ) = dom ∅ )
99 dm0 ⊢ dom ∅ = ∅
100 98 99 eqtrdi ⊢ ( ¬ ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → dom ( 𝑆 D 𝐹 ) = ∅ )
101 97 100 feq12d ⊢ ( ¬ ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → ( ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ ↔ ∅ : ∅ ⟶ ℂ ) )
102 94 101 mpbiri ⊢ ( ¬ ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
103 102 a1d ⊢ ( ¬ ⟨ 𝑆 , 𝐹 ⟩ ∈ dom D → ( ( 𝐾 ↾t 𝑆 ) ∈ Perf → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ ) )
104 93 103 pm2.61i ⊢ ( ( 𝐾 ↾t 𝑆 ) ∈ Perf → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )