Metamath Proof Explorer


Theorem diag12

Description: Value of the constant functor at a morphism. (Contributed by Mario Carneiro, 6-Jan-2017) (Revised by Mario Carneiro, 15-Jan-2017)

Ref Expression
Hypotheses diagval.l 𝐿 = ( 𝐶 Δfunc 𝐷 )
diagval.c ( 𝜑𝐶 ∈ Cat )
diagval.d ( 𝜑𝐷 ∈ Cat )
diag11.a 𝐴 = ( Base ‘ 𝐶 )
diag11.c ( 𝜑𝑋𝐴 )
diag11.k 𝐾 = ( ( 1st𝐿 ) ‘ 𝑋 )
diag11.b 𝐵 = ( Base ‘ 𝐷 )
diag11.y ( 𝜑𝑌𝐵 )
diag12.j 𝐽 = ( Hom ‘ 𝐷 )
diag12.i 1 = ( Id ‘ 𝐶 )
diag12.z ( 𝜑𝑍𝐵 )
diag12.f ( 𝜑𝐹 ∈ ( 𝑌 𝐽 𝑍 ) )
Assertion diag12 ( 𝜑 → ( ( 𝑌 ( 2nd𝐾 ) 𝑍 ) ‘ 𝐹 ) = ( 1𝑋 ) )

Proof

