Step | Hyp | Ref
| Expression |
1 | | df-prmidl 32256 |
. 2
β’ PrmIdeal
= (π β Ring β¦
{π β
(LIdealβπ) β£
(π β (Baseβπ) β§ βπ β (LIdealβπ)βπ β (LIdealβπ)(βπ₯ β π βπ¦ β π (π₯(.rβπ)π¦) β π β (π β π β¨ π β π)))}) |
2 | | fveq2 6843 |
. . 3
β’ (π = π
β (LIdealβπ) = (LIdealβπ
)) |
3 | | fveq2 6843 |
. . . . . 6
β’ (π = π
β (Baseβπ) = (Baseβπ
)) |
4 | | prmidlval.1 |
. . . . . 6
β’ π΅ = (Baseβπ
) |
5 | 3, 4 | eqtr4di 2791 |
. . . . 5
β’ (π = π
β (Baseβπ) = π΅) |
6 | 5 | neeq2d 3001 |
. . . 4
β’ (π = π
β (π β (Baseβπ) β π β π΅)) |
7 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π = π
β (.rβπ) = (.rβπ
)) |
8 | | prmidlval.2 |
. . . . . . . . . . 11
β’ Β· =
(.rβπ
) |
9 | 7, 8 | eqtr4di 2791 |
. . . . . . . . . 10
β’ (π = π
β (.rβπ) = Β· ) |
10 | 9 | oveqd 7375 |
. . . . . . . . 9
β’ (π = π
β (π₯(.rβπ)π¦) = (π₯ Β· π¦)) |
11 | 10 | eleq1d 2819 |
. . . . . . . 8
β’ (π = π
β ((π₯(.rβπ)π¦) β π β (π₯ Β· π¦) β π)) |
12 | 11 | 2ralbidv 3209 |
. . . . . . 7
β’ (π = π
β (βπ₯ β π βπ¦ β π (π₯(.rβπ)π¦) β π β βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π)) |
13 | 12 | imbi1d 342 |
. . . . . 6
β’ (π = π
β ((βπ₯ β π βπ¦ β π (π₯(.rβπ)π¦) β π β (π β π β¨ π β π)) β (βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π)))) |
14 | 2, 13 | raleqbidv 3318 |
. . . . 5
β’ (π = π
β (βπ β (LIdealβπ)(βπ₯ β π βπ¦ β π (π₯(.rβπ)π¦) β π β (π β π β¨ π β π)) β βπ β (LIdealβπ
)(βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π)))) |
15 | 2, 14 | raleqbidv 3318 |
. . . 4
β’ (π = π
β (βπ β (LIdealβπ)βπ β (LIdealβπ)(βπ₯ β π βπ¦ β π (π₯(.rβπ)π¦) β π β (π β π β¨ π β π)) β βπ β (LIdealβπ
)βπ β (LIdealβπ
)(βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π)))) |
16 | 6, 15 | anbi12d 632 |
. . 3
β’ (π = π
β ((π β (Baseβπ) β§ βπ β (LIdealβπ)βπ β (LIdealβπ)(βπ₯ β π βπ¦ β π (π₯(.rβπ)π¦) β π β (π β π β¨ π β π))) β (π β π΅ β§ βπ β (LIdealβπ
)βπ β (LIdealβπ
)(βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π))))) |
17 | 2, 16 | rabeqbidv 3423 |
. 2
β’ (π = π
β {π β (LIdealβπ) β£ (π β (Baseβπ) β§ βπ β (LIdealβπ)βπ β (LIdealβπ)(βπ₯ β π βπ¦ β π (π₯(.rβπ)π¦) β π β (π β π β¨ π β π)))} = {π β (LIdealβπ
) β£ (π β π΅ β§ βπ β (LIdealβπ
)βπ β (LIdealβπ
)(βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π)))}) |
18 | | id 22 |
. 2
β’ (π
β Ring β π
β Ring) |
19 | | eqid 2733 |
. . 3
β’ {π β (LIdealβπ
) β£ (π β π΅ β§ βπ β (LIdealβπ
)βπ β (LIdealβπ
)(βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π)))} = {π β (LIdealβπ
) β£ (π β π΅ β§ βπ β (LIdealβπ
)βπ β (LIdealβπ
)(βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π)))} |
20 | | fvexd 6858 |
. . 3
β’ (π
β Ring β
(LIdealβπ
) β
V) |
21 | 19, 20 | rabexd 5291 |
. 2
β’ (π
β Ring β {π β (LIdealβπ
) β£ (π β π΅ β§ βπ β (LIdealβπ
)βπ β (LIdealβπ
)(βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π)))} β V) |
22 | 1, 17, 18, 21 | fvmptd3 6972 |
1
β’ (π
β Ring β
(PrmIdealβπ
) = {π β (LIdealβπ
) β£ (π β π΅ β§ βπ β (LIdealβπ
)βπ β (LIdealβπ
)(βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π)))}) |