Step | Hyp | Ref
| Expression |
1 | | mzpclval 41095 |
. . 3
โข (๐ โ V โ
(mzPolyCldโ๐) =
{๐ โ ๐ซ
(โค โm (โค โm ๐)) โฃ ((โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐ โง โ๐ โ ๐ (๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐))}) |
2 | 1 | eleq2d 2820 |
. 2
โข (๐ โ V โ (๐ โ (mzPolyCldโ๐) โ ๐ โ {๐ โ ๐ซ (โค โm
(โค โm ๐)) โฃ ((โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐ โง โ๐ โ ๐ (๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐))})) |
3 | | eleq2 2823 |
. . . . . . 7
โข (๐ = ๐ โ (((โค โm ๐) ร {๐}) โ ๐ โ ((โค โm ๐) ร {๐}) โ ๐)) |
4 | 3 | ralbidv 3171 |
. . . . . 6
โข (๐ = ๐ โ (โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐ โ โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐)) |
5 | | eleq2 2823 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) โ ๐ โ (๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) โ ๐)) |
6 | 5 | ralbidv 3171 |
. . . . . 6
โข (๐ = ๐ โ (โ๐ โ ๐ (๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) โ ๐ โ โ๐ โ ๐ (๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) โ ๐)) |
7 | 4, 6 | anbi12d 632 |
. . . . 5
โข (๐ = ๐ โ ((โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐ โง โ๐ โ ๐ (๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) โ ๐) โ (โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐ โง โ๐ โ ๐ (๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) โ ๐))) |
8 | | eleq2 2823 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐ โf + ๐) โ ๐ โ (๐ โf + ๐) โ ๐)) |
9 | | eleq2 2823 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐ โf ยท ๐) โ ๐ โ (๐ โf ยท ๐) โ ๐)) |
10 | 8, 9 | anbi12d 632 |
. . . . . . 7
โข (๐ = ๐ โ (((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐) โ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐))) |
11 | 10 | raleqbi1dv 3306 |
. . . . . 6
โข (๐ = ๐ โ (โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐) โ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐))) |
12 | 11 | raleqbi1dv 3306 |
. . . . 5
โข (๐ = ๐ โ (โ๐ โ ๐ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐) โ โ๐ โ ๐ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐))) |
13 | 7, 12 | anbi12d 632 |
. . . 4
โข (๐ = ๐ โ (((โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐ โง โ๐ โ ๐ (๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐)) โ ((โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐ โง โ๐ โ ๐ (๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐)))) |
14 | 13 | elrab 3649 |
. . 3
โข (๐ โ {๐ โ ๐ซ (โค โm
(โค โm ๐)) โฃ ((โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐ โง โ๐ โ ๐ (๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐))} โ (๐ โ ๐ซ (โค
โm (โค โm ๐)) โง ((โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐ โง โ๐ โ ๐ (๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐)))) |
15 | | ovex 7394 |
. . . . 5
โข (โค
โm (โค โm ๐)) โ V |
16 | 15 | elpw2 5306 |
. . . 4
โข (๐ โ ๐ซ (โค
โm (โค โm ๐)) โ ๐ โ (โค โm
(โค โm ๐))) |
17 | 16 | anbi1i 625 |
. . 3
โข ((๐ โ ๐ซ (โค
โm (โค โm ๐)) โง ((โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐ โง โ๐ โ ๐ (๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐))) โ (๐ โ (โค โm
(โค โm ๐)) โง ((โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐ โง โ๐ โ ๐ (๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐)))) |
18 | 14, 17 | bitri 275 |
. 2
โข (๐ โ {๐ โ ๐ซ (โค โm
(โค โm ๐)) โฃ ((โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐ โง โ๐ โ ๐ (๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐))} โ (๐ โ (โค โm
(โค โm ๐)) โง ((โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐ โง โ๐ โ ๐ (๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐)))) |
19 | 2, 18 | bitrdi 287 |
1
โข (๐ โ V โ (๐ โ (mzPolyCldโ๐) โ (๐ โ (โค โm
(โค โm ๐)) โง ((โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐ โง โ๐ โ ๐ (๐ฅ โ (โค โm ๐) โฆ (๐ฅโ๐)) โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐))))) |