Metamath Proof Explorer

Theorem cpnfval

Description: Condition for n-times continuous differentiability. (Contributed by Stefan O'Rear, 15-Nov-2014) (Revised by Mario Carneiro, 11-Feb-2015)

		Ref	Expression
	Assertion	cpnfval	$⊢ S \subseteq ℂ \to C^{n} (S) = (n \in ℕ_{0} ⟼ \{f \in (ℂ ↑_{𝑝𝑚} S) \| (S D^{n} f) (n) : dom f \underset{cn}{⟶} ℂ\})$

Proof

Step	Hyp	Ref	Expression
1		cnex	$⊢ ℂ \in V$
2	1	elpw2	$⊢ S \in 𝒫 ℂ \leftrightarrow S \subseteq ℂ$
3		oveq2	$⊢ s = S \to ℂ ↑_{𝑝𝑚} s = ℂ ↑_{𝑝𝑚} S$
4		oveq1	$⊢ s = S \to s D^{n} f = S D^{n} f$
5	4	fveq1d	$⊢ s = S \to (s D^{n} f) (n) = (S D^{n} f) (n)$
6	5	eleq1d	$⊢ s = S \to ((s D^{n} f) (n) : dom f \underset{cn}{⟶} ℂ \leftrightarrow (S D^{n} f) (n) : dom f \underset{cn}{⟶} ℂ)$
7	3 6	rabeqbidv	$⊢ s = S \to \{f \in (ℂ ↑_{𝑝𝑚} s) \| (s D^{n} f) (n) : dom f \underset{cn}{⟶} ℂ\} = \{f \in (ℂ ↑_{𝑝𝑚} S) \| (S D^{n} f) (n) : dom f \underset{cn}{⟶} ℂ\}$
8	7	mpteq2dv	$⊢ s = S \to (n \in ℕ_{0} ⟼ \{f \in (ℂ ↑_{𝑝𝑚} s) \| (s D^{n} f) (n) : dom f \underset{cn}{⟶} ℂ\}) = (n \in ℕ_{0} ⟼ \{f \in (ℂ ↑_{𝑝𝑚} S) \| (S D^{n} f) (n) : dom f \underset{cn}{⟶} ℂ\})$
9		df-cpn	$⊢ C^{n} = (s \in 𝒫 ℂ ⟼ (n \in ℕ_{0} ⟼ \{f \in (ℂ ↑_{𝑝𝑚} s) \| (s D^{n} f) (n) : dom f \underset{cn}{⟶} ℂ\}))$
10		nn0ex	$⊢ ℕ_{0} \in V$
11	10	mptex	$⊢ (n \in ℕ_{0} ⟼ \{f \in (ℂ ↑_{𝑝𝑚} S) \| (S D^{n} f) (n) : dom f \underset{cn}{⟶} ℂ\}) \in V$
12	8 9 11	fvmpt	$⊢ S \in 𝒫 ℂ \to C^{n} (S) = (n \in ℕ_{0} ⟼ \{f \in (ℂ ↑_{𝑝𝑚} S) \| (S D^{n} f) (n) : dom f \underset{cn}{⟶} ℂ\})$
13	2 12	sylbir	$⊢ S \subseteq ℂ \to C^{n} (S) = (n \in ℕ_{0} ⟼ \{f \in (ℂ ↑_{𝑝𝑚} S) \| (S D^{n} f) (n) : dom f \underset{cn}{⟶} ℂ\})$