Metamath Proof Explorer


Theorem rhmsubcsetc

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

Ref Expression
Hypotheses rhmsubcsetc.c C = ExtStrCat U
rhmsubcsetc.u φ U V
rhmsubcsetc.b φ B = Ring U
rhmsubcsetc.h φ H = RingHom B × B
Assertion rhmsubcsetc φ H Subcat C

Proof

Step Hyp Ref Expression
1 rhmsubcsetc.c C = ExtStrCat U
2 rhmsubcsetc.u φ U V
3 rhmsubcsetc.b φ B = Ring U
4 rhmsubcsetc.h φ H = RingHom B × B
5 2 3 rhmsscmap φ RingHom B × B cat x U , y U Base y Base x
6 eqid Hom C = Hom C
7 1 2 6 estrchomfeqhom φ Hom 𝑓 C = Hom C
8 1 2 6 estrchomfval φ Hom C = x U , y U Base y Base x
9 7 8 eqtrd φ Hom 𝑓 C = x U , y U Base y Base x
10 5 4 9 3brtr4d φ H cat Hom 𝑓 C
11 1 2 3 4 rhmsubcsetclem1 φ x B Id C x x H x
12 1 2 3 4 rhmsubcsetclem2 φ x B y B z B f x H y g y H z g x y comp C z f x H z
13 11 12 jca φ x B Id C x x H x y B z B f x H y g y H z g x y comp C z f x H z
14 13 ralrimiva φ x B Id C x x H x y B z B f x H y g y H z g x y comp C z f x H z
15 eqid Hom 𝑓 C = Hom 𝑓 C
16 eqid Id C = Id C
17 eqid comp C = comp C
18 1 estrccat U V C Cat
19 2 18 syl φ C Cat
20 incom Ring U = U Ring
21 3 20 syl6eq φ B = U Ring
22 21 4 rhmresfn φ H Fn B × B
23 15 16 17 19 22 issubc2 φ H Subcat C H cat Hom 𝑓 C x B Id C x x H x y B z B f x H y g y H z g x y comp C z f x H z
24 10 14 23 mpbir2and φ H Subcat C