This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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