Metamath Proof Explorer

Theorem srhmsubc

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 special ring homomorphisms (i.e., ring homomorphisms from a special ring to another ring of that kind) is a subcategory of the category of (unital) rings. (Contributed by AV, 19-Feb-2020)

Ref Expression
Hypotheses srhmsubc.s 
|- A. r e. S r e. Ring
srhmsubc.c 
|- C = ( U i^i S )
srhmsubc.j 
|- J = ( r e. C , s e. C |-> ( r RingHom s ) )
Assertion srhmsubc 
|- ( U e. V -> J e. ( Subcat ` ( RingCat ` U ) ) )

Proof

Step Hyp Ref Expression
1 srhmsubc.s 
 |-  A. r e. S r e. Ring
2 srhmsubc.c 
 |-  C = ( U i^i S )
3 srhmsubc.j 
 |-  J = ( r e. C , s e. C |-> ( r RingHom s ) )
4 eleq1w 
 |-  ( r = x -> ( r e. Ring <-> x e. Ring ) )
5 4 1 vtoclri 
 |-  ( x e. S -> x e. Ring )
6 5 ssriv 
 |-  S C_ Ring
7 sslin 
 |-  ( S C_ Ring -> ( U i^i S ) C_ ( U i^i Ring ) )
8 6 7 mp1i 
 |-  ( U e. V -> ( U i^i S ) C_ ( U i^i Ring ) )
9 2 8 eqsstrid 
 |-  ( U e. V -> C C_ ( U i^i Ring ) )
10 ssid 
 |-  ( x RingHom y ) C_ ( x RingHom y )
11 eqid 
 |-  ( RingCat ` U ) = ( RingCat ` U )
12 eqid 
 |-  ( Base ` ( RingCat ` U ) ) = ( Base ` ( RingCat ` U ) )
13 simpl 
 |-  ( ( U e. V /\ ( x e. C /\ y e. C ) ) -> U e. V )
14 eqid 
 |-  ( Hom ` ( RingCat ` U ) ) = ( Hom ` ( RingCat ` U ) )
15 1 2 srhmsubclem2 
 |-  ( ( U e. V /\ x e. C ) -> x e. ( Base ` ( RingCat ` U ) ) )
16 15 adantrr 
 |-  ( ( U e. V /\ ( x e. C /\ y e. C ) ) -> x e. ( Base ` ( RingCat ` U ) ) )
17 1 2 srhmsubclem2 
 |-  ( ( U e. V /\ y e. C ) -> y e. ( Base ` ( RingCat ` U ) ) )
18 17 adantrl 
 |-  ( ( U e. V /\ ( x e. C /\ y e. C ) ) -> y e. ( Base ` ( RingCat ` U ) ) )
19 11 12 13 14 16 18 ringchom 
 |-  ( ( U e. V /\ ( x e. C /\ y e. C ) ) -> ( x ( Hom ` ( RingCat ` U ) ) y ) = ( x RingHom y ) )
20 10 19 sseqtrrid 
 |-  ( ( U e. V /\ ( x e. C /\ y e. C ) ) -> ( x RingHom y ) C_ ( x ( Hom ` ( RingCat ` U ) ) y ) )
21 3 a1i 
 |-  ( ( U e. V /\ ( x e. C /\ y e. C ) ) -> J = ( r e. C , s e. C |-> ( r RingHom s ) ) )
22 oveq12 
 |-  ( ( r = x /\ s = y ) -> ( r RingHom s ) = ( x RingHom y ) )
23 22 adantl 
 |-  ( ( ( U e. V /\ ( x e. C /\ y e. C ) ) /\ ( r = x /\ s = y ) ) -> ( r RingHom s ) = ( x RingHom y ) )
24 simprl 
 |-  ( ( U e. V /\ ( x e. C /\ y e. C ) ) -> x e. C )
25 simprr 
 |-  ( ( U e. V /\ ( x e. C /\ y e. C ) ) -> y e. C )
26 ovexd 
 |-  ( ( U e. V /\ ( x e. C /\ y e. C ) ) -> ( x RingHom y ) e. _V )
27 21 23 24 25 26 ovmpod 
 |-  ( ( U e. V /\ ( x e. C /\ y e. C ) ) -> ( x J y ) = ( x RingHom y ) )
28 eqid 
 |-  ( Homf ` ( RingCat ` U ) ) = ( Homf ` ( RingCat ` U ) )
29 28 12 14 16 18 homfval 
 |-  ( ( U e. V /\ ( x e. C /\ y e. C ) ) -> ( x ( Homf ` ( RingCat ` U ) ) y ) = ( x ( Hom ` ( RingCat ` U ) ) y ) )
30 20 27 29 3sstr4d 
 |-  ( ( U e. V /\ ( x e. C /\ y e. C ) ) -> ( x J y ) C_ ( x ( Homf ` ( RingCat ` U ) ) y ) )
31 30 ralrimivva 
 |-  ( U e. V -> A. x e. C A. y e. C ( x J y ) C_ ( x ( Homf ` ( RingCat ` U ) ) y ) )
32 ovex 
 |-  ( r RingHom s ) e. _V
33 3 32 fnmpoi 
 |-  J Fn ( C X. C )
34 33 a1i 
 |-  ( U e. V -> J Fn ( C X. C ) )
35 28 12 homffn 
 |-  ( Homf ` ( RingCat ` U ) ) Fn ( ( Base ` ( RingCat ` U ) ) X. ( Base ` ( RingCat ` U ) ) )
36 id 
 |-  ( U e. V -> U e. V )
37 11 12 36 ringcbas 
 |-  ( U e. V -> ( Base ` ( RingCat ` U ) ) = ( U i^i Ring ) )
38 37 eqcomd 
 |-  ( U e. V -> ( U i^i Ring ) = ( Base ` ( RingCat ` U ) ) )
39 38 sqxpeqd 
 |-  ( U e. V -> ( ( U i^i Ring ) X. ( U i^i Ring ) ) = ( ( Base ` ( RingCat ` U ) ) X. ( Base ` ( RingCat ` U ) ) ) )
40 39 fneq2d 
 |-  ( U e. V -> ( ( Homf ` ( RingCat ` U ) ) Fn ( ( U i^i Ring ) X. ( U i^i Ring ) ) <-> ( Homf ` ( RingCat ` U ) ) Fn ( ( Base ` ( RingCat ` U ) ) X. ( Base ` ( RingCat ` U ) ) ) ) )
41 35 40 mpbiri 
 |-  ( U e. V -> ( Homf ` ( RingCat ` U ) ) Fn ( ( U i^i Ring ) X. ( U i^i Ring ) ) )
42 inex1g 
 |-  ( U e. V -> ( U i^i Ring ) e. _V )
43 34 41 42 isssc 
 |-  ( U e. V -> ( J C_cat ( Homf ` ( RingCat ` U ) ) <-> ( C C_ ( U i^i Ring ) /\ A. x e. C A. y e. C ( x J y ) C_ ( x ( Homf ` ( RingCat ` U ) ) y ) ) ) )
44 9 31 43 mpbir2and 
 |-  ( U e. V -> J C_cat ( Homf ` ( RingCat ` U ) ) )
45 2 elin2 
 |-  ( x e. C <-> ( x e. U /\ x e. S ) )
46 5 adantl 
 |-  ( ( x e. U /\ x e. S ) -> x e. Ring )
47 45 46 sylbi 
 |-  ( x e. C -> x e. Ring )
48 47 adantl 
 |-  ( ( U e. V /\ x e. C ) -> x e. Ring )
49 eqid 
 |-  ( Base ` x ) = ( Base ` x )
50 49 idrhm 
 |-  ( x e. Ring -> ( _I |` ( Base ` x ) ) e. ( x RingHom x ) )
51 48 50 syl 
 |-  ( ( U e. V /\ x e. C ) -> ( _I |` ( Base ` x ) ) e. ( x RingHom x ) )
52 eqid 
 |-  ( Id ` ( RingCat ` U ) ) = ( Id ` ( RingCat ` U ) )
53 simpl 
 |-  ( ( U e. V /\ x e. C ) -> U e. V )
