Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. 2
โข ((๐ โ (mzPolyCldโ๐) โง ๐น โ โค) โ ๐น โ โค) |
2 | | simpl 484 |
. . . 4
โข ((๐ โ (mzPolyCldโ๐) โง ๐น โ โค) โ ๐ โ (mzPolyCldโ๐)) |
3 | | elfvex 6884 |
. . . . . 6
โข (๐ โ (mzPolyCldโ๐) โ ๐ โ V) |
4 | 3 | adantr 482 |
. . . . 5
โข ((๐ โ (mzPolyCldโ๐) โง ๐น โ โค) โ ๐ โ V) |
5 | | elmzpcl 41096 |
. . . . 5
โข (๐ โ V โ (๐ โ (mzPolyCldโ๐) โ (๐ โ (โค โm
(โค โm ๐)) โง ((โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐ โง โ๐ โ ๐ (๐ โ (โค โm ๐) โฆ (๐โ๐)) โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐))))) |
6 | 4, 5 | syl 17 |
. . . 4
โข ((๐ โ (mzPolyCldโ๐) โง ๐น โ โค) โ (๐ โ (mzPolyCldโ๐) โ (๐ โ (โค โm
(โค โm ๐)) โง ((โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐ โง โ๐ โ ๐ (๐ โ (โค โm ๐) โฆ (๐โ๐)) โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐))))) |
7 | 2, 6 | mpbid 231 |
. . 3
โข ((๐ โ (mzPolyCldโ๐) โง ๐น โ โค) โ (๐ โ (โค โm
(โค โm ๐)) โง ((โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐ โง โ๐ โ ๐ (๐ โ (โค โm ๐) โฆ (๐โ๐)) โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐)))) |
8 | | simprll 778 |
. . 3
โข ((๐ โ (โค
โm (โค โm ๐)) โง ((โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐ โง โ๐ โ ๐ (๐ โ (โค โm ๐) โฆ (๐โ๐)) โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐))) โ โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐) |
9 | 7, 8 | syl 17 |
. 2
โข ((๐ โ (mzPolyCldโ๐) โง ๐น โ โค) โ โ๐ โ โค ((โค
โm ๐)
ร {๐}) โ ๐) |
10 | | sneq 4600 |
. . . . 5
โข (๐ = ๐น โ {๐} = {๐น}) |
11 | 10 | xpeq2d 5667 |
. . . 4
โข (๐ = ๐น โ ((โค โm ๐) ร {๐}) = ((โค โm ๐) ร {๐น})) |
12 | 11 | eleq1d 2819 |
. . 3
โข (๐ = ๐น โ (((โค โm ๐) ร {๐}) โ ๐ โ ((โค โm ๐) ร {๐น}) โ ๐)) |
13 | 12 | rspcva 3581 |
. 2
โข ((๐น โ โค โง
โ๐ โ โค
((โค โm ๐) ร {๐}) โ ๐) โ ((โค โm ๐) ร {๐น}) โ ๐) |
14 | 1, 9, 13 | syl2anc 585 |
1
โข ((๐ โ (mzPolyCldโ๐) โง ๐น โ โค) โ ((โค
โm ๐)
ร {๐น}) โ ๐) |