Step | Hyp | Ref
| Expression |
1 | | oveq12 7367 |
. . 3
β’ ((π = π
β§ π = π) β (π RngHom π ) = (π
RngHom π)) |
2 | | fveq2 6843 |
. . . . . . . 8
β’ (π = π
β (1st βπ) = (1st βπ
)) |
3 | | rngisoval.1 |
. . . . . . . 8
β’ πΊ = (1st βπ
) |
4 | 2, 3 | eqtr4di 2795 |
. . . . . . 7
β’ (π = π
β (1st βπ) = πΊ) |
5 | 4 | rneqd 5894 |
. . . . . 6
β’ (π = π
β ran (1st βπ) = ran πΊ) |
6 | | rngisoval.2 |
. . . . . 6
β’ π = ran πΊ |
7 | 5, 6 | eqtr4di 2795 |
. . . . 5
β’ (π = π
β ran (1st βπ) = π) |
8 | 7 | f1oeq2d 6781 |
. . . 4
β’ (π = π
β (π:ran (1st βπ)β1-1-ontoβran
(1st βπ )
β π:πβ1-1-ontoβran
(1st βπ ))) |
9 | | fveq2 6843 |
. . . . . . . 8
β’ (π = π β (1st βπ ) = (1st βπ)) |
10 | | rngisoval.3 |
. . . . . . . 8
β’ π½ = (1st βπ) |
11 | 9, 10 | eqtr4di 2795 |
. . . . . . 7
β’ (π = π β (1st βπ ) = π½) |
12 | 11 | rneqd 5894 |
. . . . . 6
β’ (π = π β ran (1st βπ ) = ran π½) |
13 | | rngisoval.4 |
. . . . . 6
β’ π = ran π½ |
14 | 12, 13 | eqtr4di 2795 |
. . . . 5
β’ (π = π β ran (1st βπ ) = π) |
15 | 14 | f1oeq3d 6782 |
. . . 4
β’ (π = π β (π:πβ1-1-ontoβran
(1st βπ )
β π:πβ1-1-ontoβπ)) |
16 | 8, 15 | sylan9bb 511 |
. . 3
β’ ((π = π
β§ π = π) β (π:ran (1st βπ)β1-1-ontoβran
(1st βπ )
β π:πβ1-1-ontoβπ)) |
17 | 1, 16 | rabeqbidv 3425 |
. 2
β’ ((π = π
β§ π = π) β {π β (π RngHom π ) β£ π:ran (1st βπ)β1-1-ontoβran
(1st βπ )}
= {π β (π
RngHom π) β£ π:πβ1-1-ontoβπ}) |
18 | | df-rngoiso 36438 |
. 2
β’ RngIso =
(π β RingOps, π β RingOps β¦ {π β (π RngHom π ) β£ π:ran (1st βπ)β1-1-ontoβran
(1st βπ )}) |
19 | | ovex 7391 |
. . 3
β’ (π
RngHom π) β V |
20 | 19 | rabex 5290 |
. 2
β’ {π β (π
RngHom π) β£ π:πβ1-1-ontoβπ} β V |
21 | 17, 18, 20 | ovmpoa 7511 |
1
β’ ((π
β RingOps β§ π β RingOps) β (π
RngIso π) = {π β (π
RngHom π) β£ π:πβ1-1-ontoβπ}) |