Step | Hyp | Ref
| Expression |
1 | | mdegaddle.y |
. . . . . . 7
β’ π = (πΌ mPoly π
) |
2 | | mdegvsca.p |
. . . . . . 7
β’ Β· = (
Β·π βπ) |
3 | | eqid 2733 |
. . . . . . 7
β’
(Baseβπ
) =
(Baseβπ
) |
4 | | mdegvsca.b |
. . . . . . 7
β’ π΅ = (Baseβπ) |
5 | | eqid 2733 |
. . . . . . 7
β’
(.rβπ
) = (.rβπ
) |
6 | | eqid 2733 |
. . . . . . 7
β’ {π₯ β (β0
βm πΌ)
β£ (β‘π₯ β β) β Fin} = {π₯ β (β0
βm πΌ)
β£ (β‘π₯ β β) β
Fin} |
7 | | mdegvsca.e |
. . . . . . . . 9
β’ πΈ = (RLRegβπ
) |
8 | 7, 3 | rrgss 20785 |
. . . . . . . 8
β’ πΈ β (Baseβπ
) |
9 | | mdegvsca.f |
. . . . . . . 8
β’ (π β πΉ β πΈ) |
10 | 8, 9 | sselid 3946 |
. . . . . . 7
β’ (π β πΉ β (Baseβπ
)) |
11 | | mdegvsca.g |
. . . . . . 7
β’ (π β πΊ β π΅) |
12 | 1, 2, 3, 4, 5, 6, 10, 11 | mplvsca 21442 |
. . . . . 6
β’ (π β (πΉ Β· πΊ) = (({π₯ β (β0
βm πΌ)
β£ (β‘π₯ β β) β Fin} Γ {πΉ}) βf
(.rβπ
)πΊ)) |
13 | 12 | oveq1d 7376 |
. . . . 5
β’ (π β ((πΉ Β· πΊ) supp (0gβπ
)) = ((({π₯ β (β0
βm πΌ)
β£ (β‘π₯ β β) β Fin} Γ {πΉ}) βf
(.rβπ
)πΊ) supp (0gβπ
))) |
14 | | eqid 2733 |
. . . . . 6
β’
(0gβπ
) = (0gβπ
) |
15 | | ovex 7394 |
. . . . . . . 8
β’
(β0 βm πΌ) β V |
16 | 15 | rabex 5293 |
. . . . . . 7
β’ {π₯ β (β0
βm πΌ)
β£ (β‘π₯ β β) β Fin} β
V |
17 | 16 | a1i 11 |
. . . . . 6
β’ (π β {π₯ β (β0
βm πΌ)
β£ (β‘π₯ β β) β Fin} β
V) |
18 | | mdegaddle.r |
. . . . . 6
β’ (π β π
β Ring) |
19 | 1, 3, 4, 6, 11 | mplelf 21427 |
. . . . . 6
β’ (π β πΊ:{π₯ β (β0
βm πΌ)
β£ (β‘π₯ β β) β
Fin}βΆ(Baseβπ
)) |
20 | 7, 3, 5, 14, 17, 18, 9, 19 | rrgsupp 20784 |
. . . . 5
β’ (π β ((({π₯ β (β0
βm πΌ)
β£ (β‘π₯ β β) β Fin} Γ {πΉ}) βf
(.rβπ
)πΊ) supp (0gβπ
)) = (πΊ supp (0gβπ
))) |
21 | 13, 20 | eqtrd 2773 |
. . . 4
β’ (π β ((πΉ Β· πΊ) supp (0gβπ
)) = (πΊ supp (0gβπ
))) |
22 | 21 | imaeq2d 6017 |
. . 3
β’ (π β ((π¦ β {π₯ β (β0
βm πΌ)
β£ (β‘π₯ β β) β Fin} β¦
(βfld Ξ£g π¦)) β ((πΉ Β· πΊ) supp (0gβπ
))) = ((π¦ β {π₯ β (β0
βm πΌ)
β£ (β‘π₯ β β) β Fin} β¦
(βfld Ξ£g π¦)) β (πΊ supp (0gβπ
)))) |
23 | 22 | supeq1d 9390 |
. 2
β’ (π β sup(((π¦ β {π₯ β (β0
βm πΌ)
β£ (β‘π₯ β β) β Fin} β¦
(βfld Ξ£g π¦)) β ((πΉ Β· πΊ) supp (0gβπ
))), β*, < )
= sup(((π¦ β {π₯ β (β0
βm πΌ)
β£ (β‘π₯ β β) β Fin} β¦
(βfld Ξ£g π¦)) β (πΊ supp (0gβπ
))), β*, <
)) |
24 | | mdegaddle.i |
. . . . 5
β’ (π β πΌ β π) |
25 | 1 | mpllmod 21446 |
. . . . 5
β’ ((πΌ β π β§ π
β Ring) β π β LMod) |
26 | 24, 18, 25 | syl2anc 585 |
. . . 4
β’ (π β π β LMod) |
27 | 1, 24, 18 | mplsca 21440 |
. . . . . 6
β’ (π β π
= (Scalarβπ)) |
28 | 27 | fveq2d 6850 |
. . . . 5
β’ (π β (Baseβπ
) =
(Baseβ(Scalarβπ))) |
29 | 10, 28 | eleqtrd 2836 |
. . . 4
β’ (π β πΉ β (Baseβ(Scalarβπ))) |
30 | | eqid 2733 |
. . . . 5
β’
(Scalarβπ) =
(Scalarβπ) |
31 | | eqid 2733 |
. . . . 5
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
32 | 4, 30, 2, 31 | lmodvscl 20383 |
. . . 4
β’ ((π β LMod β§ πΉ β
(Baseβ(Scalarβπ)) β§ πΊ β π΅) β (πΉ Β· πΊ) β π΅) |
33 | 26, 29, 11, 32 | syl3anc 1372 |
. . 3
β’ (π β (πΉ Β· πΊ) β π΅) |
34 | | mdegaddle.d |
. . . 4
β’ π· = (πΌ mDeg π
) |
35 | | eqid 2733 |
. . . 4
β’ (π¦ β {π₯ β (β0
βm πΌ)
β£ (β‘π₯ β β) β Fin} β¦
(βfld Ξ£g π¦)) = (π¦ β {π₯ β (β0
βm πΌ)
β£ (β‘π₯ β β) β Fin} β¦
(βfld Ξ£g π¦)) |
36 | 34, 1, 4, 14, 6, 35 | mdegval 25451 |
. . 3
β’ ((πΉ Β· πΊ) β π΅ β (π·β(πΉ Β· πΊ)) = sup(((π¦ β {π₯ β (β0
βm πΌ)
β£ (β‘π₯ β β) β Fin} β¦
(βfld Ξ£g π¦)) β ((πΉ Β· πΊ) supp (0gβπ
))), β*, <
)) |
37 | 33, 36 | syl 17 |
. 2
β’ (π β (π·β(πΉ Β· πΊ)) = sup(((π¦ β {π₯ β (β0
βm πΌ)
β£ (β‘π₯ β β) β Fin} β¦
(βfld Ξ£g π¦)) β ((πΉ Β· πΊ) supp (0gβπ
))), β*, <
)) |
38 | 34, 1, 4, 14, 6, 35 | mdegval 25451 |
. . 3
β’ (πΊ β π΅ β (π·βπΊ) = sup(((π¦ β {π₯ β (β0
βm πΌ)
β£ (β‘π₯ β β) β Fin} β¦
(βfld Ξ£g π¦)) β (πΊ supp (0gβπ
))), β*, <
)) |
39 | 11, 38 | syl 17 |
. 2
β’ (π β (π·βπΊ) = sup(((π¦ β {π₯ β (β0
βm πΌ)
β£ (β‘π₯ β β) β Fin} β¦
(βfld Ξ£g π¦)) β (πΊ supp (0gβπ
))), β*, <
)) |
40 | 23, 37, 39 | 3eqtr4d 2783 |
1
β’ (π β (π·β(πΉ Β· πΊ)) = (π·βπΊ)) |