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{RngHom}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{RngHom}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{RngHom}\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		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)$$
15		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)}$$
16	1 4 8 12	rngcval	$$⊢\phi \to R=\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\mathrm{Hom}\left(R\right)$$
17	16	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\mathrm{Hom}\left(R\right)\right)}$$
18	3 17	eqtrid	$$⊢\phi \to B={\mathrm{Base}}_{\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\mathrm{Hom}\left(R\right)\right)}$$
19	18	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)}}$$
20	5 19	eqtrd	$$⊢\phi \to F={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_{\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\mathrm{Hom}\left(R\right)\right)}}$$
21	18	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)}$$
22	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{RngHom}\upharpoonright }_{\left(B\times B\right)}\right)y$$
23		ovres	$$⊢\left(x\in B\wedge y\in B\right)\to x\left({\mathrm{RngHom}\upharpoonright }_{\left(B\times B\right)}\right)y=x\mathrm{RngHom}y$$
24	23	adantl	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x\left({\mathrm{RngHom}\upharpoonright }_{\left(B\times B\right)}\right)y=x\mathrm{RngHom}y$$
25	22 24	eqtr2d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x\mathrm{RngHom}y=x\mathrm{Hom}\left(R\right)y$$
26	25	reseq2d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to {\mathrm{I}\upharpoonright }_{\left(x\mathrm{RngHom}y\right)}={\mathrm{I}\upharpoonright }_{\left(x\mathrm{Hom}\left(R\right)y\right)}$$
27	18 21 26	mpoeq123dva	$$⊢\phi \to \left(x\in B,y\in B⟼{\mathrm{I}\upharpoonright }_{\left(x\mathrm{RngHom}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)$$
28	6 27	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)$$
29	13 14 15 20 28	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$$
30	2	a1i	$$⊢\phi \to E=\mathrm{ExtStrCat}\left(U\right)$$
31	16 30	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)$$
32	31	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)$$
33	29 32	mpbird	$$⊢\phi \to F\left(R\mathrm{Func}E\right)G$$