| Step |
Hyp |
Ref |
Expression |
| 1 |
|
xpchomfval.t |
|- T = ( C Xc. D ) |
| 2 |
|
xpchomfval.y |
|- B = ( Base ` T ) |
| 3 |
|
xpchomfval.h |
|- H = ( Hom ` C ) |
| 4 |
|
xpchomfval.j |
|- J = ( Hom ` D ) |
| 5 |
|
xpchomfval.k |
|- K = ( Hom ` T ) |
| 6 |
|
xpchom.x |
|- ( ph -> X e. B ) |
| 7 |
|
xpchom.y |
|- ( ph -> Y e. B ) |
| 8 |
|
simpl |
|- ( ( u = X /\ v = Y ) -> u = X ) |
| 9 |
8
|
fveq2d |
|- ( ( u = X /\ v = Y ) -> ( 1st ` u ) = ( 1st ` X ) ) |
| 10 |
|
simpr |
|- ( ( u = X /\ v = Y ) -> v = Y ) |
| 11 |
10
|
fveq2d |
|- ( ( u = X /\ v = Y ) -> ( 1st ` v ) = ( 1st ` Y ) ) |
| 12 |
9 11
|
oveq12d |
|- ( ( u = X /\ v = Y ) -> ( ( 1st ` u ) H ( 1st ` v ) ) = ( ( 1st ` X ) H ( 1st ` Y ) ) ) |
| 13 |
8
|
fveq2d |
|- ( ( u = X /\ v = Y ) -> ( 2nd ` u ) = ( 2nd ` X ) ) |
| 14 |
10
|
fveq2d |
|- ( ( u = X /\ v = Y ) -> ( 2nd ` v ) = ( 2nd ` Y ) ) |
| 15 |
13 14
|
oveq12d |
|- ( ( u = X /\ v = Y ) -> ( ( 2nd ` u ) J ( 2nd ` v ) ) = ( ( 2nd ` X ) J ( 2nd ` Y ) ) ) |
| 16 |
12 15
|
xpeq12d |
|- ( ( u = X /\ v = Y ) -> ( ( ( 1st ` u ) H ( 1st ` v ) ) X. ( ( 2nd ` u ) J ( 2nd ` v ) ) ) = ( ( ( 1st ` X ) H ( 1st ` Y ) ) X. ( ( 2nd ` X ) J ( 2nd ` Y ) ) ) ) |
| 17 |
1 2 3 4 5
|
xpchomfval |
|- K = ( u e. B , v e. B |-> ( ( ( 1st ` u ) H ( 1st ` v ) ) X. ( ( 2nd ` u ) J ( 2nd ` v ) ) ) ) |
| 18 |
|
ovex |
|- ( ( 1st ` X ) H ( 1st ` Y ) ) e. _V |
| 19 |
|
ovex |
|- ( ( 2nd ` X ) J ( 2nd ` Y ) ) e. _V |
| 20 |
18 19
|
xpex |
|- ( ( ( 1st ` X ) H ( 1st ` Y ) ) X. ( ( 2nd ` X ) J ( 2nd ` Y ) ) ) e. _V |
| 21 |
16 17 20
|
ovmpoa |
|- ( ( X e. B /\ Y e. B ) -> ( X K Y ) = ( ( ( 1st ` X ) H ( 1st ` Y ) ) X. ( ( 2nd ` X ) J ( 2nd ` Y ) ) ) ) |
| 22 |
6 7 21
|
syl2anc |
|- ( ph -> ( X K Y ) = ( ( ( 1st ` X ) H ( 1st ` Y ) ) X. ( ( 2nd ` X ) J ( 2nd ` Y ) ) ) ) |