Metamath Proof Explorer


Theorem plycpn

Description: Polynomials are smooth. (Contributed by Stefan O'Rear, 16-Nov-2014) (Revised by Mario Carneiro, 11-Feb-2015)

Ref Expression
Assertion plycpn ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 ran ( 𝓑C𝑛 ‘ ℂ ) )

Proof

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𝑛 ‘ ℂ ) )