Metamath Proof Explorer


Theorem ringcsectALTV

Description: A section in the category of rings, written out. (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 )
ringcsectALTV.e
|- E = ( Base ` X )
ringcsectALTV.n
|- S = ( Sect ` C )
Assertion ringcsectALTV
|- ( ph -> ( F ( X S Y ) G <-> ( F e. ( X RingHom Y ) /\ G e. ( Y RingHom X ) /\ ( G o. F ) = ( _I |` E ) ) ) )

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 ringcsectALTV.e
 |-  E = ( Base ` X )
7 ringcsectALTV.n
 |-  S = ( Sect ` C )
8 eqid
 |-  ( Hom ` C ) = ( Hom ` C )
9 eqid
 |-  ( comp ` C ) = ( comp ` C )
10 eqid
 |-  ( Id ` C ) = ( Id ` C )
11 1 ringccatALTV
 |-  ( 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 ringchomALTV
 |-  ( ph -> ( X ( Hom ` C ) Y ) = ( X RingHom Y ) )
15 14 eleq2d
 |-  ( ph -> ( F e. ( X ( Hom ` C ) Y ) <-> F e. ( X RingHom Y ) ) )
16 1 2 3 8 5 4 ringchomALTV
 |-  ( ph -> ( Y ( Hom ` C ) X ) = ( Y RingHom X ) )
17 16 eleq2d
 |-  ( ph -> ( G e. ( Y ( Hom ` C ) X ) <-> G e. ( Y RingHom X ) ) )
18 15 17 anbi12d
 |-  ( ph -> ( ( F e. ( X ( Hom ` C ) Y ) /\ G e. ( Y ( Hom ` C ) X ) ) <-> ( F e. ( X RingHom Y ) /\ G e. ( Y RingHom 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 RingHom Y ) /\ G e. ( Y RingHom X ) ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) ) )
20 3 adantr
 |-  ( ( ph /\ ( F e. ( X RingHom Y ) /\ G e. ( Y RingHom X ) ) ) -> U e. V )
21 4 adantr
 |-  ( ( ph /\ ( F e. ( X RingHom Y ) /\ G e. ( Y RingHom X ) ) ) -> X e. B )
22 5 adantr
 |-  ( ( ph /\ ( F e. ( X RingHom Y ) /\ G e. ( Y RingHom X ) ) ) -> Y e. B )
23 simprl
 |-  ( ( ph /\ ( F e. ( X RingHom Y ) /\ G e. ( Y RingHom X ) ) ) -> F e. ( X RingHom Y ) )
24 simprr
 |-  ( ( ph /\ ( F e. ( X RingHom Y ) /\ G e. ( Y RingHom X ) ) ) -> G e. ( Y RingHom X ) )
25 1 2 20 9 21 22 21 23 24 ringccoALTV
 |-  ( ( ph /\ ( F e. ( X RingHom Y ) /\ G e. ( Y RingHom X ) ) ) -> ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( G o. F ) )
26 1 2 10 3 4 6 ringcidALTV
 |-  ( ph -> ( ( Id ` C ) ` X ) = ( _I |` E ) )
27 26 adantr
 |-  ( ( ph /\ ( F e. ( X RingHom Y ) /\ G e. ( Y RingHom X ) ) ) -> ( ( Id ` C ) ` X ) = ( _I |` E ) )
28 25 27 eqeq12d
 |-  ( ( ph /\ ( F e. ( X RingHom Y ) /\ G e. ( Y RingHom X ) ) ) -> ( ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) <-> ( G o. F ) = ( _I |` E ) ) )
29 28 pm5.32da
 |-  ( ph -> ( ( ( F e. ( X RingHom Y ) /\ G e. ( Y RingHom X ) ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) <-> ( ( F e. ( X RingHom Y ) /\ G e. ( Y RingHom 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 RingHom Y ) /\ G e. ( Y RingHom 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 RingHom Y ) /\ G e. ( Y RingHom X ) /\ ( G o. F ) = ( _I |` E ) ) <-> ( ( F e. ( X RingHom Y ) /\ G e. ( Y RingHom 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 RingHom Y ) /\ G e. ( Y RingHom X ) /\ ( G o. F ) = ( _I |` E ) ) ) )
34 13 33 bitrd
 |-  ( ph -> ( F ( X S Y ) G <-> ( F e. ( X RingHom Y ) /\ G e. ( Y RingHom X ) /\ ( G o. F ) = ( _I |` E ) ) ) )