Step | Hyp | Ref
| Expression |
1 | | nn0uz 12004 |
. . 3
⊢
ℕ0 = (ℤ≥‘0) |
2 | | 0zd 11716 |
. . 3
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) → 0 ∈ ℤ) |
3 | | fvconst2g 6723 |
. . . . 5
⊢ ((𝐹 ∈ (ℂ
↑pm 𝑆) ∧ 𝑘 ∈ ℕ0) →
((ℕ0 × {𝐹})‘𝑘) = 𝐹) |
4 | 3 | adantll 707 |
. . . 4
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑘 ∈ ℕ0) →
((ℕ0 × {𝐹})‘𝑘) = 𝐹) |
5 | | dmexg 7358 |
. . . . . 6
⊢ (𝐹 ∈ (ℂ
↑pm 𝑆) → dom 𝐹 ∈ V) |
6 | 5 | ad2antlr 720 |
. . . . 5
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑘 ∈ ℕ0) → dom 𝐹 ∈ V) |
7 | | cnex 10333 |
. . . . . 6
⊢ ℂ
∈ V |
8 | 7 | a1i 11 |
. . . . 5
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑘 ∈ ℕ0) → ℂ
∈ V) |
9 | | elpm2g 8139 |
. . . . . . . . 9
⊢ ((ℂ
∈ V ∧ 𝑆 ∈
{ℝ, ℂ}) → (𝐹 ∈ (ℂ ↑pm
𝑆) ↔ (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ 𝑆))) |
10 | 7, 9 | mpan 683 |
. . . . . . . 8
⊢ (𝑆 ∈ {ℝ, ℂ}
→ (𝐹 ∈ (ℂ
↑pm 𝑆) ↔ (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ 𝑆))) |
11 | 10 | biimpa 470 |
. . . . . . 7
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ 𝑆)) |
12 | 11 | simpld 490 |
. . . . . 6
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) → 𝐹:dom 𝐹⟶ℂ) |
13 | 12 | adantr 474 |
. . . . 5
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑘 ∈ ℕ0) → 𝐹:dom 𝐹⟶ℂ) |
14 | | fpmg 8148 |
. . . . 5
⊢ ((dom
𝐹 ∈ V ∧ ℂ
∈ V ∧ 𝐹:dom 𝐹⟶ℂ) → 𝐹 ∈ (ℂ
↑pm dom 𝐹)) |
15 | 6, 8, 13, 14 | syl3anc 1496 |
. . . 4
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑘 ∈ ℕ0) → 𝐹 ∈ (ℂ
↑pm dom 𝐹)) |
16 | 4, 15 | eqeltrd 2906 |
. . 3
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑘 ∈ ℕ0) →
((ℕ0 × {𝐹})‘𝑘) ∈ (ℂ ↑pm
dom 𝐹)) |
17 | | vex 3417 |
. . . . . 6
⊢ 𝑘 ∈ V |
18 | | vex 3417 |
. . . . . 6
⊢ 𝑛 ∈ V |
19 | 17, 18 | algrflem 7550 |
. . . . 5
⊢ (𝑘((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1st )𝑛) = ((𝑥 ∈ V ↦ (𝑆 D 𝑥))‘𝑘) |
20 | | oveq2 6913 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (𝑆 D 𝑥) = (𝑆 D 𝑘)) |
21 | | eqid 2825 |
. . . . . . 7
⊢ (𝑥 ∈ V ↦ (𝑆 D 𝑥)) = (𝑥 ∈ V ↦ (𝑆 D 𝑥)) |
22 | | ovex 6937 |
. . . . . . 7
⊢ (𝑆 D 𝑘) ∈ V |
23 | 20, 21, 22 | fvmpt 6529 |
. . . . . 6
⊢ (𝑘 ∈ V → ((𝑥 ∈ V ↦ (𝑆 D 𝑥))‘𝑘) = (𝑆 D 𝑘)) |
24 | 17, 23 | ax-mp 5 |
. . . . 5
⊢ ((𝑥 ∈ V ↦ (𝑆 D 𝑥))‘𝑘) = (𝑆 D 𝑘) |
25 | 19, 24 | eqtri 2849 |
. . . 4
⊢ (𝑘((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1st )𝑛) = (𝑆 D 𝑘) |
26 | 7 | a1i 11 |
. . . . 5
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ (𝑘 ∈ (ℂ ↑pm
dom 𝐹) ∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → ℂ ∈
V) |
27 | 5 | ad2antlr 720 |
. . . . 5
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ (𝑘 ∈ (ℂ ↑pm
dom 𝐹) ∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → dom 𝐹 ∈ V) |
28 | | dvfg 24069 |
. . . . . 6
⊢ (𝑆 ∈ {ℝ, ℂ}
→ (𝑆 D 𝑘):dom (𝑆 D 𝑘)⟶ℂ) |
29 | 28 | ad2antrr 719 |
. . . . 5
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ (𝑘 ∈ (ℂ ↑pm
dom 𝐹) ∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → (𝑆 D 𝑘):dom (𝑆 D 𝑘)⟶ℂ) |
30 | | recnprss 24067 |
. . . . . . . 8
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
31 | 30 | ad2antrr 719 |
. . . . . . 7
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ (𝑘 ∈ (ℂ ↑pm
dom 𝐹) ∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → 𝑆 ⊆ ℂ) |
32 | | simprl 789 |
. . . . . . . . 9
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ (𝑘 ∈ (ℂ ↑pm
dom 𝐹) ∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → 𝑘 ∈ (ℂ ↑pm
dom 𝐹)) |
33 | | elpm2g 8139 |
. . . . . . . . . 10
⊢ ((ℂ
∈ V ∧ dom 𝐹 ∈
V) → (𝑘 ∈
(ℂ ↑pm dom 𝐹) ↔ (𝑘:dom 𝑘⟶ℂ ∧ dom 𝑘 ⊆ dom 𝐹))) |
34 | 7, 27, 33 | sylancr 583 |
. . . . . . . . 9
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ (𝑘 ∈ (ℂ ↑pm
dom 𝐹) ∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → (𝑘 ∈ (ℂ ↑pm
dom 𝐹) ↔ (𝑘:dom 𝑘⟶ℂ ∧ dom 𝑘 ⊆ dom 𝐹))) |
35 | 32, 34 | mpbid 224 |
. . . . . . . 8
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ (𝑘 ∈ (ℂ ↑pm
dom 𝐹) ∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → (𝑘:dom 𝑘⟶ℂ ∧ dom 𝑘 ⊆ dom 𝐹)) |
36 | 35 | simpld 490 |
. . . . . . 7
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ (𝑘 ∈ (ℂ ↑pm
dom 𝐹) ∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → 𝑘:dom 𝑘⟶ℂ) |
37 | 35 | simprd 491 |
. . . . . . . 8
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ (𝑘 ∈ (ℂ ↑pm
dom 𝐹) ∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → dom 𝑘 ⊆ dom 𝐹) |
38 | 11 | simprd 491 |
. . . . . . . . 9
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) → dom 𝐹 ⊆ 𝑆) |
39 | 38 | adantr 474 |
. . . . . . . 8
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ (𝑘 ∈ (ℂ ↑pm
dom 𝐹) ∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → dom 𝐹 ⊆ 𝑆) |
40 | 37, 39 | sstrd 3837 |
. . . . . . 7
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ (𝑘 ∈ (ℂ ↑pm
dom 𝐹) ∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → dom 𝑘 ⊆ 𝑆) |
41 | 31, 36, 40 | dvbss 24064 |
. . . . . 6
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ (𝑘 ∈ (ℂ ↑pm
dom 𝐹) ∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → dom (𝑆 D 𝑘) ⊆ dom 𝑘) |
42 | 41, 37 | sstrd 3837 |
. . . . 5
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ (𝑘 ∈ (ℂ ↑pm
dom 𝐹) ∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → dom (𝑆 D 𝑘) ⊆ dom 𝐹) |
43 | | elpm2r 8140 |
. . . . 5
⊢
(((ℂ ∈ V ∧ dom 𝐹 ∈ V) ∧ ((𝑆 D 𝑘):dom (𝑆 D 𝑘)⟶ℂ ∧ dom (𝑆 D 𝑘) ⊆ dom 𝐹)) → (𝑆 D 𝑘) ∈ (ℂ ↑pm
dom 𝐹)) |
44 | 26, 27, 29, 42, 43 | syl22anc 874 |
. . . 4
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ (𝑘 ∈ (ℂ ↑pm
dom 𝐹) ∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → (𝑆 D 𝑘) ∈ (ℂ ↑pm
dom 𝐹)) |
45 | 25, 44 | syl5eqel 2910 |
. . 3
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ (𝑘 ∈ (ℂ ↑pm
dom 𝐹) ∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → (𝑘((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1st )𝑛) ∈ (ℂ ↑pm
dom 𝐹)) |
46 | 1, 2, 16, 45 | seqf 13116 |
. 2
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) → seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1st ),
(ℕ0 × {𝐹})):ℕ0⟶(ℂ
↑pm dom 𝐹)) |
47 | 21 | dvnfval 24084 |
. . . 4
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆)) → (𝑆 D𝑛 𝐹) = seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1st ),
(ℕ0 × {𝐹}))) |
48 | 30, 47 | sylan 577 |
. . 3
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) → (𝑆 D𝑛 𝐹) = seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1st ),
(ℕ0 × {𝐹}))) |
49 | 48 | feq1d 6263 |
. 2
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) → ((𝑆 D𝑛 𝐹):ℕ0⟶(ℂ
↑pm dom 𝐹) ↔ seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1st ),
(ℕ0 × {𝐹})):ℕ0⟶(ℂ
↑pm dom 𝐹))) |
50 | 46, 49 | mpbird 249 |
1
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) → (𝑆 D𝑛 𝐹):ℕ0⟶(ℂ
↑pm dom 𝐹)) |