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}\upharpoonright }_{\left(B\times 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}\upharpoonright }_{\left(B\times B\right)}={\mathrm{RingHom}\upharpoonright }_{\left(B\times B\right)}$$
7	1 3 5 6	ringcval	$$⊢\phi \to C=\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RingHom}\upharpoonright }_{\left(B\times B\right)}\right)$$
8	7	fveq2d	$$⊢\phi \to \mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RingHom}\upharpoonright }_{\left(B\times B\right)}\right)\right)$$
9	4 8	syl5eq	$$⊢\phi \to H=\mathrm{Hom}\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RingHom}\upharpoonright }_{\left(B\times B\right)}\right)\right)$$
10		eqid	$$⊢\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RingHom}\upharpoonright }_{\left(B\times B\right)}\right)=\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RingHom}\upharpoonright }_{\left(B\times 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}\upharpoonright }_{\left(B\times B\right)}\right)Fn\left(B\times 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}\upharpoonright }_{\left(B\times B\right)}=\mathrm{Hom}\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RingHom}\upharpoonright }_{\left(B\times B\right)}\right)\right)$$
21	9 20	eqtr4d	$$⊢\phi \to H={\mathrm{RingHom}\upharpoonright }_{\left(B\times B\right)}$$