Theorem rngcco

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

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		rngcco.x	$$⊢\phi \to X\in U$$
5		rngcco.y	$$⊢\phi \to Y\in U$$
6		rngcco.z	$$⊢\phi \to Z\in U$$
7		rngcco.f	$$⊢\phi \to F:{\mathrm{Base}}_X⟶{\mathrm{Base}}_Y$$
8		rngcco.g	$$⊢\phi \to G:{\mathrm{Base}}_Y⟶{\mathrm{Base}}_Z$$
9	1 2 3	rngccofval	$$⊢\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$$