Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . 4
β’ ((πΉ β (π
RingHom π) β§ π΄ β (Unitβπ
)) β πΉ β (π
RingHom π)) |
2 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ
) =
(Baseβπ
) |
3 | | eqid 2733 |
. . . . . 6
β’
(Unitβπ
) =
(Unitβπ
) |
4 | 2, 3 | unitss 20097 |
. . . . 5
β’
(Unitβπ
)
β (Baseβπ
) |
5 | | simpr 486 |
. . . . 5
β’ ((πΉ β (π
RingHom π) β§ π΄ β (Unitβπ
)) β π΄ β (Unitβπ
)) |
6 | 4, 5 | sselid 3946 |
. . . 4
β’ ((πΉ β (π
RingHom π) β§ π΄ β (Unitβπ
)) β π΄ β (Baseβπ
)) |
7 | | rhmrcl1 20160 |
. . . . 5
β’ (πΉ β (π
RingHom π) β π
β Ring) |
8 | | eqid 2733 |
. . . . . 6
β’
(1rβπ
) = (1rβπ
) |
9 | 2, 8 | ringidcl 19997 |
. . . . 5
β’ (π
β Ring β
(1rβπ
)
β (Baseβπ
)) |
10 | 1, 7, 9 | 3syl 18 |
. . . 4
β’ ((πΉ β (π
RingHom π) β§ π΄ β (Unitβπ
)) β (1rβπ
) β (Baseβπ
)) |
11 | | eqid 2733 |
. . . . . . 7
β’
(β₯rβπ
) = (β₯rβπ
) |
12 | | eqid 2733 |
. . . . . . 7
β’
(opprβπ
) = (opprβπ
) |
13 | | eqid 2733 |
. . . . . . 7
β’
(β₯rβ(opprβπ
)) =
(β₯rβ(opprβπ
)) |
14 | 3, 8, 11, 12, 13 | isunit 20094 |
. . . . . 6
β’ (π΄ β (Unitβπ
) β (π΄(β₯rβπ
)(1rβπ
) β§ π΄(β₯rβ(opprβπ
))(1rβπ
))) |
15 | 5, 14 | sylib 217 |
. . . . 5
β’ ((πΉ β (π
RingHom π) β§ π΄ β (Unitβπ
)) β (π΄(β₯rβπ
)(1rβπ
) β§ π΄(β₯rβ(opprβπ
))(1rβπ
))) |
16 | 15 | simpld 496 |
. . . 4
β’ ((πΉ β (π
RingHom π) β§ π΄ β (Unitβπ
)) β π΄(β₯rβπ
)(1rβπ
)) |
17 | | eqid 2733 |
. . . . 5
β’
(β₯rβπ) = (β₯rβπ) |
18 | 2, 11, 17 | rhmdvdsr 20191 |
. . . 4
β’ (((πΉ β (π
RingHom π) β§ π΄ β (Baseβπ
) β§ (1rβπ
) β (Baseβπ
)) β§ π΄(β₯rβπ
)(1rβπ
)) β (πΉβπ΄)(β₯rβπ)(πΉβ(1rβπ
))) |
19 | 1, 6, 10, 16, 18 | syl31anc 1374 |
. . 3
β’ ((πΉ β (π
RingHom π) β§ π΄ β (Unitβπ
)) β (πΉβπ΄)(β₯rβπ)(πΉβ(1rβπ
))) |
20 | | eqid 2733 |
. . . . . 6
β’
(1rβπ) = (1rβπ) |
21 | 8, 20 | rhm1 20172 |
. . . . 5
β’ (πΉ β (π
RingHom π) β (πΉβ(1rβπ
)) = (1rβπ)) |
22 | 21 | breq2d 5121 |
. . . 4
β’ (πΉ β (π
RingHom π) β ((πΉβπ΄)(β₯rβπ)(πΉβ(1rβπ
)) β (πΉβπ΄)(β₯rβπ)(1rβπ))) |
23 | 22 | adantr 482 |
. . 3
β’ ((πΉ β (π
RingHom π) β§ π΄ β (Unitβπ
)) β ((πΉβπ΄)(β₯rβπ)(πΉβ(1rβπ
)) β (πΉβπ΄)(β₯rβπ)(1rβπ))) |
24 | 19, 23 | mpbid 231 |
. 2
β’ ((πΉ β (π
RingHom π) β§ π΄ β (Unitβπ
)) β (πΉβπ΄)(β₯rβπ)(1rβπ)) |
25 | | rhmopp 20192 |
. . . . 5
β’ (πΉ β (π
RingHom π) β πΉ β ((opprβπ
) RingHom
(opprβπ))) |
26 | 25 | adantr 482 |
. . . 4
β’ ((πΉ β (π
RingHom π) β§ π΄ β (Unitβπ
)) β πΉ β ((opprβπ
) RingHom
(opprβπ))) |
27 | 15 | simprd 497 |
. . . 4
β’ ((πΉ β (π
RingHom π) β§ π΄ β (Unitβπ
)) β π΄(β₯rβ(opprβπ
))(1rβπ
)) |
28 | 12, 2 | opprbas 20064 |
. . . . 5
β’
(Baseβπ
) =
(Baseβ(opprβπ
)) |
29 | | eqid 2733 |
. . . . 5
β’
(β₯rβ(opprβπ)) =
(β₯rβ(opprβπ)) |
30 | 28, 13, 29 | rhmdvdsr 20191 |
. . . 4
β’ (((πΉ β
((opprβπ
) RingHom
(opprβπ)) β§ π΄ β (Baseβπ
) β§ (1rβπ
) β (Baseβπ
)) β§ π΄(β₯rβ(opprβπ
))(1rβπ
)) β (πΉβπ΄)(β₯rβ(opprβπ))(πΉβ(1rβπ
))) |
31 | 26, 6, 10, 27, 30 | syl31anc 1374 |
. . 3
β’ ((πΉ β (π
RingHom π) β§ π΄ β (Unitβπ
)) β (πΉβπ΄)(β₯rβ(opprβπ))(πΉβ(1rβπ
))) |
32 | 21 | breq2d 5121 |
. . . 4
β’ (πΉ β (π
RingHom π) β ((πΉβπ΄)(β₯rβ(opprβπ))(πΉβ(1rβπ
)) β (πΉβπ΄)(β₯rβ(opprβπ))(1rβπ))) |
33 | 32 | adantr 482 |
. . 3
β’ ((πΉ β (π
RingHom π) β§ π΄ β (Unitβπ
)) β ((πΉβπ΄)(β₯rβ(opprβπ))(πΉβ(1rβπ
)) β (πΉβπ΄)(β₯rβ(opprβπ))(1rβπ))) |
34 | 31, 33 | mpbid 231 |
. 2
β’ ((πΉ β (π
RingHom π) β§ π΄ β (Unitβπ
)) β (πΉβπ΄)(β₯rβ(opprβπ))(1rβπ)) |
35 | | eqid 2733 |
. . 3
β’
(Unitβπ) =
(Unitβπ) |
36 | | eqid 2733 |
. . 3
β’
(opprβπ) = (opprβπ) |
37 | 35, 20, 17, 36, 29 | isunit 20094 |
. 2
β’ ((πΉβπ΄) β (Unitβπ) β ((πΉβπ΄)(β₯rβπ)(1rβπ) β§ (πΉβπ΄)(β₯rβ(opprβπ))(1rβπ))) |
38 | 24, 34, 37 | sylanbrc 584 |
1
β’ ((πΉ β (π
RingHom π) β§ π΄ β (Unitβπ
)) β (πΉβπ΄) β (Unitβπ)) |