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 ⊢ 𝑇 = ( 𝐶 ×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 ⊢ ( 𝜑 → ( ⟨ 𝑀 , 𝑁 ⟩ 𝐾 ⟨ 𝑃 , 𝑄 ⟩ ) = ( ( 𝑀 𝐻 𝑃 ) × ( 𝑁 𝐽 𝑄 ) ) )