Step |
Hyp |
Ref |
Expression |
1 |
|
plyssc |
โข ( Poly โ ๐ ) โ ( Poly โ โ ) |
2 |
1
|
sseli |
โข ( ๐น โ ( Poly โ ๐ ) โ ๐น โ ( Poly โ โ ) ) |
3 |
|
elply2 |
โข ( ๐น โ ( Poly โ โ ) โ ( โ โ โ โง โ ๐ โ โ0 โ ๐ โ ( ( โ โช { 0 } ) โm โ0 ) ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) ) |
4 |
3
|
simprbi |
โข ( ๐น โ ( Poly โ โ ) โ โ ๐ โ โ0 โ ๐ โ ( ( โ โช { 0 } ) โm โ0 ) ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) |
5 |
|
rexcom |
โข ( โ ๐ โ โ0 โ ๐ โ ( ( โ โช { 0 } ) โm โ0 ) ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โ โ ๐ โ ( ( โ โช { 0 } ) โm โ0 ) โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) |
6 |
4 5
|
sylib |
โข ( ๐น โ ( Poly โ โ ) โ โ ๐ โ ( ( โ โช { 0 } ) โm โ0 ) โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) |
7 |
2 6
|
syl |
โข ( ๐น โ ( Poly โ ๐ ) โ โ ๐ โ ( ( โ โช { 0 } ) โm โ0 ) โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) |
8 |
|
0cn |
โข 0 โ โ |
9 |
|
snssi |
โข ( 0 โ โ โ { 0 } โ โ ) |
10 |
8 9
|
ax-mp |
โข { 0 } โ โ |
11 |
|
ssequn2 |
โข ( { 0 } โ โ โ ( โ โช { 0 } ) = โ ) |
12 |
10 11
|
mpbi |
โข ( โ โช { 0 } ) = โ |
13 |
12
|
oveq1i |
โข ( ( โ โช { 0 } ) โm โ0 ) = ( โ โm โ0 ) |
14 |
13
|
rexeqi |
โข ( โ ๐ โ ( ( โ โช { 0 } ) โm โ0 ) โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โ โ ๐ โ ( โ โm โ0 ) โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) |
15 |
7 14
|
sylib |
โข ( ๐น โ ( Poly โ ๐ ) โ โ ๐ โ ( โ โm โ0 ) โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) |
16 |
|
reeanv |
โข ( โ ๐ โ โ0 โ ๐ โ โ0 ( ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โง ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) โ ( โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โง โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) ) |
17 |
|
simp1l |
โข ( ( ( ๐น โ ( Poly โ ๐ ) โง ( ๐ โ ( โ โm โ0 ) โง ๐ โ ( โ โm โ0 ) ) ) โง ( ๐ โ โ0 โง ๐ โ โ0 ) โง ( ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โง ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) ) โ ๐น โ ( Poly โ ๐ ) ) |
18 |
|
simp1rl |
โข ( ( ( ๐น โ ( Poly โ ๐ ) โง ( ๐ โ ( โ โm โ0 ) โง ๐ โ ( โ โm โ0 ) ) ) โง ( ๐ โ โ0 โง ๐ โ โ0 ) โง ( ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โง ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) ) โ ๐ โ ( โ โm โ0 ) ) |
19 |
|
simp1rr |
โข ( ( ( ๐น โ ( Poly โ ๐ ) โง ( ๐ โ ( โ โm โ0 ) โง ๐ โ ( โ โm โ0 ) ) ) โง ( ๐ โ โ0 โง ๐ โ โ0 ) โง ( ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โง ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) ) โ ๐ โ ( โ โm โ0 ) ) |
20 |
|
simp2l |
โข ( ( ( ๐น โ ( Poly โ ๐ ) โง ( ๐ โ ( โ โm โ0 ) โง ๐ โ ( โ โm โ0 ) ) ) โง ( ๐ โ โ0 โง ๐ โ โ0 ) โง ( ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โง ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) ) โ ๐ โ โ0 ) |
21 |
|
simp2r |
โข ( ( ( ๐น โ ( Poly โ ๐ ) โง ( ๐ โ ( โ โm โ0 ) โง ๐ โ ( โ โm โ0 ) ) ) โง ( ๐ โ โ0 โง ๐ โ โ0 ) โง ( ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โง ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) ) โ ๐ โ โ0 ) |
22 |
|
simp3ll |
โข ( ( ( ๐น โ ( Poly โ ๐ ) โง ( ๐ โ ( โ โm โ0 ) โง ๐ โ ( โ โm โ0 ) ) ) โง ( ๐ โ โ0 โง ๐ โ โ0 ) โง ( ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โง ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) ) โ ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } ) |
23 |
|
simp3rl |
โข ( ( ( ๐น โ ( Poly โ ๐ ) โง ( ๐ โ ( โ โm โ0 ) โง ๐ โ ( โ โm โ0 ) ) ) โง ( ๐ โ โ0 โง ๐ โ โ0 ) โง ( ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โง ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) ) โ ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } ) |
24 |
|
simp3lr |
โข ( ( ( ๐น โ ( Poly โ ๐ ) โง ( ๐ โ ( โ โm โ0 ) โง ๐ โ ( โ โm โ0 ) ) ) โง ( ๐ โ โ0 โง ๐ โ โ0 ) โง ( ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โง ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) ) โ ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) |
25 |
|
oveq1 |
โข ( ๐ง = ๐ค โ ( ๐ง โ ๐ ) = ( ๐ค โ ๐ ) ) |
26 |
25
|
oveq2d |
โข ( ๐ง = ๐ค โ ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) = ( ( ๐ โ ๐ ) ยท ( ๐ค โ ๐ ) ) ) |
27 |
26
|
sumeq2sdv |
โข ( ๐ง = ๐ค โ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) = ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ค โ ๐ ) ) ) |
28 |
|
fveq2 |
โข ( ๐ = ๐ โ ( ๐ โ ๐ ) = ( ๐ โ ๐ ) ) |
29 |
|
oveq2 |
โข ( ๐ = ๐ โ ( ๐ค โ ๐ ) = ( ๐ค โ ๐ ) ) |
30 |
28 29
|
oveq12d |
โข ( ๐ = ๐ โ ( ( ๐ โ ๐ ) ยท ( ๐ค โ ๐ ) ) = ( ( ๐ โ ๐ ) ยท ( ๐ค โ ๐ ) ) ) |
31 |
30
|
cbvsumv |
โข ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ค โ ๐ ) ) = ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ค โ ๐ ) ) |
32 |
27 31
|
eqtrdi |
โข ( ๐ง = ๐ค โ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) = ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ค โ ๐ ) ) ) |
33 |
32
|
cbvmptv |
โข ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) = ( ๐ค โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ค โ ๐ ) ) ) |
34 |
24 33
|
eqtrdi |
โข ( ( ( ๐น โ ( Poly โ ๐ ) โง ( ๐ โ ( โ โm โ0 ) โง ๐ โ ( โ โm โ0 ) ) ) โง ( ๐ โ โ0 โง ๐ โ โ0 ) โง ( ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โง ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) ) โ ๐น = ( ๐ค โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ค โ ๐ ) ) ) ) |
35 |
|
simp3rr |
โข ( ( ( ๐น โ ( Poly โ ๐ ) โง ( ๐ โ ( โ โm โ0 ) โง ๐ โ ( โ โm โ0 ) ) ) โง ( ๐ โ โ0 โง ๐ โ โ0 ) โง ( ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โง ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) ) โ ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) |
36 |
25
|
oveq2d |
โข ( ๐ง = ๐ค โ ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) = ( ( ๐ โ ๐ ) ยท ( ๐ค โ ๐ ) ) ) |
37 |
36
|
sumeq2sdv |
โข ( ๐ง = ๐ค โ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) = ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ค โ ๐ ) ) ) |
38 |
|
fveq2 |
โข ( ๐ = ๐ โ ( ๐ โ ๐ ) = ( ๐ โ ๐ ) ) |
39 |
38 29
|
oveq12d |
โข ( ๐ = ๐ โ ( ( ๐ โ ๐ ) ยท ( ๐ค โ ๐ ) ) = ( ( ๐ โ ๐ ) ยท ( ๐ค โ ๐ ) ) ) |
40 |
39
|
cbvsumv |
โข ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ค โ ๐ ) ) = ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ค โ ๐ ) ) |
41 |
37 40
|
eqtrdi |
โข ( ๐ง = ๐ค โ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) = ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ค โ ๐ ) ) ) |
42 |
41
|
cbvmptv |
โข ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) = ( ๐ค โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ค โ ๐ ) ) ) |
43 |
35 42
|
eqtrdi |
โข ( ( ( ๐น โ ( Poly โ ๐ ) โง ( ๐ โ ( โ โm โ0 ) โง ๐ โ ( โ โm โ0 ) ) ) โง ( ๐ โ โ0 โง ๐ โ โ0 ) โง ( ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โง ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) ) โ ๐น = ( ๐ค โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ค โ ๐ ) ) ) ) |
44 |
17 18 19 20 21 22 23 34 43
|
coeeulem |
โข ( ( ( ๐น โ ( Poly โ ๐ ) โง ( ๐ โ ( โ โm โ0 ) โง ๐ โ ( โ โm โ0 ) ) ) โง ( ๐ โ โ0 โง ๐ โ โ0 ) โง ( ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โง ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) ) โ ๐ = ๐ ) |
45 |
44
|
3expia |
โข ( ( ( ๐น โ ( Poly โ ๐ ) โง ( ๐ โ ( โ โm โ0 ) โง ๐ โ ( โ โm โ0 ) ) ) โง ( ๐ โ โ0 โง ๐ โ โ0 ) ) โ ( ( ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โง ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) โ ๐ = ๐ ) ) |
46 |
45
|
rexlimdvva |
โข ( ( ๐น โ ( Poly โ ๐ ) โง ( ๐ โ ( โ โm โ0 ) โง ๐ โ ( โ โm โ0 ) ) ) โ ( โ ๐ โ โ0 โ ๐ โ โ0 ( ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โง ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) โ ๐ = ๐ ) ) |
47 |
16 46
|
syl5bir |
โข ( ( ๐น โ ( Poly โ ๐ ) โง ( ๐ โ ( โ โm โ0 ) โง ๐ โ ( โ โm โ0 ) ) ) โ ( ( โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โง โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) โ ๐ = ๐ ) ) |
48 |
47
|
ralrimivva |
โข ( ๐น โ ( Poly โ ๐ ) โ โ ๐ โ ( โ โm โ0 ) โ ๐ โ ( โ โm โ0 ) ( ( โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โง โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) โ ๐ = ๐ ) ) |
49 |
|
imaeq1 |
โข ( ๐ = ๐ โ ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) ) |
50 |
49
|
eqeq1d |
โข ( ๐ = ๐ โ ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โ ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } ) ) |
51 |
|
fveq1 |
โข ( ๐ = ๐ โ ( ๐ โ ๐ ) = ( ๐ โ ๐ ) ) |
52 |
51
|
oveq1d |
โข ( ๐ = ๐ โ ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) = ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) |
53 |
52
|
sumeq2sdv |
โข ( ๐ = ๐ โ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) = ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) |
54 |
53
|
mpteq2dv |
โข ( ๐ = ๐ โ ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) |
55 |
54
|
eqeq2d |
โข ( ๐ = ๐ โ ( ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) โ ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) |
56 |
50 55
|
anbi12d |
โข ( ๐ = ๐ โ ( ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โ ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) ) |
57 |
56
|
rexbidv |
โข ( ๐ = ๐ โ ( โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โ โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) ) |
58 |
|
fvoveq1 |
โข ( ๐ = ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) = ( โคโฅ โ ( ๐ + 1 ) ) ) |
59 |
58
|
imaeq2d |
โข ( ๐ = ๐ โ ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) ) |
60 |
59
|
eqeq1d |
โข ( ๐ = ๐ โ ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โ ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } ) ) |
61 |
|
oveq2 |
โข ( ๐ = ๐ โ ( 0 ... ๐ ) = ( 0 ... ๐ ) ) |
62 |
61
|
sumeq1d |
โข ( ๐ = ๐ โ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) = ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) |
63 |
62
|
mpteq2dv |
โข ( ๐ = ๐ โ ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) |
64 |
63
|
eqeq2d |
โข ( ๐ = ๐ โ ( ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) โ ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) |
65 |
60 64
|
anbi12d |
โข ( ๐ = ๐ โ ( ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โ ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) ) |
66 |
65
|
cbvrexvw |
โข ( โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โ โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) |
67 |
57 66
|
bitrdi |
โข ( ๐ = ๐ โ ( โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โ โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) ) |
68 |
67
|
reu4 |
โข ( โ! ๐ โ ( โ โm โ0 ) โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โ ( โ ๐ โ ( โ โm โ0 ) โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โง โ ๐ โ ( โ โm โ0 ) โ ๐ โ ( โ โm โ0 ) ( ( โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) โง โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) โ ๐ = ๐ ) ) ) |
69 |
15 48 68
|
sylanbrc |
โข ( ๐น โ ( Poly โ ๐ ) โ โ! ๐ โ ( โ โm โ0 ) โ ๐ โ โ0 ( ( ๐ โ ( โคโฅ โ ( ๐ + 1 ) ) ) = { 0 } โง ๐น = ( ๐ง โ โ โฆ ฮฃ ๐ โ ( 0 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( ๐ง โ ๐ ) ) ) ) ) |