Metamath Proof Explorer


Theorem rhmsubc

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 unital ring homomorphisms is a "subcategory" of the category of non-unital rings. (Contributed by AV, 2-Mar-2020)

Ref Expression
Hypotheses rngcrescrhm.u φUV
rngcrescrhm.c C=RngCatU
rngcrescrhm.r φR=RingU
rngcrescrhm.h H=RingHomR×R
Assertion rhmsubc φHSubcatRngCatU

Proof

Step Hyp Ref Expression
1 rngcrescrhm.u φUV
2 rngcrescrhm.c C=RngCatU
3 rngcrescrhm.r φR=RingU
4 rngcrescrhm.h H=RingHomR×R
5 eqidd φRngU=RngU
6 1 3 5 rhmsscrnghm φRingHomR×RcatRngHomoRngU×RngU
7 4 a1i φH=RingHomR×R
8 2 a1i φC=RngCatU
9 8 eqcomd φRngCatU=C
10 9 fveq2d φHom𝑓RngCatU=Hom𝑓C
11 eqid BaseC=BaseC
12 2 11 1 rngchomfeqhom φHom𝑓C=HomC
13 eqid HomC=HomC
14 2 11 1 13 rngchomfval φHomC=RngHomoBaseC×BaseC
15 2 11 1 rngcbas φBaseC=URng
16 incom URng=RngU
17 15 16 eqtrdi φBaseC=RngU
18 17 sqxpeqd φBaseC×BaseC=RngU×RngU
19 18 reseq2d φRngHomoBaseC×BaseC=RngHomoRngU×RngU
20 14 19 eqtrd φHomC=RngHomoRngU×RngU
21 10 12 20 3eqtrd φHom𝑓RngCatU=RngHomoRngU×RngU
22 6 7 21 3brtr4d φHcatHom𝑓RngCatU
23 1 2 3 4 rhmsubclem3 φxRIdRngCatUxxHx
24 1 2 3 4 rhmsubclem4 φxRyRzRfxHygyHzgxycompRngCatUzfxHz
25 24 ralrimivva φxRyRzRfxHygyHzgxycompRngCatUzfxHz
26 25 ralrimivva φxRyRzRfxHygyHzgxycompRngCatUzfxHz
27 23 26 jca φxRIdRngCatUxxHxyRzRfxHygyHzgxycompRngCatUzfxHz
28 27 ralrimiva φxRIdRngCatUxxHxyRzRfxHygyHzgxycompRngCatUzfxHz
29 eqid Hom𝑓RngCatU=Hom𝑓RngCatU
30 eqid IdRngCatU=IdRngCatU
31 eqid compRngCatU=compRngCatU
32 eqid RngCatU=RngCatU
33 32 rngccat UVRngCatUCat
34 1 33 syl φRngCatUCat
35 1 2 3 4 rhmsubclem1 φHFnR×R
36 29 30 31 34 35 issubc2 φHSubcatRngCatUHcatHom𝑓RngCatUxRIdRngCatUxxHxyRzRfxHygyHzgxycompRngCatUzfxHz
37 22 28 36 mpbir2and φHSubcatRngCatU