Theorem rngccofval

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

	Ref	Expression
Hypotheses	rngcco.c	$$⊢C=\mathrm{RngCat}\left(U\right)$$
	rngcco.u	$$⊢\phi \to U\in V$$
	rngcco.o	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
Assertion	rngccofval	$$⊢\phi \to \underset{\dot{}}{·}=\mathrm{comp}\left(\mathrm{ExtStrCat}\left(U\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		rngcco.c	$$⊢C=\mathrm{RngCat}\left(U\right)$$
2		rngcco.u	$$⊢\phi \to U\in V$$
3		rngcco.o	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
4		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
5	1 4 2	rngcbas	$$⊢\phi \to {\mathrm{Base}}_C=U\cap \mathrm{Rng}$$
6		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
7	1 4 2 6	rngchomfval	$$⊢\phi \to \mathrm{Hom}\left(C\right)={\mathrm{RngHomo}\upharpoonright }_{\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)}$$
8	1 2 5 7	rngcval	$$⊢\phi \to C=\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\mathrm{Hom}\left(C\right)$$
9	8	fveq2d	$$⊢\phi \to \mathrm{comp}\left(C\right)=\mathrm{comp}\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\mathrm{Hom}\left(C\right)\right)$$
10	3	a1i	$$⊢\phi \to \underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
11		eqid	$$⊢\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\mathrm{Hom}\left(C\right)=\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\mathrm{Hom}\left(C\right)$$
12		eqid	$$⊢{\mathrm{Base}}_{\mathrm{ExtStrCat}\left(U\right)}={\mathrm{Base}}_{\mathrm{ExtStrCat}\left(U\right)}$$
13		fvexd	$$⊢\phi \to \mathrm{ExtStrCat}\left(U\right)\in \mathrm{V}$$
14	5 7	rnghmresfn	$$⊢\phi \to \mathrm{Hom}\left(C\right)Fn\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)$$
15		inss1	$$⊢U\cap \mathrm{Rng}\subseteq U$$
16	15	a1i	$$⊢\phi \to U\cap \mathrm{Rng}\subseteq U$$
17		eqid	$$⊢\mathrm{ExtStrCat}\left(U\right)=\mathrm{ExtStrCat}\left(U\right)$$
18	17 2	estrcbas	$$⊢\phi \to U={\mathrm{Base}}_{\mathrm{ExtStrCat}\left(U\right)}$$
19	18	eqcomd	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{ExtStrCat}\left(U\right)}=U$$
20	16 5 19	3sstr4d	$$⊢\phi \to {\mathrm{Base}}_C\subseteq {\mathrm{Base}}_{\mathrm{ExtStrCat}\left(U\right)}$$
21		eqid	$$⊢\mathrm{comp}\left(\mathrm{ExtStrCat}\left(U\right)\right)=\mathrm{comp}\left(\mathrm{ExtStrCat}\left(U\right)\right)$$
22	11 12 13 14 20 21	rescco	$$⊢\phi \to \mathrm{comp}\left(\mathrm{ExtStrCat}\left(U\right)\right)=\mathrm{comp}\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\mathrm{Hom}\left(C\right)\right)$$
23	9 10 22	3eqtr4d	$$⊢\phi \to \underset{\dot{}}{·}=\mathrm{comp}\left(\mathrm{ExtStrCat}\left(U\right)\right)$$