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 |
|
xpchom2.k |
|- K = ( Hom ` T ) |
11 |
1 2 3
|
xpcbas |
|- ( X X. Y ) = ( Base ` T ) |
12 |
6 7
|
opelxpd |
|- ( ph -> <. M , N >. e. ( X X. Y ) ) |
13 |
8 9
|
opelxpd |
|- ( ph -> <. P , Q >. e. ( X X. Y ) ) |
14 |
1 11 4 5 10 12 13
|
xpchom |
|- ( ph -> ( <. M , N >. K <. P , Q >. ) = ( ( ( 1st ` <. M , N >. ) H ( 1st ` <. P , Q >. ) ) X. ( ( 2nd ` <. M , N >. ) J ( 2nd ` <. P , Q >. ) ) ) ) |
15 |
|
op1stg |
|- ( ( M e. X /\ N e. Y ) -> ( 1st ` <. M , N >. ) = M ) |
16 |
6 7 15
|
syl2anc |
|- ( ph -> ( 1st ` <. M , N >. ) = M ) |
17 |
|
op1stg |
|- ( ( P e. X /\ Q e. Y ) -> ( 1st ` <. P , Q >. ) = P ) |
18 |
8 9 17
|
syl2anc |
|- ( ph -> ( 1st ` <. P , Q >. ) = P ) |
19 |
16 18
|
oveq12d |
|- ( ph -> ( ( 1st ` <. M , N >. ) H ( 1st ` <. P , Q >. ) ) = ( M H P ) ) |
20 |
|
op2ndg |
|- ( ( M e. X /\ N e. Y ) -> ( 2nd ` <. M , N >. ) = N ) |
21 |
6 7 20
|
syl2anc |
|- ( ph -> ( 2nd ` <. M , N >. ) = N ) |
22 |
|
op2ndg |
|- ( ( P e. X /\ Q e. Y ) -> ( 2nd ` <. P , Q >. ) = Q ) |
23 |
8 9 22
|
syl2anc |
|- ( ph -> ( 2nd ` <. P , Q >. ) = Q ) |
24 |
21 23
|
oveq12d |
|- ( ph -> ( ( 2nd ` <. M , N >. ) J ( 2nd ` <. P , Q >. ) ) = ( N J Q ) ) |
25 |
19 24
|
xpeq12d |
|- ( ph -> ( ( ( 1st ` <. M , N >. ) H ( 1st ` <. P , Q >. ) ) X. ( ( 2nd ` <. M , N >. ) J ( 2nd ` <. P , Q >. ) ) ) = ( ( M H P ) X. ( N J Q ) ) ) |
26 |
14 25
|
eqtrd |
|- ( ph -> ( <. M , N >. K <. P , Q >. ) = ( ( M H P ) X. ( N J Q ) ) ) |