Theorem ringcco

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)$$
	ringcco.x	$$⊢\phi \to X\in U$$
	ringcco.y	$$⊢\phi \to Y\in U$$
	ringcco.z	$$⊢\phi \to Z\in U$$
	ringcco.f	$$⊢\phi \to F:{\mathrm{Base}}_X⟶{\mathrm{Base}}_Y$$
	ringcco.g	$$⊢\phi \to G:{\mathrm{Base}}_Y⟶{\mathrm{Base}}_Z$$
Assertion	ringcco	$$⊢\phi \to G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F=G\circ F$$

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		ringcco.x	$$⊢\phi \to X\in U$$
5		ringcco.y	$$⊢\phi \to Y\in U$$
6		ringcco.z	$$⊢\phi \to Z\in U$$
7		ringcco.f	$$⊢\phi \to F:{\mathrm{Base}}_X⟶{\mathrm{Base}}_Y$$
8		ringcco.g	$$⊢\phi \to G:{\mathrm{Base}}_Y⟶{\mathrm{Base}}_Z$$
9	1 2 3	ringccofval	$$⊢\phi \to \underset{\dot{}}{·}=\mathrm{comp}\left(\mathrm{ExtStrCat}\left(U\right)\right)$$
10	9	oveqd	$$⊢\phi \to ⟨X,Y⟩\underset{\dot{}}{·}Z=⟨X,Y⟩\mathrm{comp}\left(\mathrm{ExtStrCat}\left(U\right)\right)Z$$
11	10	oveqd	$$⊢\phi \to G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F=G\left(⟨X,Y⟩\mathrm{comp}\left(\mathrm{ExtStrCat}\left(U\right)\right)Z\right)F$$
12		eqid	$$⊢\mathrm{ExtStrCat}\left(U\right)=\mathrm{ExtStrCat}\left(U\right)$$
13		eqid	$$⊢\mathrm{comp}\left(\mathrm{ExtStrCat}\left(U\right)\right)=\mathrm{comp}\left(\mathrm{ExtStrCat}\left(U\right)\right)$$
14		eqid	$$⊢{\mathrm{Base}}_X={\mathrm{Base}}_X$$
15		eqid	$$⊢{\mathrm{Base}}_Y={\mathrm{Base}}_Y$$
16		eqid	$$⊢{\mathrm{Base}}_Z={\mathrm{Base}}_Z$$
17	12 2 13 4 5 6 14 15 16 7 8	estrcco	$$⊢\phi \to G\left(⟨X,Y⟩\mathrm{comp}\left(\mathrm{ExtStrCat}\left(U\right)\right)Z\right)F=G\circ F$$
18	11 17	eqtrd	$$⊢\phi \to G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F=G\circ F$$