Metamath Proof Explorer

Theorem xpcco

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

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

Proof

Step Hyp Ref Expression
1 xpccofval.t 
 |-  T = ( C Xc. D )
2 xpccofval.b 
 |-  B = ( Base ` T )
3 xpccofval.k 
 |-  K = ( Hom ` T )
4 xpccofval.o1 
 |-  .x. = ( comp ` C )
5 xpccofval.o2 
 |-  .xb = ( comp ` D )
6 xpccofval.o 
 |-  O = ( comp ` T )
7 xpcco.x 
 |-  ( ph -> X e. B )
8 xpcco.y 
 |-  ( ph -> Y e. B )
9 xpcco.z 
 |-  ( ph -> Z e. B )
10 xpcco.f 
 |-  ( ph -> F e. ( X K Y ) )
11 xpcco.g 
 |-  ( ph -> G e. ( Y K Z ) )
12 1 2 3 4 5 6 xpccofval 
 |-  O = ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) K y ) , f e. ( K ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. .x. ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. .xb ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) )
13 7 8 opelxpd 
 |-  ( ph -> <. X , Y >. e. ( B X. B ) )
14 9 adantr 
 |-  ( ( ph /\ x = <. X , Y >. ) -> Z e. B )
15 ovex 
 |-  ( ( 2nd ` x ) K y ) e. _V
16 fvex 
 |-  ( K ` x ) e. _V
17 15 16 mpoex 
 |-  ( g e. ( ( 2nd ` x ) K y ) , f e. ( K ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. .x. ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. .xb ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) e. _V
18 17 a1i 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) -> ( g e. ( ( 2nd ` x ) K y ) , f e. ( K ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. .x. ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. .xb ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) e. _V )
19 11 adantr 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) -> G e. ( Y K Z ) )
20 simprl 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) -> x = <. X , Y >. )
21 20 fveq2d 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) -> ( 2nd ` x ) = ( 2nd ` <. X , Y >. ) )
22 op2ndg 
 |-  ( ( X e. B /\ Y e. B ) -> ( 2nd ` <. X , Y >. ) = Y )
23 7 8 22 syl2anc 
 |-  ( ph -> ( 2nd ` <. X , Y >. ) = Y )
24 23 adantr 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) -> ( 2nd ` <. X , Y >. ) = Y )
25 21 24 eqtrd 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) -> ( 2nd ` x ) = Y )
26 simprr 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) -> y = Z )
27 25 26 oveq12d 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) -> ( ( 2nd ` x ) K y ) = ( Y K Z ) )
28 19 27 eleqtrrd 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) -> G e. ( ( 2nd ` x ) K y ) )
29 10 adantr 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) -> F e. ( X K Y ) )
30 20 fveq2d 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) -> ( K ` x ) = ( K ` <. X , Y >. ) )
31 df-ov 
 |-  ( X K Y ) = ( K ` <. X , Y >. )
32 30 31 eqtr4di 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) -> ( K ` x ) = ( X K Y ) )
33 29 32 eleqtrrd 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) -> F e. ( K ` x ) )
34 33 adantr 
 |-  ( ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) /\ g = G ) -> F e. ( K ` x ) )
35 opex 
 |-  <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. .x. ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. .xb ( 2nd ` y ) ) ( 2nd ` f ) ) >. e. _V
36 35 a1i 
 |-  ( ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) /\ ( g = G /\ f = F ) ) -> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. .x. ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. .xb ( 2nd ` y ) ) ( 2nd ` f ) ) >. e. _V )
37 20 fveq2d 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) -> ( 1st ` x ) = ( 1st ` <. X , Y >. ) )
38 op1stg 
 |-  ( ( X e. B /\ Y e. B ) -> ( 1st ` <. X , Y >. ) = X )
39 7 8 38 syl2anc 
 |-  ( ph -> ( 1st ` <. X , Y >. ) = X )
40 39 adantr 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) -> ( 1st ` <. X , Y >. ) = X )
41 37 40 eqtrd 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) -> ( 1st ` x ) = X )
42 41 adantr 
 |-  ( ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) /\ ( g = G /\ f = F ) ) -> ( 1st ` x ) = X )
43 42 fveq2d 
 |-  ( ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) /\ ( g = G /\ f = F ) ) -> ( 1st ` ( 1st ` x ) ) = ( 1st ` X ) )
44 25 adantr 
 |-  ( ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) /\ ( g = G /\ f = F ) ) -> ( 2nd ` x ) = Y )
