cpnres

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

		Ref	Expression
	Assertion	cpnres	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℂ ) ‘ 𝑁 ) ) → ( 𝐹 ↾ 𝑆 ) ∈ ( ( 𝓑C^𝑛 ‘ 𝑆 ) ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℂ ) ‘ 𝑁 ) ) → 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℂ ) ‘ 𝑁 ) )
2		ssid	⊢ ℂ ⊆ ℂ
3		elfvdm	⊢ ( 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℂ ) ‘ 𝑁 ) → 𝑁 ∈ dom ( 𝓑C^𝑛 ‘ ℂ ) )
4	3	adantl	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℂ ) ‘ 𝑁 ) ) → 𝑁 ∈ dom ( 𝓑C^𝑛 ‘ ℂ ) )
5		fncpn	⊢ ( ℂ ⊆ ℂ → ( 𝓑C^𝑛 ‘ ℂ ) Fn ℕ₀ )
6	2 5	ax-mp	⊢ ( 𝓑C^𝑛 ‘ ℂ ) Fn ℕ₀
7		fndm	⊢ ( ( 𝓑C^𝑛 ‘ ℂ ) Fn ℕ₀ → dom ( 𝓑C^𝑛 ‘ ℂ ) = ℕ₀ )
8	6 7	mp1i	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℂ ) ‘ 𝑁 ) ) → dom ( 𝓑C^𝑛 ‘ ℂ ) = ℕ₀ )
9	4 8	eleqtrd	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℂ ) ‘ 𝑁 ) ) → 𝑁 ∈ ℕ₀ )
10		elcpn	⊢ ( ( ℂ ⊆ ℂ ∧ 𝑁 ∈ ℕ₀ ) → ( 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℂ ) ‘ 𝑁 ) ↔ ( 𝐹 ∈ ( ℂ ↑_pm ℂ ) ∧ ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( dom 𝐹 –cn→ ℂ ) ) ) )
11	2 9 10	sylancr	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℂ ) ‘ 𝑁 ) ) → ( 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℂ ) ‘ 𝑁 ) ↔ ( 𝐹 ∈ ( ℂ ↑_pm ℂ ) ∧ ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( dom 𝐹 –cn→ ℂ ) ) ) )
12	1 11	mpbid	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℂ ) ‘ 𝑁 ) ) → ( 𝐹 ∈ ( ℂ ↑_pm ℂ ) ∧ ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( dom 𝐹 –cn→ ℂ ) ) )
13	12	simpld	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℂ ) ‘ 𝑁 ) ) → 𝐹 ∈ ( ℂ ↑_pm ℂ ) )
14		pmresg	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm ℂ ) ) → ( 𝐹 ↾ 𝑆 ) ∈ ( ℂ ↑_pm 𝑆 ) )
15	13 14	syldan	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℂ ) ‘ 𝑁 ) ) → ( 𝐹 ↾ 𝑆 ) ∈ ( ℂ ↑_pm 𝑆 ) )
16		simpl	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℂ ) ‘ 𝑁 ) ) → 𝑆 ∈ { ℝ , ℂ } )
17	12	simprd	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℂ ) ‘ 𝑁 ) ) → ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( dom 𝐹 –cn→ ℂ ) )
18		cncff	⊢ ( ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( dom 𝐹 –cn→ ℂ ) → ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) : dom 𝐹 ⟶ ℂ )
19	17 18	syl	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℂ ) ‘ 𝑁 ) ) → ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) : dom 𝐹 ⟶ ℂ )
20	19	fdmd	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℂ ) ‘ 𝑁 ) ) → dom ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) = dom 𝐹 )
21		dvnres	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm ℂ ) ∧ 𝑁 ∈ ℕ₀ ) ∧ dom ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) = dom 𝐹 ) → ( ( 𝑆 D^𝑛 ( 𝐹 ↾ 𝑆 ) ) ‘ 𝑁 ) = ( ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) ↾ 𝑆 ) )
22	16 13 9 20 21	syl31anc	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℂ ) ‘ 𝑁 ) ) → ( ( 𝑆 D^𝑛 ( 𝐹 ↾ 𝑆 ) ) ‘ 𝑁 ) = ( ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) ↾ 𝑆 ) )
23		resres	⊢ ( ( ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) ↾ 𝑆 ) ↾ dom 𝐹 ) = ( ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) ↾ ( 𝑆 ∩ dom 𝐹 ) )
24		rescom	⊢ ( ( ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) ↾ 𝑆 ) ↾ dom 𝐹 ) = ( ( ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) ↾ dom 𝐹 ) ↾ 𝑆 )
25	23 24	eqtr3i	⊢ ( ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) ↾ ( 𝑆 ∩ dom 𝐹 ) ) = ( ( ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) ↾ dom 𝐹 ) ↾ 𝑆 )
26		ffn	⊢ ( ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) : dom 𝐹 ⟶ ℂ → ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) Fn dom 𝐹 )
27		fnresdm	⊢ ( ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) Fn dom 𝐹 → ( ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) ↾ dom 𝐹 ) = ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) )
28	19 26 27	3syl	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℂ ) ‘ 𝑁 ) ) → ( ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) ↾ dom 𝐹 ) = ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) )
29	28	reseq1d	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℂ ) ‘ 𝑁 ) ) → ( ( ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) ↾ dom 𝐹 ) ↾ 𝑆 ) = ( ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) ↾ 𝑆 ) )
30	25 29	syl5eq	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℂ ) ‘ 𝑁 ) ) → ( ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) ↾ ( 𝑆 ∩ dom 𝐹 ) ) = ( ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) ↾ 𝑆 ) )
31		inss2	⊢ ( 𝑆 ∩ dom 𝐹 ) ⊆ dom 𝐹
32		rescncf	⊢ ( ( 𝑆 ∩ dom 𝐹 ) ⊆ dom 𝐹 → ( ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( dom 𝐹 –cn→ ℂ ) → ( ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) ↾ ( 𝑆 ∩ dom 𝐹 ) ) ∈ ( ( 𝑆 ∩ dom 𝐹 ) –cn→ ℂ ) ) )
33	31 17 32	mpsyl	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℂ ) ‘ 𝑁 ) ) → ( ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) ↾ ( 𝑆 ∩ dom 𝐹 ) ) ∈ ( ( 𝑆 ∩ dom 𝐹 ) –cn→ ℂ ) )
34	30 33	eqeltrrd	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℂ ) ‘ 𝑁 ) ) → ( ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) ↾ 𝑆 ) ∈ ( ( 𝑆 ∩ dom 𝐹 ) –cn→ ℂ ) )
35		dmres	⊢ dom ( 𝐹 ↾ 𝑆 ) = ( 𝑆 ∩ dom 𝐹 )
36	35	oveq1i	⊢ ( dom ( 𝐹 ↾ 𝑆 ) –cn→ ℂ ) = ( ( 𝑆 ∩ dom 𝐹 ) –cn→ ℂ )
37	34 36	eleqtrrdi	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℂ ) ‘ 𝑁 ) ) → ( ( ( ℂ D^𝑛 𝐹 ) ‘ 𝑁 ) ↾ 𝑆 ) ∈ ( dom ( 𝐹 ↾ 𝑆 ) –cn→ ℂ ) )
38	22 37	eqeltrd	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℂ ) ‘ 𝑁 ) ) → ( ( 𝑆 D^𝑛 ( 𝐹 ↾ 𝑆 ) ) ‘ 𝑁 ) ∈ ( dom ( 𝐹 ↾ 𝑆 ) –cn→ ℂ ) )
39		recnprss	⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
40		elcpn	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ₀ ) → ( ( 𝐹 ↾ 𝑆 ) ∈ ( ( 𝓑C^𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ↔ ( ( 𝐹 ↾ 𝑆 ) ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 ( 𝐹 ↾ 𝑆 ) ) ‘ 𝑁 ) ∈ ( dom ( 𝐹 ↾ 𝑆 ) –cn→ ℂ ) ) ) )
41	39 9 40	syl2an2r	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℂ ) ‘ 𝑁 ) ) → ( ( 𝐹 ↾ 𝑆 ) ∈ ( ( 𝓑C^𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ↔ ( ( 𝐹 ↾ 𝑆 ) ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( ( 𝑆 D^𝑛 ( 𝐹 ↾ 𝑆 ) ) ‘ 𝑁 ) ∈ ( dom ( 𝐹 ↾ 𝑆 ) –cn→ ℂ ) ) ) )
42	15 38 41	mpbir2and	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C^𝑛 ‘ ℂ ) ‘ 𝑁 ) ) → ( 𝐹 ↾ 𝑆 ) ∈ ( ( 𝓑C^𝑛 ‘ 𝑆 ) ‘ 𝑁 ) )

Metamath Proof Explorer

Theorem cpnres

Proof