Metamath Proof Explorer

Theorem rhmsubcrngc

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

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

Proof

Step Hyp Ref Expression
1 rhmsubcrngc.c 
 |-  C = ( RngCat ` U )
2 rhmsubcrngc.u 
 |-  ( ph -> U e. V )
3 rhmsubcrngc.b 
 |-  ( ph -> B = ( Ring i^i U ) )
4 rhmsubcrngc.h 
 |-  ( ph -> H = ( RingHom |` ( B X. B ) ) )
5 eqid 
 |-  ( RngCat ` U ) = ( RngCat ` U )
6 eqid 
 |-  ( Base ` ( RngCat ` U ) ) = ( Base ` ( RngCat ` U ) )
7 5 6 2 rngcbas 
 |-  ( ph -> ( Base ` ( RngCat ` U ) ) = ( U i^i Rng ) )
8 incom 
 |-  ( U i^i Rng ) = ( Rng i^i U )
9 7 8 eqtrdi 
 |-  ( ph -> ( Base ` ( RngCat ` U ) ) = ( Rng i^i U ) )
10 2 3 9 rhmsscrnghm 
 |-  ( ph -> ( RingHom |` ( B X. B ) ) C_cat ( RngHomo |` ( ( Base ` ( RngCat ` U ) ) X. ( Base ` ( RngCat ` U ) ) ) ) )
11 1 a1i 
 |-  ( ph -> C = ( RngCat ` U ) )
12 11 fveq2d 
 |-  ( ph -> ( Base ` C ) = ( Base ` ( RngCat ` U ) ) )
13 12 sqxpeqd 
 |-  ( ph -> ( ( Base ` C ) X. ( Base ` C ) ) = ( ( Base ` ( RngCat ` U ) ) X. ( Base ` ( RngCat ` U ) ) ) )
14 13 reseq2d 
 |-  ( ph -> ( RngHomo |` ( ( Base ` C ) X. ( Base ` C ) ) ) = ( RngHomo |` ( ( Base ` ( RngCat ` U ) ) X. ( Base ` ( RngCat ` U ) ) ) ) )
15 10 14 breqtrrd 
 |-  ( ph -> ( RingHom |` ( B X. B ) ) C_cat ( RngHomo |` ( ( Base ` C ) X. ( Base ` C ) ) ) )
16 eqid 
 |-  ( Base ` C ) = ( Base ` C )
17 1 16 2 rngchomfeqhom 
 |-  ( ph -> ( Homf ` C ) = ( Hom ` C ) )
18 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
19 1 16 2 18 rngchomfval 
 |-  ( ph -> ( Hom ` C ) = ( RngHomo |` ( ( Base ` C ) X. ( Base ` C ) ) ) )
20 17 19 eqtrd 
 |-  ( ph -> ( Homf ` C ) = ( RngHomo |` ( ( Base ` C ) X. ( Base ` C ) ) ) )
21 15 4 20 3brtr4d 
 |-  ( ph -> H C_cat ( Homf ` C ) )
22 1 2 3 4 rhmsubcrngclem1 
 |-  ( ( ph /\ x e. B ) -> ( ( Id ` C ) ` x ) e. ( x H x ) )
23 1 2 3 4 rhmsubcrngclem2 
 |-  ( ( 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 ) )
24 22 23 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 ) ) )
25 24 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 ) ) )
26 eqid 
 |-  ( Homf ` C ) = ( Homf ` C )
27 eqid 
 |-  ( Id ` C ) = ( Id ` C )
28 eqid 
 |-  ( comp ` C ) = ( comp ` C )
29 1 rngccat 
 |-  ( U e. V -> C e. Cat )
30 2 29 syl 
 |-  ( ph -> C e. Cat )
31 incom 
 |-  ( Ring i^i U ) = ( U i^i Ring )
32 3 31 eqtrdi 
 |-  ( ph -> B = ( U i^i Ring ) )
33 32 4 rhmresfn 
 |-  ( ph -> H Fn ( B X. B ) )
34 26 27 28 30 33 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 ) ) ) ) )
35 21 25 34 mpbir2and 
 |-  ( ph -> H e. ( Subcat ` C ) )