Metamath Proof Explorer

Theorem xpcco2

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

Ref Expression
Hypotheses xpcco2.t 
|- T = ( C Xc. D )
xpcco2.x 
|- X = ( Base ` C )
xpcco2.y 
|- Y = ( Base ` D )
xpcco2.h 
|- H = ( Hom ` C )
xpcco2.j 
|- J = ( Hom ` D )
xpcco2.m 
|- ( ph -> M e. X )
xpcco2.n 
|- ( ph -> N e. Y )
xpcco2.p 
|- ( ph -> P e. X )
xpcco2.q 
|- ( ph -> Q e. Y )
xpcco2.o1 
|- .x. = ( comp ` C )
xpcco2.o2 
|- .xb = ( comp ` D )
xpcco2.o 
|- O = ( comp ` T )
xpcco2.r 
|- ( ph -> R e. X )
xpcco2.s 
|- ( ph -> S e. Y )
xpcco2.f 
|- ( ph -> F e. ( M H P ) )
xpcco2.g 
|- ( ph -> G e. ( N J Q ) )
xpcco2.k 
|- ( ph -> K e. ( P H R ) )
xpcco2.l 
|- ( ph -> L e. ( Q J S ) )
Assertion xpcco2 
|- ( ph -> ( <. K , L >. ( <. <. M , N >. , <. P , Q >. >. O <. R , S >. ) <. F , G >. ) = <. ( K ( <. M , P >. .x. R ) F ) , ( L ( <. N , Q >. .xb S ) G ) >. )

Proof

Step Hyp Ref Expression
1 xpcco2.t 
 |-  T = ( C Xc. D )
2 xpcco2.x 
 |-  X = ( Base ` C )
3 xpcco2.y 
 |-  Y = ( Base ` D )
4 xpcco2.h 
 |-  H = ( Hom ` C )
5 xpcco2.j 
 |-  J = ( Hom ` D )
6 xpcco2.m 
 |-  ( ph -> M e. X )
7 xpcco2.n 
 |-  ( ph -> N e. Y )
8 xpcco2.p 
 |-  ( ph -> P e. X )
9 xpcco2.q 
 |-  ( ph -> Q e. Y )
10 xpcco2.o1 
 |-  .x. = ( comp ` C )
11 xpcco2.o2 
 |-  .xb = ( comp ` D )
12 xpcco2.o 
 |-  O = ( comp ` T )
13 xpcco2.r 
 |-  ( ph -> R e. X )
14 xpcco2.s 
 |-  ( ph -> S e. Y )
15 xpcco2.f 
 |-  ( ph -> F e. ( M H P ) )
16 xpcco2.g 
 |-  ( ph -> G e. ( N J Q ) )
17 xpcco2.k 
 |-  ( ph -> K e. ( P H R ) )
18 xpcco2.l 
 |-  ( ph -> L e. ( Q J S ) )
19 1 2 3 xpcbas 
 |-  ( X X. Y ) = ( Base ` T )
20 eqid 
 |-  ( Hom ` T ) = ( Hom ` T )
21 6 7 opelxpd 
 |-  ( ph -> <. M , N >. e. ( X X. Y ) )
22 8 9 opelxpd 
 |-  ( ph -> <. P , Q >. e. ( X X. Y ) )
23 13 14 opelxpd 
 |-  ( ph -> <. R , S >. e. ( X X. Y ) )
24 15 16 opelxpd 
 |-  ( ph -> <. F , G >. e. ( ( M H P ) X. ( N J Q ) ) )
25 1 2 3 4 5 6 7 8 9 20 xpchom2 
 |-  ( ph -> ( <. M , N >. ( Hom ` T ) <. P , Q >. ) = ( ( M H P ) X. ( N J Q ) ) )
26 24 25 eleqtrrd 
 |-  ( ph -> <. F , G >. e. ( <. M , N >. ( Hom ` T ) <. P , Q >. ) )
27 17 18 opelxpd 
 |-  ( ph -> <. K , L >. e. ( ( P H R ) X. ( Q J S ) ) )
28 1 2 3 4 5 8 9 13 14 20 xpchom2 
 |-  ( ph -> ( <. P , Q >. ( Hom ` T ) <. R , S >. ) = ( ( P H R ) X. ( Q J S ) ) )
