Step | Hyp | Ref
| Expression |
1 | | nfmpt1 5257 |
. . . . 5
β’
β²π₯(π₯ β (β€ βm π) β¦ π΄) |
2 | 1 | nfel1 2920 |
. . . 4
β’
β²π₯(π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) |
3 | | nfmpt1 5257 |
. . . . 5
β’
β²π₯(π₯ β (β€ βm π) β¦ π΅) |
4 | 3 | nfel1 2920 |
. . . 4
β’
β²π₯(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ) |
5 | 2, 4 | nfan 1903 |
. . 3
β’
β²π₯((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) |
6 | | mzpf 41474 |
. . . . . . . . 9
β’ ((π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ) β
(π₯ β (β€
βm π)
β¦ π΅):(β€
βm π)βΆβ€) |
7 | 6 | ad2antlr 726 |
. . . . . . . 8
β’ ((((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) β§
π₯ β (β€
βm π))
β (π₯ β (β€
βm π)
β¦ π΅):(β€
βm π)βΆβ€) |
8 | | simpr 486 |
. . . . . . . 8
β’ ((((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) β§
π₯ β (β€
βm π))
β π₯ β (β€
βm π)) |
9 | | mptfcl 41458 |
. . . . . . . 8
β’ ((π₯ β (β€
βm π)
β¦ π΅):(β€
βm π)βΆβ€ β (π₯ β (β€ βm π) β π΅ β β€)) |
10 | 7, 8, 9 | sylc 65 |
. . . . . . 7
β’ ((((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) β§
π₯ β (β€
βm π))
β π΅ β
β€) |
11 | 10 | zcnd 12667 |
. . . . . 6
β’ ((((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) β§
π₯ β (β€
βm π))
β π΅ β
β) |
12 | 11 | mulm1d 11666 |
. . . . 5
β’ ((((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) β§
π₯ β (β€
βm π))
β (-1 Β· π΅) =
-π΅) |
13 | 12 | oveq2d 7425 |
. . . 4
β’ ((((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) β§
π₯ β (β€
βm π))
β (π΄ + (-1 Β·
π΅)) = (π΄ + -π΅)) |
14 | | mzpf 41474 |
. . . . . . . 8
β’ ((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β
(π₯ β (β€
βm π)
β¦ π΄):(β€
βm π)βΆβ€) |
15 | 14 | ad2antrr 725 |
. . . . . . 7
β’ ((((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) β§
π₯ β (β€
βm π))
β (π₯ β (β€
βm π)
β¦ π΄):(β€
βm π)βΆβ€) |
16 | | mptfcl 41458 |
. . . . . . 7
β’ ((π₯ β (β€
βm π)
β¦ π΄):(β€
βm π)βΆβ€ β (π₯ β (β€ βm π) β π΄ β β€)) |
17 | 15, 8, 16 | sylc 65 |
. . . . . 6
β’ ((((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) β§
π₯ β (β€
βm π))
β π΄ β
β€) |
18 | 17 | zcnd 12667 |
. . . . 5
β’ ((((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) β§
π₯ β (β€
βm π))
β π΄ β
β) |
19 | 18, 11 | negsubd 11577 |
. . . 4
β’ ((((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) β§
π₯ β (β€
βm π))
β (π΄ + -π΅) = (π΄ β π΅)) |
20 | 13, 19 | eqtr2d 2774 |
. . 3
β’ ((((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) β§
π₯ β (β€
βm π))
β (π΄ β π΅) = (π΄ + (-1 Β· π΅))) |
21 | 5, 20 | mpteq2da 5247 |
. 2
β’ (((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) β
(π₯ β (β€
βm π)
β¦ (π΄ β π΅)) = (π₯ β (β€ βm π) β¦ (π΄ + (-1 Β· π΅)))) |
22 | | elfvex 6930 |
. . . . 5
β’ ((π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ) β
π β
V) |
23 | | neg1z 12598 |
. . . . 5
β’ -1 β
β€ |
24 | | mzpconstmpt 41478 |
. . . . 5
β’ ((π β V β§ -1 β
β€) β (π₯ β
(β€ βm π) β¦ -1) β (mzPolyβπ)) |
25 | 22, 23, 24 | sylancl 587 |
. . . 4
β’ ((π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ) β
(π₯ β (β€
βm π)
β¦ -1) β (mzPolyβπ)) |
26 | | mzpmulmpt 41480 |
. . . 4
β’ (((π₯ β (β€
βm π)
β¦ -1) β (mzPolyβπ) β§ (π₯ β (β€ βm π) β¦ π΅) β (mzPolyβπ)) β (π₯ β (β€ βm π) β¦ (-1 Β· π΅)) β (mzPolyβπ)) |
27 | 25, 26 | mpancom 687 |
. . 3
β’ ((π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ) β
(π₯ β (β€
βm π)
β¦ (-1 Β· π΅))
β (mzPolyβπ)) |
28 | | mzpaddmpt 41479 |
. . 3
β’ (((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ (-1 Β· π΅))
β (mzPolyβπ))
β (π₯ β (β€
βm π)
β¦ (π΄ + (-1 Β·
π΅))) β
(mzPolyβπ)) |
29 | 27, 28 | sylan2 594 |
. 2
β’ (((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) β
(π₯ β (β€
βm π)
β¦ (π΄ + (-1 Β·
π΅))) β
(mzPolyβπ)) |
30 | 21, 29 | eqeltrd 2834 |
1
β’ (((π₯ β (β€
βm π)
β¦ π΄) β
(mzPolyβπ) β§
(π₯ β (β€
βm π)
β¦ π΅) β
(mzPolyβπ)) β
(π₯ β (β€
βm π)
β¦ (π΄ β π΅)) β (mzPolyβπ)) |