xpchom2

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

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

Metamath Proof Explorer