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