Theorem rngchomrnghmresALTV

Description: The value of the functionalized Hom-set operation in the category of non-unital rings (in a universe) as restriction of the non-unital ring homomorphisms. (Contributed by AV, 2-Mar-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	rngchomrnghmresALTV.c	$$⊢C=\mathrm{RngCatALTV}\left(U\right)$$
	rngchomrnghmresALTV.b	$$⊢B=\mathrm{Rng}\cap U$$
	rngchomrnghmresALTV.u	$$⊢\phi \to U\in V$$
	rngchomrnghmresALTV.f	$$⊢F={\mathrm{Hom}}_{𝑓}\left(C\right)$$
Assertion	rngchomrnghmresALTV	$$⊢\phi \to F={\mathrm{RngHomo}\upharpoonright }_{\left(B\times B\right)}$$

Proof

Step	Hyp	Ref	Expression
1		rngchomrnghmresALTV.c	$$⊢C=\mathrm{RngCatALTV}\left(U\right)$$
2		rngchomrnghmresALTV.b	$$⊢B=\mathrm{Rng}\cap U$$
3		rngchomrnghmresALTV.u	$$⊢\phi \to U\in V$$
4		rngchomrnghmresALTV.f	$$⊢F={\mathrm{Hom}}_{𝑓}\left(C\right)$$
5		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
6	1 5 3	rngcbasALTV	$$⊢\phi \to {\mathrm{Base}}_C=U\cap \mathrm{Rng}$$
7		inss2	$$⊢U\cap \mathrm{Rng}\subseteq \mathrm{Rng}$$
8	6 7	eqsstrdi	$$⊢\phi \to {\mathrm{Base}}_C\subseteq \mathrm{Rng}$$
9		resmpo	$$⊢\left({\mathrm{Base}}_C\subseteq \mathrm{Rng}\wedge {\mathrm{Base}}_C\subseteq \mathrm{Rng}\right)\to {\left(x\in \mathrm{Rng},y\in \mathrm{Rng}⟼x\mathrm{RngHomo}y\right)\upharpoonright }_{\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)}=\left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼x\mathrm{RngHomo}y\right)$$
10	8 8 9	syl2anc	$$⊢\phi \to {\left(x\in \mathrm{Rng},y\in \mathrm{Rng}⟼x\mathrm{RngHomo}y\right)\upharpoonright }_{\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)}=\left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼x\mathrm{RngHomo}y\right)$$
11		df-rnghomo	$$⊢\mathrm{RngHomo}=\left(r\in \mathrm{Rng},s\in \mathrm{Rng}⟼⦋{\mathrm{Base}}_r/v⦌⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\forall x\in v\forall y\in v\left(f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)\right\}\right)$$
12		ovex	$$⊢w^v\in \mathrm{V}$$
13	12	rabex	$$⊢\left\{f\in \left(w^v\right)|\forall x\in v\forall y\in v\left(f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)\right\}\in \mathrm{V}$$
14	13	csbex	$$⊢⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\forall x\in v\forall y\in v\left(f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)\right\}\in \mathrm{V}$$
15	14	csbex	$$⊢⦋{\mathrm{Base}}_r/v⦌⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\forall x\in v\forall y\in v\left(f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)\right\}\in \mathrm{V}$$
16	11 15	fnmpoi	$$⊢\mathrm{RngHomo}Fn\left(\mathrm{Rng}\times \mathrm{Rng}\right)$$
17	16	a1i	$$⊢\phi \to \mathrm{RngHomo}Fn\left(\mathrm{Rng}\times \mathrm{Rng}\right)$$
18		fnov	$$⊢\mathrm{RngHomo}Fn\left(\mathrm{Rng}\times \mathrm{Rng}\right)\leftrightarrow \mathrm{RngHomo}=\left(x\in \mathrm{Rng},y\in \mathrm{Rng}⟼x\mathrm{RngHomo}y\right)$$
19	17 18	sylib	$$⊢\phi \to \mathrm{RngHomo}=\left(x\in \mathrm{Rng},y\in \mathrm{Rng}⟼x\mathrm{RngHomo}y\right)$$
20		incom	$$⊢U\cap \mathrm{Rng}=\mathrm{Rng}\cap U$$
21	20	a1i	$$⊢\phi \to U\cap \mathrm{Rng}=\mathrm{Rng}\cap U$$
22	2	a1i	$$⊢\phi \to B=\mathrm{Rng}\cap U$$
23	21 6 22	3eqtr4rd	$$⊢\phi \to B={\mathrm{Base}}_C$$
24	23	sqxpeqd	$$⊢\phi \to B\times B={\mathrm{Base}}_C\times {\mathrm{Base}}_C$$
25	19 24	reseq12d	$$⊢\phi \to {\mathrm{RngHomo}\upharpoonright }_{\left(B\times B\right)}={\left(x\in \mathrm{Rng},y\in \mathrm{Rng}⟼x\mathrm{RngHomo}y\right)\upharpoonright }_{\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)}$$
26	1 5 3 4	rngchomffvalALTV	$$⊢\phi \to F=\left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼x\mathrm{RngHomo}y\right)$$
27	10 25 26	3eqtr4rd	$$⊢\phi \to F={\mathrm{RngHomo}\upharpoonright }_{\left(B\times B\right)}$$