Step |
Hyp |
Ref |
Expression |
1 |
|
plyf |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 : ℂ ⟶ ℂ ) |
2 |
1
|
adantr |
⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑛 ∈ ℕ0 ) → 𝐹 : ℂ ⟶ ℂ ) |
3 |
|
cnex |
⊢ ℂ ∈ V |
4 |
3 3
|
fpm |
⊢ ( 𝐹 : ℂ ⟶ ℂ → 𝐹 ∈ ( ℂ ↑pm ℂ ) ) |
5 |
2 4
|
syl |
⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑛 ∈ ℕ0 ) → 𝐹 ∈ ( ℂ ↑pm ℂ ) ) |
6 |
|
dvnply |
⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ∈ ( Poly ‘ ℂ ) ) |
7 |
|
plycn |
⊢ ( ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ∈ ( Poly ‘ ℂ ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ∈ ( ℂ –cn→ ℂ ) ) |
8 |
6 7
|
syl |
⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ∈ ( ℂ –cn→ ℂ ) ) |
9 |
2
|
fdmd |
⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑛 ∈ ℕ0 ) → dom 𝐹 = ℂ ) |
10 |
9
|
oveq1d |
⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑛 ∈ ℕ0 ) → ( dom 𝐹 –cn→ ℂ ) = ( ℂ –cn→ ℂ ) ) |
11 |
8 10
|
eleqtrrd |
⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ∈ ( dom 𝐹 –cn→ ℂ ) ) |
12 |
|
ssidd |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ℂ ⊆ ℂ ) |
13 |
|
elcpn |
⊢ ( ( ℂ ⊆ ℂ ∧ 𝑛 ∈ ℕ0 ) → ( 𝐹 ∈ ( ( 𝓑C𝑛 ‘ ℂ ) ‘ 𝑛 ) ↔ ( 𝐹 ∈ ( ℂ ↑pm ℂ ) ∧ ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ∈ ( dom 𝐹 –cn→ ℂ ) ) ) ) |
14 |
12 13
|
sylan |
⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐹 ∈ ( ( 𝓑C𝑛 ‘ ℂ ) ‘ 𝑛 ) ↔ ( 𝐹 ∈ ( ℂ ↑pm ℂ ) ∧ ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ∈ ( dom 𝐹 –cn→ ℂ ) ) ) ) |
15 |
5 11 14
|
mpbir2and |
⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑛 ∈ ℕ0 ) → 𝐹 ∈ ( ( 𝓑C𝑛 ‘ ℂ ) ‘ 𝑛 ) ) |
16 |
15
|
ralrimiva |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∀ 𝑛 ∈ ℕ0 𝐹 ∈ ( ( 𝓑C𝑛 ‘ ℂ ) ‘ 𝑛 ) ) |
17 |
|
ssid |
⊢ ℂ ⊆ ℂ |
18 |
|
fncpn |
⊢ ( ℂ ⊆ ℂ → ( 𝓑C𝑛 ‘ ℂ ) Fn ℕ0 ) |
19 |
|
eleq2 |
⊢ ( 𝑥 = ( ( 𝓑C𝑛 ‘ ℂ ) ‘ 𝑛 ) → ( 𝐹 ∈ 𝑥 ↔ 𝐹 ∈ ( ( 𝓑C𝑛 ‘ ℂ ) ‘ 𝑛 ) ) ) |
20 |
19
|
ralrn |
⊢ ( ( 𝓑C𝑛 ‘ ℂ ) Fn ℕ0 → ( ∀ 𝑥 ∈ ran ( 𝓑C𝑛 ‘ ℂ ) 𝐹 ∈ 𝑥 ↔ ∀ 𝑛 ∈ ℕ0 𝐹 ∈ ( ( 𝓑C𝑛 ‘ ℂ ) ‘ 𝑛 ) ) ) |
21 |
17 18 20
|
mp2b |
⊢ ( ∀ 𝑥 ∈ ran ( 𝓑C𝑛 ‘ ℂ ) 𝐹 ∈ 𝑥 ↔ ∀ 𝑛 ∈ ℕ0 𝐹 ∈ ( ( 𝓑C𝑛 ‘ ℂ ) ‘ 𝑛 ) ) |
22 |
16 21
|
sylibr |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∀ 𝑥 ∈ ran ( 𝓑C𝑛 ‘ ℂ ) 𝐹 ∈ 𝑥 ) |
23 |
|
elintg |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐹 ∈ ∩ ran ( 𝓑C𝑛 ‘ ℂ ) ↔ ∀ 𝑥 ∈ ran ( 𝓑C𝑛 ‘ ℂ ) 𝐹 ∈ 𝑥 ) ) |
24 |
22 23
|
mpbird |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 ∈ ∩ ran ( 𝓑C𝑛 ‘ ℂ ) ) |