Metamath Proof Explorer

Theorem rngcsectALTV

Description: A section in the category of non-unital rings, written out. (Contributed by AV, 28-Feb-2020) (New usage is discouraged.)

Ref Expression
Hypotheses rngcsectALTV.c 
|- C = ( RngCatALTV ` U )
rngcsectALTV.b 
|- B = ( Base ` C )
rngcsectALTV.u 
|- ( ph -> U e. V )
rngcsectALTV.x 
|- ( ph -> X e. B )
rngcsectALTV.y 
|- ( ph -> Y e. B )
rngcsectALTV.e 
|- E = ( Base ` X )
rngcsectALTV.n 
|- S = ( Sect ` C )
Assertion rngcsectALTV 
|- ( ph -> ( F ( X S Y ) G <-> ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) /\ ( G o. F ) = ( _I |` E ) ) ) )

Proof

Step Hyp Ref Expression
1 rngcsectALTV.c 
 |-  C = ( RngCatALTV ` U )
2 rngcsectALTV.b 
 |-  B = ( Base ` C )
3 rngcsectALTV.u 
 |-  ( ph -> U e. V )
4 rngcsectALTV.x 
 |-  ( ph -> X e. B )
5 rngcsectALTV.y 
 |-  ( ph -> Y e. B )
6 rngcsectALTV.e 
 |-  E = ( Base ` X )
7 rngcsectALTV.n 
 |-  S = ( Sect ` C )
8 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
9 eqid 
 |-  ( comp ` C ) = ( comp ` C )
10 eqid 
 |-  ( Id ` C ) = ( Id ` C )
11 1 rngccatALTV 
 |-  ( U e. V -> C e. Cat )
12 3 11 syl 
 |-  ( ph -> C e. Cat )
13 2 8 9 10 7 12 4 5 issect 
 |-  ( ph -> ( F ( X S Y ) G <-> ( F e. ( X ( Hom ` C ) Y ) /\ G e. ( Y ( Hom ` C ) X ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) ) )
14 1 2 3 8 4 5 rngchomALTV 
 |-  ( ph -> ( X ( Hom ` C ) Y ) = ( X RngHomo Y ) )
15 14 eleq2d 
 |-  ( ph -> ( F e. ( X ( Hom ` C ) Y ) <-> F e. ( X RngHomo Y ) ) )
16 1 2 3 8 5 4 rngchomALTV 
 |-  ( ph -> ( Y ( Hom ` C ) X ) = ( Y RngHomo X ) )
17 16 eleq2d 
 |-  ( ph -> ( G e. ( Y ( Hom ` C ) X ) <-> G e. ( Y RngHomo X ) ) )
18 15 17 anbi12d 
 |-  ( ph -> ( ( F e. ( X ( Hom ` C ) Y ) /\ G e. ( Y ( Hom ` C ) X ) ) <-> ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) )
19 18 anbi1d 
 |-  ( ph -> ( ( ( F e. ( X ( Hom ` C ) Y ) /\ G e. ( Y ( Hom ` C ) X ) ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) <-> ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) ) )
20 3 adantr 
 |-  ( ( ph /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) -> U e. V )
21 4 adantr 
 |-  ( ( ph /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) -> X e. B )
22 5 adantr 
 |-  ( ( ph /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) -> Y e. B )
23 simprl 
 |-  ( ( ph /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) -> F e. ( X RngHomo Y ) )
24 simprr 
 |-  ( ( ph /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) -> G e. ( Y RngHomo X ) )
25 1 2 20 9 21 22 21 23 24 rngccoALTV 
 |-  ( ( ph /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) -> ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( G o. F ) )
26 1 2 10 3 4 6 rngcidALTV 
 |-  ( ph -> ( ( Id ` C ) ` X ) = ( _I |` E ) )
27 26 adantr 
 |-  ( ( ph /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) -> ( ( Id ` C ) ` X ) = ( _I |` E ) )
28 25 27 eqeq12d 
 |-  ( ( ph /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) -> ( ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) <-> ( G o. F ) = ( _I |` E ) ) )
29 28 pm5.32da 
 |-  ( ph -> ( ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) <-> ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` E ) ) ) )
30 19 29 bitrd 
 |-  ( ph -> ( ( ( F e. ( X ( Hom ` C ) Y ) /\ G e. ( Y ( Hom ` C ) X ) ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) <-> ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` E ) ) ) )
31 df-3an 
 |-  ( ( F e. ( X ( Hom ` C ) Y ) /\ G e. ( Y ( Hom ` C ) X ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) <-> ( ( F e. ( X ( Hom ` C ) Y ) /\ G e. ( Y ( Hom ` C ) X ) ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) )
32 df-3an 
 |-  ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) /\ ( G o. F ) = ( _I |` E ) ) <-> ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) /\ ( G o. F ) = ( _I |` E ) ) )
33 30 31 32 3bitr4g 
 |-  ( ph -> ( ( F e. ( X ( Hom ` C ) Y ) /\ G e. ( Y ( Hom ` C ) X ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) <-> ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) /\ ( G o. F ) = ( _I |` E ) ) ) )
34 13 33 bitrd 
 |-  ( ph -> ( F ( X S Y ) G <-> ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) /\ ( G o. F ) = ( _I |` E ) ) ) )