Step | Hyp | Ref
| Expression |
1 | | df-mnc 41489 |
. . . . 5
β’ Monic =
(π β π« β
β¦ {π β
(Polyβπ ) β£
((coeffβπ)β(degβπ)) = 1}) |
2 | 1 | dmmptss 6198 |
. . . 4
β’ dom Monic
β π« β |
3 | | elfvdm 6884 |
. . . 4
β’ (π β ( Monic βπ) β π β dom Monic ) |
4 | 2, 3 | sselid 3947 |
. . 3
β’ (π β ( Monic βπ) β π β π« β) |
5 | 4 | elpwid 4574 |
. 2
β’ (π β ( Monic βπ) β π β β) |
6 | | plybss 25571 |
. . 3
β’ (π β (Polyβπ) β π β β) |
7 | 6 | adantr 482 |
. 2
β’ ((π β (Polyβπ) β§ ((coeffβπ)β(degβπ)) = 1) β π β β) |
8 | | cnex 11139 |
. . . . . 6
β’ β
β V |
9 | 8 | elpw2 5307 |
. . . . 5
β’ (π β π« β β
π β
β) |
10 | | fveq2 6847 |
. . . . . . 7
β’ (π = π β (Polyβπ ) = (Polyβπ)) |
11 | | rabeq 3424 |
. . . . . . 7
β’
((Polyβπ ) =
(Polyβπ) β
{π β (Polyβπ ) β£ ((coeffβπ)β(degβπ)) = 1} = {π β (Polyβπ) β£ ((coeffβπ)β(degβπ)) = 1}) |
12 | 10, 11 | syl 17 |
. . . . . 6
β’ (π = π β {π β (Polyβπ ) β£ ((coeffβπ)β(degβπ)) = 1} = {π β (Polyβπ) β£ ((coeffβπ)β(degβπ)) = 1}) |
13 | | fvex 6860 |
. . . . . . 7
β’
(Polyβπ)
β V |
14 | 13 | rabex 5294 |
. . . . . 6
β’ {π β (Polyβπ) β£ ((coeffβπ)β(degβπ)) = 1} β
V |
15 | 12, 1, 14 | fvmpt 6953 |
. . . . 5
β’ (π β π« β β
( Monic βπ) = {π β (Polyβπ) β£ ((coeffβπ)β(degβπ)) = 1}) |
16 | 9, 15 | sylbir 234 |
. . . 4
β’ (π β β β ( Monic
βπ) = {π β (Polyβπ) β£ ((coeffβπ)β(degβπ)) = 1}) |
17 | 16 | eleq2d 2824 |
. . 3
β’ (π β β β (π β ( Monic βπ) β π β {π β (Polyβπ) β£ ((coeffβπ)β(degβπ)) = 1})) |
18 | | fveq2 6847 |
. . . . . 6
β’ (π = π β (coeffβπ) = (coeffβπ)) |
19 | | fveq2 6847 |
. . . . . 6
β’ (π = π β (degβπ) = (degβπ)) |
20 | 18, 19 | fveq12d 6854 |
. . . . 5
β’ (π = π β ((coeffβπ)β(degβπ)) = ((coeffβπ)β(degβπ))) |
21 | 20 | eqeq1d 2739 |
. . . 4
β’ (π = π β (((coeffβπ)β(degβπ)) = 1 β ((coeffβπ)β(degβπ)) = 1)) |
22 | 21 | elrab 3650 |
. . 3
β’ (π β {π β (Polyβπ) β£ ((coeffβπ)β(degβπ)) = 1} β (π β (Polyβπ) β§ ((coeffβπ)β(degβπ)) = 1)) |
23 | 17, 22 | bitrdi 287 |
. 2
β’ (π β β β (π β ( Monic βπ) β (π β (Polyβπ) β§ ((coeffβπ)β(degβπ)) = 1))) |
24 | 5, 7, 23 | pm5.21nii 380 |
1
β’ (π β ( Monic βπ) β (π β (Polyβπ) β§ ((coeffβπ)β(degβπ)) = 1)) |