plycpn

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

		Ref	Expression
	Assertion	plycpn	$⊢ F \in Poly (S) \to F \in ⋂ ran C^{n} (ℂ)$

Proof

Step	Hyp	Ref	Expression
1		plyf	$⊢ F \in Poly (S) \to F : ℂ ⟶ ℂ$
2	1	adantr	$⊢ (F \in Poly (S) \land n \in ℕ_{0}) \to F : ℂ ⟶ ℂ$
3		cnex	$⊢ ℂ \in V$
4	3 3	fpm	$⊢ F : ℂ ⟶ ℂ \to F \in (ℂ ↑_{𝑝𝑚} ℂ)$
5	2 4	syl	$⊢ (F \in Poly (S) \land n \in ℕ_{0}) \to F \in (ℂ ↑_{𝑝𝑚} ℂ)$
6		dvnply	$⊢ (F \in Poly (S) \land n \in ℕ_{0}) \to (ℂ D^{n} F) (n) \in Poly (ℂ)$
7		plycn	$⊢ (ℂ D^{n} F) (n) \in Poly (ℂ) \to (ℂ D^{n} F) (n) : ℂ \underset{cn}{⟶} ℂ$
8	6 7	syl	$⊢ (F \in Poly (S) \land n \in ℕ_{0}) \to (ℂ D^{n} F) (n) : ℂ \underset{cn}{⟶} ℂ$
9	2	fdmd	$⊢ (F \in Poly (S) \land n \in ℕ_{0}) \to dom F = ℂ$
10	9	oveq1d	$⊢ (F \in Poly (S) \land n \in ℕ_{0}) \to dom F \underset{cn}{⟶} ℂ = ℂ \underset{cn}{⟶} ℂ$
11	8 10	eleqtrrd	$⊢ (F \in Poly (S) \land n \in ℕ_{0}) \to (ℂ D^{n} F) (n) : dom F \underset{cn}{⟶} ℂ$
12		ssidd	$⊢ F \in Poly (S) \to ℂ \subseteq ℂ$
13		elcpn	$⊢ (ℂ \subseteq ℂ \land n \in ℕ_{0}) \to (F \in C^{n} (ℂ) (n) \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℂ) \land (ℂ D^{n} F) (n) : dom F \underset{cn}{⟶} ℂ))$
14	12 13	sylan	$⊢ (F \in Poly (S) \land n \in ℕ_{0}) \to (F \in C^{n} (ℂ) (n) \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℂ) \land (ℂ D^{n} F) (n) : dom F \underset{cn}{⟶} ℂ))$
15	5 11 14	mpbir2and	$⊢ (F \in Poly (S) \land n \in ℕ_{0}) \to F \in C^{n} (ℂ) (n)$
16	15	ralrimiva	$⊢ F \in Poly (S) \to \forall n \in ℕ_{0} F \in C^{n} (ℂ) (n)$
17		ssid	$⊢ ℂ \subseteq ℂ$
18		fncpn	$⊢ ℂ \subseteq ℂ \to C^{n} (ℂ) Fn ℕ_{0}$
19		eleq2	$⊢ x = C^{n} (ℂ) (n) \to (F \in x \leftrightarrow F \in C^{n} (ℂ) (n))$
20	19	ralrn	$⊢ C^{n} (ℂ) Fn ℕ_{0} \to (\forall x \in ran C^{n} (ℂ) F \in x \leftrightarrow \forall n \in ℕ_{0} F \in C^{n} (ℂ) (n))$
21	17 18 20	mp2b	$⊢ \forall x \in ran C^{n} (ℂ) F \in x \leftrightarrow \forall n \in ℕ_{0} F \in C^{n} (ℂ) (n)$
22	16 21	sylibr	$⊢ F \in Poly (S) \to \forall x \in ran C^{n} (ℂ) F \in x$
23		elintg	$⊢ F \in Poly (S) \to (F \in ⋂ ran C^{n} (ℂ) \leftrightarrow \forall x \in ran C^{n} (ℂ) F \in x)$
24	22 23	mpbird	$⊢ F \in Poly (S) \to F \in ⋂ ran C^{n} (ℂ)$

Metamath Proof Explorer

Theorem plycpn

Proof