Metamath Proof Explorer


Theorem isrim0

Description: An isomorphism of rings is a homomorphism whose converse is also a homomorphism . (Contributed by AV, 22-Oct-2019)

Ref Expression
Assertion isrim0 R V S W F R RingIso S F R RingHom S F -1 S RingHom R

Proof

Step Hyp Ref Expression
1 df-rngiso RingIso = r V , s V f r RingHom s | f -1 s RingHom r
2 1 a1i R V S W RingIso = r V , s V f r RingHom s | f -1 s RingHom r
3 oveq12 r = R s = S r RingHom s = R RingHom S
4 3 adantl R V S W r = R s = S r RingHom s = R RingHom S
5 oveq12 s = S r = R s RingHom r = S RingHom R
6 5 ancoms r = R s = S s RingHom r = S RingHom R
7 6 adantl R V S W r = R s = S s RingHom r = S RingHom R
8 7 eleq2d R V S W r = R s = S f -1 s RingHom r f -1 S RingHom R
9 4 8 rabeqbidv R V S W r = R s = S f r RingHom s | f -1 s RingHom r = f R RingHom S | f -1 S RingHom R
10 elex R V R V
11 10 adantr R V S W R V
12 elex S W S V
13 12 adantl R V S W S V
14 ovex R RingHom S V
15 14 rabex f R RingHom S | f -1 S RingHom R V
16 15 a1i R V S W f R RingHom S | f -1 S RingHom R V
17 2 9 11 13 16 ovmpod R V S W R RingIso S = f R RingHom S | f -1 S RingHom R
18 17 eleq2d R V S W F R RingIso S F f R RingHom S | f -1 S RingHom R
19 cnveq f = F f -1 = F -1
20 19 eleq1d f = F f -1 S RingHom R F -1 S RingHom R
21 20 elrab F f R RingHom S | f -1 S RingHom R F R RingHom S F -1 S RingHom R
22 18 21 bitrdi R V S W F R RingIso S F R RingHom S F -1 S RingHom R