Step | Hyp | Ref
| Expression |
1 | | ply1term.1 |
. 2
โข ๐น = (๐ง โ โ โฆ (๐ด ยท (๐งโ๐))) |
2 | | simplr 768 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โ ๐ โ
โ0) |
3 | | nn0uz 12810 |
. . . . . . 7
โข
โ0 = (โคโฅโ0) |
4 | 2, 3 | eleqtrdi 2844 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โ ๐ โ
(โคโฅโ0)) |
5 | | fzss1 13486 |
. . . . . 6
โข (๐ โ
(โคโฅโ0) โ (๐...๐) โ (0...๐)) |
6 | 4, 5 | syl 17 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โ (๐...๐) โ (0...๐)) |
7 | | elfz1eq 13458 |
. . . . . . . . 9
โข (๐ โ (๐...๐) โ ๐ = ๐) |
8 | 7 | adantl 483 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โง ๐ โ (๐...๐)) โ ๐ = ๐) |
9 | | iftrue 4493 |
. . . . . . . 8
โข (๐ = ๐ โ if(๐ = ๐, ๐ด, 0) = ๐ด) |
10 | 8, 9 | syl 17 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โง ๐ โ (๐...๐)) โ if(๐ = ๐, ๐ด, 0) = ๐ด) |
11 | | simpll 766 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โ ๐ด โ
โ) |
12 | 11 | adantr 482 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โง ๐ โ (๐...๐)) โ ๐ด โ โ) |
13 | 10, 12 | eqeltrd 2834 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โง ๐ โ (๐...๐)) โ if(๐ = ๐, ๐ด, 0) โ โ) |
14 | | simplr 768 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โง ๐ โ (๐...๐)) โ ๐ง โ โ) |
15 | 2 | adantr 482 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โง ๐ โ (๐...๐)) โ ๐ โ
โ0) |
16 | 8, 15 | eqeltrd 2834 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โง ๐ โ (๐...๐)) โ ๐ โ โ0) |
17 | 14, 16 | expcld 14057 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โง ๐ โ (๐...๐)) โ (๐งโ๐) โ โ) |
18 | 13, 17 | mulcld 11180 |
. . . . 5
โข ((((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โง ๐ โ (๐...๐)) โ (if(๐ = ๐, ๐ด, 0) ยท (๐งโ๐)) โ โ) |
19 | | eldifn 4088 |
. . . . . . . . . 10
โข (๐ โ ((0...๐) โ (๐...๐)) โ ยฌ ๐ โ (๐...๐)) |
20 | 19 | adantl 483 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โง ๐ โ ((0...๐) โ (๐...๐))) โ ยฌ ๐ โ (๐...๐)) |
21 | 2 | adantr 482 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โง ๐ โ ((0...๐) โ (๐...๐))) โ ๐ โ
โ0) |
22 | 21 | nn0zd 12530 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โง ๐ โ ((0...๐) โ (๐...๐))) โ ๐ โ โค) |
23 | | fzsn 13489 |
. . . . . . . . . . . 12
โข (๐ โ โค โ (๐...๐) = {๐}) |
24 | 23 | eleq2d 2820 |
. . . . . . . . . . 11
โข (๐ โ โค โ (๐ โ (๐...๐) โ ๐ โ {๐})) |
25 | | elsn2g 4625 |
. . . . . . . . . . 11
โข (๐ โ โค โ (๐ โ {๐} โ ๐ = ๐)) |
26 | 24, 25 | bitrd 279 |
. . . . . . . . . 10
โข (๐ โ โค โ (๐ โ (๐...๐) โ ๐ = ๐)) |
27 | 22, 26 | syl 17 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โง ๐ โ ((0...๐) โ (๐...๐))) โ (๐ โ (๐...๐) โ ๐ = ๐)) |
28 | 20, 27 | mtbid 324 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โง ๐ โ ((0...๐) โ (๐...๐))) โ ยฌ ๐ = ๐) |
29 | 28 | iffalsed 4498 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โง ๐ โ ((0...๐) โ (๐...๐))) โ if(๐ = ๐, ๐ด, 0) = 0) |
30 | 29 | oveq1d 7373 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โง ๐ โ ((0...๐) โ (๐...๐))) โ (if(๐ = ๐, ๐ด, 0) ยท (๐งโ๐)) = (0 ยท (๐งโ๐))) |
31 | | simpr 486 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โ ๐ง โ
โ) |
32 | | eldifi 4087 |
. . . . . . . . 9
โข (๐ โ ((0...๐) โ (๐...๐)) โ ๐ โ (0...๐)) |
33 | | elfznn0 13540 |
. . . . . . . . 9
โข (๐ โ (0...๐) โ ๐ โ โ0) |
34 | 32, 33 | syl 17 |
. . . . . . . 8
โข (๐ โ ((0...๐) โ (๐...๐)) โ ๐ โ โ0) |
35 | | expcl 13991 |
. . . . . . . 8
โข ((๐ง โ โ โง ๐ โ โ0)
โ (๐งโ๐) โ
โ) |
36 | 31, 34, 35 | syl2an 597 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โง ๐ โ ((0...๐) โ (๐...๐))) โ (๐งโ๐) โ โ) |
37 | 36 | mul02d 11358 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โง ๐ โ ((0...๐) โ (๐...๐))) โ (0 ยท (๐งโ๐)) = 0) |
38 | 30, 37 | eqtrd 2773 |
. . . . 5
โข ((((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โง ๐ โ ((0...๐) โ (๐...๐))) โ (if(๐ = ๐, ๐ด, 0) ยท (๐งโ๐)) = 0) |
39 | | fzfid 13884 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โ (0...๐) โ
Fin) |
40 | 6, 18, 38, 39 | fsumss 15615 |
. . . 4
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โ ฮฃ๐ โ
(๐...๐)(if(๐ = ๐, ๐ด, 0) ยท (๐งโ๐)) = ฮฃ๐ โ (0...๐)(if(๐ = ๐, ๐ด, 0) ยท (๐งโ๐))) |
41 | 2 | nn0zd 12530 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โ ๐ โ
โค) |
42 | 31, 2 | expcld 14057 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โ (๐งโ๐) โ
โ) |
43 | 11, 42 | mulcld 11180 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โ (๐ด ยท (๐งโ๐)) โ โ) |
44 | | oveq2 7366 |
. . . . . . 7
โข (๐ = ๐ โ (๐งโ๐) = (๐งโ๐)) |
45 | 9, 44 | oveq12d 7376 |
. . . . . 6
โข (๐ = ๐ โ (if(๐ = ๐, ๐ด, 0) ยท (๐งโ๐)) = (๐ด ยท (๐งโ๐))) |
46 | 45 | fsum1 15637 |
. . . . 5
โข ((๐ โ โค โง (๐ด ยท (๐งโ๐)) โ โ) โ ฮฃ๐ โ (๐...๐)(if(๐ = ๐, ๐ด, 0) ยท (๐งโ๐)) = (๐ด ยท (๐งโ๐))) |
47 | 41, 43, 46 | syl2anc 585 |
. . . 4
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โ ฮฃ๐ โ
(๐...๐)(if(๐ = ๐, ๐ด, 0) ยท (๐งโ๐)) = (๐ด ยท (๐งโ๐))) |
48 | 40, 47 | eqtr3d 2775 |
. . 3
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ง โ โ)
โ ฮฃ๐ โ
(0...๐)(if(๐ = ๐, ๐ด, 0) ยท (๐งโ๐)) = (๐ด ยท (๐งโ๐))) |
49 | 48 | mpteq2dva 5206 |
. 2
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ง โ โ
โฆ ฮฃ๐ โ
(0...๐)(if(๐ = ๐, ๐ด, 0) ยท (๐งโ๐))) = (๐ง โ โ โฆ (๐ด ยท (๐งโ๐)))) |
50 | 1, 49 | eqtr4id 2792 |
1
โข ((๐ด โ โ โง ๐ โ โ0)
โ ๐น = (๐ง โ โ โฆ
ฮฃ๐ โ (0...๐)(if(๐ = ๐, ๐ด, 0) ยท (๐งโ๐)))) |