Step |
Hyp |
Ref |
Expression |
1 |
|
coeeq.1 |
โข ( ๐ โ ๐น โ ( Poly โ ๐ ) ) |
2 |
|
coeeq.2 |
โข ( ๐ โ ๐ โ โ0 ) |
3 |
|
coeeq.3 |
โข ( ๐ โ ๐ด : โ0 โถ โ ) |
4 |
|
coeeq.4 |
โข ( ๐ โ ( ๐ด โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } ) |
5 |
|
coeeq.5 |
โข ( ๐ โ ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ด โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) |
6 |
|
coeval |
โข ( ๐น โ ( Poly โ ๐ ) โ ( coeff โ ๐น ) = ( โฉ ๐ โ ( โ โm โ0 ) โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) ) |
7 |
1 6
|
syl |
โข ( ๐ โ ( coeff โ ๐น ) = ( โฉ ๐ โ ( โ โm โ0 ) โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) ) |
8 |
|
fvoveq1 |
โข ( ๐ = ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) = ( โคโฅ โ ( ๐ + 1 ) ) ) |
9 |
8
|
imaeq2d |
โข ( ๐ = ๐ โ ( ๐ด โ ( โคโฅ โ ( ๐ + 1 ) ) ) = ( ๐ด โ ( โคโฅ โ ( ๐ + 1 ) ) ) ) |
10 |
9
|
eqeq1d |
โข ( ๐ = ๐ โ ( ( ๐ด โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โ ( ๐ด โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } ) ) |
11 |
|
oveq2 |
โข ( ๐ = ๐ โ ( 0 ... ๐ ) = ( 0 ... ๐ ) ) |
12 |
11
|
sumeq1d |
โข ( ๐ = ๐ โ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ด โ ๐ ) ยท ( ๐ง โ ๐ ) ) = ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ด โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) |
13 |
12
|
mpteq2dv |
โข ( ๐ = ๐ โ ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ด โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ด โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) |
14 |
13
|
eqeq2d |
โข ( ๐ = ๐ โ ( ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ด โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) โ ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ด โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) |
15 |
10 14
|
anbi12d |
โข ( ๐ = ๐ โ ( ( ( ๐ด โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ด โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โ ( ( ๐ด โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ด โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) ) |
16 |
15
|
rspcev |
โข ( ( ๐ โ โ0 โง ( ( ๐ด โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ด โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) โ โ ๐ โ โ0 ( ( ๐ด โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ด โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) |
17 |
2 4 5 16
|
syl12anc |
โข ( ๐ โ โ ๐ โ โ0 ( ( ๐ด โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ด โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) |
18 |
|
cnex |
โข โ โ V |
19 |
|
nn0ex |
โข โ0 โ V |
20 |
18 19
|
elmap |
โข ( ๐ด โ ( โ โm โ0 ) โ ๐ด : โ0 โถ โ ) |
21 |
3 20
|
sylibr |
โข ( ๐ โ ๐ด โ ( โ โm โ0 ) ) |
22 |
|
coeeu |
โข ( ๐น โ ( Poly โ ๐ ) โ โ! ๐ โ ( โ โm โ0 ) โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) |
23 |
1 22
|
syl |
โข ( ๐ โ โ! ๐ โ ( โ โm โ0 ) โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) |
24 |
|
imaeq1 |
โข ( ๐ = ๐ด โ ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = ( ๐ด โ ( โคโฅ โ ( ๐ + 1 ) ) ) ) |
25 |
24
|
eqeq1d |
โข ( ๐ = ๐ด โ ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โ ( ๐ด โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } ) ) |
26 |
|
fveq1 |
โข ( ๐ = ๐ด โ ( ๐ โ ๐ ) = ( ๐ด โ ๐ ) ) |
27 |
26
|
oveq1d |
โข ( ๐ = ๐ด โ ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) = ( ( ๐ด โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) |
28 |
27
|
sumeq2sdv |
โข ( ๐ = ๐ด โ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) = ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ด โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) |
29 |
28
|
mpteq2dv |
โข ( ๐ = ๐ด โ ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ด โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) |
30 |
29
|
eqeq2d |
โข ( ๐ = ๐ด โ ( ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) โ ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ด โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) |
31 |
25 30
|
anbi12d |
โข ( ๐ = ๐ด โ ( ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โ ( ( ๐ด โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ด โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) ) |
32 |
31
|
rexbidv |
โข ( ๐ = ๐ด โ ( โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โ โ ๐ โ โ0 ( ( ๐ด โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ด โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) ) |
33 |
32
|
riota2 |
โข ( ( ๐ด โ ( โ โm โ0 ) โง โ! ๐ โ ( โ โm โ0 ) โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) โ ( โ ๐ โ โ0 ( ( ๐ด โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ด โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โ ( โฉ ๐ โ ( โ โm โ0 ) โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) = ๐ด ) ) |
34 |
21 23 33
|
syl2anc |
โข ( ๐ โ ( โ ๐ โ โ0 ( ( ๐ด โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ด โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โ ( โฉ ๐ โ ( โ โm โ0 ) โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) = ๐ด ) ) |
35 |
17 34
|
mpbid |
โข ( ๐ โ ( โฉ ๐ โ ( โ โm โ0 ) โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) = ๐ด ) |
36 |
7 35
|
eqtrd |
โข ( ๐ โ ( coeff โ ๐น ) = ๐ด ) |