Metamath Proof Explorer

Theorem xpchom

Description: Set of morphisms of the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses xpchomfval.t 
|- T = ( C Xc. D )
xpchomfval.y 
|- B = ( Base ` T )
xpchomfval.h 
|- H = ( Hom ` C )
xpchomfval.j 
|- J = ( Hom ` D )
xpchomfval.k 
|- K = ( Hom ` T )
xpchom.x 
|- ( ph -> X e. B )
xpchom.y 
|- ( ph -> Y e. B )
Assertion xpchom 
|- ( ph -> ( X K Y ) = ( ( ( 1st ` X ) H ( 1st ` Y ) ) X. ( ( 2nd ` X ) J ( 2nd ` Y ) ) ) )

Proof

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