This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )