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

Metamath Proof Explorer

Theorem oppcco

Description: Composition in the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses oppcco.b 
|- B = ( Base ` C )
oppcco.c 
|- .x. = ( comp ` C )
oppcco.o 
|- O = ( oppCat ` C )
oppcco.x 
|- ( ph -> X e. B )
oppcco.y 
|- ( ph -> Y e. B )
oppcco.z 
|- ( ph -> Z e. B )
Assertion oppcco 
|- ( ph -> ( G ( <. X , Y >. ( comp ` O ) Z ) F ) = ( F ( <. Z , Y >. .x. X ) G ) )

Proof

Step Hyp Ref Expression
1 oppcco.b 
 |-  B = ( Base ` C )
2 oppcco.c 
 |-  .x. = ( comp ` C )
3 oppcco.o 
 |-  O = ( oppCat ` C )
4 oppcco.x 
 |-  ( ph -> X e. B )
5 oppcco.y 
 |-  ( ph -> Y e. B )
6 oppcco.z 
 |-  ( ph -> Z e. B )
7 1 2 3 4 5 6 oppccofval 
 |-  ( ph -> ( <. X , Y >. ( comp ` O ) Z ) = tpos ( <. Z , Y >. .x. X ) )
8 7 oveqd 
 |-  ( ph -> ( G ( <. X , Y >. ( comp ` O ) Z ) F ) = ( G tpos ( <. Z , Y >. .x. X ) F ) )
9 ovtpos 
 |-  ( G tpos ( <. Z , Y >. .x. X ) F ) = ( F ( <. Z , Y >. .x. X ) G )
10 8 9 eqtrdi 
 |-  ( ph -> ( G ( <. X , Y >. ( comp ` O ) Z ) F ) = ( F ( <. Z , Y >. .x. X ) G ) )