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 r S r Ring
srhmsubc.c C = U S
srhmsubc.j J = r C , s C r RingHom s
Assertion srhmsubc U V J Subcat RingCat U

Proof

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