Step | Hyp | Ref
| Expression |
1 | | mdegaddle.y |
. . . . . . 7
β’ π = (πΌ mPoly π
) |
2 | | mdegvscale.p |
. . . . . . 7
β’ Β· = (
Β·π βπ) |
3 | | mdegvscale.k |
. . . . . . 7
β’ πΎ = (Baseβπ
) |
4 | | mdegvscale.b |
. . . . . . 7
β’ π΅ = (Baseβπ) |
5 | | eqid 2733 |
. . . . . . 7
β’
(.rβπ
) = (.rβπ
) |
6 | | eqid 2733 |
. . . . . . 7
β’ {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} = {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin} |
7 | | mdegvscale.f |
. . . . . . . 8
β’ (π β πΉ β πΎ) |
8 | 7 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β πΉ β πΎ) |
9 | | mdegvscale.g |
. . . . . . . 8
β’ (π β πΊ β π΅) |
10 | 9 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β πΊ β π΅) |
11 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}) |
12 | 1, 2, 3, 4, 5, 6, 8, 10, 11 | mplvscaval 21443 |
. . . . . 6
β’ ((π β§ π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β ((πΉ Β· πΊ)βπ₯) = (πΉ(.rβπ
)(πΊβπ₯))) |
13 | 12 | adantrr 716 |
. . . . 5
β’ ((π β§ (π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ (π·βπΊ) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯))) β ((πΉ Β· πΊ)βπ₯) = (πΉ(.rβπ
)(πΊβπ₯))) |
14 | | mdegaddle.d |
. . . . . . 7
β’ π· = (πΌ mDeg π
) |
15 | | eqid 2733 |
. . . . . . 7
β’
(0gβπ
) = (0gβπ
) |
16 | | eqid 2733 |
. . . . . . 7
β’ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) = (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) |
17 | 9 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ (π·βπΊ) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯))) β πΊ β π΅) |
18 | | simprl 770 |
. . . . . . 7
β’ ((π β§ (π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ (π·βπΊ) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯))) β π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}) |
19 | | simprr 772 |
. . . . . . 7
β’ ((π β§ (π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ (π·βπΊ) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯))) β (π·βπΊ) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯)) |
20 | 14, 1, 4, 15, 6, 16, 17, 18, 19 | mdeglt 25453 |
. . . . . 6
β’ ((π β§ (π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ (π·βπΊ) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯))) β (πΊβπ₯) = (0gβπ
)) |
21 | 20 | oveq2d 7377 |
. . . . 5
β’ ((π β§ (π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ (π·βπΊ) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯))) β (πΉ(.rβπ
)(πΊβπ₯)) = (πΉ(.rβπ
)(0gβπ
))) |
22 | | mdegaddle.r |
. . . . . . 7
β’ (π β π
β Ring) |
23 | 3, 5, 15 | ringrz 20020 |
. . . . . . 7
β’ ((π
β Ring β§ πΉ β πΎ) β (πΉ(.rβπ
)(0gβπ
)) = (0gβπ
)) |
24 | 22, 7, 23 | syl2anc 585 |
. . . . . 6
β’ (π β (πΉ(.rβπ
)(0gβπ
)) = (0gβπ
)) |
25 | 24 | adantr 482 |
. . . . 5
β’ ((π β§ (π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ (π·βπΊ) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯))) β (πΉ(.rβπ
)(0gβπ
)) = (0gβπ
)) |
26 | 13, 21, 25 | 3eqtrd 2777 |
. . . 4
β’ ((π β§ (π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ (π·βπΊ) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯))) β ((πΉ Β· πΊ)βπ₯) = (0gβπ
)) |
27 | 26 | expr 458 |
. . 3
β’ ((π β§ π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β ((π·βπΊ) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯) β ((πΉ Β· πΊ)βπ₯) = (0gβπ
))) |
28 | 27 | ralrimiva 3140 |
. 2
β’ (π β βπ₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} ((π·βπΊ) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯) β ((πΉ Β· πΊ)βπ₯) = (0gβπ
))) |
29 | | mdegaddle.i |
. . . . 5
β’ (π β πΌ β π) |
30 | 1 | mpllmod 21446 |
. . . . 5
β’ ((πΌ β π β§ π
β Ring) β π β LMod) |
31 | 29, 22, 30 | syl2anc 585 |
. . . 4
β’ (π β π β LMod) |
32 | 1, 29, 22 | mplsca 21440 |
. . . . . . 7
β’ (π β π
= (Scalarβπ)) |
33 | 32 | fveq2d 6850 |
. . . . . 6
β’ (π β (Baseβπ
) =
(Baseβ(Scalarβπ))) |
34 | 3, 33 | eqtrid 2785 |
. . . . 5
β’ (π β πΎ = (Baseβ(Scalarβπ))) |
35 | 7, 34 | eleqtrd 2836 |
. . . 4
β’ (π β πΉ β (Baseβ(Scalarβπ))) |
36 | | eqid 2733 |
. . . . 5
β’
(Scalarβπ) =
(Scalarβπ) |
37 | | eqid 2733 |
. . . . 5
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
38 | 4, 36, 2, 37 | lmodvscl 20383 |
. . . 4
β’ ((π β LMod β§ πΉ β
(Baseβ(Scalarβπ)) β§ πΊ β π΅) β (πΉ Β· πΊ) β π΅) |
39 | 31, 35, 9, 38 | syl3anc 1372 |
. . 3
β’ (π β (πΉ Β· πΊ) β π΅) |
40 | 14, 1, 4 | mdegxrcl 25455 |
. . . 4
β’ (πΊ β π΅ β (π·βπΊ) β
β*) |
41 | 9, 40 | syl 17 |
. . 3
β’ (π β (π·βπΊ) β
β*) |
42 | 14, 1, 4, 15, 6, 16 | mdegleb 25452 |
. . 3
β’ (((πΉ Β· πΊ) β π΅ β§ (π·βπΊ) β β*) β ((π·β(πΉ Β· πΊ)) β€ (π·βπΊ) β βπ₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} ((π·βπΊ) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯) β ((πΉ Β· πΊ)βπ₯) = (0gβπ
)))) |
43 | 39, 41, 42 | syl2anc 585 |
. 2
β’ (π β ((π·β(πΉ Β· πΊ)) β€ (π·βπΊ) β βπ₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} ((π·βπΊ) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯) β ((πΉ Β· πΊ)βπ₯) = (0gβπ
)))) |
44 | 28, 43 | mpbird 257 |
1
β’ (π β (π·β(πΉ Β· πΊ)) β€ (π·βπΊ)) |