This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvmptres3

Description: Function-builder for derivative: restrict a derivative to a subset. (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypotheses dvmptres3.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
dvmptres3.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
dvmptres3.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐽 )
dvmptres3.y ⊢ ( 𝜑 → ( 𝑆 ∩ 𝑋 ) = 𝑌 )
dvmptres3.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
dvmptres3.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
dvmptres3.d ⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
Assertion dvmptres3 ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑌 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑌 ↦ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 dvmptres3.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2 dvmptres3.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
3 dvmptres3.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐽 )
4 dvmptres3.y ⊢ ( 𝜑 → ( 𝑆 ∩ 𝑋 ) = 𝑌 )
5 dvmptres3.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
6 dvmptres3.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
7 dvmptres3.d ⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
8 5 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ℂ )
9 7 dmeqd ⊢ ( 𝜑 → dom ( ℂ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
10 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 )
11 10 6 dmmptd ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = 𝑋 )
12 9 11 eqtrd ⊢ ( 𝜑 → dom ( ℂ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = 𝑋 )
13 1 dvres3a ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ℂ ) ∧ ( 𝑋 ∈ 𝐽 ∧ dom ( ℂ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = 𝑋 ) ) → ( 𝑆 D ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑆 ) ) = ( ( ℂ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ↾ 𝑆 ) )
14 2 8 3 12 13 syl22anc ⊢ ( 𝜑 → ( 𝑆 D ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑆 ) ) = ( ( ℂ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ↾ 𝑆 ) )
15 rescom ⊢ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑋 ) ↾ 𝑆 ) = ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑆 ) ↾ 𝑋 )
16 resres ⊢ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑆 ) ↾ 𝑋 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ ( 𝑆 ∩ 𝑋 ) )
17 15 16 eqtri ⊢ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑋 ) ↾ 𝑆 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ ( 𝑆 ∩ 𝑋 ) )
18 4 reseq2d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ ( 𝑆 ∩ 𝑋 ) ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑌 ) )
19 17 18 eqtrid ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑋 ) ↾ 𝑆 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑌 ) )
20 ffn ⊢ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ℂ → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) Fn 𝑋 )
21 fnresdm ⊢ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) Fn 𝑋 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑋 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) )
22 8 20 21 3syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑋 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) )
23 22 reseq1d ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑋 ) ↾ 𝑆 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑆 ) )
24 inss2 ⊢ ( 𝑆 ∩ 𝑋 ) ⊆ 𝑋
25 4 24 eqsstrrdi ⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
26 25 resmptd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑌 ) = ( 𝑥 ∈ 𝑌 ↦ 𝐴 ) )
27 19 23 26 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑆 ) = ( 𝑥 ∈ 𝑌 ↦ 𝐴 ) )
28 27 oveq2d ⊢ ( 𝜑 → ( 𝑆 D ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑆 ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑌 ↦ 𝐴 ) ) )
29 rescom ⊢ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ 𝑋 ) ↾ 𝑆 ) = ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ 𝑆 ) ↾ 𝑋 )
30 resres ⊢ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ 𝑆 ) ↾ 𝑋 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ ( 𝑆 ∩ 𝑋 ) )
31 29 30 eqtri ⊢ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ 𝑋 ) ↾ 𝑆 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ ( 𝑆 ∩ 𝑋 ) )
32 4 reseq2d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ ( 𝑆 ∩ 𝑋 ) ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ 𝑌 ) )
33 31 32 eqtrid ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ 𝑋 ) ↾ 𝑆 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ 𝑌 ) )
34 6 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 𝐵 ∈ 𝑉 )
35 10 fnmpt ⊢ ( ∀ 𝑥 ∈ 𝑋 𝐵 ∈ 𝑉 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) Fn 𝑋 )
36 fnresdm ⊢ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) Fn 𝑋 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ 𝑋 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
37 34 35 36 3syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ 𝑋 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
38 37 7 eqtr4d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ 𝑋 ) = ( ℂ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) )
39 38 reseq1d ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ 𝑋 ) ↾ 𝑆 ) = ( ( ℂ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ↾ 𝑆 ) )
40 25 resmptd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ↾ 𝑌 ) = ( 𝑥 ∈ 𝑌 ↦ 𝐵 ) )
41 33 39 40 3eqtr3d ⊢ ( 𝜑 → ( ( ℂ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ↾ 𝑆 ) = ( 𝑥 ∈ 𝑌 ↦ 𝐵 ) )
42 14 28 41 3eqtr3d ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑌 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑌 ↦ 𝐵 ) )