Step | Hyp | Ref
| Expression |
1 | | fveq2 6843 |
. . 3
β’ (π = π
β (Idlβπ) = (Idlβπ
)) |
2 | | fveq2 6843 |
. . . . . . . 8
β’ (π = π
β (1st βπ) = (1st βπ
)) |
3 | | pridlval.1 |
. . . . . . . 8
β’ πΊ = (1st βπ
) |
4 | 2, 3 | eqtr4di 2795 |
. . . . . . 7
β’ (π = π
β (1st βπ) = πΊ) |
5 | 4 | rneqd 5894 |
. . . . . 6
β’ (π = π
β ran (1st βπ) = ran πΊ) |
6 | | pridlval.3 |
. . . . . 6
β’ π = ran πΊ |
7 | 5, 6 | eqtr4di 2795 |
. . . . 5
β’ (π = π
β ran (1st βπ) = π) |
8 | 7 | neeq2d 3005 |
. . . 4
β’ (π = π
β (π β ran (1st βπ) β π β π)) |
9 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π = π
β (2nd βπ) = (2nd βπ
)) |
10 | | pridlval.2 |
. . . . . . . . . . 11
β’ π» = (2nd βπ
) |
11 | 9, 10 | eqtr4di 2795 |
. . . . . . . . . 10
β’ (π = π
β (2nd βπ) = π») |
12 | 11 | oveqd 7375 |
. . . . . . . . 9
β’ (π = π
β (π₯(2nd βπ)π¦) = (π₯π»π¦)) |
13 | 12 | eleq1d 2823 |
. . . . . . . 8
β’ (π = π
β ((π₯(2nd βπ)π¦) β π β (π₯π»π¦) β π)) |
14 | 13 | 2ralbidv 3213 |
. . . . . . 7
β’ (π = π
β (βπ₯ β π βπ¦ β π (π₯(2nd βπ)π¦) β π β βπ₯ β π βπ¦ β π (π₯π»π¦) β π)) |
15 | 14 | imbi1d 342 |
. . . . . 6
β’ (π = π
β ((βπ₯ β π βπ¦ β π (π₯(2nd βπ)π¦) β π β (π β π β¨ π β π)) β (βπ₯ β π βπ¦ β π (π₯π»π¦) β π β (π β π β¨ π β π)))) |
16 | 1, 15 | raleqbidv 3320 |
. . . . 5
β’ (π = π
β (βπ β (Idlβπ)(βπ₯ β π βπ¦ β π (π₯(2nd βπ)π¦) β π β (π β π β¨ π β π)) β βπ β (Idlβπ
)(βπ₯ β π βπ¦ β π (π₯π»π¦) β π β (π β π β¨ π β π)))) |
17 | 1, 16 | raleqbidv 3320 |
. . . 4
β’ (π = π
β (βπ β (Idlβπ)βπ β (Idlβπ)(βπ₯ β π βπ¦ β π (π₯(2nd βπ)π¦) β π β (π β π β¨ π β π)) β βπ β (Idlβπ
)βπ β (Idlβπ
)(βπ₯ β π βπ¦ β π (π₯π»π¦) β π β (π β π β¨ π β π)))) |
18 | 8, 17 | anbi12d 632 |
. . 3
β’ (π = π
β ((π β ran (1st βπ) β§ βπ β (Idlβπ)βπ β (Idlβπ)(βπ₯ β π βπ¦ β π (π₯(2nd βπ)π¦) β π β (π β π β¨ π β π))) β (π β π β§ βπ β (Idlβπ
)βπ β (Idlβπ
)(βπ₯ β π βπ¦ β π (π₯π»π¦) β π β (π β π β¨ π β π))))) |
19 | 1, 18 | rabeqbidv 3425 |
. 2
β’ (π = π
β {π β (Idlβπ) β£ (π β ran (1st βπ) β§ βπ β (Idlβπ)βπ β (Idlβπ)(βπ₯ β π βπ¦ β π (π₯(2nd βπ)π¦) β π β (π β π β¨ π β π)))} = {π β (Idlβπ
) β£ (π β π β§ βπ β (Idlβπ
)βπ β (Idlβπ
)(βπ₯ β π βπ¦ β π (π₯π»π¦) β π β (π β π β¨ π β π)))}) |
20 | | df-pridl 36473 |
. 2
β’ PrIdl =
(π β RingOps β¦
{π β (Idlβπ) β£ (π β ran (1st βπ) β§ βπ β (Idlβπ)βπ β (Idlβπ)(βπ₯ β π βπ¦ β π (π₯(2nd βπ)π¦) β π β (π β π β¨ π β π)))}) |
21 | | fvex 6856 |
. . 3
β’
(Idlβπ
) β
V |
22 | 21 | rabex 5290 |
. 2
β’ {π β (Idlβπ
) β£ (π β π β§ βπ β (Idlβπ
)βπ β (Idlβπ
)(βπ₯ β π βπ¦ β π (π₯π»π¦) β π β (π β π β¨ π β π)))} β V |
23 | 19, 20, 22 | fvmpt 6949 |
1
β’ (π
β RingOps β
(PrIdlβπ
) = {π β (Idlβπ
) β£ (π β π β§ βπ β (Idlβπ
)βπ β (Idlβπ
)(βπ₯ β π βπ¦ β π (π₯π»π¦) β π β (π β π β¨ π β π)))}) |