Metamath Proof Explorer


Theorem dvresntr

Description: Function-builder for derivative: expand the function from an open set to its closure. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dvresntr.s φ S
dvresntr.x φ X S
dvresntr.f φ F : X
dvresntr.j J = K 𝑡 S
dvresntr.k K = TopOpen fld
dvresntr.i φ int J X = Y
Assertion dvresntr φ S D F = S D F Y

Proof

Step Hyp Ref Expression
1 dvresntr.s φ S
2 dvresntr.x φ X S
3 dvresntr.f φ F : X
4 dvresntr.j J = K 𝑡 S
5 dvresntr.k K = TopOpen fld
6 dvresntr.i φ int J X = Y
7 5 4 dvres S F : X X S X S S D F X = F S int J X
8 1 3 2 2 7 syl22anc φ S D F X = F S int J X
9 ffn F : X F Fn X
10 fnresdm F Fn X F X = F
11 3 9 10 3syl φ F X = F
12 11 oveq2d φ S D F X = S D F
13 5 cnfldtopon K TopOn
14 resttopon K TopOn S K 𝑡 S TopOn S
15 13 1 14 sylancr φ K 𝑡 S TopOn S
16 4 15 eqeltrid φ J TopOn S
17 topontop J TopOn S J Top
18 16 17 syl φ J Top
19 toponuni J TopOn S S = J
20 16 19 syl φ S = J
21 2 20 sseqtrd φ X J
22 eqid J = J
23 22 ntridm J Top X J int J int J X = int J X
24 18 21 23 syl2anc φ int J int J X = int J X
25 6 fveq2d φ int J int J X = int J Y
26 24 25 6 3eqtr3d φ int J Y = Y
27 26 reseq2d φ F S int J Y = F S Y
28 22 ntrss2 J Top X J int J X X
29 18 21 28 syl2anc φ int J X X
30 6 29 eqsstrrd φ Y X
31 30 2 sstrd φ Y S
32 5 4 dvres S F : X X S Y S S D F Y = F S int J Y
33 1 3 2 31 32 syl22anc φ S D F Y = F S int J Y
34 6 reseq2d φ F S int J X = F S Y
35 27 33 34 3eqtr4rd φ F S int J X = S D F Y
36 8 12 35 3eqtr3d φ S D F = S D F Y