# Metamath Proof Explorer

## Theorem xpcco2

Description: Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses xpcco2.t ${⊢}{T}={C}{×}_{c}{D}$
xpcco2.x ${⊢}{X}={\mathrm{Base}}_{{C}}$
xpcco2.y ${⊢}{Y}={\mathrm{Base}}_{{D}}$
xpcco2.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
xpcco2.j ${⊢}{J}=\mathrm{Hom}\left({D}\right)$
xpcco2.m ${⊢}{\phi }\to {M}\in {X}$
xpcco2.n ${⊢}{\phi }\to {N}\in {Y}$
xpcco2.p ${⊢}{\phi }\to {P}\in {X}$
xpcco2.q ${⊢}{\phi }\to {Q}\in {Y}$
xpcco2.o1
xpcco2.o2
xpcco2.o ${⊢}{O}=\mathrm{comp}\left({T}\right)$
xpcco2.r ${⊢}{\phi }\to {R}\in {X}$
xpcco2.s ${⊢}{\phi }\to {S}\in {Y}$
xpcco2.f ${⊢}{\phi }\to {F}\in \left({M}{H}{P}\right)$
xpcco2.g ${⊢}{\phi }\to {G}\in \left({N}{J}{Q}\right)$
xpcco2.k ${⊢}{\phi }\to {K}\in \left({P}{H}{R}\right)$
xpcco2.l ${⊢}{\phi }\to {L}\in \left({Q}{J}{S}\right)$
Assertion xpcco2

### Proof

