Step | Hyp | Ref
| Expression |
1 | | nffvmpt1 6903 |
. . . . . . 7
โข
โฒ๐((๐ โ โ0 โฆ if(๐ โ (0...๐), ๐ด, 0))โ๐) |
2 | | nfcv 2904 |
. . . . . . 7
โข
โฒ๐
ยท |
3 | | nfcv 2904 |
. . . . . . 7
โข
โฒ๐(๐งโ๐) |
4 | 1, 2, 3 | nfov 7439 |
. . . . . 6
โข
โฒ๐(((๐ โ โ0 โฆ if(๐ โ (0...๐), ๐ด, 0))โ๐) ยท (๐งโ๐)) |
5 | | nfcv 2904 |
. . . . . 6
โข
โฒ๐(((๐ โ โ0 โฆ if(๐ โ (0...๐), ๐ด, 0))โ๐) ยท (๐งโ๐)) |
6 | | fveq2 6892 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ โ โ0 โฆ if(๐ โ (0...๐), ๐ด, 0))โ๐) = ((๐ โ โ0 โฆ if(๐ โ (0...๐), ๐ด, 0))โ๐)) |
7 | | oveq2 7417 |
. . . . . . 7
โข (๐ = ๐ โ (๐งโ๐) = (๐งโ๐)) |
8 | 6, 7 | oveq12d 7427 |
. . . . . 6
โข (๐ = ๐ โ (((๐ โ โ0 โฆ if(๐ โ (0...๐), ๐ด, 0))โ๐) ยท (๐งโ๐)) = (((๐ โ โ0 โฆ if(๐ โ (0...๐), ๐ด, 0))โ๐) ยท (๐งโ๐))) |
9 | 4, 5, 8 | cbvsumi 15643 |
. . . . 5
โข
ฮฃ๐ โ
(0...๐)(((๐ โ โ0
โฆ if(๐ โ
(0...๐), ๐ด, 0))โ๐) ยท (๐งโ๐)) = ฮฃ๐ โ (0...๐)(((๐ โ โ0 โฆ if(๐ โ (0...๐), ๐ด, 0))โ๐) ยท (๐งโ๐)) |
10 | | elfznn0 13594 |
. . . . . . . . 9
โข (๐ โ (0...๐) โ ๐ โ โ0) |
11 | | iftrue 4535 |
. . . . . . . . . . 11
โข (๐ โ (0...๐) โ if(๐ โ (0...๐), ๐ด, 0) = ๐ด) |
12 | 11 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (0...๐)) โ if(๐ โ (0...๐), ๐ด, 0) = ๐ด) |
13 | | elplyd.3 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (0...๐)) โ ๐ด โ ๐) |
14 | 12, 13 | eqeltrd 2834 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...๐)) โ if(๐ โ (0...๐), ๐ด, 0) โ ๐) |
15 | | eqid 2733 |
. . . . . . . . . 10
โข (๐ โ โ0
โฆ if(๐ โ
(0...๐), ๐ด, 0)) = (๐ โ โ0 โฆ if(๐ โ (0...๐), ๐ด, 0)) |
16 | 15 | fvmpt2 7010 |
. . . . . . . . 9
โข ((๐ โ โ0
โง if(๐ โ
(0...๐), ๐ด, 0) โ ๐) โ ((๐ โ โ0 โฆ if(๐ โ (0...๐), ๐ด, 0))โ๐) = if(๐ โ (0...๐), ๐ด, 0)) |
17 | 10, 14, 16 | syl2an2 685 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0...๐)) โ ((๐ โ โ0 โฆ if(๐ โ (0...๐), ๐ด, 0))โ๐) = if(๐ โ (0...๐), ๐ด, 0)) |
18 | 17, 12 | eqtrd 2773 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...๐)) โ ((๐ โ โ0 โฆ if(๐ โ (0...๐), ๐ด, 0))โ๐) = ๐ด) |
19 | 18 | oveq1d 7424 |
. . . . . 6
โข ((๐ โง ๐ โ (0...๐)) โ (((๐ โ โ0 โฆ if(๐ โ (0...๐), ๐ด, 0))โ๐) ยท (๐งโ๐)) = (๐ด ยท (๐งโ๐))) |
20 | 19 | sumeq2dv 15649 |
. . . . 5
โข (๐ โ ฮฃ๐ โ (0...๐)(((๐ โ โ0 โฆ if(๐ โ (0...๐), ๐ด, 0))โ๐) ยท (๐งโ๐)) = ฮฃ๐ โ (0...๐)(๐ด ยท (๐งโ๐))) |
21 | 9, 20 | eqtrid 2785 |
. . . 4
โข (๐ โ ฮฃ๐ โ (0...๐)(((๐ โ โ0 โฆ if(๐ โ (0...๐), ๐ด, 0))โ๐) ยท (๐งโ๐)) = ฮฃ๐ โ (0...๐)(๐ด ยท (๐งโ๐))) |
22 | 21 | mpteq2dv 5251 |
. . 3
โข (๐ โ (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)(((๐ โ โ0 โฆ if(๐ โ (0...๐), ๐ด, 0))โ๐) ยท (๐งโ๐))) = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)(๐ด ยท (๐งโ๐)))) |
23 | | elplyd.1 |
. . . . 5
โข (๐ โ ๐ โ โ) |
24 | | 0cnd 11207 |
. . . . . 6
โข (๐ โ 0 โ
โ) |
25 | 24 | snssd 4813 |
. . . . 5
โข (๐ โ {0} โ
โ) |
26 | 23, 25 | unssd 4187 |
. . . 4
โข (๐ โ (๐ โช {0}) โ
โ) |
27 | | elplyd.2 |
. . . 4
โข (๐ โ ๐ โ
โ0) |
28 | | elun1 4177 |
. . . . . . . 8
โข (๐ด โ ๐ โ ๐ด โ (๐ โช {0})) |
29 | 13, 28 | syl 17 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...๐)) โ ๐ด โ (๐ โช {0})) |
30 | 29 | adantlr 714 |
. . . . . 6
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ ๐ด โ (๐ โช {0})) |
31 | | ssun2 4174 |
. . . . . . . 8
โข {0}
โ (๐ โช
{0}) |
32 | | c0ex 11208 |
. . . . . . . . 9
โข 0 โ
V |
33 | 32 | snss 4790 |
. . . . . . . 8
โข (0 โ
(๐ โช {0}) โ {0}
โ (๐ โช
{0})) |
34 | 31, 33 | mpbir 230 |
. . . . . . 7
โข 0 โ
(๐ โช
{0}) |
35 | 34 | a1i 11 |
. . . . . 6
โข (((๐ โง ๐ โ โ0) โง ยฌ
๐ โ (0...๐)) โ 0 โ (๐ โช {0})) |
36 | 30, 35 | ifclda 4564 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ if(๐ โ (0...๐), ๐ด, 0) โ (๐ โช {0})) |
37 | 36 | fmpttd 7115 |
. . . 4
โข (๐ โ (๐ โ โ0 โฆ if(๐ โ (0...๐), ๐ด, 0)):โ0โถ(๐ โช {0})) |
38 | | elplyr 25715 |
. . . 4
โข (((๐ โช {0}) โ โ
โง ๐ โ
โ0 โง (๐ โ โ0 โฆ if(๐ โ (0...๐), ๐ด, 0)):โ0โถ(๐ โช {0})) โ (๐ง โ โ โฆ
ฮฃ๐ โ (0...๐)(((๐ โ โ0 โฆ if(๐ โ (0...๐), ๐ด, 0))โ๐) ยท (๐งโ๐))) โ (Polyโ(๐ โช {0}))) |
39 | 26, 27, 37, 38 | syl3anc 1372 |
. . 3
โข (๐ โ (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)(((๐ โ โ0 โฆ if(๐ โ (0...๐), ๐ด, 0))โ๐) ยท (๐งโ๐))) โ (Polyโ(๐ โช {0}))) |
40 | 22, 39 | eqeltrrd 2835 |
. 2
โข (๐ โ (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)(๐ด ยท (๐งโ๐))) โ (Polyโ(๐ โช {0}))) |
41 | | plyun0 25711 |
. 2
โข
(Polyโ(๐ โช
{0})) = (Polyโ๐) |
42 | 40, 41 | eleqtrdi 2844 |
1
โข (๐ โ (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)(๐ด ยท (๐งโ๐))) โ (Polyโ๐)) |