Step | Hyp | Ref
| Expression |
1 | | nfmpt1 5255 |
. . . . 5
β’
β²π₯(π₯ β (β€ βm π) β¦ π΄) |
2 | 1 | nfel1 2917 |
. . . 4
β’
β²π₯(π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) |
3 | | nfmpt1 5255 |
. . . . 5
β’
β²π₯(π₯ β (β€ βm π) β¦ π΅) |
4 | 3 | nfel1 2917 |
. . . 4
β’
β²π₯(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ) |
5 | 2, 4 | nfan 1900 |
. . 3
β’
β²π₯((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) |
6 | | mzpf 41776 |
. . . . . . . . 9
β’ ((π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ) β
(π₯ β (β€
βm π)
β¦ π΅):(β€
βm π)βΆβ€) |
7 | 6 | ad2antlr 723 |
. . . . . . . 8
β’ ((((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) β§
π₯ β (β€
βm π))
β (π₯ β (β€
βm π)
β¦ π΅):(β€
βm π)βΆβ€) |
8 | | simpr 483 |
. . . . . . . 8
β’ ((((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) β§
π₯ β (β€
βm π))
β π₯ β (β€
βm π)) |
9 | | mptfcl 41760 |
. . . . . . . 8
β’ ((π₯ β (β€
βm π)
β¦ π΅):(β€
βm π)βΆβ€ β (π₯ β (β€ βm π) β π΅ β β€)) |
10 | 7, 8, 9 | sylc 65 |
. . . . . . 7
β’ ((((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) β§
π₯ β (β€
βm π))
β π΅ β
β€) |
11 | 10 | zcnd 12671 |
. . . . . 6
β’ ((((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) β§
π₯ β (β€
βm π))
β π΅ β
β) |
12 | 11 | mulm1d 11670 |
. . . . 5
β’ ((((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) β§
π₯ β (β€
βm π))
β (-1 Β· π΅) =
-π΅) |
13 | 12 | oveq2d 7427 |
. . . 4
β’ ((((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) β§
π₯ β (β€
βm π))
β (π΄ + (-1 Β·
π΅)) = (π΄ + -π΅)) |
14 | | mzpf 41776 |
. . . . . . . 8
β’ ((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β
(π₯ β (β€
βm π)
β¦ π΄):(β€
βm π)βΆβ€) |
15 | 14 | ad2antrr 722 |
. . . . . . 7
β’ ((((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) β§
π₯ β (β€
βm π))
β (π₯ β (β€
βm π)
β¦ π΄):(β€
βm π)βΆβ€) |
16 | | mptfcl 41760 |
. . . . . . 7
β’ ((π₯ β (β€
βm π)
β¦ π΄):(β€
βm π)βΆβ€ β (π₯ β (β€ βm π) β π΄ β β€)) |
17 | 15, 8, 16 | sylc 65 |
. . . . . 6
β’ ((((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) β§
π₯ β (β€
βm π))
β π΄ β
β€) |
18 | 17 | zcnd 12671 |
. . . . 5
β’ ((((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) β§
π₯ β (β€
βm π))
β π΄ β
β) |
19 | 18, 11 | negsubd 11581 |
. . . 4
β’ ((((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) β§
π₯ β (β€
βm π))
β (π΄ + -π΅) = (π΄ β π΅)) |
20 | 13, 19 | eqtr2d 2771 |
. . 3
β’ ((((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) β§
π₯ β (β€
βm π))
β (π΄ β π΅) = (π΄ + (-1 Β· π΅))) |
21 | 5, 20 | mpteq2da 5245 |
. 2
β’ (((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) β
(π₯ β (β€
βm π)
β¦ (π΄ β π΅)) = (π₯ β (β€ βm π) β¦ (π΄ + (-1 Β· π΅)))) |
22 | | elfvex 6928 |
. . . . 5
β’ ((π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ) β
π β
V) |
23 | | neg1z 12602 |
. . . . 5
β’ -1 β
β€ |
24 | | mzpconstmpt 41780 |
. . . . 5
β’ ((π β V β§ -1 β
β€) β (π₯ β
(β€ βm π) β¦ -1) β (mzPolyβπ)) |
25 | 22, 23, 24 | sylancl 584 |
. . . 4
β’ ((π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ) β
(π₯ β (β€
βm π)
β¦ -1) β (mzPolyβπ)) |
26 | | mzpmulmpt 41782 |
. . . 4
β’ (((π₯ β (β€
βm π)
β¦ -1) β (mzPolyβπ) β§ (π₯ β (β€ βm π) β¦ π΅) β (mzPolyβπ)) β (π₯ β (β€ βm π) β¦ (-1 Β· π΅)) β (mzPolyβπ)) |
27 | 25, 26 | mpancom 684 |
. . 3
β’ ((π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ) β
(π₯ β (β€
βm π)
β¦ (-1 Β· π΅))
β (mzPolyβπ)) |
28 | | mzpaddmpt 41781 |
. . 3
β’ (((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ (-1 Β· π΅))
β (mzPolyβπ))
β (π₯ β (β€
βm π)
β¦ (π΄ + (-1 Β·
π΅))) β
(mzPolyβπ)) |
29 | 27, 28 | sylan2 591 |
. 2
β’ (((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) β
(π₯ β (β€
βm π)
β¦ (π΄ + (-1 Β·
π΅))) β
(mzPolyβπ)) |
30 | 21, 29 | eqeltrd 2831 |
1
β’ (((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) β
(π₯ β (β€
βm π)
β¦ (π΄ β π΅)) β (mzPolyβπ)) |