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 = ( Base ` R )
rhmf1o.c 
|- C = ( Base ` S )
Assertion rhmf1o 
|- ( F e. ( R RingHom S ) -> ( F : B -1-1-onto-> C <-> `' F e. ( S RingHom R ) ) )

Proof

Step Hyp Ref Expression
1 rhmf1o.b 
 |-  B = ( Base ` R )
2 rhmf1o.c 
 |-  C = ( Base ` S )
3 rhmrcl2 
 |-  ( F e. ( R RingHom S ) -> S e. Ring )
4 rhmrcl1 
 |-  ( F e. ( R RingHom S ) -> R e. Ring )
5 3 4 jca 
 |-  ( F e. ( R RingHom S ) -> ( S e. Ring /\ R e. Ring ) )
6 5 adantr 
 |-  ( ( F e. ( R RingHom S ) /\ F : B -1-1-onto-> C ) -> ( S e. Ring /\ R e. Ring ) )
7 simpr 
 |-  ( ( F e. ( R RingHom S ) /\ F : B -1-1-onto-> C ) -> F : B -1-1-onto-> C )
8 rhmghm 
 |-  ( F e. ( R RingHom S ) -> F e. ( R GrpHom S ) )
9 8 adantr 
 |-  ( ( F e. ( R RingHom S ) /\ F : B -1-1-onto-> C ) -> F e. ( R GrpHom S ) )
10 1 2 ghmf1o 
 |-  ( F e. ( R GrpHom S ) -> ( F : B -1-1-onto-> C <-> `' F e. ( S GrpHom R ) ) )
11 10 bicomd 
 |-  ( F e. ( R GrpHom S ) -> ( `' F e. ( S GrpHom R ) <-> F : B -1-1-onto-> C ) )
12 9 11 syl 
 |-  ( ( F e. ( R RingHom S ) /\ F : B -1-1-onto-> C ) -> ( `' F e. ( S GrpHom R ) <-> F : B -1-1-onto-> C ) )
13 7 12 mpbird 
 |-  ( ( F e. ( R RingHom S ) /\ F : B -1-1-onto-> C ) -> `' F e. ( S GrpHom R ) )
14 eqidd 
 |-  ( F e. ( R RingHom S ) -> F = F )
15 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
16 15 1 mgpbas 
 |-  B = ( Base ` ( mulGrp ` R ) )
17 16 a1i 
 |-  ( F e. ( R RingHom S ) -> B = ( Base ` ( mulGrp ` R ) ) )
18 eqid 
 |-  ( mulGrp ` S ) = ( mulGrp ` S )
19 18 2 mgpbas 
 |-  C = ( Base ` ( mulGrp ` S ) )
20 19 a1i 
 |-  ( F e. ( R RingHom S ) -> C = ( Base ` ( mulGrp ` S ) ) )
21 14 17 20 f1oeq123d 
 |-  ( F e. ( R RingHom S ) -> ( F : B -1-1-onto-> C <-> F : ( Base ` ( mulGrp ` R ) ) -1-1-onto-> ( Base ` ( mulGrp ` S ) ) ) )
22 21 biimpa 
 |-  ( ( F e. ( R RingHom S ) /\ F : B -1-1-onto-> C ) -> F : ( Base ` ( mulGrp ` R ) ) -1-1-onto-> ( Base ` ( mulGrp ` S ) ) )
23 15 18 rhmmhm 
 |-  ( F e. ( R RingHom S ) -> F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) )
24 23 adantr 
 |-  ( ( F e. ( R RingHom S ) /\ F : B -1-1-onto-> C ) -> F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) )
25 eqid 
 |-  ( Base ` ( mulGrp ` R ) ) = ( Base ` ( mulGrp ` R ) )
26 eqid 
 |-  ( Base ` ( mulGrp ` S ) ) = ( Base ` ( mulGrp ` S ) )
27 25 26 mhmf1o 
 |-  ( F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) -> ( F : ( Base ` ( mulGrp ` R ) ) -1-1-onto-> ( Base ` ( mulGrp ` S ) ) <-> `' F e. ( ( mulGrp ` S ) MndHom ( mulGrp ` R ) ) ) )
28 27 bicomd 
 |-  ( F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) -> ( `' F e. ( ( mulGrp ` S ) MndHom ( mulGrp ` R ) ) <-> F : ( Base ` ( mulGrp ` R ) ) -1-1-onto-> ( Base ` ( mulGrp ` S ) ) ) )
29 24 28 syl 
 |-  ( ( F e. ( R RingHom S ) /\ F : B -1-1-onto-> C ) -> ( `' F e. ( ( mulGrp ` S ) MndHom ( mulGrp ` R ) ) <-> F : ( Base ` ( mulGrp ` R ) ) -1-1-onto-> ( Base ` ( mulGrp ` S ) ) ) )
30 22 29 mpbird 
 |-  ( ( F e. ( R RingHom S ) /\ F : B -1-1-onto-> C ) -> `' F e. ( ( mulGrp ` S ) MndHom ( mulGrp ` R ) ) )
31 13 30 jca 
 |-  ( ( F e. ( R RingHom S ) /\ F : B -1-1-onto-> C ) -> ( `' F e. ( S GrpHom R ) /\ `' F e. ( ( mulGrp ` S ) MndHom ( mulGrp ` R ) ) ) )
32 18 15 isrhm 
 |-  ( `' F e. ( S RingHom R ) <-> ( ( S e. Ring /\ R e. Ring ) /\ ( `' F e. ( S GrpHom R ) /\ `' F e. ( ( mulGrp ` S ) MndHom ( mulGrp ` R ) ) ) ) )
33 6 31 32 sylanbrc 
 |-  ( ( F e. ( R RingHom S ) /\ F : B -1-1-onto-> C ) -> `' F e. ( S RingHom R ) )
34 1 2 rhmf 
 |-  ( F e. ( R RingHom S ) -> F : B --> C )
35 34 adantr 
 |-  ( ( F e. ( R RingHom S ) /\ `' F e. ( S RingHom R ) ) -> F : B --> C )
36 35 ffnd 
 |-  ( ( F e. ( R RingHom S ) /\ `' F e. ( S RingHom R ) ) -> F Fn B )
37 2 1 rhmf 
 |-  ( `' F e. ( S RingHom R ) -> `' F : C --> B )
38 37 adantl 
 |-  ( ( F e. ( R RingHom S ) /\ `' F e. ( S RingHom R ) ) -> `' F : C --> B )
39 38 ffnd 
 |-  ( ( F e. ( R RingHom S ) /\ `' F e. ( S RingHom R ) ) -> `' F Fn C )
40 dff1o4 
 |-  ( F : B -1-1-onto-> C <-> ( F Fn B /\ `' F Fn C ) )
41 36 39 40 sylanbrc 
 |-  ( ( F e. ( R RingHom S ) /\ `' F e. ( S RingHom R ) ) -> F : B -1-1-onto-> C )
42 33 41 impbida 
 |-  ( F e. ( R RingHom S ) -> ( F : B -1-1-onto-> C <-> `' F e. ( S RingHom R ) ) )