# Metamath Proof Explorer

## Theorem ringchomfval

Description: Set of arrows of the category of unital rings (in a universe). (Contributed by AV, 14-Feb-2020) (Revised by AV, 8-Mar-2020)

Ref Expression
Hypotheses ringcbas.c ${⊢}{C}=\mathrm{RingCat}\left({U}\right)$
ringcbas.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
ringcbas.u ${⊢}{\phi }\to {U}\in {V}$
ringchomfval.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
Assertion ringchomfval ${⊢}{\phi }\to {H}={\mathrm{RingHom}↾}_{\left({B}×{B}\right)}$

### Proof

Step Hyp Ref Expression
1 ringcbas.c ${⊢}{C}=\mathrm{RingCat}\left({U}\right)$
2 ringcbas.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
3 ringcbas.u ${⊢}{\phi }\to {U}\in {V}$
4 ringchomfval.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
5 1 2 3 ringcbas ${⊢}{\phi }\to {B}={U}\cap \mathrm{Ring}$
6 eqidd ${⊢}{\phi }\to {\mathrm{RingHom}↾}_{\left({B}×{B}\right)}={\mathrm{RingHom}↾}_{\left({B}×{B}\right)}$
7 1 3 5 6 ringcval ${⊢}{\phi }\to {C}=\mathrm{ExtStrCat}\left({U}\right){↾}_{\mathrm{cat}}\left({\mathrm{RingHom}↾}_{\left({B}×{B}\right)}\right)$
8 7 fveq2d ${⊢}{\phi }\to \mathrm{Hom}\left({C}\right)=\mathrm{Hom}\left(\mathrm{ExtStrCat}\left({U}\right){↾}_{\mathrm{cat}}\left({\mathrm{RingHom}↾}_{\left({B}×{B}\right)}\right)\right)$
9 4 8 syl5eq ${⊢}{\phi }\to {H}=\mathrm{Hom}\left(\mathrm{ExtStrCat}\left({U}\right){↾}_{\mathrm{cat}}\left({\mathrm{RingHom}↾}_{\left({B}×{B}\right)}\right)\right)$
10 eqid ${⊢}\mathrm{ExtStrCat}\left({U}\right){↾}_{\mathrm{cat}}\left({\mathrm{RingHom}↾}_{\left({B}×{B}\right)}\right)=\mathrm{ExtStrCat}\left({U}\right){↾}_{\mathrm{cat}}\left({\mathrm{RingHom}↾}_{\left({B}×{B}\right)}\right)$
11 eqid ${⊢}{\mathrm{Base}}_{\mathrm{ExtStrCat}\left({U}\right)}={\mathrm{Base}}_{\mathrm{ExtStrCat}\left({U}\right)}$
12 fvexd ${⊢}{\phi }\to \mathrm{ExtStrCat}\left({U}\right)\in \mathrm{V}$
13 5 6 rhmresfn ${⊢}{\phi }\to \left({\mathrm{RingHom}↾}_{\left({B}×{B}\right)}\right)Fn\left({B}×{B}\right)$
14 inss1 ${⊢}{U}\cap \mathrm{Ring}\subseteq {U}$
15 14 a1i ${⊢}{\phi }\to {U}\cap \mathrm{Ring}\subseteq {U}$
16 eqid ${⊢}\mathrm{ExtStrCat}\left({U}\right)=\mathrm{ExtStrCat}\left({U}\right)$
17 16 3 estrcbas ${⊢}{\phi }\to {U}={\mathrm{Base}}_{\mathrm{ExtStrCat}\left({U}\right)}$
18 17 eqcomd ${⊢}{\phi }\to {\mathrm{Base}}_{\mathrm{ExtStrCat}\left({U}\right)}={U}$
19 15 5 18 3sstr4d ${⊢}{\phi }\to {B}\subseteq {\mathrm{Base}}_{\mathrm{ExtStrCat}\left({U}\right)}$
20 10 11 12 13 19 reschom ${⊢}{\phi }\to {\mathrm{RingHom}↾}_{\left({B}×{B}\right)}=\mathrm{Hom}\left(\mathrm{ExtStrCat}\left({U}\right){↾}_{\mathrm{cat}}\left({\mathrm{RingHom}↾}_{\left({B}×{B}\right)}\right)\right)$
21 9 20 eqtr4d ${⊢}{\phi }\to {H}={\mathrm{RingHom}↾}_{\left({B}×{B}\right)}$