Metamath Proof Explorer

Theorem rhmsubcALTV

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) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 rngcrescrhmALTV.u 
 |-  ( ph -> U e. V )
2 rngcrescrhmALTV.c 
 |-  C = ( RngCatALTV ` U )
3 rngcrescrhmALTV.r 
 |-  ( ph -> R = ( Ring i^i U ) )
4 rngcrescrhmALTV.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 eqid 
 |-  ( RngCatALTV ` U ) = ( RngCatALTV ` U )
9 eqid 
 |-  ( Rng i^i U ) = ( Rng i^i U )
10 eqid 
 |-  ( Homf ` ( RngCatALTV ` U ) ) = ( Homf ` ( RngCatALTV ` U ) )
11 8 9 1 10 rngchomrnghmresALTV 
 |-  ( ph -> ( Homf ` ( RngCatALTV ` U ) ) = ( RngHomo |` ( ( Rng i^i U ) X. ( Rng i^i U ) ) ) )
12 6 7 11 3brtr4d 
 |-  ( ph -> H C_cat ( Homf ` ( RngCatALTV ` U ) ) )
13 1 2 3 4 rhmsubcALTVlem3 
 |-  ( ( ph /\ x e. R ) -> ( ( Id ` ( RngCatALTV ` U ) ) ` x ) e. ( x H x ) )
14 1 2 3 4 rhmsubcALTVlem4 
 |-  ( ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( g ( <. x , y >. ( comp ` ( RngCatALTV ` U ) ) z ) f ) e. ( x H z ) )
15 14 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 ` ( RngCatALTV ` U ) ) z ) f ) e. ( x H z ) )
16 15 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 ` ( RngCatALTV ` U ) ) z ) f ) e. ( x H z ) )
17 13 16 jca 
 |-  ( ( ph /\ x e. R ) -> ( ( ( Id ` ( RngCatALTV ` 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 ` ( RngCatALTV ` U ) ) z ) f ) e. ( x H z ) ) )
18 17 ralrimiva 
 |-  ( ph -> A. x e. R ( ( ( Id ` ( RngCatALTV ` 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 ` ( RngCatALTV ` U ) ) z ) f ) e. ( x H z ) ) )
19 eqid 
 |-  ( Id ` ( RngCatALTV ` U ) ) = ( Id ` ( RngCatALTV ` U ) )
20 eqid 
 |-  ( comp ` ( RngCatALTV ` U ) ) = ( comp ` ( RngCatALTV ` U ) )
21 8 rngccatALTV 
 |-  ( U e. V -> ( RngCatALTV ` U ) e. Cat )
22 1 21 syl 
 |-  ( ph -> ( RngCatALTV ` U ) e. Cat )
23 1 2 3 4 rhmsubcALTVlem1 
 |-  ( ph -> H Fn ( R X. R ) )
24 10 19 20 22 23 issubc2 
 |-  ( ph -> ( H e. ( Subcat ` ( RngCatALTV ` U ) ) <-> ( H C_cat ( Homf ` ( RngCatALTV ` U ) ) /\ A. x e. R ( ( ( Id ` ( RngCatALTV ` 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 ` ( RngCatALTV ` U ) ) z ) f ) e. ( x H z ) ) ) ) )
25 12 18 24 mpbir2and 
 |-  ( ph -> H e. ( Subcat ` ( RngCatALTV ` U ) ) )