54 11 12 52 53 15 49 ringcid 
 |-  ( ( U e. V /\ x e. C ) -> ( ( Id ` ( RingCat ` U ) ) ` x ) = ( _I |` ( Base ` x ) ) )
55 3 a1i 
 |-  ( ( U e. V /\ x e. C ) -> J = ( r e. C , s e. C |-> ( r RingHom s ) ) )
56 oveq12 
 |-  ( ( r = x /\ s = x ) -> ( r RingHom s ) = ( x RingHom x ) )
57 56 adantl 
 |-  ( ( ( U e. V /\ x e. C ) /\ ( r = x /\ s = x ) ) -> ( r RingHom s ) = ( x RingHom x ) )
58 simpr 
 |-  ( ( U e. V /\ x e. C ) -> x e. C )
59 ovexd 
 |-  ( ( U e. V /\ x e. C ) -> ( x RingHom x ) e. _V )
60 55 57 58 58 59 ovmpod 
 |-  ( ( U e. V /\ x e. C ) -> ( x J x ) = ( x RingHom x ) )
61 51 54 60 3eltr4d 
 |-  ( ( U e. V /\ x e. C ) -> ( ( Id ` ( RingCat ` U ) ) ` x ) e. ( x J x ) )
62 eqid 
 |-  ( comp ` ( RingCat ` U ) ) = ( comp ` ( RingCat ` U ) )
63 11 ringccat 
 |-  ( U e. V -> ( RingCat ` U ) e. Cat )
64 63 ad3antrrr 
 |-  ( ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) -> ( RingCat ` U ) e. Cat )
65 15 adantr 
 |-  ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) -> x e. ( Base ` ( RingCat ` U ) ) )
66 65 adantr 
 |-  ( ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) -> x e. ( Base ` ( RingCat ` U ) ) )
67 17 ad2ant2r 
 |-  ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) -> y e. ( Base ` ( RingCat ` U ) ) )
68 67 adantr 
 |-  ( ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) -> y e. ( Base ` ( RingCat ` U ) ) )
69 1 2 srhmsubclem2 
 |-  ( ( U e. V /\ z e. C ) -> z e. ( Base ` ( RingCat ` U ) ) )
70 69 ad2ant2rl 
 |-  ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) -> z e. ( Base ` ( RingCat ` U ) ) )
71 70 adantr 
 |-  ( ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) -> z e. ( Base ` ( RingCat ` U ) ) )
72 53 adantr 
 |-  ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) -> U e. V )
73 simpl 
 |-  ( ( y e. C /\ z e. C ) -> y e. C )
74 58 73 anim12i 
 |-  ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) -> ( x e. C /\ y e. C ) )
75 72 74 jca 
 |-  ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) -> ( U e. V /\ ( x e. C /\ y e. C ) ) )
76 1 2 3 srhmsubclem3 
 |-  ( ( U e. V /\ ( x e. C /\ y e. C ) ) -> ( x J y ) = ( x ( Hom ` ( RingCat ` U ) ) y ) )
77 75 76 syl 
 |-  ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) -> ( x J y ) = ( x ( Hom ` ( RingCat ` U ) ) y ) )
78 77 eleq2d 
 |-  ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) -> ( f e. ( x J y ) <-> f e. ( x ( Hom ` ( RingCat ` U ) ) y ) ) )
79 78 biimpcd 
 |-  ( f e. ( x J y ) -> ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) -> f e. ( x ( Hom ` ( RingCat ` U ) ) y ) ) )
80 79 adantr 
 |-  ( ( f e. ( x J y ) /\ g e. ( y J z ) ) -> ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) -> f e. ( x ( Hom ` ( RingCat ` U ) ) y ) ) )
81 80 impcom 
 |-  ( ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) -> f e. ( x ( Hom ` ( RingCat ` U ) ) y ) )
82 1 2 3 srhmsubclem3 
 |-  ( ( U e. V /\ ( y e. C /\ z e. C ) ) -> ( y J z ) = ( y ( Hom ` ( RingCat ` U ) ) z ) )
83 82 adantlr 
 |-  ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) -> ( y J z ) = ( y ( Hom ` ( RingCat ` U ) ) z ) )
