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-rim ⊢ 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 𝑅 ) ) )