This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xpchom2

Description: Value of the set of morphisms 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 )
xpchom2.k 
|- K = ( Hom ` T )
Assertion xpchom2 
|- ( ph -> ( <. M , N >. K <. P , Q >. ) = ( ( M H P ) X. ( N J Q ) ) )

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