This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rhmsubccat

Description: The restriction of the category of non-unital rings to the set of unital ring homomorphisms is a category. (Contributed by AV, 4-Mar-2020)

Ref Expression
Hypotheses rngcrescrhm.u ⊢ φ → U ∈ V
rngcrescrhm.c ⊢ C = RngCat ⁡ U
rngcrescrhm.r ⊢ φ → R = Ring ∩ U
rngcrescrhm.h ⊢ H = RingHom ↾ R × R
Assertion rhmsubccat ⊢ φ → RngCat ⁡ U ↾ cat H ∈ Cat

Proof

Step Hyp Ref Expression
1 rngcrescrhm.u ⊢ φ → U ∈ V
2 rngcrescrhm.c ⊢ C = RngCat ⁡ U
3 rngcrescrhm.r ⊢ φ → R = Ring ∩ U
4 rngcrescrhm.h ⊢ H = RingHom ↾ R × R
5 eqid ⊢ RngCat ⁡ U ↾ cat H = RngCat ⁡ U ↾ cat H
6 1 2 3 4 rhmsubc ⊢ φ → H ∈ Subcat ⁡ RngCat ⁡ U
7 5 6 subccat ⊢ φ → RngCat ⁡ U ↾ cat H ∈ Cat