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

Metamath Proof Explorer

Theorem xpcco2nd

Description: Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses xpcco1st.t 
|- T = ( C Xc. D )
xpcco1st.b 
|- B = ( Base ` T )
xpcco1st.k 
|- K = ( Hom ` T )
xpcco1st.o 
|- O = ( comp ` T )
xpcco1st.x 
|- ( ph -> X e. B )
xpcco1st.y 
|- ( ph -> Y e. B )
xpcco1st.z 
|- ( ph -> Z e. B )
xpcco1st.f 
|- ( ph -> F e. ( X K Y ) )
xpcco1st.g 
|- ( ph -> G e. ( Y K Z ) )
xpcco2nd.1 
|- .x. = ( comp ` D )
Assertion xpcco2nd 
|- ( ph -> ( 2nd ` ( G ( <. X , Y >. O Z ) F ) ) = ( ( 2nd ` G ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. .x. ( 2nd ` Z ) ) ( 2nd ` F ) ) )

Proof

Step Hyp Ref Expression
1 xpcco1st.t 
 |-  T = ( C Xc. D )
2 xpcco1st.b 
 |-  B = ( Base ` T )
3 xpcco1st.k 
 |-  K = ( Hom ` T )
4 xpcco1st.o 
 |-  O = ( comp ` T )
5 xpcco1st.x 
 |-  ( ph -> X e. B )
6 xpcco1st.y 
 |-  ( ph -> Y e. B )
7 xpcco1st.z 
 |-  ( ph -> Z e. B )
8 xpcco1st.f 
 |-  ( ph -> F e. ( X K Y ) )
9 xpcco1st.g 
 |-  ( ph -> G e. ( Y K Z ) )
10 xpcco2nd.1 
 |-  .x. = ( comp ` D )
11 eqid 
 |-  ( comp ` C ) = ( comp ` C )
12 1 2 3 11 10 4 5 6 7 8 9 xpcco 
 |-  ( ph -> ( G ( <. X , Y >. O Z ) F ) = <. ( ( 1st ` G ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. ( comp ` C ) ( 1st ` Z ) ) ( 1st ` F ) ) , ( ( 2nd ` G ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. .x. ( 2nd ` Z ) ) ( 2nd ` F ) ) >. )
13 ovex 
 |-  ( ( 1st ` G ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. ( comp ` C ) ( 1st ` Z ) ) ( 1st ` F ) ) e. _V
14 ovex 
 |-  ( ( 2nd ` G ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. .x. ( 2nd ` Z ) ) ( 2nd ` F ) ) e. _V
15 13 14 op2ndd 
 |-  ( ( G ( <. X , Y >. O Z ) F ) = <. ( ( 1st ` G ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. ( comp ` C ) ( 1st ` Z ) ) ( 1st ` F ) ) , ( ( 2nd ` G ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. .x. ( 2nd ` Z ) ) ( 2nd ` F ) ) >. -> ( 2nd ` ( G ( <. X , Y >. O Z ) F ) ) = ( ( 2nd ` G ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. .x. ( 2nd ` Z ) ) ( 2nd ` F ) ) )
16 12 15 syl 
 |-  ( ph -> ( 2nd ` ( G ( <. X , Y >. O Z ) F ) ) = ( ( 2nd ` G ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. .x. ( 2nd ` Z ) ) ( 2nd ` F ) ) )