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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
rnghmf1o.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
Assertion rnghmf1o ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) → ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ↔ ◡ 𝐹 ∈ ( 𝑆 RngHomo 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 rnghmf1o.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 rnghmf1o.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
3 rnghmrcl ⊢ ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) → ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) )
4 3 ancomd ⊢ ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) → ( 𝑆 ∈ Rng ∧ 𝑅 ∈ Rng ) )
5 4 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ( 𝑆 ∈ Rng ∧ 𝑅 ∈ Rng ) )
6 simpr ⊢ ( ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → 𝐹 : 𝐵 –1-1-onto→ 𝐶 )
7 rnghmghm ⊢ ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
8 7 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
9 1 2 ghmf1o ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ↔ ◡ 𝐹 ∈ ( 𝑆 GrpHom 𝑅 ) ) )
10 9 bicomd ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → ( ◡ 𝐹 ∈ ( 𝑆 GrpHom 𝑅 ) ↔ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) )
11 8 10 syl ⊢ ( ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ( ◡ 𝐹 ∈ ( 𝑆 GrpHom 𝑅 ) ↔ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) )
12 6 11 mpbird ⊢ ( ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ◡ 𝐹 ∈ ( 𝑆 GrpHom 𝑅 ) )
13 eqidd ⊢ ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) → 𝐹 = 𝐹 )
14 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
15 14 1 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
16 15 a1i ⊢ ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) → 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) ) )
17 eqid ⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
18 17 2 mgpbas ⊢ 𝐶 = ( Base ‘ ( mulGrp ‘ 𝑆 ) )
19 18 a1i ⊢ ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) → 𝐶 = ( Base ‘ ( mulGrp ‘ 𝑆 ) ) )
20 13 16 19 f1oeq123d ⊢ ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) → ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ↔ 𝐹 : ( Base ‘ ( mulGrp ‘ 𝑅 ) ) –1-1-onto→ ( Base ‘ ( mulGrp ‘ 𝑆 ) ) ) )
21 20 biimpa ⊢ ( ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → 𝐹 : ( Base ‘ ( mulGrp ‘ 𝑅 ) ) –1-1-onto→ ( Base ‘ ( mulGrp ‘ 𝑆 ) ) )
22 14 17 rnghmmgmhm ⊢ ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) → 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MgmHom ( mulGrp ‘ 𝑆 ) ) )
23 22 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MgmHom ( mulGrp ‘ 𝑆 ) ) )
24 eqid ⊢ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
25 eqid ⊢ ( Base ‘ ( mulGrp ‘ 𝑆 ) ) = ( Base ‘ ( mulGrp ‘ 𝑆 ) )
26 24 25 mgmhmf1o ⊢ ( 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MgmHom ( mulGrp ‘ 𝑆 ) ) → ( 𝐹 : ( Base ‘ ( mulGrp ‘ 𝑅 ) ) –1-1-onto→ ( Base ‘ ( mulGrp ‘ 𝑆 ) ) ↔ ◡ 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MgmHom ( mulGrp ‘ 𝑅 ) ) ) )
27 26 bicomd ⊢ ( 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MgmHom ( mulGrp ‘ 𝑆 ) ) → ( ◡ 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MgmHom ( mulGrp ‘ 𝑅 ) ) ↔ 𝐹 : ( Base ‘ ( mulGrp ‘ 𝑅 ) ) –1-1-onto→ ( Base ‘ ( mulGrp ‘ 𝑆 ) ) ) )
28 23 27 syl ⊢ ( ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ( ◡ 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MgmHom ( mulGrp ‘ 𝑅 ) ) ↔ 𝐹 : ( Base ‘ ( mulGrp ‘ 𝑅 ) ) –1-1-onto→ ( Base ‘ ( mulGrp ‘ 𝑆 ) ) ) )
29 21 28 mpbird ⊢ ( ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ◡ 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MgmHom ( mulGrp ‘ 𝑅 ) ) )
30 12 29 jca ⊢ ( ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ( ◡ 𝐹 ∈ ( 𝑆 GrpHom 𝑅 ) ∧ ◡ 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MgmHom ( mulGrp ‘ 𝑅 ) ) ) )
31 17 14 isrnghmmul ⊢ ( ◡ 𝐹 ∈ ( 𝑆 RngHomo 𝑅 ) ↔ ( ( 𝑆 ∈ Rng ∧ 𝑅 ∈ Rng ) ∧ ( ◡ 𝐹 ∈ ( 𝑆 GrpHom 𝑅 ) ∧ ◡ 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MgmHom ( mulGrp ‘ 𝑅 ) ) ) ) )
32 5 30 31 sylanbrc ⊢ ( ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ◡ 𝐹 ∈ ( 𝑆 RngHomo 𝑅 ) )
33 1 2 rnghmf ⊢ ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) → 𝐹 : 𝐵 ⟶ 𝐶 )
34 33 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 RngHomo 𝑅 ) ) → 𝐹 : 𝐵 ⟶ 𝐶 )
35 34 ffnd ⊢ ( ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 RngHomo 𝑅 ) ) → 𝐹 Fn 𝐵 )
36 2 1 rnghmf ⊢ ( ◡ 𝐹 ∈ ( 𝑆 RngHomo 𝑅 ) → ◡ 𝐹 : 𝐶 ⟶ 𝐵 )
37 36 adantl ⊢ ( ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 RngHomo 𝑅 ) ) → ◡ 𝐹 : 𝐶 ⟶ 𝐵 )
38 37 ffnd ⊢ ( ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 RngHomo 𝑅 ) ) → ◡ 𝐹 Fn 𝐶 )
39 dff1o4 ⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ↔ ( 𝐹 Fn 𝐵 ∧ ◡ 𝐹 Fn 𝐶 ) )
40 35 38 39 sylanbrc ⊢ ( ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 RngHomo 𝑅 ) ) → 𝐹 : 𝐵 –1-1-onto→ 𝐶 )
41 32 40 impbida ⊢ ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) → ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ↔ ◡ 𝐹 ∈ ( 𝑆 RngHomo 𝑅 ) ) )