This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ringcinv

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

Ref Expression
Hypotheses ringcsect.c 
|- C = ( RingCat ` U )
ringcsect.b 
|- B = ( Base ` C )
ringcsect.u 
|- ( ph -> U e. V )
ringcsect.x 
|- ( ph -> X e. B )
ringcsect.y 
|- ( ph -> Y e. B )
ringcinv.n 
|- N = ( Inv ` C )
Assertion ringcinv 
|- ( ph -> ( F ( X N Y ) G <-> ( F e. ( X RingIso Y ) /\ G = `' F ) ) )

Proof

Step Hyp Ref Expression
1 ringcsect.c 
 |-  C = ( RingCat ` U )
2 ringcsect.b 
 |-  B = ( Base ` C )
3 ringcsect.u 
 |-  ( ph -> U e. V )
4 ringcsect.x 
 |-  ( ph -> X e. B )
5 ringcsect.y 
 |-  ( ph -> Y e. B )
6 ringcinv.n 
 |-  N = ( Inv ` C )
7 1 ringccat 
 |-  ( 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 ringcsect 
 |-  ( 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 ringcsect 
 |-  ( 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 29 31 33 jca32 
 |-  ( ( ( ( ( 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 ) ) ) ) )
35 34 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 ) ) ) ) )
36 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 ) )
37 eqcom 
 |-  ( `' F = G <-> G = `' F )
38 37 anbi2i 
 |-  ( ( F : ( Base ` X ) -1-1-onto-> ( Base ` Y ) /\ `' F = G ) <-> ( F : ( Base ` X ) -1-1-onto-> ( Base ` Y ) /\ G = `' F ) )
39 36 38 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 ) )
40 35 39 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 ) )
41 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 ) ) )
42 25 40 41 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 ) )
43 11 15 isrim 
 |-  ( F e. ( X RingIso Y ) <-> ( F e. ( X RingHom Y ) /\ F : ( Base ` X ) -1-1-onto-> ( Base ` Y ) ) )
44 43 a1i 
 |-  ( ph -> ( F e. ( X RingIso Y ) <-> ( F e. ( X RingHom Y ) /\ F : ( Base ` X ) -1-1-onto-> ( Base ` Y ) ) ) )
45 44 anbi1d 
 |-  ( ph -> ( ( F e. ( X RingIso Y ) /\ G = `' F ) <-> ( ( F e. ( X RingHom Y ) /\ F : ( Base ` X ) -1-1-onto-> ( Base ` Y ) ) /\ G = `' F ) ) )
46 45 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 ) ) )
47 42 46 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 ) )
48 rimrhm 
 |-  ( F e. ( X RingIso Y ) -> F e. ( X RingHom Y ) )
49 48 ad2antrl 
 |-  ( ( ph /\ ( F e. ( X RingIso Y ) /\ G = `' F ) ) -> F e. ( X RingHom Y ) )
50 isrim0 
 |-  ( F e. ( X RingIso Y ) <-> ( F e. ( X RingHom Y ) /\ `' F e. ( Y RingHom X ) ) )
51 50 simprbi 
 |-  ( F e. ( X RingIso Y ) -> `' F e. ( Y RingHom X ) )
52 eleq1 
 |-  ( G = `' F -> ( G e. ( Y RingHom X ) <-> `' F e. ( Y RingHom X ) ) )
53 51 52 syl5ibrcom 
 |-  ( F e. ( X RingIso Y ) -> ( G = `' F -> G e. ( Y RingHom X ) ) )
54 53 imp 
 |-  ( ( F e. ( X RingIso Y ) /\ G = `' F ) -> G e. ( Y RingHom X ) )
55 54 adantl 
 |-  ( ( ph /\ ( F e. ( X RingIso Y ) /\ G = `' F ) ) -> G e. ( Y RingHom X ) )
56 coeq1 
 |-  ( G = `' F -> ( G o. F ) = ( `' F o. F ) )
57 56 ad2antll 
 |-  ( ( ph /\ ( F e. ( X RingIso Y ) /\ G = `' F ) ) -> ( G o. F ) = ( `' F o. F ) )
58 11 15 rimf1o 
 |-  ( F e. ( X RingIso Y ) -> F : ( Base ` X ) -1-1-onto-> ( Base ` Y ) )
59 58 ad2antrl 
 |-  ( ( ph /\ ( F e. ( X RingIso Y ) /\ G = `' F ) ) -> F : ( Base ` X ) -1-1-onto-> ( Base ` Y ) )
60 f1ococnv1 
 |-  ( F : ( Base ` X ) -1-1-onto-> ( Base ` Y ) -> ( `' F o. F ) = ( _I |` ( Base ` X ) ) )
61 59 60 syl 
 |-  ( ( ph /\ ( F e. ( X RingIso Y ) /\ G = `' F ) ) -> ( `' F o. F ) = ( _I |` ( Base ` X ) ) )
62 57 61 eqtrd 
 |-  ( ( ph /\ ( F e. ( X RingIso Y ) /\ G = `' F ) ) -> ( G o. F ) = ( _I |` ( Base ` X ) ) )
63 49 55 62 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 ) ) ) )
64 50 biimpi 
 |-  ( F e. ( X RingIso Y ) -> ( F e. ( X RingHom Y ) /\ `' F e. ( Y RingHom X ) ) )
65 64 ad2antrl 
 |-  ( ( ph /\ ( F e. ( X RingIso Y ) /\ G = `' F ) ) -> ( F e. ( X RingHom Y ) /\ `' F e. ( Y RingHom X ) ) )
66 52 ad2antll 
 |-  ( ( ph /\ ( F e. ( X RingIso Y ) /\ G = `' F ) ) -> ( G e. ( Y RingHom X ) <-> `' F e. ( Y RingHom X ) ) )
67 66 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 ) ) ) )
68 65 67 mpbird 
 |-  ( ( ph /\ ( F e. ( X RingIso Y ) /\ G = `' F ) ) -> ( F e. ( X RingHom Y ) /\ G e. ( Y RingHom X ) ) )
69 coeq2 
 |-  ( G = `' F -> ( F o. G ) = ( F o. `' F ) )
70 69 ad2antll 
 |-  ( ( ph /\ ( F e. ( X RingIso Y ) /\ G = `' F ) ) -> ( F o. G ) = ( F o. `' F ) )
71 f1ococnv2 
 |-  ( F : ( Base ` X ) -1-1-onto-> ( Base ` Y ) -> ( F o. `' F ) = ( _I |` ( Base ` Y ) ) )
72 59 71 syl 
 |-  ( ( ph /\ ( F e. ( X RingIso Y ) /\ G = `' F ) ) -> ( F o. `' F ) = ( _I |` ( Base ` Y ) ) )
73 70 72 eqtrd 
 |-  ( ( ph /\ ( F e. ( X RingIso Y ) /\ G = `' F ) ) -> ( F o. G ) = ( _I |` ( Base ` Y ) ) )
74 68 62 73 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 ) ) ) )
75 63 68 74 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 ) ) ) ) )
76 47 75 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 ) ) )
77 10 23 76 3bitrd 
 |-  ( ph -> ( F ( X N Y ) G <-> ( F e. ( X RingIso Y ) /\ G = `' F ) ) )