Metamath Proof Explorer

Theorem rhmsubc

Description: According to df-subc , the subcategories ( SubcatC ) of a category C are subsets of the homomorphisms of C (see subcssc and subcss2 ). Therefore, the set of unital ring homomorphisms is a "subcategory" of the category of non-unital rings. (Contributed by AV, 2-Mar-2020)

Ref Expression
Hypotheses rngcrescrhm.u 
|- ( ph -> U e. V )
rngcrescrhm.c 
|- C = ( RngCat ` U )
rngcrescrhm.r 
|- ( ph -> R = ( Ring i^i U ) )
rngcrescrhm.h 
|- H = ( RingHom |` ( R X. R ) )
Assertion rhmsubc 
|- ( ph -> H e. ( Subcat ` ( RngCat ` U ) ) )

Proof

Step Hyp Ref Expression
1 rngcrescrhm.u 
 |-  ( ph -> U e. V )
2 rngcrescrhm.c 
 |-  C = ( RngCat ` U )
3 rngcrescrhm.r 
 |-  ( ph -> R = ( Ring i^i U ) )
4 rngcrescrhm.h 
 |-  H = ( RingHom |` ( R X. R ) )
5 eqidd 
 |-  ( ph -> ( Rng i^i U ) = ( Rng i^i U ) )
6 1 3 5 rhmsscrnghm 
 |-  ( ph -> ( RingHom |` ( R X. R ) ) C_cat ( RngHomo |` ( ( Rng i^i U ) X. ( Rng i^i U ) ) ) )
7 4 a1i 
 |-  ( ph -> H = ( RingHom |` ( R X. R ) ) )
8 2 a1i 
 |-  ( ph -> C = ( RngCat ` U ) )
9 8 eqcomd 
 |-  ( ph -> ( RngCat ` U ) = C )
10 9 fveq2d 
 |-  ( ph -> ( Homf ` ( RngCat ` U ) ) = ( Homf ` C ) )
11 eqid 
 |-  ( Base ` C ) = ( Base ` C )
12 2 11 1 rngchomfeqhom 
 |-  ( ph -> ( Homf ` C ) = ( Hom ` C ) )
13 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
14 2 11 1 13 rngchomfval 
 |-  ( ph -> ( Hom ` C ) = ( RngHomo |` ( ( Base ` C ) X. ( Base ` C ) ) ) )
15 2 11 1 rngcbas 
 |-  ( ph -> ( Base ` C ) = ( U i^i Rng ) )
16 incom 
 |-  ( U i^i Rng ) = ( Rng i^i U )
17 15 16 eqtrdi 
 |-  ( ph -> ( Base ` C ) = ( Rng i^i U ) )
18 17 sqxpeqd 
 |-  ( ph -> ( ( Base ` C ) X. ( Base ` C ) ) = ( ( Rng i^i U ) X. ( Rng i^i U ) ) )
19 18 reseq2d 
 |-  ( ph -> ( RngHomo |` ( ( Base ` C ) X. ( Base ` C ) ) ) = ( RngHomo |` ( ( Rng i^i U ) X. ( Rng i^i U ) ) ) )
20 14 19 eqtrd 
 |-  ( ph -> ( Hom ` C ) = ( RngHomo |` ( ( Rng i^i U ) X. ( Rng i^i U ) ) ) )
21 10 12 20 3eqtrd 
 |-  ( ph -> ( Homf ` ( RngCat ` U ) ) = ( RngHomo |` ( ( Rng i^i U ) X. ( Rng i^i U ) ) ) )
22 6 7 21 3brtr4d 
 |-  ( ph -> H C_cat ( Homf ` ( RngCat ` U ) ) )
23 1 2 3 4 rhmsubclem3 
 |-  ( ( ph /\ x e. R ) -> ( ( Id ` ( RngCat ` U ) ) ` x ) e. ( x H x ) )
24 1 2 3 4 rhmsubclem4 
 |-  ( ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( g ( <. x , y >. ( comp ` ( RngCat ` U ) ) z ) f ) e. ( x H z ) )
25 24 ralrimivva 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. ( comp ` ( RngCat ` U ) ) z ) f ) e. ( x H z ) )
26 25 ralrimivva 
 |-  ( ( ph /\ x e. R ) -> A. y e. R A. z e. R A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. ( comp ` ( RngCat ` U ) ) z ) f ) e. ( x H z ) )
27 23 26 jca 
 |-  ( ( ph /\ x e. R ) -> ( ( ( Id ` ( RngCat ` U ) ) ` x ) e. ( x H x ) /\ A. y e. R A. z e. R A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. ( comp ` ( RngCat ` U ) ) z ) f ) e. ( x H z ) ) )
28 27 ralrimiva 
 |-  ( ph -> A. x e. R ( ( ( Id ` ( RngCat ` U ) ) ` x ) e. ( x H x ) /\ A. y e. R A. z e. R A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. ( comp ` ( RngCat ` U ) ) z ) f ) e. ( x H z ) ) )
29 eqid 
 |-  ( Homf ` ( RngCat ` U ) ) = ( Homf ` ( RngCat ` U ) )
30 eqid 
 |-  ( Id ` ( RngCat ` U ) ) = ( Id ` ( RngCat ` U ) )
31 eqid 
 |-  ( comp ` ( RngCat ` U ) ) = ( comp ` ( RngCat ` U ) )
32 eqid 
 |-  ( RngCat ` U ) = ( RngCat ` U )
33 32 rngccat 
 |-  ( U e. V -> ( RngCat ` U ) e. Cat )
34 1 33 syl 
 |-  ( ph -> ( RngCat ` U ) e. Cat )
35 1 2 3 4 rhmsubclem1 
 |-  ( ph -> H Fn ( R X. R ) )
36 29 30 31 34 35 issubc2 
 |-  ( ph -> ( H e. ( Subcat ` ( RngCat ` U ) ) <-> ( H C_cat ( Homf ` ( RngCat ` U ) ) /\ A. x e. R ( ( ( Id ` ( RngCat ` U ) ) ` x ) e. ( x H x ) /\ A. y e. R A. z e. R A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. ( comp ` ( RngCat ` U ) ) z ) f ) e. ( x H z ) ) ) ) )
37 22 28 36 mpbir2and 
 |-  ( ph -> H e. ( Subcat ` ( RngCat ` U ) ) )