cpnres

Description: The restriction of a C^n function is C^n . (Contributed by Mario Carneiro, 11-Feb-2015)

		Ref	Expression
	Assertion	cpnres	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (ℂ) (N)) \to {F ↾}_{S} \in C^{n} (S) (N)$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (ℂ) (N)) \to F \in C^{n} (ℂ) (N)$
2		ssid	$⊢ ℂ \subseteq ℂ$
3		elfvdm	$⊢ F \in C^{n} (ℂ) (N) \to N \in dom C^{n} (ℂ)$
4	3	adantl	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (ℂ) (N)) \to N \in dom C^{n} (ℂ)$
5		fncpn	$⊢ ℂ \subseteq ℂ \to C^{n} (ℂ) Fn ℕ_{0}$
6	2 5	ax-mp	$⊢ C^{n} (ℂ) Fn ℕ_{0}$
7		fndm	$⊢ C^{n} (ℂ) Fn ℕ_{0} \to dom C^{n} (ℂ) = ℕ_{0}$
8	6 7	mp1i	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (ℂ) (N)) \to dom C^{n} (ℂ) = ℕ_{0}$
9	4 8	eleqtrd	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (ℂ) (N)) \to N \in ℕ_{0}$
10		elcpn	$⊢ (ℂ \subseteq ℂ \land N \in ℕ_{0}) \to (F \in C^{n} (ℂ) (N) \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℂ) \land (ℂ D^{n} F) (N) : dom F \underset{cn}{⟶} ℂ))$
11	2 9 10	sylancr	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (ℂ) (N)) \to (F \in C^{n} (ℂ) (N) \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℂ) \land (ℂ D^{n} F) (N) : dom F \underset{cn}{⟶} ℂ))$
12	1 11	mpbid	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (ℂ) (N)) \to (F \in (ℂ ↑_{𝑝𝑚} ℂ) \land (ℂ D^{n} F) (N) : dom F \underset{cn}{⟶} ℂ)$
13	12	simpld	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (ℂ) (N)) \to F \in (ℂ ↑_{𝑝𝑚} ℂ)$
14		pmresg	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \to {F ↾}_{S} \in (ℂ ↑_{𝑝𝑚} S)$
15	13 14	syldan	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (ℂ) (N)) \to {F ↾}_{S} \in (ℂ ↑_{𝑝𝑚} S)$
16		simpl	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (ℂ) (N)) \to S \in \{ℝ, ℂ\}$
17	12	simprd	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (ℂ) (N)) \to (ℂ D^{n} F) (N) : dom F \underset{cn}{⟶} ℂ$
18		cncff	$⊢ (ℂ D^{n} F) (N) : dom F \underset{cn}{⟶} ℂ \to (ℂ D^{n} F) (N) : dom F ⟶ ℂ$
19	17 18	syl	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (ℂ) (N)) \to (ℂ D^{n} F) (N) : dom F ⟶ ℂ$
20	19	fdmd	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (ℂ) (N)) \to dom (ℂ D^{n} F) (N) = dom F$
21		dvnres	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℂ) \land N \in ℕ_{0}) \land dom (ℂ D^{n} F) (N) = dom F) \to (S D^{n} ({F ↾}_{S})) (N) = {(ℂ D^{n} F) (N) ↾}_{S}$
22	16 13 9 20 21	syl31anc	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (ℂ) (N)) \to (S D^{n} ({F ↾}_{S})) (N) = {(ℂ D^{n} F) (N) ↾}_{S}$
23		resres	$⊢ {({(ℂ D^{n} F) (N) ↾}_{S}) ↾}_{dom F} = {(ℂ D^{n} F) (N) ↾}_{(S \cap dom F)}$
24		rescom	$⊢ {({(ℂ D^{n} F) (N) ↾}_{S}) ↾}_{dom F} = {({(ℂ D^{n} F) (N) ↾}_{dom F}) ↾}_{S}$
25	23 24	eqtr3i	$⊢ {(ℂ D^{n} F) (N) ↾}_{(S \cap dom F)} = {({(ℂ D^{n} F) (N) ↾}_{dom F}) ↾}_{S}$
26		ffn	$⊢ (ℂ D^{n} F) (N) : dom F ⟶ ℂ \to (ℂ D^{n} F) (N) Fn dom F$
27		fnresdm	$⊢ (ℂ D^{n} F) (N) Fn dom F \to {(ℂ D^{n} F) (N) ↾}_{dom F} = (ℂ D^{n} F) (N)$
28	19 26 27	3syl	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (ℂ) (N)) \to {(ℂ D^{n} F) (N) ↾}_{dom F} = (ℂ D^{n} F) (N)$
29	28	reseq1d	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (ℂ) (N)) \to {({(ℂ D^{n} F) (N) ↾}_{dom F}) ↾}_{S} = {(ℂ D^{n} F) (N) ↾}_{S}$
30	25 29	syl5eq	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (ℂ) (N)) \to {(ℂ D^{n} F) (N) ↾}_{(S \cap dom F)} = {(ℂ D^{n} F) (N) ↾}_{S}$
31		inss2	$⊢ S \cap dom F \subseteq dom F$
32		rescncf	$⊢ S \cap dom F \subseteq dom F \to ((ℂ D^{n} F) (N) : dom F \underset{cn}{⟶} ℂ \to ({(ℂ D^{n} F) (N) ↾}_{(S \cap dom F)}) : (S \cap dom F) \underset{cn}{⟶} ℂ)$
33	31 17 32	mpsyl	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (ℂ) (N)) \to ({(ℂ D^{n} F) (N) ↾}_{(S \cap dom F)}) : (S \cap dom F) \underset{cn}{⟶} ℂ$
34	30 33	eqeltrrd	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (ℂ) (N)) \to ({(ℂ D^{n} F) (N) ↾}_{S}) : (S \cap dom F) \underset{cn}{⟶} ℂ$
35		dmres	$⊢ dom ({F ↾}_{S}) = S \cap dom F$
36	35	oveq1i	$⊢ dom ({F ↾}_{S}) \underset{cn}{⟶} ℂ = (S \cap dom F) \underset{cn}{⟶} ℂ$
37	34 36	eleqtrrdi	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (ℂ) (N)) \to ({(ℂ D^{n} F) (N) ↾}_{S}) : dom ({F ↾}_{S}) \underset{cn}{⟶} ℂ$
38	22 37	eqeltrd	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (ℂ) (N)) \to (S D^{n} ({F ↾}_{S})) (N) : dom ({F ↾}_{S}) \underset{cn}{⟶} ℂ$
39		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
40		elcpn	$⊢ (S \subseteq ℂ \land N \in ℕ_{0}) \to ({F ↾}_{S} \in C^{n} (S) (N) \leftrightarrow ({F ↾}_{S} \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} ({F ↾}_{S})) (N) : dom ({F ↾}_{S}) \underset{cn}{⟶} ℂ))$
41	39 9 40	syl2an2r	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (ℂ) (N)) \to ({F ↾}_{S} \in C^{n} (S) (N) \leftrightarrow ({F ↾}_{S} \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} ({F ↾}_{S})) (N) : dom ({F ↾}_{S}) \underset{cn}{⟶} ℂ))$
42	15 38 41	mpbir2and	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (ℂ) (N)) \to {F ↾}_{S} \in C^{n} (S) (N)$

Metamath Proof Explorer

Theorem cpnres

Proof