This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
xpcco2.x ⊢ 𝑋 = ( Base ‘ 𝐶 )
xpcco2.y ⊢ 𝑌 = ( Base ‘ 𝐷 )
xpcco2.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
xpcco2.j ⊢ 𝐽 = ( Hom ‘ 𝐷 )
xpcco2.m ⊢ ( 𝜑 → 𝑀 ∈ 𝑋 )
xpcco2.n ⊢ ( 𝜑 → 𝑁 ∈ 𝑌 )
xpcco2.p ⊢ ( 𝜑 → 𝑃 ∈ 𝑋 )
xpcco2.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑌 )
xpcco2.o1 ⊢ · = ( comp ‘ 𝐶 )
xpcco2.o2 ⊢ ∙ = ( comp ‘ 𝐷 )
xpcco2.o ⊢ 𝑂 = ( comp ‘ 𝑇 )
xpcco2.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑋 )
xpcco2.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑌 )
xpcco2.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑀 𝐻 𝑃 ) )
xpcco2.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑁 𝐽 𝑄 ) )
xpcco2.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑃 𝐻 𝑅 ) )
xpcco2.l ⊢ ( 𝜑 → 𝐿 ∈ ( 𝑄 𝐽 𝑆 ) )
Assertion xpcco2 ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ( ⟨ ⟨ 𝑀 , 𝑁 ⟩ , ⟨ 𝑃 , 𝑄 ⟩ ⟩ 𝑂 ⟨ 𝑅 , 𝑆 ⟩ ) ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ ( 𝐾 ( ⟨ 𝑀 , 𝑃 ⟩ · 𝑅 ) 𝐹 ) , ( 𝐿 ( ⟨ 𝑁 , 𝑄 ⟩ ∙ 𝑆 ) 𝐺 ) ⟩ )

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 xpcco2.o1 ⊢ · = ( comp ‘ 𝐶 )
11 xpcco2.o2 ⊢ ∙ = ( comp ‘ 𝐷 )
12 xpcco2.o ⊢ 𝑂 = ( comp ‘ 𝑇 )
13 xpcco2.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑋 )
14 xpcco2.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑌 )
15 xpcco2.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑀 𝐻 𝑃 ) )
16 xpcco2.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑁 𝐽 𝑄 ) )
17 xpcco2.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑃 𝐻 𝑅 ) )
18 xpcco2.l ⊢ ( 𝜑 → 𝐿 ∈ ( 𝑄 𝐽 𝑆 ) )
19 1 2 3 xpcbas ⊢ ( 𝑋 × 𝑌 ) = ( Base ‘ 𝑇 )
20 eqid ⊢ ( Hom ‘ 𝑇 ) = ( Hom ‘ 𝑇 )
21 6 7 opelxpd ⊢ ( 𝜑 → ⟨ 𝑀 , 𝑁 ⟩ ∈ ( 𝑋 × 𝑌 ) )
22 8 9 opelxpd ⊢ ( 𝜑 → ⟨ 𝑃 , 𝑄 ⟩ ∈ ( 𝑋 × 𝑌 ) )
23 13 14 opelxpd ⊢ ( 𝜑 → ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑋 × 𝑌 ) )
24 15 16 opelxpd ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( ( 𝑀 𝐻 𝑃 ) × ( 𝑁 𝐽 𝑄 ) ) )
25 1 2 3 4 5 6 7 8 9 20 xpchom2 ⊢ ( 𝜑 → ( ⟨ 𝑀 , 𝑁 ⟩ ( Hom ‘ 𝑇 ) ⟨ 𝑃 , 𝑄 ⟩ ) = ( ( 𝑀 𝐻 𝑃 ) × ( 𝑁 𝐽 𝑄 ) ) )
26 24 25 eleqtrrd ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( ⟨ 𝑀 , 𝑁 ⟩ ( Hom ‘ 𝑇 ) ⟨ 𝑃 , 𝑄 ⟩ ) )
27 17 18 opelxpd ⊢ ( 𝜑 → ⟨ 𝐾 , 𝐿 ⟩ ∈ ( ( 𝑃 𝐻 𝑅 ) × ( 𝑄 𝐽 𝑆 ) ) )
28 1 2 3 4 5 8 9 13 14 20 xpchom2 ⊢ ( 𝜑 → ( ⟨ 𝑃 , 𝑄 ⟩ ( Hom ‘ 𝑇 ) ⟨ 𝑅 , 𝑆 ⟩ ) = ( ( 𝑃 𝐻 𝑅 ) × ( 𝑄 𝐽 𝑆 ) ) )
29 27 28 eleqtrrd ⊢ ( 𝜑 → ⟨ 𝐾 , 𝐿 ⟩ ∈ ( ⟨ 𝑃 , 𝑄 ⟩ ( Hom ‘ 𝑇 ) ⟨ 𝑅 , 𝑆 ⟩ ) )
30 1 19 20 10 11 12 21 22 23 26 29 xpcco ⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ( ⟨ ⟨ 𝑀 , 𝑁 ⟩ , ⟨ 𝑃 , 𝑄 ⟩ ⟩ 𝑂 ⟨ 𝑅 , 𝑆 ⟩ ) ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ ( ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ( ⟨ ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 1st ‘ ⟨ 𝑃 , 𝑄 ⟩ ) ⟩ · ( 1st ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ) ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) , ( ( 2nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ( ⟨ ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 2nd ‘ ⟨ 𝑃 , 𝑄 ⟩ ) ⟩ ∙ ( 2nd ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ) ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) ⟩ )
31 op1stg ⊢ ( ( 𝑀 ∈ 𝑋 ∧ 𝑁 ∈ 𝑌 ) → ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) = 𝑀 )
32 6 7 31 syl2anc ⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) = 𝑀 )
33 op1stg ⊢ ( ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) → ( 1st ‘ ⟨ 𝑃 , 𝑄 ⟩ ) = 𝑃 )
34 8 9 33 syl2anc ⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝑃 , 𝑄 ⟩ ) = 𝑃 )
35 32 34 opeq12d ⊢ ( 𝜑 → ⟨ ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 1st ‘ ⟨ 𝑃 , 𝑄 ⟩ ) ⟩ = ⟨ 𝑀 , 𝑃 ⟩ )
36 op1stg ⊢ ( ( 𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌 ) → ( 1st ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = 𝑅 )
37 13 14 36 syl2anc ⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = 𝑅 )
38 35 37 oveq12d ⊢ ( 𝜑 → ( ⟨ ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 1st ‘ ⟨ 𝑃 , 𝑄 ⟩ ) ⟩ · ( 1st ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ) = ( ⟨ 𝑀 , 𝑃 ⟩ · 𝑅 ) )
39 op1stg ⊢ ( ( 𝐾 ∈ ( 𝑃 𝐻 𝑅 ) ∧ 𝐿 ∈ ( 𝑄 𝐽 𝑆 ) ) → ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐾 )
40 17 18 39 syl2anc ⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐾 )
41 op1stg ⊢ ( ( 𝐹 ∈ ( 𝑀 𝐻 𝑃 ) ∧ 𝐺 ∈ ( 𝑁 𝐽 𝑄 ) ) → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
42 15 16 41 syl2anc ⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
43 38 40 42 oveq123d ⊢ ( 𝜑 → ( ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ( ⟨ ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 1st ‘ ⟨ 𝑃 , 𝑄 ⟩ ) ⟩ · ( 1st ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ) ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) = ( 𝐾 ( ⟨ 𝑀 , 𝑃 ⟩ · 𝑅 ) 𝐹 ) )
44 op2ndg ⊢ ( ( 𝑀 ∈ 𝑋 ∧ 𝑁 ∈ 𝑌 ) → ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) = 𝑁 )
45 6 7 44 syl2anc ⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) = 𝑁 )
46 op2ndg ⊢ ( ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) → ( 2nd ‘ ⟨ 𝑃 , 𝑄 ⟩ ) = 𝑄 )
47 8 9 46 syl2anc ⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝑃 , 𝑄 ⟩ ) = 𝑄 )
48 45 47 opeq12d ⊢ ( 𝜑 → ⟨ ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 2nd ‘ ⟨ 𝑃 , 𝑄 ⟩ ) ⟩ = ⟨ 𝑁 , 𝑄 ⟩ )
49 op2ndg ⊢ ( ( 𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌 ) → ( 2nd ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = 𝑆 )
50 13 14 49 syl2anc ⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = 𝑆 )
51 48 50 oveq12d ⊢ ( 𝜑 → ( ⟨ ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 2nd ‘ ⟨ 𝑃 , 𝑄 ⟩ ) ⟩ ∙ ( 2nd ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ) = ( ⟨ 𝑁 , 𝑄 ⟩ ∙ 𝑆 ) )
52 op2ndg ⊢ ( ( 𝐾 ∈ ( 𝑃 𝐻 𝑅 ) ∧ 𝐿 ∈ ( 𝑄 𝐽 𝑆 ) ) → ( 2nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐿 )
53 17 18 52 syl2anc ⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐿 )
54 op2ndg ⊢ ( ( 𝐹 ∈ ( 𝑀 𝐻 𝑃 ) ∧ 𝐺 ∈ ( 𝑁 𝐽 𝑄 ) ) → ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
55 15 16 54 syl2anc ⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
56 51 53 55 oveq123d ⊢ ( 𝜑 → ( ( 2nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ( ⟨ ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 2nd ‘ ⟨ 𝑃 , 𝑄 ⟩ ) ⟩ ∙ ( 2nd ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ) ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) = ( 𝐿 ( ⟨ 𝑁 , 𝑄 ⟩ ∙ 𝑆 ) 𝐺 ) )
57 43 56 opeq12d ⊢ ( 𝜑 → ⟨ ( ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ( ⟨ ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 1st ‘ ⟨ 𝑃 , 𝑄 ⟩ ) ⟩ · ( 1st ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ) ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) , ( ( 2nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ( ⟨ ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 2nd ‘ ⟨ 𝑃 , 𝑄 ⟩ ) ⟩ ∙ ( 2nd ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ) ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) ⟩ = ⟨ ( 𝐾 ( ⟨ 𝑀 , 𝑃 ⟩ · 𝑅 ) 𝐹 ) , ( 𝐿 ( ⟨ 𝑁 , 𝑄 ⟩ ∙ 𝑆 ) 𝐺 ) ⟩ )
58 30 57 eqtrd ⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ( ⟨ ⟨ 𝑀 , 𝑁 ⟩ , ⟨ 𝑃 , 𝑄 ⟩ ⟩ 𝑂 ⟨ 𝑅 , 𝑆 ⟩ ) ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ ( 𝐾 ( ⟨ 𝑀 , 𝑃 ⟩ · 𝑅 ) 𝐹 ) , ( 𝐿 ( ⟨ 𝑁 , 𝑄 ⟩ ∙ 𝑆 ) 𝐺 ) ⟩ )