dvnfval

Description: Value of the iterated derivative. (Contributed by Mario Carneiro, 11-Feb-2015)

		Ref	Expression
	Hypothesis	dvnfval.1	$⊢ G = (x \in V ⟼ S D x)$
	Assertion	dvnfval	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \to S D^{n} F = seq 0 ((G \circ 1^{st}), (ℕ_{0} \times \{F\}))$

Proof

Step	Hyp	Ref	Expression
1		dvnfval.1	$⊢ G = (x \in V ⟼ S D x)$
2		df-dvn	$⊢ D^{n} = (s \in 𝒫 ℂ, f \in (ℂ ↑_{𝑝𝑚} s) ⟼ seq 0 (((x \in V ⟼ s D x) \circ 1^{st}), (ℕ_{0} \times \{f\})))$
3	2	a1i	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \to D^{n} = (s \in 𝒫 ℂ, f \in (ℂ ↑_{𝑝𝑚} s) ⟼ seq 0 (((x \in V ⟼ s D x) \circ 1^{st}), (ℕ_{0} \times \{f\})))$
4		simprl	$⊢ ((S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (s = S \land f = F)) \to s = S$
5	4	oveq1d	$⊢ ((S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (s = S \land f = F)) \to s D x = S D x$
6	5	mpteq2dv	$⊢ ((S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (s = S \land f = F)) \to (x \in V ⟼ s D x) = (x \in V ⟼ S D x)$
7	6 1	eqtr4di	$⊢ ((S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (s = S \land f = F)) \to (x \in V ⟼ s D x) = G$
8	7	coeq1d	$⊢ ((S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (s = S \land f = F)) \to (x \in V ⟼ s D x) \circ 1^{st} = G \circ 1^{st}$
9	8	seqeq2d	$⊢ ((S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (s = S \land f = F)) \to seq 0 (((x \in V ⟼ s D x) \circ 1^{st}), (ℕ_{0} \times \{f\})) = seq 0 ((G \circ 1^{st}), (ℕ_{0} \times \{f\}))$
10		simprr	$⊢ ((S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (s = S \land f = F)) \to f = F$
11	10	sneqd	$⊢ ((S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (s = S \land f = F)) \to \{f\} = \{F\}$
12	11	xpeq2d	$⊢ ((S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (s = S \land f = F)) \to ℕ_{0} \times \{f\} = ℕ_{0} \times \{F\}$
13	12	seqeq3d	$⊢ ((S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (s = S \land f = F)) \to seq 0 ((G \circ 1^{st}), (ℕ_{0} \times \{f\})) = seq 0 ((G \circ 1^{st}), (ℕ_{0} \times \{F\}))$
14	9 13	eqtrd	$⊢ ((S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (s = S \land f = F)) \to seq 0 (((x \in V ⟼ s D x) \circ 1^{st}), (ℕ_{0} \times \{f\})) = seq 0 ((G \circ 1^{st}), (ℕ_{0} \times \{F\}))$
15		simpr	$⊢ ((S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \land s = S) \to s = S$
16	15	oveq2d	$⊢ ((S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \land s = S) \to ℂ ↑_{𝑝𝑚} s = ℂ ↑_{𝑝𝑚} S$
17		cnex	$⊢ ℂ \in V$
18	17	elpw2	$⊢ S \in 𝒫 ℂ \leftrightarrow S \subseteq ℂ$
19	18	biranri	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \to S \in 𝒫 ℂ$
20		simpr	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \to F \in (ℂ ↑_{𝑝𝑚} S)$
21		seqex	$⊢ seq 0 ((G \circ 1^{st}), (ℕ_{0} \times \{F\})) \in V$
22	21	a1i	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \to seq 0 ((G \circ 1^{st}), (ℕ_{0} \times \{F\})) \in V$
23	3 14 16 19 20 22	ovmpodx	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \to S D^{n} F = seq 0 ((G \circ 1^{st}), (ℕ_{0} \times \{F\}))$

Metamath Proof Explorer

Theorem dvnfval

Proof