Metamath Proof Explorer

Theorem rngcinv

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

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

Proof

Step Hyp Ref Expression
1 rngcsect.c 
 |-  C = ( RngCat ` U )
2 rngcsect.b 
 |-  B = ( Base ` C )
3 rngcsect.u 
 |-  ( ph -> U e. V )
4 rngcsect.x 
 |-  ( ph -> X e. B )
5 rngcsect.y 
 |-  ( ph -> Y e. B )
6 rngcinv.n 
 |-  N = ( Inv ` C )
7 1 rngccat 
 |-  ( 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 rngcsect 
 |-  ( ph -> ( F ( X ( Sect ` C ) Y ) G <-> ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) ) )
13 df-3an 
 |-  ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) <-> ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) )
14 12 13 bitrdi 
 |-  ( ph -> ( F ( X ( Sect ` C ) Y ) G <-> ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) ) )
15 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
16 1 2 3 5 4 15 9 rngcsect 
 |-  ( ph -> ( G ( Y ( Sect ` C ) X ) F <-> ( G e. ( Y RngHomo X ) /\ F e. ( X RngHomo Y ) /\ ( F o. G ) = ( _I |` ( Base ` Y ) ) ) ) )
17 3ancoma 
 |-  ( ( G e. ( Y RngHomo X ) /\ F e. ( X RngHomo Y ) /\ ( F o. G ) = ( _I |` ( Base ` Y ) ) ) <-> ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) /\ ( F o. G ) = ( _I |` ( Base ` Y ) ) ) )
18 df-3an 
 |-  ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) /\ ( F o. G ) = ( _I |` ( Base ` Y ) ) ) <-> ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( F o. G ) = ( _I |` ( Base ` Y ) ) ) )
19 17 18 bitri 
 |-  ( ( G e. ( Y RngHomo X ) /\ F e. ( X RngHomo Y ) /\ ( F o. G ) = ( _I |` ( Base ` Y ) ) ) <-> ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( F o. G ) = ( _I |` ( Base ` Y ) ) ) )
