Step | Hyp | Ref
| Expression |
1 | | mzpval 41102 |
. 2
โข (๐ โ V โ
(mzPolyโ๐) = โฉ (mzPolyCldโ๐)) |
2 | | mzpclall 41097 |
. . . . 5
โข (๐ โ V โ (โค
โm (โค โm ๐)) โ (mzPolyCldโ๐)) |
3 | | intss1 4928 |
. . . . 5
โข ((โค
โm (โค โm ๐)) โ (mzPolyCldโ๐) โ โฉ
(mzPolyCldโ๐) โ
(โค โm (โค โm ๐))) |
4 | 2, 3 | syl 17 |
. . . 4
โข (๐ โ V โ โฉ (mzPolyCldโ๐) โ (โค โm
(โค โm ๐))) |
5 | | simpr 486 |
. . . . . . . . 9
โข (((๐ โ V โง ๐ โ โค) โง ๐ โ (mzPolyCldโ๐)) โ ๐ โ (mzPolyCldโ๐)) |
6 | | simplr 768 |
. . . . . . . . 9
โข (((๐ โ V โง ๐ โ โค) โง ๐ โ (mzPolyCldโ๐)) โ ๐ โ โค) |
7 | | mzpcl1 41099 |
. . . . . . . . 9
โข ((๐ โ (mzPolyCldโ๐) โง ๐ โ โค) โ ((โค
โm ๐)
ร {๐}) โ ๐) |
8 | 5, 6, 7 | syl2anc 585 |
. . . . . . . 8
โข (((๐ โ V โง ๐ โ โค) โง ๐ โ (mzPolyCldโ๐)) โ ((โค
โm ๐)
ร {๐}) โ ๐) |
9 | 8 | ralrimiva 3140 |
. . . . . . 7
โข ((๐ โ V โง ๐ โ โค) โ
โ๐ โ
(mzPolyCldโ๐)((โค โm ๐) ร {๐}) โ ๐) |
10 | | ovex 7394 |
. . . . . . . . 9
โข (โค
โm ๐)
โ V |
11 | | vsnex 5390 |
. . . . . . . . 9
โข {๐} โ V |
12 | 10, 11 | xpex 7691 |
. . . . . . . 8
โข ((โค
โm ๐)
ร {๐}) โ
V |
13 | 12 | elint2 4918 |
. . . . . . 7
โข
(((โค โm ๐) ร {๐}) โ โฉ
(mzPolyCldโ๐) โ
โ๐ โ
(mzPolyCldโ๐)((โค โm ๐) ร {๐}) โ ๐) |
14 | 9, 13 | sylibr 233 |
. . . . . 6
โข ((๐ โ V โง ๐ โ โค) โ
((โค โm ๐) ร {๐}) โ โฉ
(mzPolyCldโ๐)) |
15 | 14 | ralrimiva 3140 |
. . . . 5
โข (๐ โ V โ โ๐ โ โค ((โค
โm ๐)
ร {๐}) โ โฉ (mzPolyCldโ๐)) |
16 | | simpr 486 |
. . . . . . . . 9
โข (((๐ โ V โง ๐ โ ๐) โง ๐ โ (mzPolyCldโ๐)) โ ๐ โ (mzPolyCldโ๐)) |
17 | | simplr 768 |
. . . . . . . . 9
โข (((๐ โ V โง ๐ โ ๐) โง ๐ โ (mzPolyCldโ๐)) โ ๐ โ ๐) |
18 | | mzpcl2 41100 |
. . . . . . . . 9
โข ((๐ โ (mzPolyCldโ๐) โง ๐ โ ๐) โ (๐ โ (โค โm ๐) โฆ (๐โ๐)) โ ๐) |
19 | 16, 17, 18 | syl2anc 585 |
. . . . . . . 8
โข (((๐ โ V โง ๐ โ ๐) โง ๐ โ (mzPolyCldโ๐)) โ (๐ โ (โค โm ๐) โฆ (๐โ๐)) โ ๐) |
20 | 19 | ralrimiva 3140 |
. . . . . . 7
โข ((๐ โ V โง ๐ โ ๐) โ โ๐ โ (mzPolyCldโ๐)(๐ โ (โค โm ๐) โฆ (๐โ๐)) โ ๐) |
21 | 10 | mptex 7177 |
. . . . . . . 8
โข (๐ โ (โค
โm ๐)
โฆ (๐โ๐)) โ V |
22 | 21 | elint2 4918 |
. . . . . . 7
โข ((๐ โ (โค
โm ๐)
โฆ (๐โ๐)) โ โฉ (mzPolyCldโ๐) โ โ๐ โ (mzPolyCldโ๐)(๐ โ (โค โm ๐) โฆ (๐โ๐)) โ ๐) |
23 | 20, 22 | sylibr 233 |
. . . . . 6
โข ((๐ โ V โง ๐ โ ๐) โ (๐ โ (โค โm ๐) โฆ (๐โ๐)) โ โฉ
(mzPolyCldโ๐)) |
24 | 23 | ralrimiva 3140 |
. . . . 5
โข (๐ โ V โ โ๐ โ ๐ (๐ โ (โค โm ๐) โฆ (๐โ๐)) โ โฉ
(mzPolyCldโ๐)) |
25 | 15, 24 | jca 513 |
. . . 4
โข (๐ โ V โ (โ๐ โ โค ((โค
โm ๐)
ร {๐}) โ โฉ (mzPolyCldโ๐) โง โ๐ โ ๐ (๐ โ (โค โm ๐) โฆ (๐โ๐)) โ โฉ
(mzPolyCldโ๐))) |
26 | | vex 3451 |
. . . . . . . . 9
โข ๐ โ V |
27 | 26 | elint2 4918 |
. . . . . . . 8
โข (๐ โ โฉ (mzPolyCldโ๐) โ โ๐ โ (mzPolyCldโ๐)๐ โ ๐) |
28 | | vex 3451 |
. . . . . . . . 9
โข ๐ โ V |
29 | 28 | elint2 4918 |
. . . . . . . 8
โข (๐ โ โฉ (mzPolyCldโ๐) โ โ๐ โ (mzPolyCldโ๐)๐ โ ๐) |
30 | | mzpcl34 41101 |
. . . . . . . . . . 11
โข ((๐ โ (mzPolyCldโ๐) โง ๐ โ ๐ โง ๐ โ ๐) โ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐)) |
31 | 30 | 3expib 1123 |
. . . . . . . . . 10
โข (๐ โ (mzPolyCldโ๐) โ ((๐ โ ๐ โง ๐ โ ๐) โ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐))) |
32 | 31 | ralimia 3080 |
. . . . . . . . 9
โข
(โ๐ โ
(mzPolyCldโ๐)(๐ โ ๐ โง ๐ โ ๐) โ โ๐ โ (mzPolyCldโ๐)((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐)) |
33 | | r19.26 3111 |
. . . . . . . . 9
โข
(โ๐ โ
(mzPolyCldโ๐)(๐ โ ๐ โง ๐ โ ๐) โ (โ๐ โ (mzPolyCldโ๐)๐ โ ๐ โง โ๐ โ (mzPolyCldโ๐)๐ โ ๐)) |
34 | | r19.26 3111 |
. . . . . . . . 9
โข
(โ๐ โ
(mzPolyCldโ๐)((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐) โ (โ๐ โ (mzPolyCldโ๐)(๐ โf + ๐) โ ๐ โง โ๐ โ (mzPolyCldโ๐)(๐ โf ยท ๐) โ ๐)) |
35 | 32, 33, 34 | 3imtr3i 291 |
. . . . . . . 8
โข
((โ๐ โ
(mzPolyCldโ๐)๐ โ ๐ โง โ๐ โ (mzPolyCldโ๐)๐ โ ๐) โ (โ๐ โ (mzPolyCldโ๐)(๐ โf + ๐) โ ๐ โง โ๐ โ (mzPolyCldโ๐)(๐ โf ยท ๐) โ ๐)) |
36 | 27, 29, 35 | syl2anb 599 |
. . . . . . 7
โข ((๐ โ โฉ (mzPolyCldโ๐) โง ๐ โ โฉ
(mzPolyCldโ๐)) โ
(โ๐ โ
(mzPolyCldโ๐)(๐ โf + ๐) โ ๐ โง โ๐ โ (mzPolyCldโ๐)(๐ โf ยท ๐) โ ๐)) |
37 | | ovex 7394 |
. . . . . . . . 9
โข (๐ โf + ๐) โ V |
38 | 37 | elint2 4918 |
. . . . . . . 8
โข ((๐ โf + ๐) โ โฉ (mzPolyCldโ๐) โ โ๐ โ (mzPolyCldโ๐)(๐ โf + ๐) โ ๐) |
39 | | ovex 7394 |
. . . . . . . . 9
โข (๐ โf ยท
๐) โ
V |
40 | 39 | elint2 4918 |
. . . . . . . 8
โข ((๐ โf ยท
๐) โ โฉ (mzPolyCldโ๐) โ โ๐ โ (mzPolyCldโ๐)(๐ โf ยท ๐) โ ๐) |
41 | 38, 40 | anbi12i 628 |
. . . . . . 7
โข (((๐ โf + ๐) โ โฉ (mzPolyCldโ๐) โง (๐ โf ยท ๐) โ โฉ (mzPolyCldโ๐)) โ (โ๐ โ (mzPolyCldโ๐)(๐ โf + ๐) โ ๐ โง โ๐ โ (mzPolyCldโ๐)(๐ โf ยท ๐) โ ๐)) |
42 | 36, 41 | sylibr 233 |
. . . . . 6
โข ((๐ โ โฉ (mzPolyCldโ๐) โง ๐ โ โฉ
(mzPolyCldโ๐)) โ
((๐ โf +
๐) โ โฉ (mzPolyCldโ๐) โง (๐ โf ยท ๐) โ โฉ (mzPolyCldโ๐))) |
43 | 42 | a1i 11 |
. . . . 5
โข (๐ โ V โ ((๐ โ โฉ (mzPolyCldโ๐) โง ๐ โ โฉ
(mzPolyCldโ๐)) โ
((๐ โf +
๐) โ โฉ (mzPolyCldโ๐) โง (๐ โf ยท ๐) โ โฉ (mzPolyCldโ๐)))) |
44 | 43 | ralrimivv 3192 |
. . . 4
โข (๐ โ V โ โ๐ โ โฉ (mzPolyCldโ๐)โ๐ โ โฉ
(mzPolyCldโ๐)((๐ โf + ๐) โ โฉ (mzPolyCldโ๐) โง (๐ โf ยท ๐) โ โฉ (mzPolyCldโ๐))) |
45 | 4, 25, 44 | jca32 517 |
. . 3
โข (๐ โ V โ (โฉ (mzPolyCldโ๐) โ (โค โm
(โค โm ๐)) โง ((โ๐ โ โค ((โค โm
๐) ร {๐}) โ โฉ (mzPolyCldโ๐) โง โ๐ โ ๐ (๐ โ (โค โm ๐) โฆ (๐โ๐)) โ โฉ
(mzPolyCldโ๐)) โง
โ๐ โ โฉ (mzPolyCldโ๐)โ๐ โ โฉ
(mzPolyCldโ๐)((๐ โf + ๐) โ โฉ (mzPolyCldโ๐) โง (๐ โf ยท ๐) โ โฉ (mzPolyCldโ๐))))) |
46 | | elmzpcl 41096 |
. . 3
โข (๐ โ V โ (โฉ (mzPolyCldโ๐) โ (mzPolyCldโ๐) โ (โฉ
(mzPolyCldโ๐) โ
(โค โm (โค โm ๐)) โง ((โ๐ โ โค ((โค โm
๐) ร {๐}) โ โฉ (mzPolyCldโ๐) โง โ๐ โ ๐ (๐ โ (โค โm ๐) โฆ (๐โ๐)) โ โฉ
(mzPolyCldโ๐)) โง
โ๐ โ โฉ (mzPolyCldโ๐)โ๐ โ โฉ
(mzPolyCldโ๐)((๐ โf + ๐) โ โฉ (mzPolyCldโ๐) โง (๐ โf ยท ๐) โ โฉ (mzPolyCldโ๐)))))) |
47 | 45, 46 | mpbird 257 |
. 2
โข (๐ โ V โ โฉ (mzPolyCldโ๐) โ (mzPolyCldโ๐)) |
48 | 1, 47 | eqeltrd 2834 |
1
โข (๐ โ V โ
(mzPolyโ๐) โ
(mzPolyCldโ๐)) |