Metamath Proof Explorer


Theorem ringciso

Description: An isomorphism in the category of unital rings is a bijection. (Contributed by AV, 14-Feb-2020)

Ref Expression
Hypotheses ringcsect.c C = RingCat U
ringcsect.b B = Base C
ringcsect.u φ U V
ringcsect.x φ X B
ringcsect.y φ Y B
ringciso.n I = Iso C
Assertion ringciso φ F X I Y F X RingIso Y

Proof

Step Hyp Ref Expression
1 ringcsect.c C = RingCat U
2 ringcsect.b B = Base C
3 ringcsect.u φ U V
4 ringcsect.x φ X B
5 ringcsect.y φ Y B
6 ringciso.n I = Iso C
7 eqid Inv C = Inv C
8 1 ringccat U V C Cat
9 3 8 syl φ C Cat
10 2 7 9 4 5 6 isoval φ X I Y = dom X Inv C Y
11 10 eleq2d φ F X I Y F dom X Inv C Y
12 2 7 9 4 5 invfun φ Fun X Inv C Y
13 funfvbrb Fun X Inv C Y F dom X Inv C Y F X Inv C Y X Inv C Y F
14 12 13 syl φ F dom X Inv C Y F X Inv C Y X Inv C Y F
15 1 2 3 4 5 7 ringcinv φ F X Inv C Y X Inv C Y F F X RingIso Y X Inv C Y F = F -1
16 simpl F X RingIso Y X Inv C Y F = F -1 F X RingIso Y
17 15 16 syl6bi φ F X Inv C Y X Inv C Y F F X RingIso Y
18 14 17 sylbid φ F dom X Inv C Y F X RingIso Y
19 eqid F -1 = F -1
20 1 2 3 4 5 7 ringcinv φ F X Inv C Y F -1 F X RingIso Y F -1 = F -1
21 funrel Fun X Inv C Y Rel X Inv C Y
22 12 21 syl φ Rel X Inv C Y
23 releldm Rel X Inv C Y F X Inv C Y F -1 F dom X Inv C Y
24 23 ex Rel X Inv C Y F X Inv C Y F -1 F dom X Inv C Y
25 22 24 syl φ F X Inv C Y F -1 F dom X Inv C Y
26 20 25 sylbird φ F X RingIso Y F -1 = F -1 F dom X Inv C Y
27 19 26 mpan2i φ F X RingIso Y F dom X Inv C Y
28 18 27 impbid φ F dom X Inv C Y F X RingIso Y
29 11 28 bitrd φ F X I Y F X RingIso Y