Metamath Proof Explorer

Theorem dvnff

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

Ref Expression
Assertion dvnff ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( 𝑆 D𝑛 𝐹 ) : ℕ0 ⟶ ( ℂ ↑pm dom 𝐹 ) )

Proof

Step Hyp Ref Expression
1 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
2 0zd ⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → 0 ∈ ℤ )
3 fvconst2g ⊢ ( ( 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ℕ0 × { 𝐹 } ) ‘ 𝑘 ) = 𝐹 )
4 3 adantll ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ℕ0 × { 𝐹 } ) ‘ 𝑘 ) = 𝐹 )
5 dmexg ⊢ ( 𝐹 ∈ ( ℂ ↑pm 𝑆 ) → dom 𝐹 ∈ V )
6 5 ad2antlr ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → dom 𝐹 ∈ V )
7 cnex ⊢ ℂ ∈ V
8 7 a1i ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ℂ ∈ V )
9 elpm2g ⊢ ( ( ℂ ∈ V ∧ 𝑆 ∈ { ℝ , ℂ } ) → ( 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ↔ ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ 𝑆 ) ) )
10 7 9 mpan ⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ↔ ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ 𝑆 ) ) )
11 10 biimpa ⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ 𝑆 ) )
12 11 simpld ⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → 𝐹 : dom 𝐹 ⟶ ℂ )
13 12 adantr ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝐹 : dom 𝐹 ⟶ ℂ )
14 fpmg ⊢ ( ( dom 𝐹 ∈ V ∧ ℂ ∈ V ∧ 𝐹 : dom 𝐹 ⟶ ℂ ) → 𝐹 ∈ ( ℂ ↑pm dom 𝐹 ) )
15 6 8 13 14 syl3anc ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝐹 ∈ ( ℂ ↑pm dom 𝐹 ) )
16 4 15 eqeltrd ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ℕ0 × { 𝐹 } ) ‘ 𝑘 ) ∈ ( ℂ ↑pm dom 𝐹 ) )
17 vex ⊢ 𝑘 ∈ V
18 vex ⊢ 𝑛 ∈ V
19 17 18 opco1i ⊢ ( 𝑘 ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) 𝑛 ) = ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ‘ 𝑘 )
20 oveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝑆 D 𝑥 ) = ( 𝑆 D 𝑘 ) )
21 eqid ⊢ ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) = ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) )
22 ovex ⊢ ( 𝑆 D 𝑘 ) ∈ V
23 20 21 22 fvmpt ⊢ ( 𝑘 ∈ V → ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ‘ 𝑘 ) = ( 𝑆 D 𝑘 ) )
24 23 elv ⊢ ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ‘ 𝑘 ) = ( 𝑆 D 𝑘 )
25 19 24 eqtri ⊢ ( 𝑘 ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) 𝑛 ) = ( 𝑆 D 𝑘 )
26 7 a1i ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑘 ∈ ( ℂ ↑pm dom 𝐹 ) ∧ 𝑛 ∈ ( ℂ ↑pm dom 𝐹 ) ) ) → ℂ ∈ V )
27 5 ad2antlr ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑘 ∈ ( ℂ ↑pm dom 𝐹 ) ∧ 𝑛 ∈ ( ℂ ↑pm dom 𝐹 ) ) ) → dom 𝐹 ∈ V )
28 dvfg ⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝑘 ) : dom ( 𝑆 D 𝑘 ) ⟶ ℂ )
29 28 ad2antrr ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑘 ∈ ( ℂ ↑pm dom 𝐹 ) ∧ 𝑛 ∈ ( ℂ ↑pm dom 𝐹 ) ) ) → ( 𝑆 D 𝑘 ) : dom ( 𝑆 D 𝑘 ) ⟶ ℂ )
30 recnprss ⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
31 30 ad2antrr ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑘 ∈ ( ℂ ↑pm dom 𝐹 ) ∧ 𝑛 ∈ ( ℂ ↑pm dom 𝐹 ) ) ) → 𝑆 ⊆ ℂ )
32 simprl ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑘 ∈ ( ℂ ↑pm dom 𝐹 ) ∧ 𝑛 ∈ ( ℂ ↑pm dom 𝐹 ) ) ) → 𝑘 ∈ ( ℂ ↑pm dom 𝐹 ) )
33 elpm2g ⊢ ( ( ℂ ∈ V ∧ dom 𝐹 ∈ V ) → ( 𝑘 ∈ ( ℂ ↑pm dom 𝐹 ) ↔ ( 𝑘 : dom 𝑘 ⟶ ℂ ∧ dom 𝑘 ⊆ dom 𝐹 ) ) )
34 7 27 33 sylancr ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑘 ∈ ( ℂ ↑pm dom 𝐹 ) ∧ 𝑛 ∈ ( ℂ ↑pm dom 𝐹 ) ) ) → ( 𝑘 ∈ ( ℂ ↑pm dom 𝐹 ) ↔ ( 𝑘 : dom 𝑘 ⟶ ℂ ∧ dom 𝑘 ⊆ dom 𝐹 ) ) )
35 32 34 mpbid ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑘 ∈ ( ℂ ↑pm dom 𝐹 ) ∧ 𝑛 ∈ ( ℂ ↑pm dom 𝐹 ) ) ) → ( 𝑘 : dom 𝑘 ⟶ ℂ ∧ dom 𝑘 ⊆ dom 𝐹 ) )
36 35 simpld ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑘 ∈ ( ℂ ↑pm dom 𝐹 ) ∧ 𝑛 ∈ ( ℂ ↑pm dom 𝐹 ) ) ) → 𝑘 : dom 𝑘 ⟶ ℂ )
37 35 simprd ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑘 ∈ ( ℂ ↑pm dom 𝐹 ) ∧ 𝑛 ∈ ( ℂ ↑pm dom 𝐹 ) ) ) → dom 𝑘 ⊆ dom 𝐹 )
38 11 simprd ⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → dom 𝐹 ⊆ 𝑆 )
39 38 adantr ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑘 ∈ ( ℂ ↑pm dom 𝐹 ) ∧ 𝑛 ∈ ( ℂ ↑pm dom 𝐹 ) ) ) → dom 𝐹 ⊆ 𝑆 )
40 37 39 sstrd ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑘 ∈ ( ℂ ↑pm dom 𝐹 ) ∧ 𝑛 ∈ ( ℂ ↑pm dom 𝐹 ) ) ) → dom 𝑘 ⊆ 𝑆 )
41 31 36 40 dvbss ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑘 ∈ ( ℂ ↑pm dom 𝐹 ) ∧ 𝑛 ∈ ( ℂ ↑pm dom 𝐹 ) ) ) → dom ( 𝑆 D 𝑘 ) ⊆ dom 𝑘 )
42 41 37 sstrd ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑘 ∈ ( ℂ ↑pm dom 𝐹 ) ∧ 𝑛 ∈ ( ℂ ↑pm dom 𝐹 ) ) ) → dom ( 𝑆 D 𝑘 ) ⊆ dom 𝐹 )
43 elpm2r ⊢ ( ( ( ℂ ∈ V ∧ dom 𝐹 ∈ V ) ∧ ( ( 𝑆 D 𝑘 ) : dom ( 𝑆 D 𝑘 ) ⟶ ℂ ∧ dom ( 𝑆 D 𝑘 ) ⊆ dom 𝐹 ) ) → ( 𝑆 D 𝑘 ) ∈ ( ℂ ↑pm dom 𝐹 ) )
44 26 27 29 42 43 syl22anc ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑘 ∈ ( ℂ ↑pm dom 𝐹 ) ∧ 𝑛 ∈ ( ℂ ↑pm dom 𝐹 ) ) ) → ( 𝑆 D 𝑘 ) ∈ ( ℂ ↑pm dom 𝐹 ) )
45 25 44 eqeltrid ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑘 ∈ ( ℂ ↑pm dom 𝐹 ) ∧ 𝑛 ∈ ( ℂ ↑pm dom 𝐹 ) ) ) → ( 𝑘 ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) 𝑛 ) ∈ ( ℂ ↑pm dom 𝐹 ) )
46 1 2 16 45 seqf ⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) : ℕ0 ⟶ ( ℂ ↑pm dom 𝐹 ) )
47 21 dvnfval ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( 𝑆 D𝑛 𝐹 ) = seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) )
48 30 47 sylan ⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( 𝑆 D𝑛 𝐹 ) = seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) )
49 48 feq1d ⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( ( 𝑆 D𝑛 𝐹 ) : ℕ0 ⟶ ( ℂ ↑pm dom 𝐹 ) ↔ seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) : ℕ0 ⟶ ( ℂ ↑pm dom 𝐹 ) ) )
50 46 49 mpbird ⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( 𝑆 D𝑛 𝐹 ) : ℕ0 ⟶ ( ℂ ↑pm dom 𝐹 ) )