Description: A ring homomorphism is bijective iff its converse is also a ring homomorphism. (Contributed by AV, 22-Oct-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rhmf1o.b | |
|
rhmf1o.c | |
||
Assertion | rhmf1o | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rhmf1o.b | |
|
2 | rhmf1o.c | |
|
3 | rhmrcl2 | |
|
4 | rhmrcl1 | |
|
5 | 3 4 | jca | |
6 | 5 | adantr | |
7 | simpr | |
|
8 | rhmghm | |
|
9 | 8 | adantr | |
10 | 1 2 | ghmf1o | |
11 | 10 | bicomd | |
12 | 9 11 | syl | |
13 | 7 12 | mpbird | |
14 | eqidd | |
|
15 | eqid | |
|
16 | 15 1 | mgpbas | |
17 | 16 | a1i | |
18 | eqid | |
|
19 | 18 2 | mgpbas | |
20 | 19 | a1i | |
21 | 14 17 20 | f1oeq123d | |
22 | 21 | biimpa | |
23 | 15 18 | rhmmhm | |
24 | 23 | adantr | |
25 | eqid | |
|
26 | eqid | |
|
27 | 25 26 | mhmf1o | |
28 | 27 | bicomd | |
29 | 24 28 | syl | |
30 | 22 29 | mpbird | |
31 | 13 30 | jca | |
32 | 18 15 | isrhm | |
33 | 6 31 32 | sylanbrc | |
34 | 1 2 | rhmf | |
35 | 34 | adantr | |
36 | 35 | ffnd | |
37 | 2 1 | rhmf | |
38 | 37 | adantl | |
39 | 38 | ffnd | |
40 | dff1o4 | |
|
41 | 36 39 40 | sylanbrc | |
42 | 33 41 | impbida | |