Metamath Proof Explorer

Theorem rngcsect

Description: A section in the category of non-unital rings, written out. (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 )
rngcsect.e 
|- E = ( Base ` X )
rngcsect.n 
|- S = ( Sect ` C )
Assertion rngcsect 
|- ( 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 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 rngcsect.e 
 |-  E = ( Base ` X )
7 rngcsect.n 
 |-  S = ( Sect ` C )
8 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
9 eqid 
 |-  ( comp ` C ) = ( comp ` C )
10 eqid 
 |-  ( Id ` C ) = ( Id ` C )
11 1 rngccat 
 |-  ( 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 rngchom 
 |-  ( 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 rngchom 
 |-  ( 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 1 2 3 rngcbas 
 |-  ( ph -> B = ( U i^i Rng ) )
23 22 eleq2d 
 |-  ( ph -> ( X e. B <-> X e. ( U i^i Rng ) ) )
24 inss1 
 |-  ( U i^i Rng ) C_ U
25 24 a1i 
 |-  ( ph -> ( U i^i Rng ) C_ U )
26 25 sseld 
 |-  ( ph -> ( X e. ( U i^i Rng ) -> X e. U ) )
27 23 26 sylbid 
 |-  ( ph -> ( X e. B -> X e. U ) )
28 27 adantr 
 |-  ( ( ph /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) -> ( X e. B -> X e. U ) )
29 21 28 mpd 
 |-  ( ( ph /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) -> X e. U )
30 5 adantr 
 |-  ( ( ph /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) -> Y e. B )
31 22 eleq2d 
 |-  ( ph -> ( Y e. B <-> Y e. ( U i^i Rng ) ) )
32 25 sseld 
 |-  ( ph -> ( Y e. ( U i^i Rng ) -> Y e. U ) )
33 31 32 sylbid 
 |-  ( ph -> ( Y e. B -> Y e. U ) )
34 33 adantr 
 |-  ( ( ph /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) -> ( Y e. B -> Y e. U ) )
35 30 34 mpd 
 |-  ( ( ph /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) -> Y e. U )
36 eqid 
 |-  ( Base ` X ) = ( Base ` X )
37 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
38 36 37 rnghmf 
 |-  ( F e. ( X RngHomo Y ) -> F : ( Base ` X ) --> ( Base ` Y ) )
39 38 adantr 
 |-  ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) -> F : ( Base ` X ) --> ( Base ` Y ) )
40 39 adantl 
 |-  ( ( ph /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) -> F : ( Base ` X ) --> ( Base ` Y ) )
41 37 36 rnghmf 
 |-  ( G e. ( Y RngHomo X ) -> G : ( Base ` Y ) --> ( Base ` X ) )
42 41 adantl 
 |-  ( ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) -> G : ( Base ` Y ) --> ( Base ` X ) )
43 42 adantl 
 |-  ( ( ph /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) -> G : ( Base ` Y ) --> ( Base ` X ) )
44 1 20 9 29 35 29 40 43 rngcco 
 |-  ( ( ph /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) -> ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( G o. F ) )
45 1 2 10 3 4 6 rngcid 
 |-  ( ph -> ( ( Id ` C ) ` X ) = ( _I |` E ) )
46 45 adantr 
 |-  ( ( ph /\ ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) ) ) -> ( ( Id ` C ) ` X ) = ( _I |` E ) )
47 44 46 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 ) ) )
48 47 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 ) ) ) )
49 19 48 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 ) ) ) )
50 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 ) ) )
51 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 ) ) )
52 49 50 51 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 ) ) ) )
53 13 52 bitrd 
 |-  ( ph -> ( F ( X S Y ) G <-> ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) /\ ( G o. F ) = ( _I |` E ) ) ) )