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

Proof

Step	Hyp	Ref	Expression
1		ringcco.c	|- C = ( RingCat ` U )
2		ringcco.u	|- ( ph -> U e. V )
3		ringcco.o	|- .x. = ( comp ` C )
4		ringcco.x	|- ( ph -> X e. U )
5		ringcco.y	|- ( ph -> Y e. U )
6		ringcco.z	|- ( ph -> Z e. U )
7		ringcco.f	|- ( ph -> F : ( Base ` X ) --> ( Base ` Y ) )
8		ringcco.g	|- ( ph -> G : ( Base ` Y ) --> ( Base ` Z ) )
9	1 2 3	ringccofval	|- ( 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 ) )