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 ∈ R RngHomo S → F : B ⟶ 1-1 onto C ↔ F -1 ∈ S RngHomo R

Proof

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