Step Hyp Ref Expression
1 xpcco2.t ${⊢}{T}={C}{×}_{c}{D}$
2 xpcco2.x ${⊢}{X}={\mathrm{Base}}_{{C}}$
3 xpcco2.y ${⊢}{Y}={\mathrm{Base}}_{{D}}$
4 xpcco2.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
5 xpcco2.j ${⊢}{J}=\mathrm{Hom}\left({D}\right)$
6 xpcco2.m ${⊢}{\phi }\to {M}\in {X}$
7 xpcco2.n ${⊢}{\phi }\to {N}\in {Y}$
8 xpcco2.p ${⊢}{\phi }\to {P}\in {X}$
9 xpcco2.q ${⊢}{\phi }\to {Q}\in {Y}$
10 xpcco2.o1
11 xpcco2.o2
12 xpcco2.o ${⊢}{O}=\mathrm{comp}\left({T}\right)$
13 xpcco2.r ${⊢}{\phi }\to {R}\in {X}$
14 xpcco2.s ${⊢}{\phi }\to {S}\in {Y}$
15 xpcco2.f ${⊢}{\phi }\to {F}\in \left({M}{H}{P}\right)$
16 xpcco2.g ${⊢}{\phi }\to {G}\in \left({N}{J}{Q}\right)$
17 xpcco2.k ${⊢}{\phi }\to {K}\in \left({P}{H}{R}\right)$
18 xpcco2.l ${⊢}{\phi }\to {L}\in \left({Q}{J}{S}\right)$
19 1 2 3 xpcbas ${⊢}{X}×{Y}={\mathrm{Base}}_{{T}}$
20 eqid ${⊢}\mathrm{Hom}\left({T}\right)=\mathrm{Hom}\left({T}\right)$
21 6 7 opelxpd ${⊢}{\phi }\to ⟨{M},{N}⟩\in \left({X}×{Y}\right)$
22 8 9 opelxpd ${⊢}{\phi }\to ⟨{P},{Q}⟩\in \left({X}×{Y}\right)$
23 13 14 opelxpd ${⊢}{\phi }\to ⟨{R},{S}⟩\in \left({X}×{Y}\right)$
24 15 16 opelxpd ${⊢}{\phi }\to ⟨{F},{G}⟩\in \left(\left({M}{H}{P}\right)×\left({N}{J}{Q}\right)\right)$
25 1 2 3 4 5 6 7 8 9 20 xpchom2 ${⊢}{\phi }\to ⟨{M},{N}⟩\mathrm{Hom}\left({T}\right)⟨{P},{Q}⟩=\left({M}{H}{P}\right)×\left({N}{J}{Q}\right)$
26 24 25 eleqtrrd ${⊢}{\phi }\to ⟨{F},{G}⟩\in \left(⟨{M},{N}⟩\mathrm{Hom}\left({T}\right)⟨{P},{Q}⟩\right)$
27 17 18 opelxpd ${⊢}{\phi }\to ⟨{K},{L}⟩\in \left(\left({P}{H}{R}\right)×\left({Q}{J}{S}\right)\right)$
28 1 2 3 4 5 8 9 13 14 20 xpchom2 ${⊢}{\phi }\to ⟨{P},{Q}⟩\mathrm{Hom}\left({T}\right)⟨{R},{S}⟩=\left({P}{H}{R}\right)×\left({Q}{J}{S}\right)$
29 27 28 eleqtrrd ${⊢}{\phi }\to ⟨{K},{L}⟩\in \left(⟨{P},{Q}⟩\mathrm{Hom}\left({T}\right)⟨{R},{S}⟩\right)$
30 1 19 20 10 11 12 21 22 23 26 29 xpcco
31 op1stg ${⊢}\left({M}\in {X}\wedge {N}\in {Y}\right)\to {1}^{st}\left(⟨{M},{N}⟩\right)={M}$
32 6 7 31 syl2anc ${⊢}{\phi }\to {1}^{st}\left(⟨{M},{N}⟩\right)={M}$
33 op1stg ${⊢}\left({P}\in {X}\wedge {Q}\in {Y}\right)\to {1}^{st}\left(⟨{P},{Q}⟩\right)={P}$
34 8 9 33 syl2anc ${⊢}{\phi }\to {1}^{st}\left(⟨{P},{Q}⟩\right)={P}$
35 32 34 opeq12d ${⊢}{\phi }\to ⟨{1}^{st}\left(⟨{M},{N}⟩\right),{1}^{st}\left(⟨{P},{Q}⟩\right)⟩=⟨{M},{P}⟩$
36 op1stg ${⊢}\left({R}\in {X}\wedge {S}\in {Y}\right)\to {1}^{st}\left(⟨{R},{S}⟩\right)={R}$
37 13 14 36 syl2anc ${⊢}{\phi }\to {1}^{st}\left(⟨{R},{S}⟩\right)={R}$
38 35 37 oveq12d
39 op1stg ${⊢}\left({K}\in \left({P}{H}{R}\right)\wedge {L}\in \left({Q}{J}{S}\right)\right)\to {1}^{st}\left(⟨{K},{L}⟩\right)={K}$
40 17 18 39 syl2anc ${⊢}{\phi }\to {1}^{st}\left(⟨{K},{L}⟩\right)={K}$
41 op1stg ${⊢}\left({F}\in \left({M}{H}{P}\right)\wedge {G}\in \left({N}{J}{Q}\right)\right)\to {1}^{st}\left(⟨{F},{G}⟩\right)={F}$
42 15 16 41 syl2anc ${⊢}{\phi }\to {1}^{st}\left(⟨{F},{G}⟩\right)={F}$
43 38 40 42 oveq123d
44 op2ndg ${⊢}\left({M}\in {X}\wedge {N}\in {Y}\right)\to {2}^{nd}\left(⟨{M},{N}⟩\right)={N}$
45 6 7 44 syl2anc ${⊢}{\phi }\to {2}^{nd}\left(⟨{M},{N}⟩\right)={N}$
46 op2ndg ${⊢}\left({P}\in {X}\wedge {Q}\in {Y}\right)\to {2}^{nd}\left(⟨{P},{Q}⟩\right)={Q}$
47 8 9 46 syl2anc ${⊢}{\phi }\to {2}^{nd}\left(⟨{P},{Q}⟩\right)={Q}$
48 45 47 opeq12d ${⊢}{\phi }\to ⟨{2}^{nd}\left(⟨{M},{N}⟩\right),{2}^{nd}\left(⟨{P},{Q}⟩\right)⟩=⟨{N},{Q}⟩$
49 op2ndg ${⊢}\left({R}\in {X}\wedge {S}\in {Y}\right)\to {2}^{nd}\left(⟨{R},{S}⟩\right)={S}$
50 13 14 49 syl2anc ${⊢}{\phi }\to {2}^{nd}\left(⟨{R},{S}⟩\right)={S}$
51 48 50 oveq12d
52 op2ndg ${⊢}\left({K}\in \left({P}{H}{R}\right)\wedge {L}\in \left({Q}{J}{S}\right)\right)\to {2}^{nd}\left(⟨{K},{L}⟩\right)={L}$
53 17 18 52 syl2anc ${⊢}{\phi }\to {2}^{nd}\left(⟨{K},{L}⟩\right)={L}$
54 op2ndg ${⊢}\left({F}\in \left({M}{H}{P}\right)\wedge {G}\in \left({N}{J}{Q}\right)\right)\to {2}^{nd}\left(⟨{F},{G}⟩\right)={G}$
55 15 16 54 syl2anc ${⊢}{\phi }\to {2}^{nd}\left(⟨{F},{G}⟩\right)={G}$
56 51 53 55 oveq123d
57 43 56 opeq12d
58 30 57 eqtrd