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	⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
	xpcco2.x	⊢ 𝑋 = ( Base ‘ 𝐶 )
	xpcco2.y	⊢ 𝑌 = ( Base ‘ 𝐷 )
	xpcco2.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	xpcco2.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
	xpcco2.m	⊢ ( 𝜑 → 𝑀 ∈ 𝑋 )
	xpcco2.n	⊢ ( 𝜑 → 𝑁 ∈ 𝑌 )
	xpcco2.p	⊢ ( 𝜑 → 𝑃 ∈ 𝑋 )
	xpcco2.q	⊢ ( 𝜑 → 𝑄 ∈ 𝑌 )
	xpchom2.k	⊢ 𝐾 = ( Hom ‘ 𝑇 )
Assertion	xpchom2	⊢ ( 𝜑 → ( ⟨ 𝑀 , 𝑁 ⟩ 𝐾 ⟨ 𝑃 , 𝑄 ⟩ ) = ( ( 𝑀 𝐻 𝑃 ) × ( 𝑁 𝐽 𝑄 ) ) )

Proof

Step	Hyp	Ref	Expression
1		xpcco2.t	⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
2		xpcco2.x	⊢ 𝑋 = ( Base ‘ 𝐶 )
3		xpcco2.y	⊢ 𝑌 = ( Base ‘ 𝐷 )
4		xpcco2.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
5		xpcco2.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
6		xpcco2.m	⊢ ( 𝜑 → 𝑀 ∈ 𝑋 )
7		xpcco2.n	⊢ ( 𝜑 → 𝑁 ∈ 𝑌 )
8		xpcco2.p	⊢ ( 𝜑 → 𝑃 ∈ 𝑋 )
9		xpcco2.q	⊢ ( 𝜑 → 𝑄 ∈ 𝑌 )
10		xpchom2.k	⊢ 𝐾 = ( Hom ‘ 𝑇 )
11	1 2 3	xpcbas	⊢ ( 𝑋 × 𝑌 ) = ( Base ‘ 𝑇 )
12	6 7	opelxpd	⊢ ( 𝜑 → ⟨ 𝑀 , 𝑁 ⟩ ∈ ( 𝑋 × 𝑌 ) )
13	8 9	opelxpd	⊢ ( 𝜑 → ⟨ 𝑃 , 𝑄 ⟩ ∈ ( 𝑋 × 𝑌 ) )
14	1 11 4 5 10 12 13	xpchom	⊢ ( 𝜑 → ( ⟨ 𝑀 , 𝑁 ⟩ 𝐾 ⟨ 𝑃 , 𝑄 ⟩ ) = ( ( ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) 𝐻 ( 1st ‘ ⟨ 𝑃 , 𝑄 ⟩ ) ) × ( ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) 𝐽 ( 2nd ‘ ⟨ 𝑃 , 𝑄 ⟩ ) ) ) )
15		op1stg	⊢ ( ( 𝑀 ∈ 𝑋 ∧ 𝑁 ∈ 𝑌 ) → ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) = 𝑀 )
16	6 7 15	syl2anc	⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) = 𝑀 )
17		op1stg	⊢ ( ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) → ( 1st ‘ ⟨ 𝑃 , 𝑄 ⟩ ) = 𝑃 )
18	8 9 17	syl2anc	⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝑃 , 𝑄 ⟩ ) = 𝑃 )
19	16 18	oveq12d	⊢ ( 𝜑 → ( ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) 𝐻 ( 1st ‘ ⟨ 𝑃 , 𝑄 ⟩ ) ) = ( 𝑀 𝐻 𝑃 ) )
20		op2ndg	⊢ ( ( 𝑀 ∈ 𝑋 ∧ 𝑁 ∈ 𝑌 ) → ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) = 𝑁 )
21	6 7 20	syl2anc	⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) = 𝑁 )
22		op2ndg	⊢ ( ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) → ( 2nd ‘ ⟨ 𝑃 , 𝑄 ⟩ ) = 𝑄 )
23	8 9 22	syl2anc	⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝑃 , 𝑄 ⟩ ) = 𝑄 )
24	21 23	oveq12d	⊢ ( 𝜑 → ( ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) 𝐽 ( 2nd ‘ ⟨ 𝑃 , 𝑄 ⟩ ) ) = ( 𝑁 𝐽 𝑄 ) )
25	19 24	xpeq12d	⊢ ( 𝜑 → ( ( ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) 𝐻 ( 1st ‘ ⟨ 𝑃 , 𝑄 ⟩ ) ) × ( ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) 𝐽 ( 2nd ‘ ⟨ 𝑃 , 𝑄 ⟩ ) ) ) = ( ( 𝑀 𝐻 𝑃 ) × ( 𝑁 𝐽 𝑄 ) ) )
26	14 25	eqtrd	⊢ ( 𝜑 → ( ⟨ 𝑀 , 𝑁 ⟩ 𝐾 ⟨ 𝑃 , 𝑄 ⟩ ) = ( ( 𝑀 𝐻 𝑃 ) × ( 𝑁 𝐽 𝑄 ) ) )