Theorem rngcifuestrc

Description: The "inclusion functor" from the category of non-unital rings into the category of extensible structures. (Contributed by AV, 30-Mar-2020)

	Ref	Expression
Hypotheses	rngcifuestrc.r	$$⊢R=\mathrm{RngCat}\left(U\right)$$
	rngcifuestrc.e	$$⊢E=\mathrm{ExtStrCat}\left(U\right)$$
	rngcifuestrc.b	$$⊢B={\mathrm{Base}}_R$$
	rngcifuestrc.u	$$⊢\phi \to U\in V$$
	rngcifuestrc.f	$$⊢\phi \to F={\mathrm{I}\upharpoonright }_B$$
	rngcifuestrc.g	$$⊢\phi \to G=\left(x\in B,y\in B⟼{\mathrm{I}\upharpoonright }_{\left(x\mathrm{RngHomo}y\right)}\right)$$
Assertion	rngcifuestrc	$$⊢\phi \to F\left(R\mathrm{Func}E\right)G$$

Proof

Step	Hyp	Ref	Expression
1		rngcifuestrc.r	$$⊢R=\mathrm{RngCat}\left(U\right)$$
2		rngcifuestrc.e	$$⊢E=\mathrm{ExtStrCat}\left(U\right)$$
3		rngcifuestrc.b	$$⊢B={\mathrm{Base}}_R$$
4		rngcifuestrc.u	$$⊢\phi \to U\in V$$
5		rngcifuestrc.f	$$⊢\phi \to F={\mathrm{I}\upharpoonright }_B$$
6		rngcifuestrc.g	$$⊢\phi \to G=\left(x\in B,y\in B⟼{\mathrm{I}\upharpoonright }_{\left(x\mathrm{RngHomo}y\right)}\right)$$
7		eqid	$$⊢\mathrm{ExtStrCat}\left(U\right)=\mathrm{ExtStrCat}\left(U\right)$$
8	1 3 4	rngcbas	$$⊢\phi \to B=U\cap \mathrm{Rng}$$
9		incom	$$⊢U\cap \mathrm{Rng}=\mathrm{Rng}\cap U$$
10	8 9	eqtrdi	$$⊢\phi \to B=\mathrm{Rng}\cap U$$
11		eqid	$$⊢\mathrm{Hom}\left(R\right)=\mathrm{Hom}\left(R\right)$$
12	1 3 4 11	rngchomfval	$$⊢\phi \to \mathrm{Hom}\left(R\right)={\mathrm{RngHomo}\upharpoonright }_{\left(B\times B\right)}$$
13	7 4 10 12	rnghmsubcsetc	$$⊢\phi \to \mathrm{Hom}\left(R\right)\in \mathrm{Subcat}\left(\mathrm{ExtStrCat}\left(U\right)\right)$$
14	13	idi	$$⊢\phi \to \mathrm{Hom}\left(R\right)\in \mathrm{Subcat}\left(\mathrm{ExtStrCat}\left(U\right)\right)$$
15		eqid	$$⊢\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\mathrm{Hom}\left(R\right)=\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\mathrm{Hom}\left(R\right)$$
16		eqid	$$⊢{\mathrm{Base}}_{\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\mathrm{Hom}\left(R\right)\right)}={\mathrm{Base}}_{\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\mathrm{Hom}\left(R\right)\right)}$$
17	1 4 8 12	rngcval	$$⊢\phi \to R=\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\mathrm{Hom}\left(R\right)$$
18	17	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\mathrm{Hom}\left(R\right)\right)}$$
19	3 18	syl5eq	$$⊢\phi \to B={\mathrm{Base}}_{\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\mathrm{Hom}\left(R\right)\right)}$$
20	19	reseq2d	$$⊢\phi \to {\mathrm{I}\upharpoonright }_B={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_{\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\mathrm{Hom}\left(R\right)\right)}}$$
21	5 20	eqtrd	$$⊢\phi \to F={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_{\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\mathrm{Hom}\left(R\right)\right)}}$$
22	19	adantr	$$⊢\left(\phi \wedge x\in B\right)\to B={\mathrm{Base}}_{\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\mathrm{Hom}\left(R\right)\right)}$$
23	12	oveqdr	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x\mathrm{Hom}\left(R\right)y=x\left({\mathrm{RngHomo}\upharpoonright }_{\left(B\times B\right)}\right)y$$
24		ovres	$$⊢\left(x\in B\wedge y\in B\right)\to x\left({\mathrm{RngHomo}\upharpoonright }_{\left(B\times B\right)}\right)y=x\mathrm{RngHomo}y$$
25	24	adantl	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x\left({\mathrm{RngHomo}\upharpoonright }_{\left(B\times B\right)}\right)y=x\mathrm{RngHomo}y$$
26	23 25	eqtr2d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x\mathrm{RngHomo}y=x\mathrm{Hom}\left(R\right)y$$
27	26	reseq2d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to {\mathrm{I}\upharpoonright }_{\left(x\mathrm{RngHomo}y\right)}={\mathrm{I}\upharpoonright }_{\left(x\mathrm{Hom}\left(R\right)y\right)}$$
28	19 22 27	mpoeq123dva	$$⊢\phi \to \left(x\in B,y\in B⟼{\mathrm{I}\upharpoonright }_{\left(x\mathrm{RngHomo}y\right)}\right)=\left(x\in {\mathrm{Base}}_{\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\mathrm{Hom}\left(R\right)\right)},y\in {\mathrm{Base}}_{\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\mathrm{Hom}\left(R\right)\right)}⟼{\mathrm{I}\upharpoonright }_{\left(x\mathrm{Hom}\left(R\right)y\right)}\right)$$
29	6 28	eqtrd	$$⊢\phi \to G=\left(x\in {\mathrm{Base}}_{\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\mathrm{Hom}\left(R\right)\right)},y\in {\mathrm{Base}}_{\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\mathrm{Hom}\left(R\right)\right)}⟼{\mathrm{I}\upharpoonright }_{\left(x\mathrm{Hom}\left(R\right)y\right)}\right)$$
30	14 15 16 21 29	inclfusubc	$$⊢\phi \to F\left(\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\mathrm{Hom}\left(R\right)\right)\mathrm{Func}\mathrm{ExtStrCat}\left(U\right)\right)G$$
31	2	a1i	$$⊢\phi \to E=\mathrm{ExtStrCat}\left(U\right)$$
32	17 31	oveq12d	$$⊢\phi \to R\mathrm{Func}E=\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\mathrm{Hom}\left(R\right)\right)\mathrm{Func}\mathrm{ExtStrCat}\left(U\right)$$
33	32	breqd	$$⊢\phi \to \left(F\left(R\mathrm{Func}E\right)G\leftrightarrow F\left(\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\mathrm{Hom}\left(R\right)\right)\mathrm{Func}\mathrm{ExtStrCat}\left(U\right)\right)G\right)$$
34	30 33	mpbird	$$⊢\phi \to F\left(R\mathrm{Func}E\right)G$$