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 ) )