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 ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
dvresntr.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
dvresntr.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
dvresntr.j ⊢ 𝐽 = ( 𝐾 ↾t 𝑆 )
dvresntr.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
dvresntr.i ⊢ ( 𝜑 → ( ( int ‘ 𝐽 ) ‘ 𝑋 ) = 𝑌 )
Assertion dvresntr ( 𝜑 → ( 𝑆 D 𝐹 ) = ( 𝑆 D ( 𝐹 ↾ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 dvresntr.s ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
2 dvresntr.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
3 dvresntr.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
4 dvresntr.j ⊢ 𝐽 = ( 𝐾 ↾t 𝑆 )
5 dvresntr.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
6 dvresntr.i ⊢ ( 𝜑 → ( ( int ‘ 𝐽 ) ‘ 𝑋 ) = 𝑌 )
7 5 4 dvres ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝑋 ⟶ ℂ ) ∧ ( 𝑋 ⊆ 𝑆 ∧ 𝑋 ⊆ 𝑆 ) ) → ( 𝑆 D ( 𝐹 ↾ 𝑋 ) ) = ( ( 𝑆 D 𝐹 ) ↾ ( ( int ‘ 𝐽 ) ‘ 𝑋 ) ) )
8 1 3 2 2 7 syl22anc ⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ↾ 𝑋 ) ) = ( ( 𝑆 D 𝐹 ) ↾ ( ( int ‘ 𝐽 ) ‘ 𝑋 ) ) )
9 ffn ⊢ ( 𝐹 : 𝑋 ⟶ ℂ → 𝐹 Fn 𝑋 )
10 fnresdm ⊢ ( 𝐹 Fn 𝑋 → ( 𝐹 ↾ 𝑋 ) = 𝐹 )
11 3 9 10 3syl ⊢ ( 𝜑 → ( 𝐹 ↾ 𝑋 ) = 𝐹 )
12 11 oveq2d ⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ↾ 𝑋 ) ) = ( 𝑆 D 𝐹 ) )
13 5 cnfldtopon ⊢ 𝐾 ∈ ( TopOn ‘ ℂ )
14 resttopon ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( 𝐾 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
15 13 1 14 sylancr ⊢ ( 𝜑 → ( 𝐾 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
16 4 15 eqeltrid ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑆 ) )
17 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑆 ) → 𝐽 ∈ Top )
18 16 17 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
19 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑆 ) → 𝑆 = ∪ 𝐽 )
20 16 19 syl ⊢ ( 𝜑 → 𝑆 = ∪ 𝐽 )
21 2 20 sseqtrd ⊢ ( 𝜑 → 𝑋 ⊆ ∪ 𝐽 )
22 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
23 22 ntridm ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 ⊆ ∪ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ ( ( int ‘ 𝐽 ) ‘ 𝑋 ) ) = ( ( int ‘ 𝐽 ) ‘ 𝑋 ) )
24 18 21 23 syl2anc ⊢ ( 𝜑 → ( ( int ‘ 𝐽 ) ‘ ( ( int ‘ 𝐽 ) ‘ 𝑋 ) ) = ( ( int ‘ 𝐽 ) ‘ 𝑋 ) )
25 6 fveq2d ⊢ ( 𝜑 → ( ( int ‘ 𝐽 ) ‘ ( ( int ‘ 𝐽 ) ‘ 𝑋 ) ) = ( ( int ‘ 𝐽 ) ‘ 𝑌 ) )
26 24 25 6 3eqtr3d ⊢ ( 𝜑 → ( ( int ‘ 𝐽 ) ‘ 𝑌 ) = 𝑌 )
27 26 reseq2d ⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) ↾ ( ( int ‘ 𝐽 ) ‘ 𝑌 ) ) = ( ( 𝑆 D 𝐹 ) ↾ 𝑌 ) )
28 22 ntrss2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 ⊆ ∪ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ 𝑋 ) ⊆ 𝑋 )
29 18 21 28 syl2anc ⊢ ( 𝜑 → ( ( int ‘ 𝐽 ) ‘ 𝑋 ) ⊆ 𝑋 )
30 6 29 eqsstrrd ⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
31 30 2 sstrd ⊢ ( 𝜑 → 𝑌 ⊆ 𝑆 )
32 5 4 dvres ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝑋 ⟶ ℂ ) ∧ ( 𝑋 ⊆ 𝑆 ∧ 𝑌 ⊆ 𝑆 ) ) → ( 𝑆 D ( 𝐹 ↾ 𝑌 ) ) = ( ( 𝑆 D 𝐹 ) ↾ ( ( int ‘ 𝐽 ) ‘ 𝑌 ) ) )
33 1 3 2 31 32 syl22anc ⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ↾ 𝑌 ) ) = ( ( 𝑆 D 𝐹 ) ↾ ( ( int ‘ 𝐽 ) ‘ 𝑌 ) ) )
34 6 reseq2d ⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) ↾ ( ( int ‘ 𝐽 ) ‘ 𝑋 ) ) = ( ( 𝑆 D 𝐹 ) ↾ 𝑌 ) )
35 27 33 34 3eqtr4rd ⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) ↾ ( ( int ‘ 𝐽 ) ‘ 𝑋 ) ) = ( 𝑆 D ( 𝐹 ↾ 𝑌 ) ) )
36 8 12 35 3eqtr3d ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) = ( 𝑆 D ( 𝐹 ↾ 𝑌 ) ) )