Metamath Proof Explorer


Theorem isrim0

Description: A ring isomorphism is a homomorphism whose converse is also a homomorphism. Compare isgim2 . (Contributed by AV, 22-Oct-2019) Remove sethood antecedent. (Revised by SN, 10-Jan-2025)

Ref Expression
Assertion isrim0 ( 𝐹 ∈ ( 𝑅 RingIso 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 ∈ ( 𝑆 RingHom 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 rimrcl ( 𝐹 ∈ ( 𝑅 RingIso 𝑆 ) → ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) )
2 rhmrcl1 ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑅 ∈ Ring )
3 2 elexd ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑅 ∈ V )
4 rhmrcl2 ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑆 ∈ Ring )
5 4 elexd ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑆 ∈ V )
6 3 5 jca ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) )
7 6 adantr ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 ∈ ( 𝑆 RingHom 𝑅 ) ) → ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) )
8 df-rngiso RingIso = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ { 𝑓 ∈ ( 𝑟 RingHom 𝑠 ) ∣ 𝑓 ∈ ( 𝑠 RingHom 𝑟 ) } )
9 8 a1i ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) → RingIso = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ { 𝑓 ∈ ( 𝑟 RingHom 𝑠 ) ∣ 𝑓 ∈ ( 𝑠 RingHom 𝑟 ) } ) )
10 oveq12 ( ( 𝑟 = 𝑅𝑠 = 𝑆 ) → ( 𝑟 RingHom 𝑠 ) = ( 𝑅 RingHom 𝑆 ) )
11 10 adantl ( ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) ∧ ( 𝑟 = 𝑅𝑠 = 𝑆 ) ) → ( 𝑟 RingHom 𝑠 ) = ( 𝑅 RingHom 𝑆 ) )
12 oveq12 ( ( 𝑠 = 𝑆𝑟 = 𝑅 ) → ( 𝑠 RingHom 𝑟 ) = ( 𝑆 RingHom 𝑅 ) )
13 12 ancoms ( ( 𝑟 = 𝑅𝑠 = 𝑆 ) → ( 𝑠 RingHom 𝑟 ) = ( 𝑆 RingHom 𝑅 ) )
14 13 adantl ( ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) ∧ ( 𝑟 = 𝑅𝑠 = 𝑆 ) ) → ( 𝑠 RingHom 𝑟 ) = ( 𝑆 RingHom 𝑅 ) )
15 14 eleq2d ( ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) ∧ ( 𝑟 = 𝑅𝑠 = 𝑆 ) ) → ( 𝑓 ∈ ( 𝑠 RingHom 𝑟 ) ↔ 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) ) )
16 11 15 rabeqbidv ( ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) ∧ ( 𝑟 = 𝑅𝑠 = 𝑆 ) ) → { 𝑓 ∈ ( 𝑟 RingHom 𝑠 ) ∣ 𝑓 ∈ ( 𝑠 RingHom 𝑟 ) } = { 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) ∣ 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) } )
17 simpl ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) → 𝑅 ∈ V )
18 simpr ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) → 𝑆 ∈ V )
19 ovex ( 𝑅 RingHom 𝑆 ) ∈ V
20 19 rabex { 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) ∣ 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) } ∈ V
21 20 a1i ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) → { 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) ∣ 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) } ∈ V )
22 9 16 17 18 21 ovmpod ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) → ( 𝑅 RingIso 𝑆 ) = { 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) ∣ 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) } )
23 22 eleq2d ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) → ( 𝐹 ∈ ( 𝑅 RingIso 𝑆 ) ↔ 𝐹 ∈ { 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) ∣ 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) } ) )
24 cnveq ( 𝑓 = 𝐹 𝑓 = 𝐹 )
25 24 eleq1d ( 𝑓 = 𝐹 → ( 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) ↔ 𝐹 ∈ ( 𝑆 RingHom 𝑅 ) ) )
26 25 elrab ( 𝐹 ∈ { 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) ∣ 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) } ↔ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 ∈ ( 𝑆 RingHom 𝑅 ) ) )
27 23 26 bitrdi ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) → ( 𝐹 ∈ ( 𝑅 RingIso 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 ∈ ( 𝑆 RingHom 𝑅 ) ) ) )
28 1 7 27 pm5.21nii ( 𝐹 ∈ ( 𝑅 RingIso 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 ∈ ( 𝑆 RingHom 𝑅 ) ) )