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 | | simprlr 779 |
. . 3
โข ((๐ โ (โค
โm (โค โm ๐)) โง ((โ๐ โ โค ((โค โm
๐) ร {๐}) โ ๐ โง โ๐ โ ๐ (๐ โ (โค โm ๐) โฆ (๐โ๐)) โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((๐ โf + ๐) โ ๐ โง (๐ โf ยท ๐) โ ๐))) โ โ๐ โ ๐ (๐ โ (โค โm ๐) โฆ (๐โ๐)) โ ๐) |
9 | 7, 8 | syl 17 |
. 2
โข ((๐ โ (mzPolyCldโ๐) โง ๐น โ ๐) โ โ๐ โ ๐ (๐ โ (โค โm ๐) โฆ (๐โ๐)) โ ๐) |
10 | | fveq2 6846 |
. . . . 5
โข (๐ = ๐น โ (๐โ๐) = (๐โ๐น)) |
11 | 10 | mpteq2dv 5211 |
. . . 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 ๐) โฆ (๐โ๐น)) โ ๐) |