dvnff

Description: The iterated derivative is a function. (Contributed by Mario Carneiro, 11-Feb-2015)

		Ref	Expression
	Assertion	dvnff	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \to (S D^{n} F) : ℕ_{0} ⟶ ℂ ↑_{𝑝𝑚} dom F$

Proof

Step	Hyp	Ref	Expression
1		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
2		0zd	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \to 0 \in ℤ$
3		fvconst2g	$⊢ (F \in (ℂ ↑_{𝑝𝑚} S) \land k \in ℕ_{0}) \to (ℕ_{0} \times \{F\}) (k) = F$
4	3	adantll	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land k \in ℕ_{0}) \to (ℕ_{0} \times \{F\}) (k) = F$
5		dmexg	$⊢ F \in (ℂ ↑_{𝑝𝑚} S) \to dom F \in V$
6	5	ad2antlr	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land k \in ℕ_{0}) \to dom F \in V$
7		cnex	$⊢ ℂ \in V$
8	7	a1i	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land k \in ℕ_{0}) \to ℂ \in V$
9		elpm2g	$⊢ (ℂ \in V \land S \in \{ℝ, ℂ\}) \to (F \in (ℂ ↑_{𝑝𝑚} S) \leftrightarrow (F : dom F ⟶ ℂ \land dom F \subseteq S))$
10	7 9	mpan	$⊢ S \in \{ℝ, ℂ\} \to (F \in (ℂ ↑_{𝑝𝑚} S) \leftrightarrow (F : dom F ⟶ ℂ \land dom F \subseteq S))$
11	10	biimpa	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \to (F : dom F ⟶ ℂ \land dom F \subseteq S)$
12	11	simpld	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \to F : dom F ⟶ ℂ$
13	12	adantr	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land k \in ℕ_{0}) \to F : dom F ⟶ ℂ$
14		fpmg	$⊢ (dom F \in V \land ℂ \in V \land F : dom F ⟶ ℂ) \to F \in (ℂ ↑_{𝑝𝑚} dom F)$
15	6 8 13 14	syl3anc	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land k \in ℕ_{0}) \to F \in (ℂ ↑_{𝑝𝑚} dom F)$
16	4 15	eqeltrd	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land k \in ℕ_{0}) \to (ℕ_{0} \times \{F\}) (k) \in (ℂ ↑_{𝑝𝑚} dom F)$
17		vex	$⊢ k \in V$
18		vex	$⊢ n \in V$
19	17 18	opco1i	$⊢ k ((x \in V ⟼ S D x) \circ 1^{st}) n = (x \in V ⟼ S D x) (k)$
20		oveq2	$⊢ x = k \to S D x = S D k$
21		eqid	$⊢ (x \in V ⟼ S D x) = (x \in V ⟼ S D x)$
22		ovex	$⊢ S D k \in V$
23	20 21 22	fvmpt	$⊢ k \in V \to (x \in V ⟼ S D x) (k) = S D k$
24	23	elv	$⊢ (x \in V ⟼ S D x) (k) = S D k$
25	19 24	eqtri	$⊢ k ((x \in V ⟼ S D x) \circ 1^{st}) n = S D k$
26	7	a1i	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (k \in (ℂ ↑_{𝑝𝑚} dom F) \land n \in (ℂ ↑_{𝑝𝑚} dom F))) \to ℂ \in V$
27	5	ad2antlr	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (k \in (ℂ ↑_{𝑝𝑚} dom F) \land n \in (ℂ ↑_{𝑝𝑚} dom F))) \to dom F \in V$
28		dvfg	$⊢ S \in \{ℝ, ℂ\} \to k_{S}^{'} : dom k_{S}^{'} ⟶ ℂ$
29	28	ad2antrr	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (k \in (ℂ ↑_{𝑝𝑚} dom F) \land n \in (ℂ ↑_{𝑝𝑚} dom F))) \to k_{S}^{'} : dom k_{S}^{'} ⟶ ℂ$
30		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
31	30	ad2antrr	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (k \in (ℂ ↑_{𝑝𝑚} dom F) \land n \in (ℂ ↑_{𝑝𝑚} dom F))) \to S \subseteq ℂ$
32		simprl	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (k \in (ℂ ↑_{𝑝𝑚} dom F) \land n \in (ℂ ↑_{𝑝𝑚} dom F))) \to k \in (ℂ ↑_{𝑝𝑚} dom F)$
33		elpm2g	$⊢ (ℂ \in V \land dom F \in V) \to (k \in (ℂ ↑_{𝑝𝑚} dom F) \leftrightarrow (k : dom k ⟶ ℂ \land dom k \subseteq dom F))$
34	7 27 33	sylancr	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (k \in (ℂ ↑_{𝑝𝑚} dom F) \land n \in (ℂ ↑_{𝑝𝑚} dom F))) \to (k \in (ℂ ↑_{𝑝𝑚} dom F) \leftrightarrow (k : dom k ⟶ ℂ \land dom k \subseteq dom F))$
35	32 34	mpbid	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (k \in (ℂ ↑_{𝑝𝑚} dom F) \land n \in (ℂ ↑_{𝑝𝑚} dom F))) \to (k : dom k ⟶ ℂ \land dom k \subseteq dom F)$
36	35	simpld	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (k \in (ℂ ↑_{𝑝𝑚} dom F) \land n \in (ℂ ↑_{𝑝𝑚} dom F))) \to k : dom k ⟶ ℂ$
37	35	simprd	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (k \in (ℂ ↑_{𝑝𝑚} dom F) \land n \in (ℂ ↑_{𝑝𝑚} dom F))) \to dom k \subseteq dom F$
38	11	simprd	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \to dom F \subseteq S$
39	38	adantr	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (k \in (ℂ ↑_{𝑝𝑚} dom F) \land n \in (ℂ ↑_{𝑝𝑚} dom F))) \to dom F \subseteq S$
40	37 39	sstrd	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (k \in (ℂ ↑_{𝑝𝑚} dom F) \land n \in (ℂ ↑_{𝑝𝑚} dom F))) \to dom k \subseteq S$
41	31 36 40	dvbss	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (k \in (ℂ ↑_{𝑝𝑚} dom F) \land n \in (ℂ ↑_{𝑝𝑚} dom F))) \to dom k_{S}^{'} \subseteq dom k$
42	41 37	sstrd	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (k \in (ℂ ↑_{𝑝𝑚} dom F) \land n \in (ℂ ↑_{𝑝𝑚} dom F))) \to dom k_{S}^{'} \subseteq dom F$
43		elpm2r	$⊢ ((ℂ \in V \land dom F \in V) \land (k_{S}^{'} : dom k_{S}^{'} ⟶ ℂ \land dom k_{S}^{'} \subseteq dom F)) \to S D k \in (ℂ ↑_{𝑝𝑚} dom F)$
44	26 27 29 42 43	syl22anc	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (k \in (ℂ ↑_{𝑝𝑚} dom F) \land n \in (ℂ ↑_{𝑝𝑚} dom F))) \to S D k \in (ℂ ↑_{𝑝𝑚} dom F)$
45	25 44	eqeltrid	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land (k \in (ℂ ↑_{𝑝𝑚} dom F) \land n \in (ℂ ↑_{𝑝𝑚} dom F))) \to k ((x \in V ⟼ S D x) \circ 1^{st}) n \in (ℂ ↑_{𝑝𝑚} dom F)$
46	1 2 16 45	seqf	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \to seq 0 (((x \in V ⟼ S D x) \circ 1^{st}), (ℕ_{0} \times \{F\})) : ℕ_{0} ⟶ ℂ ↑_{𝑝𝑚} dom F$
47	21	dvnfval	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \to S D^{n} F = seq 0 (((x \in V ⟼ S D x) \circ 1^{st}), (ℕ_{0} \times \{F\}))$
48	30 47	sylan	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \to S D^{n} F = seq 0 (((x \in V ⟼ S D x) \circ 1^{st}), (ℕ_{0} \times \{F\}))$
49	48	feq1d	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \to ((S D^{n} F) : ℕ_{0} ⟶ ℂ ↑_{𝑝𝑚} dom F \leftrightarrow seq 0 (((x \in V ⟼ S D x) \circ 1^{st}), (ℕ_{0} \times \{F\})) : ℕ_{0} ⟶ ℂ ↑_{𝑝𝑚} dom F)$
50	46 49	mpbird	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \to (S D^{n} F) : ℕ_{0} ⟶ ℂ ↑_{𝑝𝑚} dom F$

Metamath Proof Explorer

Theorem dvnff

Proof