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{\times }_{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$$
	xpchom2.k	$$⊢K=\mathrm{Hom}\left(T\right)$$
Assertion	xpchom2	$$⊢\phi \to ⟨M,N⟩K⟨P,Q⟩=\left(MHP\right)\times \left(NJQ\right)$$

Proof

Step	Hyp	Ref	Expression
1		xpcco2.t	$$⊢T=C{\times }_{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		xpchom2.k	$$⊢K=\mathrm{Hom}\left(T\right)$$
11	1 2 3	xpcbas	$$⊢X\times Y={\mathrm{Base}}_T$$
12	6 7	opelxpd	$$⊢\phi \to ⟨M,N⟩\in \left(X\times Y\right)$$
13	8 9	opelxpd	$$⊢\phi \to ⟨P,Q⟩\in \left(X\times Y\right)$$
14	1 11 4 5 10 12 13	xpchom	$$⊢\phi \to ⟨M,N⟩K⟨P,Q⟩=\left(1^{st}\left(⟨M,N⟩\right)H{1}^{st}\left(⟨P,Q⟩\right)\right)\times \left(2^{nd}\left(⟨M,N⟩\right)J{2}^{nd}\left(⟨P,Q⟩\right)\right)$$
15		op1stg	$$⊢\left(M\in X\wedge N\in Y\right)\to 1^{st}\left(⟨M,N⟩\right)=M$$
16	6 7 15	syl2anc	$$⊢\phi \to 1^{st}\left(⟨M,N⟩\right)=M$$
17		op1stg	$$⊢\left(P\in X\wedge Q\in Y\right)\to 1^{st}\left(⟨P,Q⟩\right)=P$$
18	8 9 17	syl2anc	$$⊢\phi \to 1^{st}\left(⟨P,Q⟩\right)=P$$
19	16 18	oveq12d	$$⊢\phi \to 1^{st}\left(⟨M,N⟩\right)H{1}^{st}\left(⟨P,Q⟩\right)=MHP$$
20		op2ndg	$$⊢\left(M\in X\wedge N\in Y\right)\to 2^{nd}\left(⟨M,N⟩\right)=N$$
21	6 7 20	syl2anc	$$⊢\phi \to 2^{nd}\left(⟨M,N⟩\right)=N$$
22		op2ndg	$$⊢\left(P\in X\wedge Q\in Y\right)\to 2^{nd}\left(⟨P,Q⟩\right)=Q$$
23	8 9 22	syl2anc	$$⊢\phi \to 2^{nd}\left(⟨P,Q⟩\right)=Q$$
24	21 23	oveq12d	$$⊢\phi \to 2^{nd}\left(⟨M,N⟩\right)J{2}^{nd}\left(⟨P,Q⟩\right)=NJQ$$
25	19 24	xpeq12d	$$⊢\phi \to \left(1^{st}\left(⟨M,N⟩\right)H{1}^{st}\left(⟨P,Q⟩\right)\right)\times \left(2^{nd}\left(⟨M,N⟩\right)J{2}^{nd}\left(⟨P,Q⟩\right)\right)=\left(MHP\right)\times \left(NJQ\right)$$
26	14 25	eqtrd	$$⊢\phi \to ⟨M,N⟩K⟨P,Q⟩=\left(MHP\right)\times \left(NJQ\right)$$