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

Proof

Step Hyp Ref Expression
1 rhmf1o.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 rhmf1o.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
3 rhmrcl2 ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑆 ∈ Ring )
4 rhmrcl1 ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑅 ∈ Ring )
5 3 4 jca ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝑆 ∈ Ring ∧ 𝑅 ∈ Ring ) )
6 5 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ( 𝑆 ∈ Ring ∧ 𝑅 ∈ Ring ) )
7 simpr ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → 𝐹 : 𝐵 –1-1-onto→ 𝐶 )
8 rhmghm ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
9 8 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
10 1 2 ghmf1o ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ↔ ◡ 𝐹 ∈ ( 𝑆 GrpHom 𝑅 ) ) )
11 10 bicomd ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → ( ◡ 𝐹 ∈ ( 𝑆 GrpHom 𝑅 ) ↔ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) )
12 9 11 syl ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ( ◡ 𝐹 ∈ ( 𝑆 GrpHom 𝑅 ) ↔ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) )
13 7 12 mpbird ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ◡ 𝐹 ∈ ( 𝑆 GrpHom 𝑅 ) )
14 eqidd ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 = 𝐹 )
15 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
16 15 1 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
17 16 a1i ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) ) )
18 eqid ⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
19 18 2 mgpbas ⊢ 𝐶 = ( Base ‘ ( mulGrp ‘ 𝑆 ) )
20 19 a1i ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐶 = ( Base ‘ ( mulGrp ‘ 𝑆 ) ) )
21 14 17 20 f1oeq123d ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ↔ 𝐹 : ( Base ‘ ( mulGrp ‘ 𝑅 ) ) –1-1-onto→ ( Base ‘ ( mulGrp ‘ 𝑆 ) ) ) )
22 21 biimpa ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → 𝐹 : ( Base ‘ ( mulGrp ‘ 𝑅 ) ) –1-1-onto→ ( Base ‘ ( mulGrp ‘ 𝑆 ) ) )
23 15 18 rhmmhm ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) )
24 23 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) )
25 eqid ⊢ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
26 eqid ⊢ ( Base ‘ ( mulGrp ‘ 𝑆 ) ) = ( Base ‘ ( mulGrp ‘ 𝑆 ) )
27 25 26 mhmf1o ⊢ ( 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) → ( 𝐹 : ( Base ‘ ( mulGrp ‘ 𝑅 ) ) –1-1-onto→ ( Base ‘ ( mulGrp ‘ 𝑆 ) ) ↔ ◡ 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑅 ) ) ) )
28 27 bicomd ⊢ ( 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) → ( ◡ 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑅 ) ) ↔ 𝐹 : ( Base ‘ ( mulGrp ‘ 𝑅 ) ) –1-1-onto→ ( Base ‘ ( mulGrp ‘ 𝑆 ) ) ) )
29 24 28 syl ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ( ◡ 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑅 ) ) ↔ 𝐹 : ( Base ‘ ( mulGrp ‘ 𝑅 ) ) –1-1-onto→ ( Base ‘ ( mulGrp ‘ 𝑆 ) ) ) )
30 22 29 mpbird ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ◡ 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑅 ) ) )
31 13 30 jca ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ( ◡ 𝐹 ∈ ( 𝑆 GrpHom 𝑅 ) ∧ ◡ 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑅 ) ) ) )
32 18 15 isrhm ⊢ ( ◡ 𝐹 ∈ ( 𝑆 RingHom 𝑅 ) ↔ ( ( 𝑆 ∈ Ring ∧ 𝑅 ∈ Ring ) ∧ ( ◡ 𝐹 ∈ ( 𝑆 GrpHom 𝑅 ) ∧ ◡ 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑅 ) ) ) ) )
33 6 31 32 sylanbrc ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ◡ 𝐹 ∈ ( 𝑆 RingHom 𝑅 ) )
34 1 2 rhmf ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 : 𝐵 ⟶ 𝐶 )
35 34 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 RingHom 𝑅 ) ) → 𝐹 : 𝐵 ⟶ 𝐶 )
36 35 ffnd ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 RingHom 𝑅 ) ) → 𝐹 Fn 𝐵 )
37 2 1 rhmf ⊢ ( ◡ 𝐹 ∈ ( 𝑆 RingHom 𝑅 ) → ◡ 𝐹 : 𝐶 ⟶ 𝐵 )
38 37 adantl ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 RingHom 𝑅 ) ) → ◡ 𝐹 : 𝐶 ⟶ 𝐵 )
39 38 ffnd ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 RingHom 𝑅 ) ) → ◡ 𝐹 Fn 𝐶 )
40 dff1o4 ⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ↔ ( 𝐹 Fn 𝐵 ∧ ◡ 𝐹 Fn 𝐶 ) )
41 36 39 40 sylanbrc ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 RingHom 𝑅 ) ) → 𝐹 : 𝐵 –1-1-onto→ 𝐶 )
42 33 41 impbida ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ↔ ◡ 𝐹 ∈ ( 𝑆 RingHom 𝑅 ) ) )