Metamath Proof Explorer

Theorem rhmsubcsetc

Description: The unital ring homomorphisms between unital rings (in a universe) are a subcategory of the category of extensible structures. (Contributed by AV, 9-Mar-2020)

Ref Expression
Hypotheses rhmsubcsetc.c 
|- C = ( ExtStrCat ` U )
rhmsubcsetc.u 
|- ( ph -> U e. V )
rhmsubcsetc.b 
|- ( ph -> B = ( Ring i^i U ) )
rhmsubcsetc.h 
|- ( ph -> H = ( RingHom |` ( B X. B ) ) )
Assertion rhmsubcsetc 
|- ( ph -> H e. ( Subcat ` C ) )

Proof

Step Hyp Ref Expression
1 rhmsubcsetc.c 
 |-  C = ( ExtStrCat ` U )
2 rhmsubcsetc.u 
 |-  ( ph -> U e. V )
3 rhmsubcsetc.b 
 |-  ( ph -> B = ( Ring i^i U ) )
4 rhmsubcsetc.h 
 |-  ( ph -> H = ( RingHom |` ( B X. B ) ) )
5 2 3 rhmsscmap 
 |-  ( ph -> ( RingHom |` ( B X. B ) ) C_cat ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) )
6 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
7 1 2 6 estrchomfeqhom 
 |-  ( ph -> ( Homf ` C ) = ( Hom ` C ) )
8 1 2 6 estrchomfval 
 |-  ( ph -> ( Hom ` C ) = ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) )
9 7 8 eqtrd 
 |-  ( ph -> ( Homf ` C ) = ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) )
10 5 4 9 3brtr4d 
 |-  ( ph -> H C_cat ( Homf ` C ) )
11 1 2 3 4 rhmsubcsetclem1 
 |-  ( ( ph /\ x e. B ) -> ( ( Id ` C ) ` x ) e. ( x H x ) )
12 1 2 3 4 rhmsubcsetclem2 
 |-  ( ( ph /\ x e. B ) -> A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x H z ) )
13 11 12 jca 
 |-  ( ( ph /\ x e. B ) -> ( ( ( Id ` C ) ` x ) e. ( x H x ) /\ A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x H z ) ) )
14 13 ralrimiva 
 |-  ( ph -> A. x e. B ( ( ( Id ` C ) ` x ) e. ( x H x ) /\ A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x H z ) ) )
15 eqid 
 |-  ( Homf ` C ) = ( Homf ` C )
16 eqid 
 |-  ( Id ` C ) = ( Id ` C )
17 eqid 
 |-  ( comp ` C ) = ( comp ` C )
18 1 estrccat 
 |-  ( U e. V -> C e. Cat )
19 2 18 syl 
 |-  ( ph -> C e. Cat )
20 incom 
 |-  ( Ring i^i U ) = ( U i^i Ring )
21 3 20 eqtrdi 
 |-  ( ph -> B = ( U i^i Ring ) )
22 21 4 rhmresfn 
 |-  ( ph -> H Fn ( B X. B ) )
23 15 16 17 19 22 issubc2 
 |-  ( ph -> ( H e. ( Subcat ` C ) <-> ( H C_cat ( Homf ` C ) /\ A. x e. B ( ( ( Id ` C ) ` x ) e. ( x H x ) /\ A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x H z ) ) ) ) )
24 10 14 23 mpbir2and 
 |-  ( ph -> H e. ( Subcat ` C ) )