Metamath Proof Explorer

Theorem rnghmf1o

Description: A non-unital ring homomorphism is bijective iff its converse is also a non-unital ring homomorphism. (Contributed by AV, 27-Feb-2020)

Ref Expression
Hypotheses rnghmf1o.b 
|- B = ( Base ` R )
rnghmf1o.c 
|- C = ( Base ` S )
Assertion rnghmf1o 
|- ( F e. ( R RngHomo S ) -> ( F : B -1-1-onto-> C <-> `' F e. ( S RngHomo R ) ) )

Proof

Step Hyp Ref Expression
1 rnghmf1o.b 
 |-  B = ( Base ` R )
2 rnghmf1o.c 
 |-  C = ( Base ` S )
3 rnghmrcl 
 |-  ( F e. ( R RngHomo S ) -> ( R e. Rng /\ S e. Rng ) )
4 3 ancomd 
 |-  ( F e. ( R RngHomo S ) -> ( S e. Rng /\ R e. Rng ) )
5 4 adantr 
 |-  ( ( F e. ( R RngHomo S ) /\ F : B -1-1-onto-> C ) -> ( S e. Rng /\ R e. Rng ) )
6 simpr 
 |-  ( ( F e. ( R RngHomo S ) /\ F : B -1-1-onto-> C ) -> F : B -1-1-onto-> C )
7 rnghmghm 
 |-  ( F e. ( R RngHomo S ) -> F e. ( R GrpHom S ) )
8 7 adantr 
 |-  ( ( F e. ( R RngHomo S ) /\ F : B -1-1-onto-> C ) -> F e. ( R GrpHom S ) )
9 1 2 ghmf1o 
 |-  ( F e. ( R GrpHom S ) -> ( F : B -1-1-onto-> C <-> `' F e. ( S GrpHom R ) ) )
10 9 bicomd 
 |-  ( F e. ( R GrpHom S ) -> ( `' F e. ( S GrpHom R ) <-> F : B -1-1-onto-> C ) )
11 8 10 syl 
 |-  ( ( F e. ( R RngHomo S ) /\ F : B -1-1-onto-> C ) -> ( `' F e. ( S GrpHom R ) <-> F : B -1-1-onto-> C ) )
12 6 11 mpbird 
 |-  ( ( F e. ( R RngHomo S ) /\ F : B -1-1-onto-> C ) -> `' F e. ( S GrpHom R ) )
13 eqidd 
 |-  ( F e. ( R RngHomo S ) -> F = F )
14 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
15 14 1 mgpbas 
 |-  B = ( Base ` ( mulGrp ` R ) )
16 15 a1i 
 |-  ( F e. ( R RngHomo S ) -> B = ( Base ` ( mulGrp ` R ) ) )
17 eqid 
 |-  ( mulGrp ` S ) = ( mulGrp ` S )
18 17 2 mgpbas 
 |-  C = ( Base ` ( mulGrp ` S ) )
19 18 a1i 
 |-  ( F e. ( R RngHomo S ) -> C = ( Base ` ( mulGrp ` S ) ) )
20 13 16 19 f1oeq123d 
 |-  ( F e. ( R RngHomo S ) -> ( F : B -1-1-onto-> C <-> F : ( Base ` ( mulGrp ` R ) ) -1-1-onto-> ( Base ` ( mulGrp ` S ) ) ) )
21 20 biimpa 
 |-  ( ( F e. ( R RngHomo S ) /\ F : B -1-1-onto-> C ) -> F : ( Base ` ( mulGrp ` R ) ) -1-1-onto-> ( Base ` ( mulGrp ` S ) ) )
22 14 17 rnghmmgmhm 
 |-  ( F e. ( R RngHomo S ) -> F e. ( ( mulGrp ` R ) MgmHom ( mulGrp ` S ) ) )
23 22 adantr 
 |-  ( ( F e. ( R RngHomo S ) /\ F : B -1-1-onto-> C ) -> F e. ( ( mulGrp ` R ) MgmHom ( mulGrp ` S ) ) )
24 eqid 
 |-  ( Base ` ( mulGrp ` R ) ) = ( Base ` ( mulGrp ` R ) )
25 eqid 
 |-  ( Base ` ( mulGrp ` S ) ) = ( Base ` ( mulGrp ` S ) )
26 24 25 mgmhmf1o 
 |-  ( F e. ( ( mulGrp ` R ) MgmHom ( mulGrp ` S ) ) -> ( F : ( Base ` ( mulGrp ` R ) ) -1-1-onto-> ( Base ` ( mulGrp ` S ) ) <-> `' F e. ( ( mulGrp ` S ) MgmHom ( mulGrp ` R ) ) ) )
27 26 bicomd 
 |-  ( F e. ( ( mulGrp ` R ) MgmHom ( mulGrp ` S ) ) -> ( `' F e. ( ( mulGrp ` S ) MgmHom ( mulGrp ` R ) ) <-> F : ( Base ` ( mulGrp ` R ) ) -1-1-onto-> ( Base ` ( mulGrp ` S ) ) ) )
28 23 27 syl 
 |-  ( ( F e. ( R RngHomo S ) /\ F : B -1-1-onto-> C ) -> ( `' F e. ( ( mulGrp ` S ) MgmHom ( mulGrp ` R ) ) <-> F : ( Base ` ( mulGrp ` R ) ) -1-1-onto-> ( Base ` ( mulGrp ` S ) ) ) )
29 21 28 mpbird 
 |-  ( ( F e. ( R RngHomo S ) /\ F : B -1-1-onto-> C ) -> `' F e. ( ( mulGrp ` S ) MgmHom ( mulGrp ` R ) ) )
30 12 29 jca 
 |-  ( ( F e. ( R RngHomo S ) /\ F : B -1-1-onto-> C ) -> ( `' F e. ( S GrpHom R ) /\ `' F e. ( ( mulGrp ` S ) MgmHom ( mulGrp ` R ) ) ) )
31 17 14 isrnghmmul 
 |-  ( `' F e. ( S RngHomo R ) <-> ( ( S e. Rng /\ R e. Rng ) /\ ( `' F e. ( S GrpHom R ) /\ `' F e. ( ( mulGrp ` S ) MgmHom ( mulGrp ` R ) ) ) ) )
32 5 30 31 sylanbrc 
 |-  ( ( F e. ( R RngHomo S ) /\ F : B -1-1-onto-> C ) -> `' F e. ( S RngHomo R ) )
33 1 2 rnghmf 
 |-  ( F e. ( R RngHomo S ) -> F : B --> C )
34 33 adantr 
 |-  ( ( F e. ( R RngHomo S ) /\ `' F e. ( S RngHomo R ) ) -> F : B --> C )
35 34 ffnd 
 |-  ( ( F e. ( R RngHomo S ) /\ `' F e. ( S RngHomo R ) ) -> F Fn B )
36 2 1 rnghmf 
 |-  ( `' F e. ( S RngHomo R ) -> `' F : C --> B )
37 36 adantl 
 |-  ( ( F e. ( R RngHomo S ) /\ `' F e. ( S RngHomo R ) ) -> `' F : C --> B )
38 37 ffnd 
 |-  ( ( F e. ( R RngHomo S ) /\ `' F e. ( S RngHomo R ) ) -> `' F Fn C )
39 dff1o4 
 |-  ( F : B -1-1-onto-> C <-> ( F Fn B /\ `' F Fn C ) )
40 35 38 39 sylanbrc 
 |-  ( ( F e. ( R RngHomo S ) /\ `' F e. ( S RngHomo R ) ) -> F : B -1-1-onto-> C )
41 32 40 impbida 
 |-  ( F e. ( R RngHomo S ) -> ( F : B -1-1-onto-> C <-> `' F e. ( S RngHomo R ) ) )