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 F R RingIso S F R RingHom S F -1 S RingHom R

Proof

Step Hyp Ref Expression
1 rimrcl F R RingIso S R V S V
2 rhmrcl1 F R RingHom S R Ring
3 2 elexd F R RingHom S R V
4 rhmrcl2 F R RingHom S S Ring
5 4 elexd F R RingHom S S V
6 3 5 jca F R RingHom S R V S V
7 6 adantr F R RingHom S F -1 S RingHom R R V S V
8 df-rngiso RingIso = r V , s V f r RingHom s | f -1 s RingHom r
9 8 a1i R V S V RingIso = r V , s V f r RingHom s | f -1 s RingHom r
10 oveq12 r = R s = S r RingHom s = R RingHom S
11 10 adantl R V S V r = R s = S r RingHom s = R RingHom S
12 oveq12 s = S r = R s RingHom r = S RingHom R
13 12 ancoms r = R s = S s RingHom r = S RingHom R
14 13 adantl R V S V r = R s = S s RingHom r = S RingHom R
15 14 eleq2d R V S V r = R s = S f -1 s RingHom r f -1 S RingHom R
16 11 15 rabeqbidv R V S V r = R s = S f r RingHom s | f -1 s RingHom r = f R RingHom S | f -1 S RingHom R
17 simpl R V S V R V
18 simpr R V S V S V
19 ovex R RingHom S V
20 19 rabex f R RingHom S | f -1 S RingHom R V
21 20 a1i R V S V f R RingHom S | f -1 S RingHom R V
22 9 16 17 18 21 ovmpod R V S V R RingIso S = f R RingHom S | f -1 S RingHom R
23 22 eleq2d R V S V F R RingIso S F f R RingHom S | f -1 S RingHom R
24 cnveq f = F f -1 = F -1
25 24 eleq1d f = F f -1 S RingHom R F -1 S RingHom R
26 25 elrab F f R RingHom S | f -1 S RingHom R F R RingHom S F -1 S RingHom R
27 23 26 bitrdi R V S V F R RingIso S F R RingHom S F -1 S RingHom R
28 1 7 27 pm5.21nii F R RingIso S F R RingHom S F -1 S RingHom R