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 = ( RngCat ` U )
	rngcco.u	|- ( ph -> U e. V )
	rngcco.o	|- .x. = ( comp ` C )
	rngcco.x	|- ( ph -> X e. U )
	rngcco.y	|- ( ph -> Y e. U )
	rngcco.z	|- ( ph -> Z e. U )
	rngcco.f	|- ( ph -> F : ( Base ` X ) --> ( Base ` Y ) )
	rngcco.g	|- ( ph -> G : ( Base ` Y ) --> ( Base ` Z ) )
Assertion	rngcco	|- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) = ( G o. F ) )

Proof

Step	Hyp	Ref	Expression
1		rngcco.c	|- C = ( RngCat ` U )
2		rngcco.u	|- ( ph -> U e. V )
3		rngcco.o	|- .x. = ( comp ` C )
4		rngcco.x	|- ( ph -> X e. U )
5		rngcco.y	|- ( ph -> Y e. U )
6		rngcco.z	|- ( ph -> Z e. U )
7		rngcco.f	|- ( ph -> F : ( Base ` X ) --> ( Base ` Y ) )
8		rngcco.g	|- ( ph -> G : ( Base ` Y ) --> ( Base ` Z ) )
9	1 2 3	rngccofval	|- ( ph -> .x. = ( comp ` ( ExtStrCat ` U ) ) )
10	9	oveqd	|- ( ph -> ( <. X , Y >. .x. Z ) = ( <. X , Y >. ( comp ` ( ExtStrCat ` U ) ) Z ) )
11	10	oveqd	|- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) = ( G ( <. X , Y >. ( comp ` ( ExtStrCat ` U ) ) Z ) F ) )
12		eqid	|- ( ExtStrCat ` U ) = ( ExtStrCat ` U )
13		eqid	|- ( comp ` ( ExtStrCat ` U ) ) = ( comp ` ( ExtStrCat ` U ) )
14		eqid	|- ( Base ` X ) = ( Base ` X )
15		eqid	|- ( Base ` Y ) = ( Base ` Y )
16		eqid	|- ( Base ` Z ) = ( Base ` Z )
17	12 2 13 4 5 6 14 15 16 7 8	estrcco	|- ( ph -> ( G ( <. X , Y >. ( comp ` ( ExtStrCat ` U ) ) Z ) F ) = ( G o. F ) )
18	11 17	eqtrd	|- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) = ( G o. F ) )