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