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 
|- ( ( S e. { RR , CC } /\ F e. ( ( C^n ` CC ) ` N ) ) -> ( F |` S ) e. ( ( C^n ` S ) ` N ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` CC ) ` N ) ) -> F e. ( ( C^n ` CC ) ` N ) )
2 ssid 
 |-  CC C_ CC
3 elfvdm 
 |-  ( F e. ( ( C^n ` CC ) ` N ) -> N e. dom ( C^n ` CC ) )
4 3 adantl 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` CC ) ` N ) ) -> N e. dom ( C^n ` CC ) )
5 fncpn 
 |-  ( CC C_ CC -> ( C^n ` CC ) Fn NN0 )
6 2 5 ax-mp 
 |-  ( C^n ` CC ) Fn NN0
7 fndm 
 |-  ( ( C^n ` CC ) Fn NN0 -> dom ( C^n ` CC ) = NN0 )
8 6 7 mp1i 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` CC ) ` N ) ) -> dom ( C^n ` CC ) = NN0 )
9 4 8 eleqtrd 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` CC ) ` N ) ) -> N e. NN0 )
10 elcpn 
 |-  ( ( CC C_ CC /\ N e. NN0 ) -> ( F e. ( ( C^n ` CC ) ` N ) <-> ( F e. ( CC ^pm CC ) /\ ( ( CC Dn F ) ` N ) e. ( dom F -cn-> CC ) ) ) )
11 2 9 10 sylancr 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` CC ) ` N ) ) -> ( F e. ( ( C^n ` CC ) ` N ) <-> ( F e. ( CC ^pm CC ) /\ ( ( CC Dn F ) ` N ) e. ( dom F -cn-> CC ) ) ) )
12 1 11 mpbid 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` CC ) ` N ) ) -> ( F e. ( CC ^pm CC ) /\ ( ( CC Dn F ) ` N ) e. ( dom F -cn-> CC ) ) )
13 12 simpld 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` CC ) ` N ) ) -> F e. ( CC ^pm CC ) )
14 pmresg 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) ) -> ( F |` S ) e. ( CC ^pm S ) )
15 13 14 syldan 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` CC ) ` N ) ) -> ( F |` S ) e. ( CC ^pm S ) )
16 simpl 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` CC ) ` N ) ) -> S e. { RR , CC } )
17 12 simprd 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` CC ) ` N ) ) -> ( ( CC Dn F ) ` N ) e. ( dom F -cn-> CC ) )
18 cncff 
 |-  ( ( ( CC Dn F ) ` N ) e. ( dom F -cn-> CC ) -> ( ( CC Dn F ) ` N ) : dom F --> CC )
19 17 18 syl 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` CC ) ` N ) ) -> ( ( CC Dn F ) ` N ) : dom F --> CC )
20 19 fdmd 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` CC ) ` N ) ) -> dom ( ( CC Dn F ) ` N ) = dom F )
21 dvnres 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) /\ N e. NN0 ) /\ dom ( ( CC Dn F ) ` N ) = dom F ) -> ( ( S Dn ( F |` S ) ) ` N ) = ( ( ( CC Dn F ) ` N ) |` S ) )
22 16 13 9 20 21 syl31anc 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` CC ) ` N ) ) -> ( ( S Dn ( F |` S ) ) ` N ) = ( ( ( CC Dn F ) ` N ) |` S ) )
23 resres 
 |-  ( ( ( ( CC Dn F ) ` N ) |` S ) |` dom F ) = ( ( ( CC Dn F ) ` N ) |` ( S i^i dom F ) )
24 rescom 
 |-  ( ( ( ( CC Dn F ) ` N ) |` S ) |` dom F ) = ( ( ( ( CC Dn F ) ` N ) |` dom F ) |` S )
25 23 24 eqtr3i 
 |-  ( ( ( CC Dn F ) ` N ) |` ( S i^i dom F ) ) = ( ( ( ( CC Dn F ) ` N ) |` dom F ) |` S )
26 ffn 
 |-  ( ( ( CC Dn F ) ` N ) : dom F --> CC -> ( ( CC Dn F ) ` N ) Fn dom F )
27 fnresdm 
 |-  ( ( ( CC Dn F ) ` N ) Fn dom F -> ( ( ( CC Dn F ) ` N ) |` dom F ) = ( ( CC Dn F ) ` N ) )
28 19 26 27 3syl 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` CC ) ` N ) ) -> ( ( ( CC Dn F ) ` N ) |` dom F ) = ( ( CC Dn F ) ` N ) )
29 28 reseq1d 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` CC ) ` N ) ) -> ( ( ( ( CC Dn F ) ` N ) |` dom F ) |` S ) = ( ( ( CC Dn F ) ` N ) |` S ) )
30 25 29 eqtrid 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` CC ) ` N ) ) -> ( ( ( CC Dn F ) ` N ) |` ( S i^i dom F ) ) = ( ( ( CC Dn F ) ` N ) |` S ) )
31 inss2 
 |-  ( S i^i dom F ) C_ dom F
32 rescncf 
 |-  ( ( S i^i dom F ) C_ dom F -> ( ( ( CC Dn F ) ` N ) e. ( dom F -cn-> CC ) -> ( ( ( CC Dn F ) ` N ) |` ( S i^i dom F ) ) e. ( ( S i^i dom F ) -cn-> CC ) ) )
33 31 17 32 mpsyl 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` CC ) ` N ) ) -> ( ( ( CC Dn F ) ` N ) |` ( S i^i dom F ) ) e. ( ( S i^i dom F ) -cn-> CC ) )
34 30 33 eqeltrrd 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` CC ) ` N ) ) -> ( ( ( CC Dn F ) ` N ) |` S ) e. ( ( S i^i dom F ) -cn-> CC ) )
35 dmres 
 |-  dom ( F |` S ) = ( S i^i dom F )
36 35 oveq1i 
 |-  ( dom ( F |` S ) -cn-> CC ) = ( ( S i^i dom F ) -cn-> CC )
37 34 36 eleqtrrdi 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` CC ) ` N ) ) -> ( ( ( CC Dn F ) ` N ) |` S ) e. ( dom ( F |` S ) -cn-> CC ) )
38 22 37 eqeltrd 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` CC ) ` N ) ) -> ( ( S Dn ( F |` S ) ) ` N ) e. ( dom ( F |` S ) -cn-> CC ) )
39 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
40 elcpn 
 |-  ( ( S C_ CC /\ N e. NN0 ) -> ( ( F |` S ) e. ( ( C^n ` S ) ` N ) <-> ( ( F |` S ) e. ( CC ^pm S ) /\ ( ( S Dn ( F |` S ) ) ` N ) e. ( dom ( F |` S ) -cn-> CC ) ) ) )
41 39 9 40 syl2an2r 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` CC ) ` N ) ) -> ( ( F |` S ) e. ( ( C^n ` S ) ` N ) <-> ( ( F |` S ) e. ( CC ^pm S ) /\ ( ( S Dn ( F |` S ) ) ` N ) e. ( dom ( F |` S ) -cn-> CC ) ) ) )
42 15 38 41 mpbir2and 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` CC ) ` N ) ) -> ( F |` S ) e. ( ( C^n ` S ) ` N ) )