Theorem rngchomfval

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

	Ref	Expression
Hypotheses	rngcbas.c	$$⊢C=\mathrm{RngCat}\left(U\right)$$
	rngcbas.b	$$⊢B={\mathrm{Base}}_C$$
	rngcbas.u	$$⊢\phi \to U\in V$$
	rngchomfval.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
Assertion	rngchomfval	$$⊢\phi \to H={\mathrm{RngHom}\upharpoonright }_{\left(B\times B\right)}$$

Proof

Step	Hyp	Ref	Expression
1		rngcbas.c	$$⊢C=\mathrm{RngCat}\left(U\right)$$
2		rngcbas.b	$$⊢B={\mathrm{Base}}_C$$
3		rngcbas.u	$$⊢\phi \to U\in V$$
4		rngchomfval.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
5	1 2 3	rngcbas	$$⊢\phi \to B=U\cap \mathrm{Rng}$$
6		eqidd	$$⊢\phi \to {\mathrm{RngHom}\upharpoonright }_{\left(B\times B\right)}={\mathrm{RngHom}\upharpoonright }_{\left(B\times B\right)}$$
7	1 3 5 6	rngcval	$$⊢\phi \to C=\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RngHom}\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{RngHom}\upharpoonright }_{\left(B\times B\right)}\right)\right)$$
9	4 8	eqtrid	$$⊢\phi \to H=\mathrm{Hom}\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RngHom}\upharpoonright }_{\left(B\times B\right)}\right)\right)$$
10		eqid	$$⊢\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RngHom}\upharpoonright }_{\left(B\times B\right)}\right)=\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RngHom}\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	rnghmresfn	$$⊢\phi \to \left({\mathrm{RngHom}\upharpoonright }_{\left(B\times B\right)}\right)Fn\left(B\times B\right)$$
14		inss1	$$⊢U\cap \mathrm{Rng}\subseteq U$$
15	14	a1i	$$⊢\phi \to U\cap \mathrm{Rng}\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{RngHom}\upharpoonright }_{\left(B\times B\right)}=\mathrm{Hom}\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RngHom}\upharpoonright }_{\left(B\times B\right)}\right)\right)$$
21	9 20	eqtr4d	$$⊢\phi \to H={\mathrm{RngHom}\upharpoonright }_{\left(B\times B\right)}$$