84 83 eleq2d 
 |-  ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) -> ( g e. ( y J z ) <-> g e. ( y ( Hom ` ( RingCat ` U ) ) z ) ) )
85 84 biimpd 
 |-  ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) -> ( g e. ( y J z ) -> g e. ( y ( Hom ` ( RingCat ` U ) ) z ) ) )
86 85 adantld 
 |-  ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) -> ( ( f e. ( x J y ) /\ g e. ( y J z ) ) -> g e. ( y ( Hom ` ( RingCat ` U ) ) z ) ) )
87 86 imp 
 |-  ( ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) -> g e. ( y ( Hom ` ( RingCat ` U ) ) z ) )
88 12 14 62 64 66 68 71 81 87 catcocl 
 |-  ( ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) -> ( g ( <. x , y >. ( comp ` ( RingCat ` U ) ) z ) f ) e. ( x ( Hom ` ( RingCat ` U ) ) z ) )
89 11 12 72 14 65 70 ringchom 
 |-  ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) -> ( x ( Hom ` ( RingCat ` U ) ) z ) = ( x RingHom z ) )
90 89 eqcomd 
 |-  ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) -> ( x RingHom z ) = ( x ( Hom ` ( RingCat ` U ) ) z ) )
91 90 adantr 
 |-  ( ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) -> ( x RingHom z ) = ( x ( Hom ` ( RingCat ` U ) ) z ) )
92 88 91 eleqtrrd 
 |-  ( ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) -> ( g ( <. x , y >. ( comp ` ( RingCat ` U ) ) z ) f ) e. ( x RingHom z ) )
93 3 a1i 
 |-  ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) -> J = ( r e. C , s e. C |-> ( r RingHom s ) ) )
94 oveq12 
 |-  ( ( r = x /\ s = z ) -> ( r RingHom s ) = ( x RingHom z ) )
95 94 adantl 
 |-  ( ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) /\ ( r = x /\ s = z ) ) -> ( r RingHom s ) = ( x RingHom z ) )
96 58 adantr 
 |-  ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) -> x e. C )
97 simprr 
 |-  ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) -> z e. C )
98 ovexd 
 |-  ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) -> ( x RingHom z ) e. _V )
99 93 95 96 97 98 ovmpod 
 |-  ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) -> ( x J z ) = ( x RingHom z ) )
100 99 adantr 
 |-  ( ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) -> ( x J z ) = ( x RingHom z ) )
101 92 100 eleqtrrd 
 |-  ( ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) -> ( g ( <. x , y >. ( comp ` ( RingCat ` U ) ) z ) f ) e. ( x J z ) )
102 101 ralrimivva 
 |-  ( ( ( U e. V /\ x e. C ) /\ ( y e. C /\ z e. C ) ) -> A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` ( RingCat ` U ) ) z ) f ) e. ( x J z ) )
103 102 ralrimivva 
 |-  ( ( U e. V /\ x e. C ) -> A. y e. C A. z e. C A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` ( RingCat ` U ) ) z ) f ) e. ( x J z ) )
104 61 103 jca 
 |-  ( ( U e. V /\ x e. C ) -> ( ( ( Id ` ( RingCat ` U ) ) ` x ) e. ( x J x ) /\ A. y e. C A. z e. C A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` ( RingCat ` U ) ) z ) f ) e. ( x J z ) ) )
105 104 ralrimiva 
 |-  ( U e. V -> A. x e. C ( ( ( Id ` ( RingCat ` U ) ) ` x ) e. ( x J x ) /\ A. y e. C A. z e. C A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` ( RingCat ` U ) ) z ) f ) e. ( x J z ) ) )
106 28 52 62 63 34 issubc2 
 |-  ( U e. V -> ( J e. ( Subcat ` ( RingCat ` U ) ) <-> ( J C_cat ( Homf ` ( RingCat ` U ) ) /\ A. x e. C ( ( ( Id ` ( RingCat ` U ) ) ` x ) e. ( x J x ) /\ A. y e. C A. z e. C A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` ( RingCat ` U ) ) z ) f ) e. ( x J z ) ) ) ) )
107 44 105 106 mpbir2and 
 |-  ( U e. V -> J e. ( Subcat ` ( RingCat ` U ) ) )