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 = ( RingCatALTV ` U )
ringcsectALTV.b 
|- B = ( Base ` C )
ringcsectALTV.u 
|- ( ph -> U e. V )
ringcsectALTV.x 
|- ( ph -> X e. B )
ringcsectALTV.y 
|- ( ph -> Y e. B )
ringcinvALTV.n 
|- N = ( Inv ` C )
Assertion ringcinvALTV 
|- ( ph -> ( F ( X N Y ) G <-> ( F e. ( X RingIso Y ) /\ G = `' F ) ) )

Proof

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