Metamath Proof Explorer

Theorem rhmsubcALTV

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) (New usage is discouraged.)

Ref Expression
Hypotheses rngcrescrhmALTV.u ⊢φ→U∈V
rngcrescrhmALTV.c ⊢C=RngCatALTV⁡U
rngcrescrhmALTV.r ⊢φ→R=Ring∩U
rngcrescrhmALTV.h ⊢H=RingHom↾R×R
Assertion rhmsubcALTV ⊢φ→H∈Subcat⁡RngCatALTV⁡U

Proof

Step Hyp Ref Expression
1 rngcrescrhmALTV.u ⊢φ→U∈V
2 rngcrescrhmALTV.c ⊢C=RngCatALTV⁡U
3 rngcrescrhmALTV.r ⊢φ→R=Ring∩U
4 rngcrescrhmALTV.h ⊢H=RingHom↾R×R
5 eqidd ⊢φ→Rng∩U=Rng∩U
6 1 3 5 rhmsscrnghm ⊢φ→RingHom↾R×R⊆catRngHom↾Rng∩U×Rng∩U
7 4 a1i ⊢φ→H=RingHom↾R×R
8 eqid ⊢RngCatALTV⁡U=RngCatALTV⁡U
9 eqid ⊢Rng∩U=Rng∩U
10 eqid ⊢Hom𝑓⁡RngCatALTV⁡U=Hom𝑓⁡RngCatALTV⁡U
11 8 9 1 10 rngchomrnghmresALTV ⊢φ→Hom𝑓⁡RngCatALTV⁡U=RngHom↾Rng∩U×Rng∩U
12 6 7 11 3brtr4d ⊢φ→H⊆catHom𝑓⁡RngCatALTV⁡U
13 1 2 3 4 rhmsubcALTVlem3 ⊢φ∧x∈R→Id⁡RngCatALTV⁡U⁡x∈xHx
14 1 2 3 4 rhmsubcALTVlem4 ⊢φ∧x∈R∧y∈R∧z∈R∧f∈xHy∧g∈yHz→gxycomp⁡RngCatALTV⁡Uzf∈xHz
15 14 ralrimivva ⊢φ∧x∈R∧y∈R∧z∈R→∀f∈xHy∀g∈yHzgxycomp⁡RngCatALTV⁡Uzf∈xHz
16 15 ralrimivva ⊢φ∧x∈R→∀y∈R∀z∈R∀f∈xHy∀g∈yHzgxycomp⁡RngCatALTV⁡Uzf∈xHz
17 13 16 jca ⊢φ∧x∈R→Id⁡RngCatALTV⁡U⁡x∈xHx∧∀y∈R∀z∈R∀f∈xHy∀g∈yHzgxycomp⁡RngCatALTV⁡Uzf∈xHz
18 17 ralrimiva ⊢φ→∀x∈RId⁡RngCatALTV⁡U⁡x∈xHx∧∀y∈R∀z∈R∀f∈xHy∀g∈yHzgxycomp⁡RngCatALTV⁡Uzf∈xHz
19 eqid ⊢Id⁡RngCatALTV⁡U=Id⁡RngCatALTV⁡U
20 eqid ⊢comp⁡RngCatALTV⁡U=comp⁡RngCatALTV⁡U
21 8 rngccatALTV ⊢U∈V→RngCatALTV⁡U∈Cat
22 1 21 syl ⊢φ→RngCatALTV⁡U∈Cat
23 1 2 3 4 rhmsubcALTVlem1 ⊢φ→HFnR×R
24 10 19 20 22 23 issubc2 ⊢φ→H∈Subcat⁡RngCatALTV⁡U↔H⊆catHom𝑓⁡RngCatALTV⁡U∧∀x∈RId⁡RngCatALTV⁡U⁡x∈xHx∧∀y∈R∀z∈R∀f∈xHy∀g∈yHzgxycomp⁡RngCatALTV⁡Uzf∈xHz
25 12 18 24 mpbir2and ⊢φ→H∈Subcat⁡RngCatALTV⁡U