Metamath Proof Explorer

Theorem 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 e. ( Poly ` S ) -> F e. |^| ran ( C^n ` CC ) )

Proof

Step Hyp Ref Expression
1 plyf 
 |-  ( F e. ( Poly ` S ) -> F : CC --> CC )
2 1 adantr 
 |-  ( ( F e. ( Poly ` S ) /\ n e. NN0 ) -> F : CC --> CC )
3 cnex 
 |-  CC e. _V
4 3 3 fpm 
 |-  ( F : CC --> CC -> F e. ( CC ^pm CC ) )
5 2 4 syl 
 |-  ( ( F e. ( Poly ` S ) /\ n e. NN0 ) -> F e. ( CC ^pm CC ) )
6 dvnply 
 |-  ( ( F e. ( Poly ` S ) /\ n e. NN0 ) -> ( ( CC Dn F ) ` n ) e. ( Poly ` CC ) )
7 plycn 
 |-  ( ( ( CC Dn F ) ` n ) e. ( Poly ` CC ) -> ( ( CC Dn F ) ` n ) e. ( CC -cn-> CC ) )
8 6 7 syl 
 |-  ( ( F e. ( Poly ` S ) /\ n e. NN0 ) -> ( ( CC Dn F ) ` n ) e. ( CC -cn-> CC ) )
9 2 fdmd 
 |-  ( ( F e. ( Poly ` S ) /\ n e. NN0 ) -> dom F = CC )
10 9 oveq1d 
 |-  ( ( F e. ( Poly ` S ) /\ n e. NN0 ) -> ( dom F -cn-> CC ) = ( CC -cn-> CC ) )
11 8 10 eleqtrrd 
 |-  ( ( F e. ( Poly ` S ) /\ n e. NN0 ) -> ( ( CC Dn F ) ` n ) e. ( dom F -cn-> CC ) )
12 ssidd 
 |-  ( F e. ( Poly ` S ) -> CC C_ CC )
13 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 ) ) ) )
14 12 13 sylan 
 |-  ( ( F e. ( Poly ` S ) /\ n e. NN0 ) -> ( F e. ( ( C^n ` CC ) ` n ) <-> ( F e. ( CC ^pm CC ) /\ ( ( CC Dn F ) ` n ) e. ( dom F -cn-> CC ) ) ) )
15 5 11 14 mpbir2and 
 |-  ( ( F e. ( Poly ` S ) /\ n e. NN0 ) -> F e. ( ( C^n ` CC ) ` n ) )
16 15 ralrimiva 
 |-  ( F e. ( Poly ` S ) -> A. n e. NN0 F e. ( ( C^n ` CC ) ` n ) )
17 ssid 
 |-  CC C_ CC
18 fncpn 
 |-  ( CC C_ CC -> ( C^n ` CC ) Fn NN0 )
19 eleq2 
 |-  ( x = ( ( C^n ` CC ) ` n ) -> ( F e. x <-> F e. ( ( C^n ` CC ) ` n ) ) )
20 19 ralrn 
 |-  ( ( C^n ` CC ) Fn NN0 -> ( A. x e. ran ( C^n ` CC ) F e. x <-> A. n e. NN0 F e. ( ( C^n ` CC ) ` n ) ) )
21 17 18 20 mp2b 
 |-  ( A. x e. ran ( C^n ` CC ) F e. x <-> A. n e. NN0 F e. ( ( C^n ` CC ) ` n ) )
22 16 21 sylibr 
 |-  ( F e. ( Poly ` S ) -> A. x e. ran ( C^n ` CC ) F e. x )
23 elintg 
 |-  ( F e. ( Poly ` S ) -> ( F e. |^| ran ( C^n ` CC ) <-> A. x e. ran ( C^n ` CC ) F e. x ) )
24 22 23 mpbird 
 |-  ( F e. ( Poly ` S ) -> F e. |^| ran ( C^n ` CC ) )