# 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}=\mathrm{ExtStrCat}\left({U}\right)$
rhmsubcsetc.u ${⊢}{\phi }\to {U}\in {V}$
rhmsubcsetc.b ${⊢}{\phi }\to {B}=\mathrm{Ring}\cap {U}$
rhmsubcsetc.h ${⊢}{\phi }\to {H}={\mathrm{RingHom}↾}_{\left({B}×{B}\right)}$
Assertion rhmsubcsetc ${⊢}{\phi }\to {H}\in \mathrm{Subcat}\left({C}\right)$

### Proof

Step Hyp Ref Expression
1 rhmsubcsetc.c ${⊢}{C}=\mathrm{ExtStrCat}\left({U}\right)$
2 rhmsubcsetc.u ${⊢}{\phi }\to {U}\in {V}$
3 rhmsubcsetc.b ${⊢}{\phi }\to {B}=\mathrm{Ring}\cap {U}$
4 rhmsubcsetc.h ${⊢}{\phi }\to {H}={\mathrm{RingHom}↾}_{\left({B}×{B}\right)}$
5 2 3 rhmsscmap ${⊢}{\phi }\to \left({\mathrm{RingHom}↾}_{\left({B}×{B}\right)}\right){\subseteq }_{\mathrm{cat}}\left({x}\in {U},{y}\in {U}⟼{{\mathrm{Base}}_{{y}}}^{{\mathrm{Base}}_{{x}}}\right)$
6 eqid ${⊢}\mathrm{Hom}\left({C}\right)=\mathrm{Hom}\left({C}\right)$
7 1 2 6 estrchomfeqhom ${⊢}{\phi }\to {\mathrm{Hom}}_{𝑓}\left({C}\right)=\mathrm{Hom}\left({C}\right)$
8 1 2 6 estrchomfval ${⊢}{\phi }\to \mathrm{Hom}\left({C}\right)=\left({x}\in {U},{y}\in {U}⟼{{\mathrm{Base}}_{{y}}}^{{\mathrm{Base}}_{{x}}}\right)$
9 7 8 eqtrd ${⊢}{\phi }\to {\mathrm{Hom}}_{𝑓}\left({C}\right)=\left({x}\in {U},{y}\in {U}⟼{{\mathrm{Base}}_{{y}}}^{{\mathrm{Base}}_{{x}}}\right)$
10 5 4 9 3brtr4d ${⊢}{\phi }\to {H}{\subseteq }_{\mathrm{cat}}{\mathrm{Hom}}_{𝑓}\left({C}\right)$
11 1 2 3 4 rhmsubcsetclem1 ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to \mathrm{Id}\left({C}\right)\left({x}\right)\in \left({x}{H}{x}\right)$
12 1 2 3 4 rhmsubcsetclem2 ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({x}{H}{y}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}{H}{z}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\in \left({x}{H}{z}\right)$
13 11 12 jca ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to \left(\mathrm{Id}\left({C}\right)\left({x}\right)\in \left({x}{H}{x}\right)\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({x}{H}{y}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}{H}{z}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\in \left({x}{H}{z}\right)\right)$
14 13 ralrimiva ${⊢}{\phi }\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Id}\left({C}\right)\left({x}\right)\in \left({x}{H}{x}\right)\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({x}{H}{y}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}{H}{z}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\in \left({x}{H}{z}\right)\right)$
15 eqid ${⊢}{\mathrm{Hom}}_{𝑓}\left({C}\right)={\mathrm{Hom}}_{𝑓}\left({C}\right)$
16 eqid ${⊢}\mathrm{Id}\left({C}\right)=\mathrm{Id}\left({C}\right)$
17 eqid ${⊢}\mathrm{comp}\left({C}\right)=\mathrm{comp}\left({C}\right)$
18 1 estrccat ${⊢}{U}\in {V}\to {C}\in \mathrm{Cat}$
19 2 18 syl ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
20 incom ${⊢}\mathrm{Ring}\cap {U}={U}\cap \mathrm{Ring}$
21 3 20 syl6eq ${⊢}{\phi }\to {B}={U}\cap \mathrm{Ring}$
22 21 4 rhmresfn ${⊢}{\phi }\to {H}Fn\left({B}×{B}\right)$
23 15 16 17 19 22 issubc2 ${⊢}{\phi }\to \left({H}\in \mathrm{Subcat}\left({C}\right)↔\left({H}{\subseteq }_{\mathrm{cat}}{\mathrm{Hom}}_{𝑓}\left({C}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Id}\left({C}\right)\left({x}\right)\in \left({x}{H}{x}\right)\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({x}{H}{y}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}{H}{z}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\in \left({x}{H}{z}\right)\right)\right)\right)$
24 10 14 23 mpbir2and ${⊢}{\phi }\to {H}\in \mathrm{Subcat}\left({C}\right)$