45 44 fveq2d 
 |-  ( ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) /\ ( g = G /\ f = F ) ) -> ( 1st ` ( 2nd ` x ) ) = ( 1st ` Y ) )
46 43 45 opeq12d 
 |-  ( ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) /\ ( g = G /\ f = F ) ) -> <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. = <. ( 1st ` X ) , ( 1st ` Y ) >. )
47 simplrr 
 |-  ( ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) /\ ( g = G /\ f = F ) ) -> y = Z )
48 47 fveq2d 
 |-  ( ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) /\ ( g = G /\ f = F ) ) -> ( 1st ` y ) = ( 1st ` Z ) )
49 46 48 oveq12d 
 |-  ( ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) /\ ( g = G /\ f = F ) ) -> ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. .x. ( 1st ` y ) ) = ( <. ( 1st ` X ) , ( 1st ` Y ) >. .x. ( 1st ` Z ) ) )
50 simprl 
 |-  ( ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) /\ ( g = G /\ f = F ) ) -> g = G )
51 50 fveq2d 
 |-  ( ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) /\ ( g = G /\ f = F ) ) -> ( 1st ` g ) = ( 1st ` G ) )
52 simprr 
 |-  ( ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) /\ ( g = G /\ f = F ) ) -> f = F )
53 52 fveq2d 
 |-  ( ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) /\ ( g = G /\ f = F ) ) -> ( 1st ` f ) = ( 1st ` F ) )
54 49 51 53 oveq123d 
 |-  ( ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) /\ ( g = G /\ f = F ) ) -> ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. .x. ( 1st ` y ) ) ( 1st ` f ) ) = ( ( 1st ` G ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. .x. ( 1st ` Z ) ) ( 1st ` F ) ) )
55 42 fveq2d 
 |-  ( ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) /\ ( g = G /\ f = F ) ) -> ( 2nd ` ( 1st ` x ) ) = ( 2nd ` X ) )
56 44 fveq2d 
 |-  ( ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) /\ ( g = G /\ f = F ) ) -> ( 2nd ` ( 2nd ` x ) ) = ( 2nd ` Y ) )
57 55 56 opeq12d 
 |-  ( ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) /\ ( g = G /\ f = F ) ) -> <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. = <. ( 2nd ` X ) , ( 2nd ` Y ) >. )
58 47 fveq2d 
 |-  ( ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) /\ ( g = G /\ f = F ) ) -> ( 2nd ` y ) = ( 2nd ` Z ) )
59 57 58 oveq12d 
 |-  ( ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) /\ ( g = G /\ f = F ) ) -> ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. .xb ( 2nd ` y ) ) = ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. .xb ( 2nd ` Z ) ) )
60 50 fveq2d 
 |-  ( ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) /\ ( g = G /\ f = F ) ) -> ( 2nd ` g ) = ( 2nd ` G ) )
61 52 fveq2d 
 |-  ( ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) /\ ( g = G /\ f = F ) ) -> ( 2nd ` f ) = ( 2nd ` F ) )
62 59 60 61 oveq123d 
 |-  ( ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) /\ ( g = G /\ f = F ) ) -> ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. .xb ( 2nd ` y ) ) ( 2nd ` f ) ) = ( ( 2nd ` G ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. .xb ( 2nd ` Z ) ) ( 2nd ` F ) ) )
63 54 62 opeq12d 
 |-  ( ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) /\ ( g = G /\ f = F ) ) -> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. .x. ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. .xb ( 2nd ` y ) ) ( 2nd ` f ) ) >. = <. ( ( 1st ` G ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. .x. ( 1st ` Z ) ) ( 1st ` F ) ) , ( ( 2nd ` G ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. .xb ( 2nd ` Z ) ) ( 2nd ` F ) ) >. )
64 28 34 36 63 ovmpodv2 
 |-  ( ( ph /\ ( x = <. X , Y >. /\ y = Z ) ) -> ( ( <. X , Y >. O Z ) = ( g e. ( ( 2nd ` x ) K y ) , f e. ( K ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. .x. ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. .xb ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) -> ( G ( <. X , Y >. O Z ) F ) = <. ( ( 1st ` G ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. .x. ( 1st ` Z ) ) ( 1st ` F ) ) , ( ( 2nd ` G ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. .xb ( 2nd ` Z ) ) ( 2nd ` F ) ) >. ) )
65 13 14 18 64 ovmpodv 
 |-  ( ph -> ( O = ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) K y ) , f e. ( K ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. .x. ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. .xb ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) -> ( G ( <. X , Y >. O Z ) F ) = <. ( ( 1st ` G ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. .x. ( 1st ` Z ) ) ( 1st ` F ) ) , ( ( 2nd ` G ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. .xb ( 2nd ` Z ) ) ( 2nd ` F ) ) >. ) )
66 12 65 mpi 
 |-  ( ph -> ( G ( <. X , Y >. O Z ) F ) = <. ( ( 1st ` G ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. .x. ( 1st ` Z ) ) ( 1st ` F ) ) , ( ( 2nd ` G ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. .xb ( 2nd ` Z ) ) ( 2nd ` F ) ) >. )