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