df-evlf

Description: Define the evaluation functor, which is the extension of the evaluation map f , x |-> ( fx ) of functors, to a functor ( C --> D ) X. C --> D . (Contributed by Mario Carneiro, 11-Jan-2017)

		Ref	Expression
	Assertion	df-evlf	⊢ eval_F = ( 𝑐 ∈ Cat , 𝑑 ∈ Cat ↦ ⟨ ( 𝑓 ∈ ( 𝑐 Func 𝑑 ) , 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) , ( 𝑥 ∈ ( ( 𝑐 Func 𝑑 ) × ( Base ‘ 𝑐 ) ) , 𝑦 ∈ ( ( 𝑐 Func 𝑑 ) × ( Base ‘ 𝑐 ) ) ↦ ⦋ ( 1^st ‘ 𝑥 ) / 𝑚 ⦌ ⦋ ( 1^st ‘ 𝑦 ) / 𝑛 ⦌ ( 𝑎 ∈ ( 𝑚 ( 𝑐 Nat 𝑑 ) 𝑛 ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ( 𝑎 ‘ ( 2^nd ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝑑 ) ( ( 1^st ‘ 𝑛 ) ‘ ( 2^nd ‘ 𝑦 ) ) ) ( ( ( 2^nd ‘ 𝑥 ) ( 2^nd ‘ 𝑚 ) ( 2^nd ‘ 𝑦 ) ) ‘ 𝑔 ) ) ) ) ⟩ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cevlf	⊢ eval_F
1		vc	⊢ 𝑐
2		ccat	⊢ Cat
3		vd	⊢ 𝑑
4		vf	⊢ 𝑓
5	1	cv	⊢ 𝑐
6		cfunc	⊢ Func
7	3	cv	⊢ 𝑑
8	5 7 6	co	⊢ ( 𝑐 Func 𝑑 )
9		vx	⊢ 𝑥
10		cbs	⊢ Base
11	5 10	cfv	⊢ ( Base ‘ 𝑐 )
12		c1st	⊢ 1^st
13	4	cv	⊢ 𝑓
14	13 12	cfv	⊢ ( 1^st ‘ 𝑓 )
15	9	cv	⊢ 𝑥
16	15 14	cfv	⊢ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 )
17	4 9 8 11 16	cmpo	⊢ ( 𝑓 ∈ ( 𝑐 Func 𝑑 ) , 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) )
18	8 11	cxp	⊢ ( ( 𝑐 Func 𝑑 ) × ( Base ‘ 𝑐 ) )
19		vy	⊢ 𝑦
20	15 12	cfv	⊢ ( 1^st ‘ 𝑥 )
21		vm	⊢ 𝑚
22	19	cv	⊢ 𝑦
23	22 12	cfv	⊢ ( 1^st ‘ 𝑦 )
24		vn	⊢ 𝑛
25		va	⊢ 𝑎
26	21	cv	⊢ 𝑚
27		cnat	⊢ Nat
28	5 7 27	co	⊢ ( 𝑐 Nat 𝑑 )
29	24	cv	⊢ 𝑛
30	26 29 28	co	⊢ ( 𝑚 ( 𝑐 Nat 𝑑 ) 𝑛 )
31		vg	⊢ 𝑔
32		c2nd	⊢ 2^nd
33	15 32	cfv	⊢ ( 2^nd ‘ 𝑥 )
34		chom	⊢ Hom
35	5 34	cfv	⊢ ( Hom ‘ 𝑐 )
36	22 32	cfv	⊢ ( 2^nd ‘ 𝑦 )
37	33 36 35	co	⊢ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) )
38	25	cv	⊢ 𝑎
39	36 38	cfv	⊢ ( 𝑎 ‘ ( 2^nd ‘ 𝑦 ) )
40	26 12	cfv	⊢ ( 1^st ‘ 𝑚 )
41	33 40	cfv	⊢ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) )
42	36 40	cfv	⊢ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) )
43	41 42	cop	⊢ ⟨ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) ) ⟩
44		cco	⊢ comp
45	7 44	cfv	⊢ ( comp ‘ 𝑑 )
46	29 12	cfv	⊢ ( 1^st ‘ 𝑛 )
47	36 46	cfv	⊢ ( ( 1^st ‘ 𝑛 ) ‘ ( 2^nd ‘ 𝑦 ) )
48	43 47 45	co	⊢ ( ⟨ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝑑 ) ( ( 1^st ‘ 𝑛 ) ‘ ( 2^nd ‘ 𝑦 ) ) )
49	26 32	cfv	⊢ ( 2^nd ‘ 𝑚 )
50	33 36 49	co	⊢ ( ( 2^nd ‘ 𝑥 ) ( 2^nd ‘ 𝑚 ) ( 2^nd ‘ 𝑦 ) )
51	31	cv	⊢ 𝑔
52	51 50	cfv	⊢ ( ( ( 2^nd ‘ 𝑥 ) ( 2^nd ‘ 𝑚 ) ( 2^nd ‘ 𝑦 ) ) ‘ 𝑔 )
53	39 52 48	co	⊢ ( ( 𝑎 ‘ ( 2^nd ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝑑 ) ( ( 1^st ‘ 𝑛 ) ‘ ( 2^nd ‘ 𝑦 ) ) ) ( ( ( 2^nd ‘ 𝑥 ) ( 2^nd ‘ 𝑚 ) ( 2^nd ‘ 𝑦 ) ) ‘ 𝑔 ) )
54	25 31 30 37 53	cmpo	⊢ ( 𝑎 ∈ ( 𝑚 ( 𝑐 Nat 𝑑 ) 𝑛 ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ( 𝑎 ‘ ( 2^nd ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝑑 ) ( ( 1^st ‘ 𝑛 ) ‘ ( 2^nd ‘ 𝑦 ) ) ) ( ( ( 2^nd ‘ 𝑥 ) ( 2^nd ‘ 𝑚 ) ( 2^nd ‘ 𝑦 ) ) ‘ 𝑔 ) ) )
55	24 23 54	csb	⊢ ⦋ ( 1^st ‘ 𝑦 ) / 𝑛 ⦌ ( 𝑎 ∈ ( 𝑚 ( 𝑐 Nat 𝑑 ) 𝑛 ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ( 𝑎 ‘ ( 2^nd ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝑑 ) ( ( 1^st ‘ 𝑛 ) ‘ ( 2^nd ‘ 𝑦 ) ) ) ( ( ( 2^nd ‘ 𝑥 ) ( 2^nd ‘ 𝑚 ) ( 2^nd ‘ 𝑦 ) ) ‘ 𝑔 ) ) )
56	21 20 55	csb	⊢ ⦋ ( 1^st ‘ 𝑥 ) / 𝑚 ⦌ ⦋ ( 1^st ‘ 𝑦 ) / 𝑛 ⦌ ( 𝑎 ∈ ( 𝑚 ( 𝑐 Nat 𝑑 ) 𝑛 ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ( 𝑎 ‘ ( 2^nd ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝑑 ) ( ( 1^st ‘ 𝑛 ) ‘ ( 2^nd ‘ 𝑦 ) ) ) ( ( ( 2^nd ‘ 𝑥 ) ( 2^nd ‘ 𝑚 ) ( 2^nd ‘ 𝑦 ) ) ‘ 𝑔 ) ) )
57	9 19 18 18 56	cmpo	⊢ ( 𝑥 ∈ ( ( 𝑐 Func 𝑑 ) × ( Base ‘ 𝑐 ) ) , 𝑦 ∈ ( ( 𝑐 Func 𝑑 ) × ( Base ‘ 𝑐 ) ) ↦ ⦋ ( 1^st ‘ 𝑥 ) / 𝑚 ⦌ ⦋ ( 1^st ‘ 𝑦 ) / 𝑛 ⦌ ( 𝑎 ∈ ( 𝑚 ( 𝑐 Nat 𝑑 ) 𝑛 ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ( 𝑎 ‘ ( 2^nd ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝑑 ) ( ( 1^st ‘ 𝑛 ) ‘ ( 2^nd ‘ 𝑦 ) ) ) ( ( ( 2^nd ‘ 𝑥 ) ( 2^nd ‘ 𝑚 ) ( 2^nd ‘ 𝑦 ) ) ‘ 𝑔 ) ) ) )
58	17 57	cop	⊢ ⟨ ( 𝑓 ∈ ( 𝑐 Func 𝑑 ) , 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) , ( 𝑥 ∈ ( ( 𝑐 Func 𝑑 ) × ( Base ‘ 𝑐 ) ) , 𝑦 ∈ ( ( 𝑐 Func 𝑑 ) × ( Base ‘ 𝑐 ) ) ↦ ⦋ ( 1^st ‘ 𝑥 ) / 𝑚 ⦌ ⦋ ( 1^st ‘ 𝑦 ) / 𝑛 ⦌ ( 𝑎 ∈ ( 𝑚 ( 𝑐 Nat 𝑑 ) 𝑛 ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ( 𝑎 ‘ ( 2^nd ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝑑 ) ( ( 1^st ‘ 𝑛 ) ‘ ( 2^nd ‘ 𝑦 ) ) ) ( ( ( 2^nd ‘ 𝑥 ) ( 2^nd ‘ 𝑚 ) ( 2^nd ‘ 𝑦 ) ) ‘ 𝑔 ) ) ) ) ⟩
59	1 3 2 2 58	cmpo	⊢ ( 𝑐 ∈ Cat , 𝑑 ∈ Cat ↦ ⟨ ( 𝑓 ∈ ( 𝑐 Func 𝑑 ) , 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) , ( 𝑥 ∈ ( ( 𝑐 Func 𝑑 ) × ( Base ‘ 𝑐 ) ) , 𝑦 ∈ ( ( 𝑐 Func 𝑑 ) × ( Base ‘ 𝑐 ) ) ↦ ⦋ ( 1^st ‘ 𝑥 ) / 𝑚 ⦌ ⦋ ( 1^st ‘ 𝑦 ) / 𝑛 ⦌ ( 𝑎 ∈ ( 𝑚 ( 𝑐 Nat 𝑑 ) 𝑛 ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ( 𝑎 ‘ ( 2^nd ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝑑 ) ( ( 1^st ‘ 𝑛 ) ‘ ( 2^nd ‘ 𝑦 ) ) ) ( ( ( 2^nd ‘ 𝑥 ) ( 2^nd ‘ 𝑚 ) ( 2^nd ‘ 𝑦 ) ) ‘ 𝑔 ) ) ) ) ⟩ )
60	0 59	wceq	⊢ eval_F = ( 𝑐 ∈ Cat , 𝑑 ∈ Cat ↦ ⟨ ( 𝑓 ∈ ( 𝑐 Func 𝑑 ) , 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) , ( 𝑥 ∈ ( ( 𝑐 Func 𝑑 ) × ( Base ‘ 𝑐 ) ) , 𝑦 ∈ ( ( 𝑐 Func 𝑑 ) × ( Base ‘ 𝑐 ) ) ↦ ⦋ ( 1^st ‘ 𝑥 ) / 𝑚 ⦌ ⦋ ( 1^st ‘ 𝑦 ) / 𝑛 ⦌ ( 𝑎 ∈ ( 𝑚 ( 𝑐 Nat 𝑑 ) 𝑛 ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ( 𝑎 ‘ ( 2^nd ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝑑 ) ( ( 1^st ‘ 𝑛 ) ‘ ( 2^nd ‘ 𝑦 ) ) ) ( ( ( 2^nd ‘ 𝑥 ) ( 2^nd ‘ 𝑚 ) ( 2^nd ‘ 𝑦 ) ) ‘ 𝑔 ) ) ) ) ⟩ )

Metamath Proof Explorer

Definition df-evlf

Detailed syntax breakdown