Step Hyp Ref Expression
1 diagval.l 𝐿 = ( 𝐶 Δfunc 𝐷 )
2 diagval.c ( 𝜑𝐶 ∈ Cat )
3 diagval.d ( 𝜑𝐷 ∈ Cat )
4 diag11.a 𝐴 = ( Base ‘ 𝐶 )
5 diag11.c ( 𝜑𝑋𝐴 )
6 diag11.k 𝐾 = ( ( 1st𝐿 ) ‘ 𝑋 )
7 diag11.b 𝐵 = ( Base ‘ 𝐷 )
8 diag11.y ( 𝜑𝑌𝐵 )
9 diag12.j 𝐽 = ( Hom ‘ 𝐷 )
10 diag12.i 1 = ( Id ‘ 𝐶 )
11 diag12.z ( 𝜑𝑍𝐵 )
12 diag12.f ( 𝜑𝐹 ∈ ( 𝑌 𝐽 𝑍 ) )
13 1 2 3 diagval ( 𝜑𝐿 = ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) )
14 13 fveq2d ( 𝜑 → ( 1st𝐿 ) = ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) ) )
15 14 fveq1d ( 𝜑 → ( ( 1st𝐿 ) ‘ 𝑋 ) = ( ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) ) ‘ 𝑋 ) )
16 6 15 eqtrid ( 𝜑𝐾 = ( ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) ) ‘ 𝑋 ) )
17 16 fveq2d ( 𝜑 → ( 2nd𝐾 ) = ( 2nd ‘ ( ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) ) ‘ 𝑋 ) ) )
18 17 oveqd ( 𝜑 → ( 𝑌 ( 2nd𝐾 ) 𝑍 ) = ( 𝑌 ( 2nd ‘ ( ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) ) ‘ 𝑋 ) ) 𝑍 ) )
19 18 fveq1d ( 𝜑 → ( ( 𝑌 ( 2nd𝐾 ) 𝑍 ) ‘ 𝐹 ) = ( ( 𝑌 ( 2nd ‘ ( ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) ) ‘ 𝑋 ) ) 𝑍 ) ‘ 𝐹 ) )
20 eqid ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) = ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) )
21 eqid ( 𝐶 ×c 𝐷 ) = ( 𝐶 ×c 𝐷 )
22 eqid ( 𝐶 1stF 𝐷 ) = ( 𝐶 1stF 𝐷 )
23 21 2 3 22 1stfcl ( 𝜑 → ( 𝐶 1stF 𝐷 ) ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐶 ) )
24 eqid ( ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) ) ‘ 𝑋 ) = ( ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) ) ‘ 𝑋 )
25 20 4 2 3 23 7 5 24 8 9 10 11 12 curf12 ( 𝜑 → ( ( 𝑌 ( 2nd ‘ ( ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) ) ‘ 𝑋 ) ) 𝑍 ) ‘ 𝐹 ) = ( ( 1𝑋 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ ( 𝐶 1stF 𝐷 ) ) ⟨ 𝑋 , 𝑍 ⟩ ) 𝐹 ) )
26 df-ov ( ( 1𝑋 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ ( 𝐶 1stF 𝐷 ) ) ⟨ 𝑋 , 𝑍 ⟩ ) 𝐹 ) = ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ ( 𝐶 1stF 𝐷 ) ) ⟨ 𝑋 , 𝑍 ⟩ ) ‘ ⟨ ( 1𝑋 ) , 𝐹 ⟩ )
27 21 4 7 xpcbas ( 𝐴 × 𝐵 ) = ( Base ‘ ( 𝐶 ×c 𝐷 ) )
28 eqid ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) = ( Hom ‘ ( 𝐶 ×c 𝐷 ) )
29 5 8 opelxpd ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐴 × 𝐵 ) )
30 5 11 opelxpd ( 𝜑 → ⟨ 𝑋 , 𝑍 ⟩ ∈ ( 𝐴 × 𝐵 ) )
31 21 27 28 2 3 22 29 30 1stf2 ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ ( 𝐶 1stF 𝐷 ) ) ⟨ 𝑋 , 𝑍 ⟩ ) = ( 1st ↾ ( ⟨ 𝑋 , 𝑌 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑋 , 𝑍 ⟩ ) ) )
32 31 fveq1d ( 𝜑 → ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ ( 𝐶 1stF 𝐷 ) ) ⟨ 𝑋 , 𝑍 ⟩ ) ‘ ⟨ ( 1𝑋 ) , 𝐹 ⟩ ) = ( ( 1st ↾ ( ⟨ 𝑋 , 𝑌 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑋 , 𝑍 ⟩ ) ) ‘ ⟨ ( 1𝑋 ) , 𝐹 ⟩ ) )
33 26 32 eqtrid ( 𝜑 → ( ( 1𝑋 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ ( 𝐶 1stF 𝐷 ) ) ⟨ 𝑋 , 𝑍 ⟩ ) 𝐹 ) = ( ( 1st ↾ ( ⟨ 𝑋 , 𝑌 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑋 , 𝑍 ⟩ ) ) ‘ ⟨ ( 1𝑋 ) , 𝐹 ⟩ ) )
34 eqid ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
35 4 34 10 2 5 catidcl ( 𝜑 → ( 1𝑋 ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
36 35 12 opelxpd ( 𝜑 → ⟨ ( 1𝑋 ) , 𝐹 ⟩ ∈ ( ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) × ( 𝑌 𝐽 𝑍 ) ) )
37 21 4 7 34 9 5 8 5 11 28 xpchom2 ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑋 , 𝑍 ⟩ ) = ( ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) × ( 𝑌 𝐽 𝑍 ) ) )
38 36 37 eleqtrrd ( 𝜑 → ⟨ ( 1𝑋 ) , 𝐹 ⟩ ∈ ( ⟨ 𝑋 , 𝑌 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑋 , 𝑍 ⟩ ) )
39 38 fvresd ( 𝜑 → ( ( 1st ↾ ( ⟨ 𝑋 , 𝑌 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑋 , 𝑍 ⟩ ) ) ‘ ⟨ ( 1𝑋 ) , 𝐹 ⟩ ) = ( 1st ‘ ⟨ ( 1𝑋 ) , 𝐹 ⟩ ) )
40 op1stg ( ( ( 1𝑋 ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝐹 ∈ ( 𝑌 𝐽 𝑍 ) ) → ( 1st ‘ ⟨ ( 1𝑋 ) , 𝐹 ⟩ ) = ( 1𝑋 ) )
41 35 12 40 syl2anc ( 𝜑 → ( 1st ‘ ⟨ ( 1𝑋 ) , 𝐹 ⟩ ) = ( 1𝑋 ) )
42 33 39 41 3eqtrd ( 𝜑 → ( ( 1𝑋 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ ( 𝐶 1stF 𝐷 ) ) ⟨ 𝑋 , 𝑍 ⟩ ) 𝐹 ) = ( 1𝑋 ) )
43 19 25 42 3eqtrd ( 𝜑 → ( ( 𝑌 ( 2nd𝐾 ) 𝑍 ) ‘ 𝐹 ) = ( 1𝑋 ) )