Metamath Proof Explorer


Theorem dvnbss

Description: The set of N-times differentiable points is a subset of the domain of the function. (Contributed by Stefan O'Rear, 16-Nov-2014) (Revised by Mario Carneiro, 11-Feb-2015)

Ref Expression
Assertion dvnbss ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom 𝐹 )

Proof

Step Hyp Ref Expression
1 dvnff ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( 𝑆 D𝑛 𝐹 ) : ℕ0 ⟶ ( ℂ ↑pm dom 𝐹 ) )
2 1 ffvelrnda ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( ℂ ↑pm dom 𝐹 ) )
3 2 3impa ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( ℂ ↑pm dom 𝐹 ) )
4 cnex ℂ ∈ V
5 simp2 ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
6 5 dmexd ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → dom 𝐹 ∈ V )
7 elpm2g ( ( ℂ ∈ V ∧ dom 𝐹 ∈ V ) → ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( ℂ ↑pm dom 𝐹 ) ↔ ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) : dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ⟶ ℂ ∧ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom 𝐹 ) ) )
8 4 6 7 sylancr ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( ℂ ↑pm dom 𝐹 ) ↔ ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) : dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ⟶ ℂ ∧ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom 𝐹 ) ) )
9 3 8 mpbid ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) : dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ⟶ ℂ ∧ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom 𝐹 ) )
10 9 simprd ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom 𝐹 )