# Metamath Proof Explorer

## Theorem ringcinvALTV

Description: An inverse in the category of rings is the converse operation. (Contributed by AV, 14-Feb-2020) (New usage is discouraged.)

Ref Expression
Hypotheses ringcsectALTV.c ${⊢}{C}=\mathrm{RingCatALTV}\left({U}\right)$
ringcsectALTV.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
ringcsectALTV.u ${⊢}{\phi }\to {U}\in {V}$
ringcsectALTV.x ${⊢}{\phi }\to {X}\in {B}$
ringcsectALTV.y ${⊢}{\phi }\to {Y}\in {B}$
ringcinvALTV.n ${⊢}{N}=\mathrm{Inv}\left({C}\right)$
Assertion ringcinvALTV ${⊢}{\phi }\to \left({F}\left({X}{N}{Y}\right){G}↔\left({F}\in \left({X}\mathrm{RingIso}{Y}\right)\wedge {G}={{F}}^{-1}\right)\right)$

### Proof

Step Hyp Ref Expression
1 ringcsectALTV.c ${⊢}{C}=\mathrm{RingCatALTV}\left({U}\right)$
2 ringcsectALTV.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
3 ringcsectALTV.u ${⊢}{\phi }\to {U}\in {V}$
4 ringcsectALTV.x ${⊢}{\phi }\to {X}\in {B}$
5 ringcsectALTV.y ${⊢}{\phi }\to {Y}\in {B}$
6 ringcinvALTV.n ${⊢}{N}=\mathrm{Inv}\left({C}\right)$
7 1 ringccatALTV ${⊢}{U}\in {V}\to {C}\in \mathrm{Cat}$
8 3 7 syl ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
9 eqid ${⊢}\mathrm{Sect}\left({C}\right)=\mathrm{Sect}\left({C}\right)$
10 2 6 8 4 5 9 isinv ${⊢}{\phi }\to \left({F}\left({X}{N}{Y}\right){G}↔\left({F}\left({X}\mathrm{Sect}\left({C}\right){Y}\right){G}\wedge {G}\left({Y}\mathrm{Sect}\left({C}\right){X}\right){F}\right)\right)$
11 eqid ${⊢}{\mathrm{Base}}_{{X}}={\mathrm{Base}}_{{X}}$
12 1 2 3 4 5 11 9 ringcsectALTV ${⊢}{\phi }\to \left({F}\left({X}\mathrm{Sect}\left({C}\right){Y}\right){G}↔\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\right)$
13 df-3an ${⊢}\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)↔\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)$
14 12 13 syl6bb ${⊢}{\phi }\to \left({F}\left({X}\mathrm{Sect}\left({C}\right){Y}\right){G}↔\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\right)$
15 eqid ${⊢}{\mathrm{Base}}_{{Y}}={\mathrm{Base}}_{{Y}}$
16 1 2 3 5 4 15 9 ringcsectALTV ${⊢}{\phi }\to \left({G}\left({Y}\mathrm{Sect}\left({C}\right){X}\right){F}↔\left({G}\in \left({Y}\mathrm{RingHom}{X}\right)\wedge {F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\right)\right)$
17 3ancoma ${⊢}\left({G}\in \left({Y}\mathrm{RingHom}{X}\right)\wedge {F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\right)↔\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\wedge {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\right)$
18 df-3an ${⊢}\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\wedge {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\right)↔\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\right)$
19 17 18 bitri ${⊢}\left({G}\in \left({Y}\mathrm{RingHom}{X}\right)\wedge {F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\right)↔\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\right)$
20 16 19 syl6bb ${⊢}{\phi }\to \left({G}\left({Y}\mathrm{Sect}\left({C}\right){X}\right){F}↔\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\right)\right)$
21 14 20 anbi12d ${⊢}{\phi }\to \left(\left({F}\left({X}\mathrm{Sect}\left({C}\right){Y}\right){G}\wedge {G}\left({Y}\mathrm{Sect}\left({C}\right){X}\right){F}\right)↔\left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge \left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\right)\right)\right)$
22 anandi ${⊢}\left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge \left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\right)\right)↔\left(\left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge \left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\right)\wedge \left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\right)\right)$
23 21 22 syl6bb ${⊢}{\phi }\to \left(\left({F}\left({X}\mathrm{Sect}\left({C}\right){Y}\right){G}\wedge {G}\left({Y}\mathrm{Sect}\left({C}\right){X}\right){F}\right)↔\left(\left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge \left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\right)\wedge \left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\right)\right)\right)$
24 simplrl ${⊢}\left(\left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge \left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\right)\wedge \left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\right)\right)\to {F}\in \left({X}\mathrm{RingHom}{Y}\right)$
25 24 adantl ${⊢}\left({\phi }\wedge \left(\left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge \left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\right)\wedge \left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to {F}\in \left({X}\mathrm{RingHom}{Y}\right)$
26 11 15 rhmf ${⊢}{F}\in \left({X}\mathrm{RingHom}{Y}\right)\to {F}:{\mathrm{Base}}_{{X}}⟶{\mathrm{Base}}_{{Y}}$
27 15 11 rhmf ${⊢}{G}\in \left({Y}\mathrm{RingHom}{X}\right)\to {G}:{\mathrm{Base}}_{{Y}}⟶{\mathrm{Base}}_{{X}}$
28 26 27 anim12i ${⊢}\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\to \left({F}:{\mathrm{Base}}_{{X}}⟶{\mathrm{Base}}_{{Y}}\wedge {G}:{\mathrm{Base}}_{{Y}}⟶{\mathrm{Base}}_{{X}}\right)$
29 28 ad2antlr ${⊢}\left(\left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge \left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\right)\wedge \left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\right)\right)\to \left({F}:{\mathrm{Base}}_{{X}}⟶{\mathrm{Base}}_{{Y}}\wedge {G}:{\mathrm{Base}}_{{Y}}⟶{\mathrm{Base}}_{{X}}\right)$
30 simpr ${⊢}\left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\right)\to {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}$
31 30 adantl ${⊢}\left(\left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge \left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\right)\wedge \left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\right)\right)\to {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}$
32 simpr ${⊢}\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\to {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}$
33 32 ad2antrl ${⊢}\left(\left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge \left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\right)\wedge \left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\right)\right)\to {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}$
34 31 33 jca ${⊢}\left(\left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge \left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\right)\wedge \left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\right)\right)\to \left({F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)$
35 29 34 jca ${⊢}\left(\left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge \left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\right)\wedge \left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\right)\right)\to \left(\left({F}:{\mathrm{Base}}_{{X}}⟶{\mathrm{Base}}_{{Y}}\wedge {G}:{\mathrm{Base}}_{{Y}}⟶{\mathrm{Base}}_{{X}}\right)\wedge \left({F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\right)$
36 35 adantl ${⊢}\left({\phi }\wedge \left(\left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge \left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\right)\wedge \left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to \left(\left({F}:{\mathrm{Base}}_{{X}}⟶{\mathrm{Base}}_{{Y}}\wedge {G}:{\mathrm{Base}}_{{Y}}⟶{\mathrm{Base}}_{{X}}\right)\wedge \left({F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\right)$
37 fcof1o ${⊢}\left(\left({F}:{\mathrm{Base}}_{{X}}⟶{\mathrm{Base}}_{{Y}}\wedge {G}:{\mathrm{Base}}_{{Y}}⟶{\mathrm{Base}}_{{X}}\right)\wedge \left({F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\right)\to \left({F}:{\mathrm{Base}}_{{X}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{Y}}\wedge {{F}}^{-1}={G}\right)$
38 eqcom ${⊢}{{F}}^{-1}={G}↔{G}={{F}}^{-1}$
39 38 anbi2i ${⊢}\left({F}:{\mathrm{Base}}_{{X}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{Y}}\wedge {{F}}^{-1}={G}\right)↔\left({F}:{\mathrm{Base}}_{{X}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{Y}}\wedge {G}={{F}}^{-1}\right)$
40 37 39 sylib ${⊢}\left(\left({F}:{\mathrm{Base}}_{{X}}⟶{\mathrm{Base}}_{{Y}}\wedge {G}:{\mathrm{Base}}_{{Y}}⟶{\mathrm{Base}}_{{X}}\right)\wedge \left({F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\right)\to \left({F}:{\mathrm{Base}}_{{X}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{Y}}\wedge {G}={{F}}^{-1}\right)$
41 36 40 syl ${⊢}\left({\phi }\wedge \left(\left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge \left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\right)\wedge \left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to \left({F}:{\mathrm{Base}}_{{X}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{Y}}\wedge {G}={{F}}^{-1}\right)$
42 anass ${⊢}\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {F}:{\mathrm{Base}}_{{X}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{Y}}\right)\wedge {G}={{F}}^{-1}\right)↔\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge \left({F}:{\mathrm{Base}}_{{X}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{Y}}\wedge {G}={{F}}^{-1}\right)\right)$
43 25 41 42 sylanbrc ${⊢}\left({\phi }\wedge \left(\left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge \left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\right)\wedge \left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to \left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {F}:{\mathrm{Base}}_{{X}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{Y}}\right)\wedge {G}={{F}}^{-1}\right)$
44 4 5 jca ${⊢}{\phi }\to \left({X}\in {B}\wedge {Y}\in {B}\right)$
45 11 15 isrim ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to \left({F}\in \left({X}\mathrm{RingIso}{Y}\right)↔\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {F}:{\mathrm{Base}}_{{X}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{Y}}\right)\right)$
46 44 45 syl ${⊢}{\phi }\to \left({F}\in \left({X}\mathrm{RingIso}{Y}\right)↔\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {F}:{\mathrm{Base}}_{{X}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{Y}}\right)\right)$
47 46 anbi1d ${⊢}{\phi }\to \left(\left({F}\in \left({X}\mathrm{RingIso}{Y}\right)\wedge {G}={{F}}^{-1}\right)↔\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {F}:{\mathrm{Base}}_{{X}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{Y}}\right)\wedge {G}={{F}}^{-1}\right)\right)$
48 47 adantr ${⊢}\left({\phi }\wedge \left(\left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge \left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\right)\wedge \left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to \left(\left({F}\in \left({X}\mathrm{RingIso}{Y}\right)\wedge {G}={{F}}^{-1}\right)↔\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {F}:{\mathrm{Base}}_{{X}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{Y}}\right)\wedge {G}={{F}}^{-1}\right)\right)$
49 43 48 mpbird ${⊢}\left({\phi }\wedge \left(\left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge \left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\right)\wedge \left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\right)\right)\right)\to \left({F}\in \left({X}\mathrm{RingIso}{Y}\right)\wedge {G}={{F}}^{-1}\right)$
50 11 15 rimrhm ${⊢}{F}\in \left({X}\mathrm{RingIso}{Y}\right)\to {F}\in \left({X}\mathrm{RingHom}{Y}\right)$
51 50 ad2antrl ${⊢}\left({\phi }\wedge \left({F}\in \left({X}\mathrm{RingIso}{Y}\right)\wedge {G}={{F}}^{-1}\right)\right)\to {F}\in \left({X}\mathrm{RingHom}{Y}\right)$
52 isrim0 ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to \left({F}\in \left({X}\mathrm{RingIso}{Y}\right)↔\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {{F}}^{-1}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\right)$
53 44 52 syl ${⊢}{\phi }\to \left({F}\in \left({X}\mathrm{RingIso}{Y}\right)↔\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {{F}}^{-1}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\right)$
54 eleq1 ${⊢}{{F}}^{-1}={G}\to \left({{F}}^{-1}\in \left({Y}\mathrm{RingHom}{X}\right)↔{G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)$
55 54 eqcoms ${⊢}{G}={{F}}^{-1}\to \left({{F}}^{-1}\in \left({Y}\mathrm{RingHom}{X}\right)↔{G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)$
56 55 anbi2d ${⊢}{G}={{F}}^{-1}\to \left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {{F}}^{-1}\in \left({Y}\mathrm{RingHom}{X}\right)\right)↔\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\right)$
57 53 56 sylan9bbr ${⊢}\left({G}={{F}}^{-1}\wedge {\phi }\right)\to \left({F}\in \left({X}\mathrm{RingIso}{Y}\right)↔\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\right)$
58 simpr ${⊢}\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\to {G}\in \left({Y}\mathrm{RingHom}{X}\right)$
59 57 58 syl6bi ${⊢}\left({G}={{F}}^{-1}\wedge {\phi }\right)\to \left({F}\in \left({X}\mathrm{RingIso}{Y}\right)\to {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)$
60 59 com12 ${⊢}{F}\in \left({X}\mathrm{RingIso}{Y}\right)\to \left(\left({G}={{F}}^{-1}\wedge {\phi }\right)\to {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)$
61 60 expdimp ${⊢}\left({F}\in \left({X}\mathrm{RingIso}{Y}\right)\wedge {G}={{F}}^{-1}\right)\to \left({\phi }\to {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)$
62 61 impcom ${⊢}\left({\phi }\wedge \left({F}\in \left({X}\mathrm{RingIso}{Y}\right)\wedge {G}={{F}}^{-1}\right)\right)\to {G}\in \left({Y}\mathrm{RingHom}{X}\right)$
63 coeq1 ${⊢}{G}={{F}}^{-1}\to {G}\circ {F}={{F}}^{-1}\circ {F}$
64 63 ad2antll ${⊢}\left({\phi }\wedge \left({F}\in \left({X}\mathrm{RingIso}{Y}\right)\wedge {G}={{F}}^{-1}\right)\right)\to {G}\circ {F}={{F}}^{-1}\circ {F}$
65 11 15 rimf1o ${⊢}{F}\in \left({X}\mathrm{RingIso}{Y}\right)\to {F}:{\mathrm{Base}}_{{X}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{Y}}$
66 65 ad2antrl ${⊢}\left({\phi }\wedge \left({F}\in \left({X}\mathrm{RingIso}{Y}\right)\wedge {G}={{F}}^{-1}\right)\right)\to {F}:{\mathrm{Base}}_{{X}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{Y}}$
67 f1ococnv1 ${⊢}{F}:{\mathrm{Base}}_{{X}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{Y}}\to {{F}}^{-1}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}$
68 66 67 syl ${⊢}\left({\phi }\wedge \left({F}\in \left({X}\mathrm{RingIso}{Y}\right)\wedge {G}={{F}}^{-1}\right)\right)\to {{F}}^{-1}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}$
69 64 68 eqtrd ${⊢}\left({\phi }\wedge \left({F}\in \left({X}\mathrm{RingIso}{Y}\right)\wedge {G}={{F}}^{-1}\right)\right)\to {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}$
70 51 62 69 jca31 ${⊢}\left({\phi }\wedge \left({F}\in \left({X}\mathrm{RingIso}{Y}\right)\wedge {G}={{F}}^{-1}\right)\right)\to \left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)$
71 53 biimpcd ${⊢}{F}\in \left({X}\mathrm{RingIso}{Y}\right)\to \left({\phi }\to \left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {{F}}^{-1}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\right)$
72 71 adantr ${⊢}\left({F}\in \left({X}\mathrm{RingIso}{Y}\right)\wedge {G}={{F}}^{-1}\right)\to \left({\phi }\to \left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {{F}}^{-1}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\right)$
73 72 impcom ${⊢}\left({\phi }\wedge \left({F}\in \left({X}\mathrm{RingIso}{Y}\right)\wedge {G}={{F}}^{-1}\right)\right)\to \left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {{F}}^{-1}\in \left({Y}\mathrm{RingHom}{X}\right)\right)$
74 eleq1 ${⊢}{G}={{F}}^{-1}\to \left({G}\in \left({Y}\mathrm{RingHom}{X}\right)↔{{F}}^{-1}\in \left({Y}\mathrm{RingHom}{X}\right)\right)$
75 74 ad2antll ${⊢}\left({\phi }\wedge \left({F}\in \left({X}\mathrm{RingIso}{Y}\right)\wedge {G}={{F}}^{-1}\right)\right)\to \left({G}\in \left({Y}\mathrm{RingHom}{X}\right)↔{{F}}^{-1}\in \left({Y}\mathrm{RingHom}{X}\right)\right)$
76 75 anbi2d ${⊢}\left({\phi }\wedge \left({F}\in \left({X}\mathrm{RingIso}{Y}\right)\wedge {G}={{F}}^{-1}\right)\right)\to \left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)↔\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {{F}}^{-1}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\right)$
77 73 76 mpbird ${⊢}\left({\phi }\wedge \left({F}\in \left({X}\mathrm{RingIso}{Y}\right)\wedge {G}={{F}}^{-1}\right)\right)\to \left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)$
78 coeq2 ${⊢}{G}={{F}}^{-1}\to {F}\circ {G}={F}\circ {{F}}^{-1}$
79 78 ad2antll ${⊢}\left({\phi }\wedge \left({F}\in \left({X}\mathrm{RingIso}{Y}\right)\wedge {G}={{F}}^{-1}\right)\right)\to {F}\circ {G}={F}\circ {{F}}^{-1}$
80 f1ococnv2 ${⊢}{F}:{\mathrm{Base}}_{{X}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{Y}}\to {F}\circ {{F}}^{-1}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}$
81 66 80 syl ${⊢}\left({\phi }\wedge \left({F}\in \left({X}\mathrm{RingIso}{Y}\right)\wedge {G}={{F}}^{-1}\right)\right)\to {F}\circ {{F}}^{-1}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}$
82 79 81 eqtrd ${⊢}\left({\phi }\wedge \left({F}\in \left({X}\mathrm{RingIso}{Y}\right)\wedge {G}={{F}}^{-1}\right)\right)\to {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}$
83 77 69 82 jca31 ${⊢}\left({\phi }\wedge \left({F}\in \left({X}\mathrm{RingIso}{Y}\right)\wedge {G}={{F}}^{-1}\right)\right)\to \left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\right)$
84 70 77 83 jca31 ${⊢}\left({\phi }\wedge \left({F}\in \left({X}\mathrm{RingIso}{Y}\right)\wedge {G}={{F}}^{-1}\right)\right)\to \left(\left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge \left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\right)\wedge \left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\right)\right)$
85 49 84 impbida ${⊢}{\phi }\to \left(\left(\left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge \left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\right)\wedge \left(\left(\left({F}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {G}\in \left({Y}\mathrm{RingHom}{X}\right)\right)\wedge {G}\circ {F}={\mathrm{I}↾}_{{\mathrm{Base}}_{{X}}}\right)\wedge {F}\circ {G}={\mathrm{I}↾}_{{\mathrm{Base}}_{{Y}}}\right)\right)↔\left({F}\in \left({X}\mathrm{RingIso}{Y}\right)\wedge {G}={{F}}^{-1}\right)\right)$
86 10 23 85 3bitrd ${⊢}{\phi }\to \left({F}\left({X}{N}{Y}\right){G}↔\left({F}\in \left({X}\mathrm{RingIso}{Y}\right)\wedge {G}={{F}}^{-1}\right)\right)$