Metamath Proof Explorer

Theorem cpnres

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

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

Proof

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