Step | Hyp | Ref
| Expression |
1 | | nn0uz 12620 |
. . 3
⊢
ℕ0 = (ℤ≥‘0) |
2 | | 0zd 12331 |
. . 3
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
→ 0 ∈ ℤ) |
3 | | fvconst2g 7077 |
. . . . 5
⊢ ((𝐹 ∈ (ℂ
↑pm 𝑆)
∧ 𝑘 ∈
ℕ0) → ((ℕ0 × {𝐹})‘𝑘) = 𝐹) |
4 | 3 | adantll 711 |
. . . 4
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑘 ∈
ℕ0) → ((ℕ0 × {𝐹})‘𝑘) = 𝐹) |
5 | | dmexg 7750 |
. . . . . 6
⊢ (𝐹 ∈ (ℂ
↑pm 𝑆)
→ dom 𝐹 ∈
V) |
6 | 5 | ad2antlr 724 |
. . . . 5
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑘 ∈
ℕ0) → dom 𝐹 ∈ V) |
7 | | cnex 10952 |
. . . . . 6
⊢ ℂ
∈ V |
8 | 7 | a1i 11 |
. . . . 5
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑘 ∈
ℕ0) → ℂ ∈ V) |
9 | | elpm2g 8632 |
. . . . . . . . 9
⊢ ((ℂ
∈ V ∧ 𝑆 ∈
{ℝ, ℂ}) → (𝐹 ∈ (ℂ ↑pm 𝑆) ↔ (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ 𝑆))) |
10 | 7, 9 | mpan 687 |
. . . . . . . 8
⊢ (𝑆 ∈ {ℝ, ℂ}
→ (𝐹 ∈ (ℂ
↑pm 𝑆)
↔ (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ 𝑆))) |
11 | 10 | biimpa 477 |
. . . . . . 7
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
→ (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ 𝑆)) |
12 | 11 | simpld 495 |
. . . . . 6
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
→ 𝐹:dom 𝐹⟶ℂ) |
13 | 12 | adantr 481 |
. . . . 5
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑘 ∈
ℕ0) → 𝐹:dom 𝐹⟶ℂ) |
14 | | fpmg 8656 |
. . . . 5
⊢ ((dom
𝐹 ∈ V ∧ ℂ
∈ V ∧ 𝐹:dom 𝐹⟶ℂ) → 𝐹 ∈ (ℂ
↑pm dom 𝐹)) |
15 | 6, 8, 13, 14 | syl3anc 1370 |
. . . 4
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑘 ∈
ℕ0) → 𝐹 ∈ (ℂ ↑pm dom
𝐹)) |
16 | 4, 15 | eqeltrd 2839 |
. . 3
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑘 ∈
ℕ0) → ((ℕ0 × {𝐹})‘𝑘) ∈ (ℂ ↑pm dom
𝐹)) |
17 | | vex 3436 |
. . . . . 6
⊢ 𝑘 ∈ V |
18 | | vex 3436 |
. . . . . 6
⊢ 𝑛 ∈ V |
19 | 17, 18 | opco1i 7966 |
. . . . 5
⊢ (𝑘((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1st )𝑛) = ((𝑥 ∈ V ↦ (𝑆 D 𝑥))‘𝑘) |
20 | | oveq2 7283 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (𝑆 D 𝑥) = (𝑆 D 𝑘)) |
21 | | eqid 2738 |
. . . . . . 7
⊢ (𝑥 ∈ V ↦ (𝑆 D 𝑥)) = (𝑥 ∈ V ↦ (𝑆 D 𝑥)) |
22 | | ovex 7308 |
. . . . . . 7
⊢ (𝑆 D 𝑘) ∈ V |
23 | 20, 21, 22 | fvmpt 6875 |
. . . . . 6
⊢ (𝑘 ∈ V → ((𝑥 ∈ V ↦ (𝑆 D 𝑥))‘𝑘) = (𝑆 D 𝑘)) |
24 | 23 | elv 3438 |
. . . . 5
⊢ ((𝑥 ∈ V ↦ (𝑆 D 𝑥))‘𝑘) = (𝑆 D 𝑘) |
25 | 19, 24 | eqtri 2766 |
. . . 4
⊢ (𝑘((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1st )𝑛) = (𝑆 D 𝑘) |
26 | 7 | a1i 11 |
. . . . 5
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑘 ∈ (ℂ
↑pm dom 𝐹)
∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → ℂ ∈
V) |
27 | 5 | ad2antlr 724 |
. . . . 5
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑘 ∈ (ℂ
↑pm dom 𝐹)
∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → dom 𝐹 ∈ V) |
28 | | dvfg 25070 |
. . . . . 6
⊢ (𝑆 ∈ {ℝ, ℂ}
→ (𝑆 D 𝑘):dom (𝑆 D 𝑘)⟶ℂ) |
29 | 28 | ad2antrr 723 |
. . . . 5
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑘 ∈ (ℂ
↑pm dom 𝐹)
∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → (𝑆 D 𝑘):dom (𝑆 D 𝑘)⟶ℂ) |
30 | | recnprss 25068 |
. . . . . . . 8
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
31 | 30 | ad2antrr 723 |
. . . . . . 7
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑘 ∈ (ℂ
↑pm dom 𝐹)
∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → 𝑆 ⊆ ℂ) |
32 | | simprl 768 |
. . . . . . . . 9
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑘 ∈ (ℂ
↑pm dom 𝐹)
∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → 𝑘 ∈ (ℂ ↑pm dom
𝐹)) |
33 | | elpm2g 8632 |
. . . . . . . . . 10
⊢ ((ℂ
∈ V ∧ dom 𝐹 ∈
V) → (𝑘 ∈
(ℂ ↑pm dom 𝐹) ↔ (𝑘:dom 𝑘⟶ℂ ∧ dom 𝑘 ⊆ dom 𝐹))) |
34 | 7, 27, 33 | sylancr 587 |
. . . . . . . . 9
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑘 ∈ (ℂ
↑pm dom 𝐹)
∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → (𝑘 ∈ (ℂ ↑pm dom
𝐹) ↔ (𝑘:dom 𝑘⟶ℂ ∧ dom 𝑘 ⊆ dom 𝐹))) |
35 | 32, 34 | mpbid 231 |
. . . . . . . 8
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑘 ∈ (ℂ
↑pm dom 𝐹)
∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → (𝑘:dom 𝑘⟶ℂ ∧ dom 𝑘 ⊆ dom 𝐹)) |
36 | 35 | simpld 495 |
. . . . . . 7
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑘 ∈ (ℂ
↑pm dom 𝐹)
∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → 𝑘:dom 𝑘⟶ℂ) |
37 | 35 | simprd 496 |
. . . . . . . 8
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑘 ∈ (ℂ
↑pm dom 𝐹)
∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → dom 𝑘 ⊆ dom 𝐹) |
38 | 11 | simprd 496 |
. . . . . . . . 9
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
→ dom 𝐹 ⊆ 𝑆) |
39 | 38 | adantr 481 |
. . . . . . . 8
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑘 ∈ (ℂ
↑pm dom 𝐹)
∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → dom 𝐹 ⊆ 𝑆) |
40 | 37, 39 | sstrd 3931 |
. . . . . . 7
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑘 ∈ (ℂ
↑pm dom 𝐹)
∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → dom 𝑘 ⊆ 𝑆) |
41 | 31, 36, 40 | dvbss 25065 |
. . . . . 6
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑘 ∈ (ℂ
↑pm dom 𝐹)
∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → dom (𝑆 D 𝑘) ⊆ dom 𝑘) |
42 | 41, 37 | sstrd 3931 |
. . . . 5
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑘 ∈ (ℂ
↑pm dom 𝐹)
∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → dom (𝑆 D 𝑘) ⊆ dom 𝐹) |
43 | | elpm2r 8633 |
. . . . 5
⊢
(((ℂ ∈ V ∧ dom 𝐹 ∈ V) ∧ ((𝑆 D 𝑘):dom (𝑆 D 𝑘)⟶ℂ ∧ dom (𝑆 D 𝑘) ⊆ dom 𝐹)) → (𝑆 D 𝑘) ∈ (ℂ ↑pm dom
𝐹)) |
44 | 26, 27, 29, 42, 43 | syl22anc 836 |
. . . 4
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑘 ∈ (ℂ
↑pm dom 𝐹)
∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → (𝑆 D 𝑘) ∈ (ℂ ↑pm dom
𝐹)) |
45 | 25, 44 | eqeltrid 2843 |
. . 3
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑘 ∈ (ℂ
↑pm dom 𝐹)
∧ 𝑛 ∈ (ℂ
↑pm dom 𝐹))) → (𝑘((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1st )𝑛) ∈ (ℂ ↑pm dom
𝐹)) |
46 | 1, 2, 16, 45 | seqf 13744 |
. 2
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
→ seq0(((𝑥 ∈ V
↦ (𝑆 D 𝑥)) ∘ 1st ),
(ℕ0 × {𝐹})):ℕ0⟶(ℂ
↑pm dom 𝐹)) |
47 | 21 | dvnfval 25086 |
. . . 4
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
→ (𝑆
D𝑛 𝐹) =
seq0(((𝑥 ∈ V ↦
(𝑆 D 𝑥)) ∘ 1st ),
(ℕ0 × {𝐹}))) |
48 | 30, 47 | sylan 580 |
. . 3
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
→ (𝑆
D𝑛 𝐹) =
seq0(((𝑥 ∈ V ↦
(𝑆 D 𝑥)) ∘ 1st ),
(ℕ0 × {𝐹}))) |
49 | 48 | feq1d 6585 |
. 2
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
→ ((𝑆
D𝑛 𝐹):ℕ0⟶(ℂ
↑pm dom 𝐹)
↔ seq0(((𝑥 ∈ V
↦ (𝑆 D 𝑥)) ∘ 1st ),
(ℕ0 × {𝐹})):ℕ0⟶(ℂ
↑pm dom 𝐹))) |
50 | 46, 49 | mpbird 256 |
1
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
→ (𝑆
D𝑛 𝐹):ℕ0⟶(ℂ
↑pm dom 𝐹)) |