Step | Hyp | Ref
| Expression |
1 | | mdegcl.d |
. . 3
β’ π· = (πΌ mDeg π
) |
2 | | mdegcl.p |
. . 3
β’ π = (πΌ mPoly π
) |
3 | | mdegcl.b |
. . 3
β’ π΅ = (Baseβπ) |
4 | | eqid 2733 |
. . 3
β’
(0gβπ
) = (0gβπ
) |
5 | | eqid 2733 |
. . 3
β’ {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} = {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin} |
6 | | eqid 2733 |
. . 3
β’ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) = (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) |
7 | 1, 2, 3, 4, 5, 6 | mdegval 25451 |
. 2
β’ (πΉ β π΅ β (π·βπΉ) = sup(((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))), β*, <
)) |
8 | | supeq1 9389 |
. . . 4
β’ (((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))) = β
β sup(((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))), β*, < ) =
sup(β
, β*, < )) |
9 | 8 | eleq1d 2819 |
. . 3
β’ (((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))) = β
β (sup(((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))), β*, < ) β
(β0 βͺ {-β}) β sup(β
, β*,
< ) β (β0 βͺ {-β}))) |
10 | | imassrn 6028 |
. . . . . . 7
β’ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))) β ran (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) |
11 | 5, 6 | tdeglem1 25443 |
. . . . . . . 8
β’ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)):{π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}βΆβ0 |
12 | | frn 6679 |
. . . . . . . 8
β’ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)):{π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}βΆβ0 β ran (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β
β0) |
13 | 11, 12 | mp1i 13 |
. . . . . . 7
β’ (πΉ β π΅ β ran (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β
β0) |
14 | 10, 13 | sstrid 3959 |
. . . . . 6
β’ (πΉ β π΅ β ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))) β
β0) |
15 | 14 | adantr 482 |
. . . . 5
β’ ((πΉ β π΅ β§ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))) β β
) β ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))) β
β0) |
16 | | ssun1 4136 |
. . . . 5
β’
β0 β (β0 βͺ
{-β}) |
17 | 15, 16 | sstrdi 3960 |
. . . 4
β’ ((πΉ β π΅ β§ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))) β β
) β ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))) β (β0 βͺ
{-β})) |
18 | | ffun 6675 |
. . . . . . . 8
β’ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)):{π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}βΆβ0 β Fun (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))) |
19 | 11, 18 | mp1i 13 |
. . . . . . 7
β’ (πΉ β π΅ β Fun (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))) |
20 | | id 22 |
. . . . . . . . 9
β’ (πΉ β π΅ β πΉ β π΅) |
21 | | reldmmpl 21419 |
. . . . . . . . . . 11
β’ Rel dom
mPoly |
22 | 21, 2, 3 | elbasov 17098 |
. . . . . . . . . 10
β’ (πΉ β π΅ β (πΌ β V β§ π
β V)) |
23 | 22 | simprd 497 |
. . . . . . . . 9
β’ (πΉ β π΅ β π
β V) |
24 | 2, 3, 4, 20, 23 | mplelsfi 21424 |
. . . . . . . 8
β’ (πΉ β π΅ β πΉ finSupp (0gβπ
)) |
25 | 24 | fsuppimpd 9319 |
. . . . . . 7
β’ (πΉ β π΅ β (πΉ supp (0gβπ
)) β Fin) |
26 | | imafi 9125 |
. . . . . . 7
β’ ((Fun
(π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β§ (πΉ supp (0gβπ
)) β Fin) β ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))) β Fin) |
27 | 19, 25, 26 | syl2anc 585 |
. . . . . 6
β’ (πΉ β π΅ β ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))) β Fin) |
28 | 27 | adantr 482 |
. . . . 5
β’ ((πΉ β π΅ β§ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))) β β
) β ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))) β Fin) |
29 | | simpr 486 |
. . . . 5
β’ ((πΉ β π΅ β§ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))) β β
) β ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))) β β
) |
30 | | nn0ssre 12425 |
. . . . . . 7
β’
β0 β β |
31 | | ressxr 11207 |
. . . . . . 7
β’ β
β β* |
32 | 30, 31 | sstri 3957 |
. . . . . 6
β’
β0 β β* |
33 | 15, 32 | sstrdi 3960 |
. . . . 5
β’ ((πΉ β π΅ β§ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))) β β
) β ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))) β
β*) |
34 | | xrltso 13069 |
. . . . . 6
β’ < Or
β* |
35 | | fisupcl 9413 |
. . . . . 6
β’ (( <
Or β* β§ (((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))) β Fin β§ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))) β β
β§ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))) β β*)) β
sup(((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))), β*, < ) β
((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
)))) |
36 | 34, 35 | mpan 689 |
. . . . 5
β’ ((((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))) β Fin β§ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))) β β
β§ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))) β β*) β
sup(((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))), β*, < ) β
((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
)))) |
37 | 28, 29, 33, 36 | syl3anc 1372 |
. . . 4
β’ ((πΉ β π΅ β§ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))) β β
) β sup(((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))), β*, < ) β
((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
)))) |
38 | 17, 37 | sseldd 3949 |
. . 3
β’ ((πΉ β π΅ β§ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))) β β
) β sup(((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))), β*, < ) β
(β0 βͺ {-β})) |
39 | | xrsup0 13251 |
. . . . 5
β’
sup(β
, β*, < ) = -β |
40 | | ssun2 4137 |
. . . . . 6
β’
{-β} β (β0 βͺ
{-β}) |
41 | | mnfxr 11220 |
. . . . . . . 8
β’ -β
β β* |
42 | 41 | elexi 3466 |
. . . . . . 7
β’ -β
β V |
43 | 42 | snid 4626 |
. . . . . 6
β’ -β
β {-β} |
44 | 40, 43 | sselii 3945 |
. . . . 5
β’ -β
β (β0 βͺ {-β}) |
45 | 39, 44 | eqeltri 2830 |
. . . 4
β’
sup(β
, β*, < ) β (β0
βͺ {-β}) |
46 | 45 | a1i 11 |
. . 3
β’ (πΉ β π΅ β sup(β
, β*,
< ) β (β0 βͺ {-β})) |
47 | 9, 38, 46 | pm2.61ne 3027 |
. 2
β’ (πΉ β π΅ β sup(((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) β (πΉ supp (0gβπ
))), β*, < ) β
(β0 βͺ {-β})) |
48 | 7, 47 | eqeltrd 2834 |
1
β’ (πΉ β π΅ β (π·βπΉ) β (β0 βͺ
{-β})) |