Step | Hyp | Ref
| Expression |
1 | | mdegle0.f |
. . 3
β’ (π β πΉ β π΅) |
2 | | 0xr 11202 |
. . 3
β’ 0 β
β* |
3 | | mdegaddle.d |
. . . 4
β’ π· = (πΌ mDeg π
) |
4 | | mdegaddle.y |
. . . 4
β’ π = (πΌ mPoly π
) |
5 | | mdegle0.b |
. . . 4
β’ π΅ = (Baseβπ) |
6 | | eqid 2736 |
. . . 4
β’
(0gβπ
) = (0gβπ
) |
7 | | eqid 2736 |
. . . 4
β’ {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} = {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin} |
8 | | eqid 2736 |
. . . 4
β’ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) = (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) |
9 | 3, 4, 5, 6, 7, 8 | mdegleb 25429 |
. . 3
β’ ((πΉ β π΅ β§ 0 β β*) β
((π·βπΉ) β€ 0 β βπ₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} (0 < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯) β (πΉβπ₯) = (0gβπ
)))) |
10 | 1, 2, 9 | sylancl 586 |
. 2
β’ (π β ((π·βπΉ) β€ 0 β βπ₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} (0 < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯) β (πΉβπ₯) = (0gβπ
)))) |
11 | 7, 8 | tdeglem1 25420 |
. . . . . . . . . 10
β’ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)):{π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}βΆβ0 |
12 | 11 | a1i 11 |
. . . . . . . . 9
β’ (π β (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)):{π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}βΆβ0) |
13 | 12 | ffvelcdmda 7035 |
. . . . . . . 8
β’ ((π β§ π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯) β
β0) |
14 | | nn0re 12422 |
. . . . . . . . 9
β’ (((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯) β β0 β ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯) β β) |
15 | | nn0ge0 12438 |
. . . . . . . . 9
β’ (((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯) β β0 β 0 β€
((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯)) |
16 | 14, 15 | jca 512 |
. . . . . . . 8
β’ (((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯) β β0 β (((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯) β β β§ 0 β€ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯))) |
17 | | ne0gt0 11260 |
. . . . . . . 8
β’ ((((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯) β β β§ 0 β€ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯)) β (((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯) β 0 β 0 < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯))) |
18 | 13, 16, 17 | 3syl 18 |
. . . . . . 7
β’ ((π β§ π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β
(((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯) β 0 β 0 < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯))) |
19 | 7, 8 | tdeglem4 25424 |
. . . . . . . . 9
β’ (π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β (((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯) = 0 β π₯ = (πΌ Γ {0}))) |
20 | 19 | adantl 482 |
. . . . . . . 8
β’ ((π β§ π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β
(((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯) = 0 β π₯ = (πΌ Γ {0}))) |
21 | 20 | necon3abid 2980 |
. . . . . . 7
β’ ((π β§ π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β
(((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯) β 0 β Β¬ π₯ = (πΌ Γ {0}))) |
22 | 18, 21 | bitr3d 280 |
. . . . . 6
β’ ((π β§ π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (0 <
((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯) β Β¬ π₯ = (πΌ Γ {0}))) |
23 | 22 | imbi1d 341 |
. . . . 5
β’ ((π β§ π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β ((0
< ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯) β (πΉβπ₯) = (0gβπ
)) β (Β¬ π₯ = (πΌ Γ {0}) β (πΉβπ₯) = (0gβπ
)))) |
24 | | eqeq2 2748 |
. . . . . . . 8
β’ ((πΉβ(πΌ Γ {0})) = if(π₯ = (πΌ Γ {0}), (πΉβ(πΌ Γ {0})), (0gβπ
)) β ((πΉβπ₯) = (πΉβ(πΌ Γ {0})) β (πΉβπ₯) = if(π₯ = (πΌ Γ {0}), (πΉβ(πΌ Γ {0})), (0gβπ
)))) |
25 | 24 | bibi1d 343 |
. . . . . . 7
β’ ((πΉβ(πΌ Γ {0})) = if(π₯ = (πΌ Γ {0}), (πΉβ(πΌ Γ {0})), (0gβπ
)) β (((πΉβπ₯) = (πΉβ(πΌ Γ {0})) β (Β¬ π₯ = (πΌ Γ {0}) β (πΉβπ₯) = (0gβπ
))) β ((πΉβπ₯) = if(π₯ = (πΌ Γ {0}), (πΉβ(πΌ Γ {0})), (0gβπ
)) β (Β¬ π₯ = (πΌ Γ {0}) β (πΉβπ₯) = (0gβπ
))))) |
26 | | eqeq2 2748 |
. . . . . . . 8
β’
((0gβπ
) = if(π₯ = (πΌ Γ {0}), (πΉβ(πΌ Γ {0})), (0gβπ
)) β ((πΉβπ₯) = (0gβπ
) β (πΉβπ₯) = if(π₯ = (πΌ Γ {0}), (πΉβ(πΌ Γ {0})), (0gβπ
)))) |
27 | 26 | bibi1d 343 |
. . . . . . 7
β’
((0gβπ
) = if(π₯ = (πΌ Γ {0}), (πΉβ(πΌ Γ {0})), (0gβπ
)) β (((πΉβπ₯) = (0gβπ
) β (Β¬ π₯ = (πΌ Γ {0}) β (πΉβπ₯) = (0gβπ
))) β ((πΉβπ₯) = if(π₯ = (πΌ Γ {0}), (πΉβ(πΌ Γ {0})), (0gβπ
)) β (Β¬ π₯ = (πΌ Γ {0}) β (πΉβπ₯) = (0gβπ
))))) |
28 | | fveq2 6842 |
. . . . . . . . 9
β’ (π₯ = (πΌ Γ {0}) β (πΉβπ₯) = (πΉβ(πΌ Γ {0}))) |
29 | | pm2.24 124 |
. . . . . . . . 9
β’ (π₯ = (πΌ Γ {0}) β (Β¬ π₯ = (πΌ Γ {0}) β (πΉβπ₯) = (0gβπ
))) |
30 | 28, 29 | 2thd 264 |
. . . . . . . 8
β’ (π₯ = (πΌ Γ {0}) β ((πΉβπ₯) = (πΉβ(πΌ Γ {0})) β (Β¬ π₯ = (πΌ Γ {0}) β (πΉβπ₯) = (0gβπ
)))) |
31 | 30 | adantl 482 |
. . . . . . 7
β’ ((π β§ π₯ = (πΌ Γ {0})) β ((πΉβπ₯) = (πΉβ(πΌ Γ {0})) β (Β¬ π₯ = (πΌ Γ {0}) β (πΉβπ₯) = (0gβπ
)))) |
32 | | biimt 360 |
. . . . . . . 8
β’ (Β¬
π₯ = (πΌ Γ {0}) β ((πΉβπ₯) = (0gβπ
) β (Β¬ π₯ = (πΌ Γ {0}) β (πΉβπ₯) = (0gβπ
)))) |
33 | 32 | adantl 482 |
. . . . . . 7
β’ ((π β§ Β¬ π₯ = (πΌ Γ {0})) β ((πΉβπ₯) = (0gβπ
) β (Β¬ π₯ = (πΌ Γ {0}) β (πΉβπ₯) = (0gβπ
)))) |
34 | 25, 27, 31, 33 | ifbothda 4524 |
. . . . . 6
β’ (π β ((πΉβπ₯) = if(π₯ = (πΌ Γ {0}), (πΉβ(πΌ Γ {0})), (0gβπ
)) β (Β¬ π₯ = (πΌ Γ {0}) β (πΉβπ₯) = (0gβπ
)))) |
35 | 34 | adantr 481 |
. . . . 5
β’ ((π β§ π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β ((πΉβπ₯) = if(π₯ = (πΌ Γ {0}), (πΉβ(πΌ Γ {0})), (0gβπ
)) β (Β¬ π₯ = (πΌ Γ {0}) β (πΉβπ₯) = (0gβπ
)))) |
36 | 23, 35 | bitr4d 281 |
. . . 4
β’ ((π β§ π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β ((0
< ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯) β (πΉβπ₯) = (0gβπ
)) β (πΉβπ₯) = if(π₯ = (πΌ Γ {0}), (πΉβ(πΌ Γ {0})), (0gβπ
)))) |
37 | 36 | ralbidva 3172 |
. . 3
β’ (π β (βπ₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} (0 < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯) β (πΉβπ₯) = (0gβπ
)) β βπ₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} (πΉβπ₯) = if(π₯ = (πΌ Γ {0}), (πΉβ(πΌ Γ {0})), (0gβπ
)))) |
38 | | eqid 2736 |
. . . . . . 7
β’
(Baseβπ
) =
(Baseβπ
) |
39 | 4, 38, 5, 7, 1 | mplelf 21404 |
. . . . . 6
β’ (π β πΉ:{π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}βΆ(Baseβπ
)) |
40 | 39 | feqmptd 6910 |
. . . . 5
β’ (π β πΉ = (π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦ (πΉβπ₯))) |
41 | | mdegle0.a |
. . . . . 6
β’ π΄ = (algScβπ) |
42 | | mdegaddle.i |
. . . . . 6
β’ (π β πΌ β π) |
43 | | mdegaddle.r |
. . . . . 6
β’ (π β π
β Ring) |
44 | 7 | psrbag0 21470 |
. . . . . . . 8
β’ (πΌ β π β (πΌ Γ {0}) β {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}) |
45 | 42, 44 | syl 17 |
. . . . . . 7
β’ (π β (πΌ Γ {0}) β {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}) |
46 | 39, 45 | ffvelcdmd 7036 |
. . . . . 6
β’ (π β (πΉβ(πΌ Γ {0})) β (Baseβπ
)) |
47 | 4, 7, 6, 38, 41, 42, 43, 46 | mplascl 21472 |
. . . . 5
β’ (π β (π΄β(πΉβ(πΌ Γ {0}))) = (π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π₯ = (πΌ Γ {0}), (πΉβ(πΌ Γ {0})), (0gβπ
)))) |
48 | 40, 47 | eqeq12d 2752 |
. . . 4
β’ (π β (πΉ = (π΄β(πΉβ(πΌ Γ {0}))) β (π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦ (πΉβπ₯)) = (π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π₯ = (πΌ Γ {0}), (πΉβ(πΌ Γ {0})), (0gβπ
))))) |
49 | | fvex 6855 |
. . . . . 6
β’ (πΉβπ₯) β V |
50 | 49 | rgenw 3068 |
. . . . 5
β’
βπ₯ β
{π β
(β0 βm πΌ) β£ (β‘π β β) β Fin} (πΉβπ₯) β V |
51 | | mpteqb 6967 |
. . . . 5
β’
(βπ₯ β
{π β
(β0 βm πΌ) β£ (β‘π β β) β Fin} (πΉβπ₯) β V β ((π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦ (πΉβπ₯)) = (π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π₯ = (πΌ Γ {0}), (πΉβ(πΌ Γ {0})), (0gβπ
))) β βπ₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} (πΉβπ₯) = if(π₯ = (πΌ Γ {0}), (πΉβ(πΌ Γ {0})), (0gβπ
)))) |
52 | 50, 51 | mp1i 13 |
. . . 4
β’ (π β ((π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦ (πΉβπ₯)) = (π₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π₯ = (πΌ Γ {0}), (πΉβ(πΌ Γ {0})), (0gβπ
))) β βπ₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} (πΉβπ₯) = if(π₯ = (πΌ Γ {0}), (πΉβ(πΌ Γ {0})), (0gβπ
)))) |
53 | 48, 52 | bitrd 278 |
. . 3
β’ (π β (πΉ = (π΄β(πΉβ(πΌ Γ {0}))) β βπ₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} (πΉβπ₯) = if(π₯ = (πΌ Γ {0}), (πΉβ(πΌ Γ {0})), (0gβπ
)))) |
54 | 37, 53 | bitr4d 281 |
. 2
β’ (π β (βπ₯ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} (0 < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ₯) β (πΉβπ₯) = (0gβπ
)) β πΉ = (π΄β(πΉβ(πΌ Γ {0}))))) |
55 | 10, 54 | bitrd 278 |
1
β’ (π β ((π·βπΉ) β€ 0 β πΉ = (π΄β(πΉβ(πΌ Γ {0}))))) |