Metamath Proof Explorer


Theorem rngcrescrhmALTV

Description: The category of non-unital rings (in a universe) restricted to the ring homomorphisms between unital rings (in the same universe). (Contributed by AV, 1-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 rngcrescrhmALTV φ C cat H = C 𝑠 R sSet Hom ndx H

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 eqid C cat H = C cat H
6 2 fvexi C V
7 6 a1i φ C V
8 incom Ring U = U Ring
9 3 8 eqtrdi φ R = U Ring
10 inex1g U V U Ring V
11 1 10 syl φ U Ring V
12 9 11 eqeltrd φ R V
13 inss1 Ring U Ring
14 3 13 eqsstrdi φ R Ring
15 xpss12 R Ring R Ring R × R Ring × Ring
16 14 14 15 syl2anc φ R × R Ring × Ring
17 rhmfn RingHom Fn Ring × Ring
18 fnssresb RingHom Fn Ring × Ring RingHom R × R Fn R × R R × R Ring × Ring
19 17 18 mp1i φ RingHom R × R Fn R × R R × R Ring × Ring
20 16 19 mpbird φ RingHom R × R Fn R × R
21 4 fneq1i H Fn R × R RingHom R × R Fn R × R
22 20 21 sylibr φ H Fn R × R
23 5 7 12 22 rescval2 φ C cat H = C 𝑠 R sSet Hom ndx H