Step |
Hyp |
Ref |
Expression |
1 |
|
exp0 |
|- ( z e. CC -> ( z ^ 0 ) = 1 ) |
2 |
1
|
adantl |
|- ( ( ( S C_ CC /\ A e. S ) /\ z e. CC ) -> ( z ^ 0 ) = 1 ) |
3 |
2
|
oveq2d |
|- ( ( ( S C_ CC /\ A e. S ) /\ z e. CC ) -> ( A x. ( z ^ 0 ) ) = ( A x. 1 ) ) |
4 |
|
ssel2 |
|- ( ( S C_ CC /\ A e. S ) -> A e. CC ) |
5 |
4
|
adantr |
|- ( ( ( S C_ CC /\ A e. S ) /\ z e. CC ) -> A e. CC ) |
6 |
5
|
mulid1d |
|- ( ( ( S C_ CC /\ A e. S ) /\ z e. CC ) -> ( A x. 1 ) = A ) |
7 |
3 6
|
eqtrd |
|- ( ( ( S C_ CC /\ A e. S ) /\ z e. CC ) -> ( A x. ( z ^ 0 ) ) = A ) |
8 |
7
|
mpteq2dva |
|- ( ( S C_ CC /\ A e. S ) -> ( z e. CC |-> ( A x. ( z ^ 0 ) ) ) = ( z e. CC |-> A ) ) |
9 |
|
fconstmpt |
|- ( CC X. { A } ) = ( z e. CC |-> A ) |
10 |
8 9
|
eqtr4di |
|- ( ( S C_ CC /\ A e. S ) -> ( z e. CC |-> ( A x. ( z ^ 0 ) ) ) = ( CC X. { A } ) ) |
11 |
|
0nn0 |
|- 0 e. NN0 |
12 |
|
eqid |
|- ( z e. CC |-> ( A x. ( z ^ 0 ) ) ) = ( z e. CC |-> ( A x. ( z ^ 0 ) ) ) |
13 |
12
|
ply1term |
|- ( ( S C_ CC /\ A e. S /\ 0 e. NN0 ) -> ( z e. CC |-> ( A x. ( z ^ 0 ) ) ) e. ( Poly ` S ) ) |
14 |
11 13
|
mp3an3 |
|- ( ( S C_ CC /\ A e. S ) -> ( z e. CC |-> ( A x. ( z ^ 0 ) ) ) e. ( Poly ` S ) ) |
15 |
10 14
|
eqeltrrd |
|- ( ( S C_ CC /\ A e. S ) -> ( CC X. { A } ) e. ( Poly ` S ) ) |