20 16 19 bitrdi 
 |-  ( ph -> ( G ( Y ( Sect ` C ) X ) F <-> ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo 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 RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) /\ ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( F o. G ) = ( _I |` ( Base ` Y ) ) ) ) ) )
22 anandi 
 |-  ( ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) /\ ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( F o. G ) = ( _I |` ( Base ` Y ) ) ) ) <-> ( ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) /\ ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo 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 RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) /\ ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) /\ ( F o. G ) = ( _I |` ( Base ` Y ) ) ) ) ) )
24 simplrl 
 |-  ( ( ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) /\ ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) /\ ( F o. G ) = ( _I |` ( Base ` Y ) ) ) ) -> F e. ( X RngHomo Y ) )
25 24 adantl 
 |-  ( ( ph /\ ( ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) /\ ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) /\ ( F o. G ) = ( _I |` ( Base ` Y ) ) ) ) ) -> F e. ( X RngHomo Y ) )
26 11 15 rnghmf 
 |-  ( F e. ( X RngHomo Y ) -> F : ( Base ` X ) --> ( Base ` Y ) )
27 15 11 rnghmf 
 |-  ( G e. ( Y RngHomo X ) -> G : ( Base ` Y ) --> ( Base ` X ) )
28 26 27 anim12i 
 |-  ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) -> ( F : ( Base ` X ) --> ( Base ` Y ) /\ G : ( Base ` Y ) --> ( Base ` X ) ) )
29 28 ad2antlr 
 |-  ( ( ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) /\ ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo 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 RngHomo Y ) /\ G e. ( Y RngHomo 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 RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) /\ ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) /\ ( F o. G ) = ( _I |` ( Base ` Y ) ) ) ) -> ( F o. G ) = ( _I |` ( Base ` Y ) ) )
32 simpr 
 |-  ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) -> ( G o. F ) = ( _I |` ( Base ` X ) ) )
33 32 ad2antrl 
 |-  ( ( ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) /\ ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo 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 RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) /\ ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo 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 RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) /\ ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo 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 RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) /\ ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo 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 RngHomo Y ) /\ F : ( Base ` X ) -1-1-onto-> ( Base ` Y ) ) /\ G = `' F ) <-> ( F e. ( X RngHomo Y ) /\ ( F : ( Base ` X ) -1-1-onto-> ( Base ` Y ) /\ G = `' F ) ) )
42 25 40 41 sylanbrc 
 |-  ( ( ph /\ ( ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) /\ ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) /\ ( F o. G ) = ( _I |` ( Base ` Y ) ) ) ) ) -> ( ( F e. ( X RngHomo Y ) /\ F : ( Base ` X ) -1-1-onto-> ( Base ` Y ) ) /\ G = `' F ) )
43 11 15 isrngim 
 |-  ( ( X e. B /\ Y e. B ) -> ( F e. ( X RngIsom Y ) <-> ( F e. ( X RngHomo Y ) /\ F : ( Base ` X ) -1-1-onto-> ( Base ` Y ) ) ) )
44 4 5 43 syl2anc 
 |-  ( ph -> ( F e. ( X RngIsom Y ) <-> ( F e. ( X RngHomo Y ) /\ F : ( Base ` X ) -1-1-onto-> ( Base ` Y ) ) ) )
45 44 anbi1d 
 |-  ( ph -> ( ( F e. ( X RngIsom Y ) /\ G = `' F ) <-> ( ( F e. ( X RngHomo Y ) /\ F : ( Base ` X ) -1-1-onto-> ( Base ` Y ) ) /\ G = `' F ) ) )
46 45 adantr 
 |-  ( ( ph /\ ( ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) /\ ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) /\ ( F o. G ) = ( _I |` ( Base ` Y ) ) ) ) ) -> ( ( F e. ( X RngIsom Y ) /\ G = `' F ) <-> ( ( F e. ( X RngHomo Y ) /\ F : ( Base ` X ) -1-1-onto-> ( Base ` Y ) ) /\ G = `' F ) ) )
47 42 46 mpbird 
 |-  ( ( ph /\ ( ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) /\ ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) /\ ( F o. G ) = ( _I |` ( Base ` Y ) ) ) ) ) -> ( F e. ( X RngIsom Y ) /\ G = `' F ) )
48 11 15 rngimrnghm 
 |-  ( F e. ( X RngIsom Y ) -> F e. ( X RngHomo Y ) )
49 48 ad2antrl 
 |-  ( ( ph /\ ( F e. ( X RngIsom Y ) /\ G = `' F ) ) -> F e. ( X RngHomo Y ) )
50 isrngisom 
 |-  ( ( X e. B /\ Y e. B ) -> ( F e. ( X RngIsom Y ) <-> ( F e. ( X RngHomo Y ) /\ `' F e. ( Y RngHomo X ) ) ) )
51 4 5 50 syl2anc 
 |-  ( ph -> ( F e. ( X RngIsom Y ) <-> ( F e. ( X RngHomo Y ) /\ `' F e. ( Y RngHomo X ) ) ) )
52 eleq1 
 |-  ( `' F = G -> ( `' F e. ( Y RngHomo X ) <-> G e. ( Y RngHomo X ) ) )
53 52 eqcoms 
 |-  ( G = `' F -> ( `' F e. ( Y RngHomo X ) <-> G e. ( Y RngHomo X ) ) )
54 53 anbi2d 
 |-  ( G = `' F -> ( ( F e. ( X RngHomo Y ) /\ `' F e. ( Y RngHomo X ) ) <-> ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) )
55 51 54 sylan9bbr 
 |-  ( ( G = `' F /\ ph ) -> ( F e. ( X RngIsom Y ) <-> ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) )
56 simpr 
 |-  ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) -> G e. ( Y RngHomo X ) )
57 55 56 syl6bi 
 |-  ( ( G = `' F /\ ph ) -> ( F e. ( X RngIsom Y ) -> G e. ( Y RngHomo X ) ) )
58 57 com12 
 |-  ( F e. ( X RngIsom Y ) -> ( ( G = `' F /\ ph ) -> G e. ( Y RngHomo X ) ) )
59 58 expdimp 
 |-  ( ( F e. ( X RngIsom Y ) /\ G = `' F ) -> ( ph -> G e. ( Y RngHomo X ) ) )
60 59 impcom 
 |-  ( ( ph /\ ( F e. ( X RngIsom Y ) /\ G = `' F ) ) -> G e. ( Y RngHomo X ) )
61 coeq1 
 |-  ( G = `' F -> ( G o. F ) = ( `' F o. F ) )
62 61 ad2antll 
 |-  ( ( ph /\ ( F e. ( X RngIsom Y ) /\ G = `' F ) ) -> ( G o. F ) = ( `' F o. F ) )
63 11 15 rngimf1o 
 |-  ( F e. ( X RngIsom Y ) -> F : ( Base ` X ) -1-1-onto-> ( Base ` Y ) )
64 63 ad2antrl 
 |-  ( ( ph /\ ( F e. ( X RngIsom Y ) /\ G = `' F ) ) -> F : ( Base ` X ) -1-1-onto-> ( Base ` Y ) )
65 f1ococnv1 
 |-  ( F : ( Base ` X ) -1-1-onto-> ( Base ` Y ) -> ( `' F o. F ) = ( _I |` ( Base ` X ) ) )
66 64 65 syl 
 |-  ( ( ph /\ ( F e. ( X RngIsom Y ) /\ G = `' F ) ) -> ( `' F o. F ) = ( _I |` ( Base ` X ) ) )
67 62 66 eqtrd 
 |-  ( ( ph /\ ( F e. ( X RngIsom Y ) /\ G = `' F ) ) -> ( G o. F ) = ( _I |` ( Base ` X ) ) )
68 49 60 67 jca31 
 |-  ( ( ph /\ ( F e. ( X RngIsom Y ) /\ G = `' F ) ) -> ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) )
69 51 biimpcd 
 |-  ( F e. ( X RngIsom Y ) -> ( ph -> ( F e. ( X RngHomo Y ) /\ `' F e. ( Y RngHomo X ) ) ) )
70 69 adantr 
 |-  ( ( F e. ( X RngIsom Y ) /\ G = `' F ) -> ( ph -> ( F e. ( X RngHomo Y ) /\ `' F e. ( Y RngHomo X ) ) ) )
71 70 impcom 
 |-  ( ( ph /\ ( F e. ( X RngIsom Y ) /\ G = `' F ) ) -> ( F e. ( X RngHomo Y ) /\ `' F e. ( Y RngHomo X ) ) )
72 eleq1 
 |-  ( G = `' F -> ( G e. ( Y RngHomo X ) <-> `' F e. ( Y RngHomo X ) ) )
73 72 ad2antll 
 |-  ( ( ph /\ ( F e. ( X RngIsom Y ) /\ G = `' F ) ) -> ( G e. ( Y RngHomo X ) <-> `' F e. ( Y RngHomo X ) ) )
74 73 anbi2d 
 |-  ( ( ph /\ ( F e. ( X RngIsom Y ) /\ G = `' F ) ) -> ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) <-> ( F e. ( X RngHomo Y ) /\ `' F e. ( Y RngHomo X ) ) ) )
75 71 74 mpbird 
 |-  ( ( ph /\ ( F e. ( X RngIsom Y ) /\ G = `' F ) ) -> ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) )
76 coeq2 
 |-  ( G = `' F -> ( F o. G ) = ( F o. `' F ) )
77 76 ad2antll 
 |-  ( ( ph /\ ( F e. ( X RngIsom Y ) /\ G = `' F ) ) -> ( F o. G ) = ( F o. `' F ) )
78 f1ococnv2 
 |-  ( F : ( Base ` X ) -1-1-onto-> ( Base ` Y ) -> ( F o. `' F ) = ( _I |` ( Base ` Y ) ) )
79 64 78 syl 
 |-  ( ( ph /\ ( F e. ( X RngIsom Y ) /\ G = `' F ) ) -> ( F o. `' F ) = ( _I |` ( Base ` Y ) ) )
80 77 79 eqtrd 
 |-  ( ( ph /\ ( F e. ( X RngIsom Y ) /\ G = `' F ) ) -> ( F o. G ) = ( _I |` ( Base ` Y ) ) )
81 75 67 80 jca31 
 |-  ( ( ph /\ ( F e. ( X RngIsom Y ) /\ G = `' F ) ) -> ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) /\ ( F o. G ) = ( _I |` ( Base ` Y ) ) ) )
82 68 75 81 jca31 
 |-  ( ( ph /\ ( F e. ( X RngIsom Y ) /\ G = `' F ) ) -> ( ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) /\ ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) /\ ( F o. G ) = ( _I |` ( Base ` Y ) ) ) ) )
83 47 82 impbida 
 |-  ( ph -> ( ( ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) /\ ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` ( Base ` X ) ) ) /\ ( F o. G ) = ( _I |` ( Base ` Y ) ) ) ) <-> ( F e. ( X RngIsom Y ) /\ G = `' F ) ) )
84 10 23 83 3bitrd 
 |-  ( ph -> ( F ( X N Y ) G <-> ( F e. ( X RngIsom Y ) /\ G = `' F ) ) )