Metamath Proof Explorer


Theorem rhmf1o

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 B=BaseR
rhmf1o.c C=BaseS
Assertion rhmf1o FRRingHomSF:B1-1 ontoCF-1SRingHomR

Proof

Step Hyp Ref Expression
1 rhmf1o.b B=BaseR
2 rhmf1o.c C=BaseS
3 rhmrcl2 FRRingHomSSRing
4 rhmrcl1 FRRingHomSRRing
5 3 4 jca FRRingHomSSRingRRing
6 5 adantr FRRingHomSF:B1-1 ontoCSRingRRing
7 simpr FRRingHomSF:B1-1 ontoCF:B1-1 ontoC
8 rhmghm FRRingHomSFRGrpHomS
9 8 adantr FRRingHomSF:B1-1 ontoCFRGrpHomS
10 1 2 ghmf1o FRGrpHomSF:B1-1 ontoCF-1SGrpHomR
11 10 bicomd FRGrpHomSF-1SGrpHomRF:B1-1 ontoC
12 9 11 syl FRRingHomSF:B1-1 ontoCF-1SGrpHomRF:B1-1 ontoC
13 7 12 mpbird FRRingHomSF:B1-1 ontoCF-1SGrpHomR
14 eqidd FRRingHomSF=F
15 eqid mulGrpR=mulGrpR
16 15 1 mgpbas B=BasemulGrpR
17 16 a1i FRRingHomSB=BasemulGrpR
18 eqid mulGrpS=mulGrpS
19 18 2 mgpbas C=BasemulGrpS
20 19 a1i FRRingHomSC=BasemulGrpS
21 14 17 20 f1oeq123d FRRingHomSF:B1-1 ontoCF:BasemulGrpR1-1 ontoBasemulGrpS
22 21 biimpa FRRingHomSF:B1-1 ontoCF:BasemulGrpR1-1 ontoBasemulGrpS
23 15 18 rhmmhm FRRingHomSFmulGrpRMndHommulGrpS
24 23 adantr FRRingHomSF:B1-1 ontoCFmulGrpRMndHommulGrpS
25 eqid BasemulGrpR=BasemulGrpR
26 eqid BasemulGrpS=BasemulGrpS
27 25 26 mhmf1o FmulGrpRMndHommulGrpSF:BasemulGrpR1-1 ontoBasemulGrpSF-1mulGrpSMndHommulGrpR
28 27 bicomd FmulGrpRMndHommulGrpSF-1mulGrpSMndHommulGrpRF:BasemulGrpR1-1 ontoBasemulGrpS
29 24 28 syl FRRingHomSF:B1-1 ontoCF-1mulGrpSMndHommulGrpRF:BasemulGrpR1-1 ontoBasemulGrpS
30 22 29 mpbird FRRingHomSF:B1-1 ontoCF-1mulGrpSMndHommulGrpR
31 13 30 jca FRRingHomSF:B1-1 ontoCF-1SGrpHomRF-1mulGrpSMndHommulGrpR
32 18 15 isrhm F-1SRingHomRSRingRRingF-1SGrpHomRF-1mulGrpSMndHommulGrpR
33 6 31 32 sylanbrc FRRingHomSF:B1-1 ontoCF-1SRingHomR
34 1 2 rhmf FRRingHomSF:BC
35 34 adantr FRRingHomSF-1SRingHomRF:BC
36 35 ffnd FRRingHomSF-1SRingHomRFFnB
37 2 1 rhmf F-1SRingHomRF-1:CB
38 37 adantl FRRingHomSF-1SRingHomRF-1:CB
39 38 ffnd FRRingHomSF-1SRingHomRF-1FnC
40 dff1o4 F:B1-1 ontoCFFnBF-1FnC
41 36 39 40 sylanbrc FRRingHomSF-1SRingHomRF:B1-1 ontoC
42 33 41 impbida FRRingHomSF:B1-1 ontoCF-1SRingHomR