Step | Hyp | Ref
| Expression |
1 | | oveq2 7369 |
. . . . 5
โข (๐ฃ = ๐ โ (โค โm ๐ฃ) = (โค โm
๐)) |
2 | 1 | oveq2d 7377 |
. . . 4
โข (๐ฃ = ๐ โ (โค โm (โค
โm ๐ฃ)) =
(โค โm (โค โm ๐))) |
3 | 2 | pweqd 4581 |
. . 3
โข (๐ฃ = ๐ โ ๐ซ (โค
โm (โค โm ๐ฃ)) = ๐ซ (โค โm
(โค โm ๐))) |
4 | 1 | xpeq1d 5666 |
. . . . . . . 8
โข (๐ฃ = ๐ โ ((โค โm ๐ฃ) ร {๐}) = ((โค โm ๐) ร {๐})) |
5 | 4 | eleq1d 2819 |
. . . . . . 7
โข (๐ฃ = ๐ โ (((โค โm ๐ฃ) ร {๐}) โ ๐ โ ((โค โm ๐) ร {๐}) โ ๐)) |
6 | 5 | ralbidv 3171 |
. . . . . 6
โข (๐ฃ = ๐ โ (โ๐ โ โค ((โค โm
๐ฃ) ร {๐}) โ ๐ โ โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐)) |
7 | | sneq 4600 |
. . . . . . . . 9
โข (๐ = ๐ โ {๐} = {๐}) |
8 | 7 | xpeq2d 5667 |
. . . . . . . 8
โข (๐ = ๐ โ ((โค โm ๐) ร {๐}) = ((โค โm ๐) ร {๐})) |
9 | 8 | eleq1d 2819 |
. . . . . . 7
โข (๐ = ๐ โ (((โค โm ๐) ร {๐}) โ ๐ โ ((โค โm ๐) ร {๐}) โ ๐)) |
10 | 9 | cbvralvw 3224 |
. . . . . 6
โข
(โ๐ โ
โค ((โค โm ๐) ร {๐}) โ ๐ โ โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐) |
11 | 6, 10 | bitrdi 287 |
. . . . 5
โข (๐ฃ = ๐ โ (โ๐ โ โค ((โค โm
๐ฃ) ร {๐}) โ ๐ โ โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐)) |
12 | 1 | mpteq1d 5204 |
. . . . . . . 8
โข (๐ฃ = ๐ โ (๐ โ (โค โm ๐ฃ) โฆ (๐โ๐)) = (๐ โ (โค โm ๐) โฆ (๐โ๐))) |
13 | 12 | eleq1d 2819 |
. . . . . . 7
โข (๐ฃ = ๐ โ ((๐ โ (โค โm ๐ฃ) โฆ (๐โ๐)) โ ๐ โ (๐ โ (โค โm ๐) โฆ (๐โ๐)) โ ๐)) |
14 | 13 | raleqbi1dv 3306 |
. . . . . 6
โข (๐ฃ = ๐ โ (โ๐ โ ๐ฃ (๐ โ (โค โm ๐ฃ) โฆ (๐โ๐)) โ ๐ โ โ๐ โ ๐ (๐ โ (โค โm ๐) โฆ (๐โ๐)) โ ๐)) |
15 | | fveq2 6846 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
16 | 15 | mpteq2dv 5211 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ โ (โค โm ๐) โฆ (๐โ๐)) = (๐ โ (โค โm ๐) โฆ (๐โ๐))) |
17 | 16 | eleq1d 2819 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐ โ (โค โm ๐) โฆ (๐โ๐)) โ ๐ โ (๐ โ (โค โm ๐) โฆ (๐โ๐)) โ ๐)) |
18 | | fveq1 6845 |
. . . . . . . . . 10
โข (๐ = ๐ฅ โ (๐โ๐) = (๐ฅโ๐)) |
19 | 18 | cbvmptv 5222 |
. . . . . . . . 9
โข (๐ โ (โค
โm ๐)
โฆ (๐โ๐)) = (๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) |
20 | 19 | eleq1i 2825 |
. . . . . . . 8
โข ((๐ โ (โค
โm ๐)
โฆ (๐โ๐)) โ ๐ โ (๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) โ ๐) |
21 | 17, 20 | bitrdi 287 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ โ (โค โm ๐) โฆ (๐โ๐)) โ ๐ โ (๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) โ ๐)) |
22 | 21 | cbvralvw 3224 |
. . . . . 6
โข
(โ๐ โ
๐ (๐ โ (โค โm ๐) โฆ (๐โ๐)) โ ๐ โ โ๐ โ ๐ (๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) โ ๐) |
23 | 14, 22 | bitrdi 287 |
. . . . 5
โข (๐ฃ = ๐ โ (โ๐ โ ๐ฃ (๐ โ (โค โm ๐ฃ) โฆ (๐โ๐)) โ ๐ โ โ๐ โ ๐ (๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) โ ๐)) |
24 | 11, 23 | anbi12d 632 |
. . . 4
โข (๐ฃ = ๐ โ ((โ๐ โ โค ((โค โm
๐ฃ) ร {๐}) โ ๐ โง โ๐ โ ๐ฃ (๐ โ (โค โm ๐ฃ) โฆ (๐โ๐)) โ ๐) โ (โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐ โง โ๐ โ ๐ (๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) โ ๐))) |
25 | 24 | anbi1d 631 |
. . 3
โข (๐ฃ = ๐ โ (((โ๐ โ โค ((โค โm
๐ฃ) ร {๐}) โ ๐ โง โ๐ โ ๐ฃ (๐ โ (โค โm ๐ฃ) โฆ (๐โ๐)) โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐)) โ ((โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐ โง โ๐ โ ๐ (๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐)))) |
26 | 3, 25 | rabeqbidv 3423 |
. 2
โข (๐ฃ = ๐ โ {๐ โ ๐ซ (โค โm
(โค โm ๐ฃ)) โฃ ((โ๐ โ โค ((โค โm
๐ฃ) ร {๐}) โ ๐ โง โ๐ โ ๐ฃ (๐ โ (โค โm ๐ฃ) โฆ (๐โ๐)) โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐))} = {๐ โ ๐ซ (โค โm
(โค โm ๐)) โฃ ((โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐ โง โ๐ โ ๐ (๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐))}) |
27 | | df-mzpcl 41093 |
. 2
โข mzPolyCld
= (๐ฃ โ V โฆ
{๐ โ ๐ซ
(โค โm (โค โm ๐ฃ)) โฃ ((โ๐ โ โค ((โค โm
๐ฃ) ร {๐}) โ ๐ โง โ๐ โ ๐ฃ (๐ โ (โค โm ๐ฃ) โฆ (๐โ๐)) โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐))}) |
28 | | ovex 7394 |
. . . 4
โข (โค
โm (โค โm ๐)) โ V |
29 | 28 | pwex 5339 |
. . 3
โข ๐ซ
(โค โm (โค โm ๐)) โ V |
30 | 29 | rabex 5293 |
. 2
โข {๐ โ ๐ซ (โค
โm (โค โm ๐)) โฃ ((โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐ โง โ๐ โ ๐ (๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐))} โ V |
31 | 26, 27, 30 | fvmpt 6952 |
1
โข (๐ โ V โ
(mzPolyCldโ๐) =
{๐ โ ๐ซ
(โค โm (โค โm ๐)) โฃ ((โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐ โง โ๐ โ ๐ (๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐))}) |