Step | Hyp | Ref
| Expression |
1 | | cply 25689 |
. 2
class
Poly |
2 | | vx |
. . 3
setvar ๐ฅ |
3 | | cc 11104 |
. . . 4
class
โ |
4 | 3 | cpw 4601 |
. . 3
class ๐ซ
โ |
5 | | vf |
. . . . . . . 8
setvar ๐ |
6 | 5 | cv 1540 |
. . . . . . 7
class ๐ |
7 | | vz |
. . . . . . . 8
setvar ๐ง |
8 | | cc0 11106 |
. . . . . . . . . 10
class
0 |
9 | | vn |
. . . . . . . . . . 11
setvar ๐ |
10 | 9 | cv 1540 |
. . . . . . . . . 10
class ๐ |
11 | | cfz 13480 |
. . . . . . . . . 10
class
... |
12 | 8, 10, 11 | co 7405 |
. . . . . . . . 9
class
(0...๐) |
13 | | vk |
. . . . . . . . . . . 12
setvar ๐ |
14 | 13 | cv 1540 |
. . . . . . . . . . 11
class ๐ |
15 | | va |
. . . . . . . . . . . 12
setvar ๐ |
16 | 15 | cv 1540 |
. . . . . . . . . . 11
class ๐ |
17 | 14, 16 | cfv 6540 |
. . . . . . . . . 10
class (๐โ๐) |
18 | 7 | cv 1540 |
. . . . . . . . . . 11
class ๐ง |
19 | | cexp 14023 |
. . . . . . . . . . 11
class
โ |
20 | 18, 14, 19 | co 7405 |
. . . . . . . . . 10
class (๐งโ๐) |
21 | | cmul 11111 |
. . . . . . . . . 10
class
ยท |
22 | 17, 20, 21 | co 7405 |
. . . . . . . . 9
class ((๐โ๐) ยท (๐งโ๐)) |
23 | 12, 22, 13 | csu 15628 |
. . . . . . . 8
class
ฮฃ๐ โ
(0...๐)((๐โ๐) ยท (๐งโ๐)) |
24 | 7, 3, 23 | cmpt 5230 |
. . . . . . 7
class (๐ง โ โ โฆ
ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))) |
25 | 6, 24 | wceq 1541 |
. . . . . 6
wff ๐ = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))) |
26 | 2 | cv 1540 |
. . . . . . . 8
class ๐ฅ |
27 | 8 | csn 4627 |
. . . . . . . 8
class
{0} |
28 | 26, 27 | cun 3945 |
. . . . . . 7
class (๐ฅ โช {0}) |
29 | | cn0 12468 |
. . . . . . 7
class
โ0 |
30 | | cmap 8816 |
. . . . . . 7
class
โm |
31 | 28, 29, 30 | co 7405 |
. . . . . 6
class ((๐ฅ โช {0}) โm
โ0) |
32 | 25, 15, 31 | wrex 3070 |
. . . . 5
wff
โ๐ โ
((๐ฅ โช {0})
โm โ0)๐ = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))) |
33 | 32, 9, 29 | wrex 3070 |
. . . 4
wff
โ๐ โ
โ0 โ๐ โ ((๐ฅ โช {0}) โm
โ0)๐ =
(๐ง โ โ โฆ
ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))) |
34 | 33, 5 | cab 2709 |
. . 3
class {๐ โฃ โ๐ โ โ0
โ๐ โ ((๐ฅ โช {0}) โm
โ0)๐ =
(๐ง โ โ โฆ
ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))} |
35 | 2, 4, 34 | cmpt 5230 |
. 2
class (๐ฅ โ ๐ซ โ
โฆ {๐ โฃ
โ๐ โ
โ0 โ๐ โ ((๐ฅ โช {0}) โm
โ0)๐ =
(๐ง โ โ โฆ
ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))}) |
36 | 1, 35 | wceq 1541 |
1
wff Poly =
(๐ฅ โ ๐ซ โ
โฆ {๐ โฃ
โ๐ โ
โ0 โ๐ โ ((๐ฅ โช {0}) โm
โ0)๐ =
(๐ง โ โ โฆ
ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))}) |