Step | Hyp | Ref
| Expression |
1 | | rngoisohom 36442 |
. . . . . 6
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngIso π)) β πΉ β (π
RngHom π)) |
2 | 1 | 3expa 1119 |
. . . . 5
β’ (((π
β RingOps β§ π β RingOps) β§ πΉ β (π
RngIso π)) β πΉ β (π
RngHom π)) |
3 | 2 | 3adantl3 1169 |
. . . 4
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ πΉ β (π
RngIso π)) β πΉ β (π
RngHom π)) |
4 | | rngoisohom 36442 |
. . . . . 6
β’ ((π β RingOps β§ π β RingOps β§ πΊ β (π RngIso π)) β πΊ β (π RngHom π)) |
5 | 4 | 3expa 1119 |
. . . . 5
β’ (((π β RingOps β§ π β RingOps) β§ πΊ β (π RngIso π)) β πΊ β (π RngHom π)) |
6 | 5 | 3adantl1 1167 |
. . . 4
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ πΊ β (π RngIso π)) β πΊ β (π RngHom π)) |
7 | 3, 6 | anim12dan 620 |
. . 3
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngIso π) β§ πΊ β (π RngIso π))) β (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) |
8 | | rngohomco 36436 |
. . 3
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β (πΊ β πΉ) β (π
RngHom π)) |
9 | 7, 8 | syldan 592 |
. 2
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngIso π) β§ πΊ β (π RngIso π))) β (πΊ β πΉ) β (π
RngHom π)) |
10 | | eqid 2737 |
. . . . . . 7
β’
(1st βπ) = (1st βπ) |
11 | | eqid 2737 |
. . . . . . 7
β’ ran
(1st βπ) =
ran (1st βπ) |
12 | | eqid 2737 |
. . . . . . 7
β’
(1st βπ) = (1st βπ) |
13 | | eqid 2737 |
. . . . . . 7
β’ ran
(1st βπ) =
ran (1st βπ) |
14 | 10, 11, 12, 13 | rngoiso1o 36441 |
. . . . . 6
β’ ((π β RingOps β§ π β RingOps β§ πΊ β (π RngIso π)) β πΊ:ran (1st βπ)β1-1-ontoβran
(1st βπ)) |
15 | 14 | 3expa 1119 |
. . . . 5
β’ (((π β RingOps β§ π β RingOps) β§ πΊ β (π RngIso π)) β πΊ:ran (1st βπ)β1-1-ontoβran
(1st βπ)) |
16 | 15 | 3adantl1 1167 |
. . . 4
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ πΊ β (π RngIso π)) β πΊ:ran (1st βπ)β1-1-ontoβran
(1st βπ)) |
17 | 16 | adantrl 715 |
. . 3
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngIso π) β§ πΊ β (π RngIso π))) β πΊ:ran (1st βπ)β1-1-ontoβran
(1st βπ)) |
18 | | eqid 2737 |
. . . . . . 7
β’
(1st βπ
) = (1st βπ
) |
19 | | eqid 2737 |
. . . . . . 7
β’ ran
(1st βπ
) =
ran (1st βπ
) |
20 | 18, 19, 10, 11 | rngoiso1o 36441 |
. . . . . 6
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngIso π)) β πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)) |
21 | 20 | 3expa 1119 |
. . . . 5
β’ (((π
β RingOps β§ π β RingOps) β§ πΉ β (π
RngIso π)) β πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)) |
22 | 21 | 3adantl3 1169 |
. . . 4
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ πΉ β (π
RngIso π)) β πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)) |
23 | 22 | adantrr 716 |
. . 3
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngIso π) β§ πΊ β (π RngIso π))) β πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)) |
24 | | f1oco 6808 |
. . 3
β’ ((πΊ:ran (1st
βπ)β1-1-ontoβran (1st βπ) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ))
β (πΊ β πΉ):ran (1st
βπ
)β1-1-ontoβran (1st βπ)) |
25 | 17, 23, 24 | syl2anc 585 |
. 2
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngIso π) β§ πΊ β (π RngIso π))) β (πΊ β πΉ):ran (1st βπ
)β1-1-ontoβran
(1st βπ)) |
26 | 18, 19, 12, 13 | isrngoiso 36440 |
. . . 4
β’ ((π
β RingOps β§ π β RingOps) β ((πΊ β πΉ) β (π
RngIso π) β ((πΊ β πΉ) β (π
RngHom π) β§ (πΊ β πΉ):ran (1st βπ
)β1-1-ontoβran
(1st βπ)))) |
27 | 26 | 3adant2 1132 |
. . 3
β’ ((π
β RingOps β§ π β RingOps β§ π β RingOps) β ((πΊ β πΉ) β (π
RngIso π) β ((πΊ β πΉ) β (π
RngHom π) β§ (πΊ β πΉ):ran (1st βπ
)β1-1-ontoβran
(1st βπ)))) |
28 | 27 | adantr 482 |
. 2
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngIso π) β§ πΊ β (π RngIso π))) β ((πΊ β πΉ) β (π
RngIso π) β ((πΊ β πΉ) β (π
RngHom π) β§ (πΊ β πΉ):ran (1st βπ
)β1-1-ontoβran
(1st βπ)))) |
29 | 9, 25, 28 | mpbir2and 712 |
1
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngIso π) β§ πΊ β (π RngIso π))) β (πΊ β πΉ) β (π
RngIso π)) |