Metamath Proof Explorer

Theorem dvmptntr

Description: Function-builder for derivative: expand the function from an open set to its closure. (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypotheses dvmptntr.s ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
dvmptntr.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
dvmptntr.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
dvmptntr.j ⊢ 𝐽 = ( 𝐾 ↾t 𝑆 )
dvmptntr.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
dvmptntr.i ⊢ ( 𝜑 → ( ( int ‘ 𝐽 ) ‘ 𝑋 ) = 𝑌 )
Assertion dvmptntr ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑌 ↦ 𝐴 ) ) )

Proof

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