29 27 28 eleqtrrd 
 |-  ( ph -> <. K , L >. e. ( <. P , Q >. ( Hom ` T ) <. R , S >. ) )
30 1 19 20 10 11 12 21 22 23 26 29 xpcco 
 |-  ( ph -> ( <. K , L >. ( <. <. M , N >. , <. P , Q >. >. O <. R , S >. ) <. F , G >. ) = <. ( ( 1st ` <. K , L >. ) ( <. ( 1st ` <. M , N >. ) , ( 1st ` <. P , Q >. ) >. .x. ( 1st ` <. R , S >. ) ) ( 1st ` <. F , G >. ) ) , ( ( 2nd ` <. K , L >. ) ( <. ( 2nd ` <. M , N >. ) , ( 2nd ` <. P , Q >. ) >. .xb ( 2nd ` <. R , S >. ) ) ( 2nd ` <. F , G >. ) ) >. )
31 op1stg 
 |-  ( ( M e. X /\ N e. Y ) -> ( 1st ` <. M , N >. ) = M )
32 6 7 31 syl2anc 
 |-  ( ph -> ( 1st ` <. M , N >. ) = M )
33 op1stg 
 |-  ( ( P e. X /\ Q e. Y ) -> ( 1st ` <. P , Q >. ) = P )
34 8 9 33 syl2anc 
 |-  ( ph -> ( 1st ` <. P , Q >. ) = P )
35 32 34 opeq12d 
 |-  ( ph -> <. ( 1st ` <. M , N >. ) , ( 1st ` <. P , Q >. ) >. = <. M , P >. )
36 op1stg 
 |-  ( ( R e. X /\ S e. Y ) -> ( 1st ` <. R , S >. ) = R )
37 13 14 36 syl2anc 
 |-  ( ph -> ( 1st ` <. R , S >. ) = R )
38 35 37 oveq12d 
 |-  ( ph -> ( <. ( 1st ` <. M , N >. ) , ( 1st ` <. P , Q >. ) >. .x. ( 1st ` <. R , S >. ) ) = ( <. M , P >. .x. R ) )
39 op1stg 
 |-  ( ( K e. ( P H R ) /\ L e. ( Q J S ) ) -> ( 1st ` <. K , L >. ) = K )
40 17 18 39 syl2anc 
 |-  ( ph -> ( 1st ` <. K , L >. ) = K )
41 op1stg 
 |-  ( ( F e. ( M H P ) /\ G e. ( N J Q ) ) -> ( 1st ` <. F , G >. ) = F )
42 15 16 41 syl2anc 
 |-  ( ph -> ( 1st ` <. F , G >. ) = F )
43 38 40 42 oveq123d 
 |-  ( ph -> ( ( 1st ` <. K , L >. ) ( <. ( 1st ` <. M , N >. ) , ( 1st ` <. P , Q >. ) >. .x. ( 1st ` <. R , S >. ) ) ( 1st ` <. F , G >. ) ) = ( K ( <. M , P >. .x. R ) F ) )
44 op2ndg 
 |-  ( ( M e. X /\ N e. Y ) -> ( 2nd ` <. M , N >. ) = N )
45 6 7 44 syl2anc 
 |-  ( ph -> ( 2nd ` <. M , N >. ) = N )
46 op2ndg 
 |-  ( ( P e. X /\ Q e. Y ) -> ( 2nd ` <. P , Q >. ) = Q )
47 8 9 46 syl2anc 
 |-  ( ph -> ( 2nd ` <. P , Q >. ) = Q )
48 45 47 opeq12d 
 |-  ( ph -> <. ( 2nd ` <. M , N >. ) , ( 2nd ` <. P , Q >. ) >. = <. N , Q >. )
49 op2ndg 
 |-  ( ( R e. X /\ S e. Y ) -> ( 2nd ` <. R , S >. ) = S )
50 13 14 49 syl2anc 
 |-  ( ph -> ( 2nd ` <. R , S >. ) = S )
51 48 50 oveq12d 
 |-  ( ph -> ( <. ( 2nd ` <. M , N >. ) , ( 2nd ` <. P , Q >. ) >. .xb ( 2nd ` <. R , S >. ) ) = ( <. N , Q >. .xb S ) )
52 op2ndg 
 |-  ( ( K e. ( P H R ) /\ L e. ( Q J S ) ) -> ( 2nd ` <. K , L >. ) = L )
53 17 18 52 syl2anc 
 |-  ( ph -> ( 2nd ` <. K , L >. ) = L )
54 op2ndg 
 |-  ( ( F e. ( M H P ) /\ G e. ( N J Q ) ) -> ( 2nd ` <. F , G >. ) = G )
55 15 16 54 syl2anc 
 |-  ( ph -> ( 2nd ` <. F , G >. ) = G )
56 51 53 55 oveq123d 
 |-  ( ph -> ( ( 2nd ` <. K , L >. ) ( <. ( 2nd ` <. M , N >. ) , ( 2nd ` <. P , Q >. ) >. .xb ( 2nd ` <. R , S >. ) ) ( 2nd ` <. F , G >. ) ) = ( L ( <. N , Q >. .xb S ) G ) )
57 43 56 opeq12d 
 |-  ( ph -> <. ( ( 1st ` <. K , L >. ) ( <. ( 1st ` <. M , N >. ) , ( 1st ` <. P , Q >. ) >. .x. ( 1st ` <. R , S >. ) ) ( 1st ` <. F , G >. ) ) , ( ( 2nd ` <. K , L >. ) ( <. ( 2nd ` <. M , N >. ) , ( 2nd ` <. P , Q >. ) >. .xb ( 2nd ` <. R , S >. ) ) ( 2nd ` <. F , G >. ) ) >. = <. ( K ( <. M , P >. .x. R ) F ) , ( L ( <. N , Q >. .xb S ) G ) >. )
58 30 57 eqtrd 
 |-  ( ph -> ( <. K , L >. ( <. <. M , N >. , <. P , Q >. >. O <. R , S >. ) <. F , G >. ) = <. ( K ( <. M , P >. .x. R ) F ) , ( L ( <. N , Q >. .xb S ) G ) >. )