Theorem ringccofval

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

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

Proof

Step	Hyp	Ref	Expression
1		ringcco.c	$$⊢C=\mathrm{RingCat}\left(U\right)$$
2		ringcco.u	$$⊢\phi \to U\in V$$
3		ringcco.o	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
4		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
5	1 4 2	ringcbas	$$⊢\phi \to {\mathrm{Base}}_C=U\cap \mathrm{Ring}$$
6		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
7	1 4 2 6	ringchomfval	$$⊢\phi \to \mathrm{Hom}\left(C\right)={\mathrm{RingHom}\upharpoonright }_{\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)}$$
8	1 2 5 7	ringcval	$$⊢\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	rhmresfn	$$⊢\phi \to \mathrm{Hom}\left(C\right)Fn\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)$$
15		inss1	$$⊢U\cap \mathrm{Ring}\subseteq U$$
16	15	a1i	$$⊢\phi \to U\cap \mathrm{Ring}\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)$$