Theorem dvnfval 25672

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

Hypothesis

Ref	Expression
dvnfval.1	⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑆 D 𝑥))

Assertion

Ref	Expression
dvnfval	⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → (𝑆 D𝑛 𝐹) = seq0((𝐺 ∘ 1st ), (ℕ0 × {𝐹})))

Distinct variable groups:   𝑥,𝐹   𝑥,𝑆

Allowed substitution hint:   𝐺(𝑥)

Proof of Theorem dvnfval

Dummy variables 𝑓 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-dvn 25617	. . 3 ⊢ D𝑛 = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓})))
2	1	a1i 11	. 2 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → D𝑛 = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓}))))
3		simprl 767	. . . . . . . 8 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → 𝑠 = 𝑆)
4	3	oveq1d 7426	. . . . . . 7 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → (𝑠 D 𝑥) = (𝑆 D 𝑥))
5	4	mpteq2dv 5249	. . . . . 6 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → (𝑥 ∈ V ↦ (𝑠 D 𝑥)) = (𝑥 ∈ V ↦ (𝑆 D 𝑥)))
6		dvnfval.1	. . . . . 6 ⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑆 D 𝑥))
7	5, 6	eqtr4di 2788	. . . . 5 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → (𝑥 ∈ V ↦ (𝑠 D 𝑥)) = 𝐺)
8	7	coeq1d 5860	. . . 4 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → ((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ) = (𝐺 ∘ 1st ))
9	8	seqeq2d 13977	. . 3 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓})) = seq0((𝐺 ∘ 1st ), (ℕ0 × {𝑓})))
10		simprr 769	. . . . . 6 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → 𝑓 = 𝐹)
11	10	sneqd 4639	. . . . 5 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → {𝑓} = {𝐹})
12	11	xpeq2d 5705	. . . 4 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → (ℕ0 × {𝑓}) = (ℕ0 × {𝐹}))
13	12	seqeq3d 13978	. . 3 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → seq0((𝐺 ∘ 1st ), (ℕ0 × {𝑓})) = seq0((𝐺 ∘ 1st ), (ℕ0 × {𝐹})))
14	9, 13	eqtrd 2770	. 2 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓})) = seq0((𝐺 ∘ 1st ), (ℕ0 × {𝐹})))
15		simpr 483	. . 3 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ 𝑠 = 𝑆) → 𝑠 = 𝑆)
16	15	oveq2d 7427	. 2 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ 𝑠 = 𝑆) → (ℂ ↑pm 𝑠) = (ℂ ↑pm 𝑆))
17		simpl 481	. . 3 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → 𝑆 ⊆ ℂ)
18		cnex 11193	. . . 4 ⊢ ℂ ∈ V
19	18	elpw2 5344	. . 3 ⊢ (𝑆 ∈ 𝒫 ℂ ↔ 𝑆 ⊆ ℂ)
20	17, 19	sylibr 233	. 2 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → 𝑆 ∈ 𝒫 ℂ)
21		simpr 483	. 2 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → 𝐹 ∈ (ℂ ↑pm 𝑆))
22		seqex 13972	. . 3 ⊢ seq0((𝐺 ∘ 1st ), (ℕ0 × {𝐹})) ∈ V
23	22	a1i 11	. 2 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → seq0((𝐺 ∘ 1st ), (ℕ0 × {𝐹})) ∈ V)
24	2, 14, 16, 20, 21, 23	ovmpodx 7561	1 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → (𝑆 D𝑛 𝐹) = seq0((𝐺 ∘ 1st ), (ℕ0 × {𝐹})))

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1539   ∈ wcel 2104  Vcvv 3472   ⊆ wss 3947  𝒫 cpw 4601  {csn 4627   ↦ cmpt 5230   × cxp 5673   ∘ ccom 5679  (class class class)co 7411   ∈ cmpo 7413  1^st c1st 7975   ↑_pm cpm 8823  ℂcc 11110  0cc0 11112  ℕ₀cn0 12476  seqcseq 13970   D cdv 25612   D^𝑛 cdvn 25613

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7727  ax-inf2 9638  ax-cnex 11168

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-seq 13971  df-dvn 25617

This theorem is referenced by:  dvnff  25673  dvn0  25674  dvnp1  25675