evlfval

Description: Value of the evaluation functor. (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Hypotheses	evlfval.e	$⊢ E = C {eval}_{F} D$
	evlfval.c	$⊢ φ \to C \in Cat$
	evlfval.d	$⊢ φ \to D \in Cat$
	evlfval.b	$⊢ B = {Base}_{C}$
	evlfval.h	$⊢ H = Hom (C)$
	evlfval.o	$⊢ \underset{˙}{\cdot} = comp (D)$
	evlfval.n	$⊢ N = C Nat D$
Assertion	evlfval	$⊢ φ \to E = ⟨(f \in (C Func D), x \in B ⟼ 1^{st} (f) (x)), (x \in ((C Func D) \times B), y \in ((C Func D) \times B) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m N n), g \in (2^{nd} (x) H 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ \underset{˙}{\cdot} 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)))⟩$

Proof

Step	Hyp	Ref	Expression
1		evlfval.e	$⊢ E = C {eval}_{F} D$
2		evlfval.c	$⊢ φ \to C \in Cat$
3		evlfval.d	$⊢ φ \to D \in Cat$
4		evlfval.b	$⊢ B = {Base}_{C}$
5		evlfval.h	$⊢ H = Hom (C)$
6		evlfval.o	$⊢ \underset{˙}{\cdot} = comp (D)$
7		evlfval.n	$⊢ N = C Nat D$
8		df-evlf	$⊢ {eval}_{F} = (c \in Cat, d \in Cat ⟼ ⟨(f \in (c Func d), x \in {Base}_{c} ⟼ 1^{st} (f) (x)), (x \in ((c Func d) \times {Base}_{c}), y \in ((c Func d) \times {Base}_{c}) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m (c Nat d) n), g \in (2^{nd} (x) Hom (c) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (d) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)))⟩)$
9	8	a1i	$⊢ φ \to {eval}_{F} = (c \in Cat, d \in Cat ⟼ ⟨(f \in (c Func d), x \in {Base}_{c} ⟼ 1^{st} (f) (x)), (x \in ((c Func d) \times {Base}_{c}), y \in ((c Func d) \times {Base}_{c}) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m (c Nat d) n), g \in (2^{nd} (x) Hom (c) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (d) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)))⟩)$
10		simprl	$⊢ (φ \land (c = C \land d = D)) \to c = C$
11		simprr	$⊢ (φ \land (c = C \land d = D)) \to d = D$
12	10 11	oveq12d	$⊢ (φ \land (c = C \land d = D)) \to c Func d = C Func D$
13	10	fveq2d	$⊢ (φ \land (c = C \land d = D)) \to {Base}_{c} = {Base}_{C}$
14	13 4	syl6eqr	$⊢ (φ \land (c = C \land d = D)) \to {Base}_{c} = B$
15		eqidd	$⊢ (φ \land (c = C \land d = D)) \to 1^{st} (f) (x) = 1^{st} (f) (x)$
16	12 14 15	mpoeq123dv	$⊢ (φ \land (c = C \land d = D)) \to (f \in (c Func d), x \in {Base}_{c} ⟼ 1^{st} (f) (x)) = (f \in (C Func D), x \in B ⟼ 1^{st} (f) (x))$
17	12 14	xpeq12d	$⊢ (φ \land (c = C \land d = D)) \to (c Func d) \times {Base}_{c} = (C Func D) \times B$
18	10 11	oveq12d	$⊢ (φ \land (c = C \land d = D)) \to c Nat d = C Nat D$
19	18 7	syl6eqr	$⊢ (φ \land (c = C \land d = D)) \to c Nat d = N$
20	19	oveqd	$⊢ (φ \land (c = C \land d = D)) \to m (c Nat d) n = m N n$
21	10	fveq2d	$⊢ (φ \land (c = C \land d = D)) \to Hom (c) = Hom (C)$
22	21 5	syl6eqr	$⊢ (φ \land (c = C \land d = D)) \to Hom (c) = H$
23	22	oveqd	$⊢ (φ \land (c = C \land d = D)) \to 2^{nd} (x) Hom (c) 2^{nd} (y) = 2^{nd} (x) H 2^{nd} (y)$
24	11	fveq2d	$⊢ (φ \land (c = C \land d = D)) \to comp (d) = comp (D)$
25	24 6	syl6eqr	$⊢ (φ \land (c = C \land d = D)) \to comp (d) = \underset{˙}{\cdot}$
26	25	oveqd	$⊢ (φ \land (c = C \land d = D)) \to ⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (d) 1^{st} (n) (2^{nd} (y)) = ⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ \underset{˙}{\cdot} 1^{st} (n) (2^{nd} (y))$
27	26	oveqd	$⊢ (φ \land (c = C \land d = D)) \to a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (d) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g) = a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ \underset{˙}{\cdot} 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)$
28	20 23 27	mpoeq123dv	$⊢ (φ \land (c = C \land d = D)) \to (a \in (m (c Nat d) n), g \in (2^{nd} (x) Hom (c) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (d) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)) = (a \in (m N n), g \in (2^{nd} (x) H 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ \underset{˙}{\cdot} 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g))$
29	28	csbeq2dv	$⊢ (φ \land (c = C \land d = D)) \to ⦋ 1^{st} (y) / n ⦌ (a \in (m (c Nat d) n), g \in (2^{nd} (x) Hom (c) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (d) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)) = ⦋ 1^{st} (y) / n ⦌ (a \in (m N n), g \in (2^{nd} (x) H 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ \underset{˙}{\cdot} 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g))$
30	29	csbeq2dv	$⊢ (φ \land (c = C \land d = D)) \to ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m (c Nat d) n), g \in (2^{nd} (x) Hom (c) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (d) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)) = ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m N n), g \in (2^{nd} (x) H 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ \underset{˙}{\cdot} 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g))$
31	17 17 30	mpoeq123dv	$⊢ (φ \land (c = C \land d = D)) \to (x \in ((c Func d) \times {Base}_{c}), y \in ((c Func d) \times {Base}_{c}) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m (c Nat d) n), g \in (2^{nd} (x) Hom (c) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (d) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g))) = (x \in ((C Func D) \times B), y \in ((C Func D) \times B) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m N n), g \in (2^{nd} (x) H 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ \underset{˙}{\cdot} 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)))$
32	16 31	opeq12d	$⊢ (φ \land (c = C \land d = D)) \to ⟨(f \in (c Func d), x \in {Base}_{c} ⟼ 1^{st} (f) (x)), (x \in ((c Func d) \times {Base}_{c}), y \in ((c Func d) \times {Base}_{c}) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m (c Nat d) n), g \in (2^{nd} (x) Hom (c) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (d) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)))⟩ = ⟨(f \in (C Func D), x \in B ⟼ 1^{st} (f) (x)), (x \in ((C Func D) \times B), y \in ((C Func D) \times B) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m N n), g \in (2^{nd} (x) H 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ \underset{˙}{\cdot} 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)))⟩$
33		opex	$⊢ ⟨(f \in (C Func D), x \in B ⟼ 1^{st} (f) (x)), (x \in ((C Func D) \times B), y \in ((C Func D) \times B) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m N n), g \in (2^{nd} (x) H 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ \underset{˙}{\cdot} 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)))⟩ \in V$
34	33	a1i	$⊢ φ \to ⟨(f \in (C Func D), x \in B ⟼ 1^{st} (f) (x)), (x \in ((C Func D) \times B), y \in ((C Func D) \times B) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m N n), g \in (2^{nd} (x) H 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ \underset{˙}{\cdot} 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)))⟩ \in V$
35	9 32 2 3 34	ovmpod	$⊢ φ \to C {eval}_{F} D = ⟨(f \in (C Func D), x \in B ⟼ 1^{st} (f) (x)), (x \in ((C Func D) \times B), y \in ((C Func D) \times B) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m N n), g \in (2^{nd} (x) H 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ \underset{˙}{\cdot} 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)))⟩$
36	1 35	syl5eq	$⊢ φ \to E = ⟨(f \in (C Func D), x \in B ⟼ 1^{st} (f) (x)), (x \in ((C Func D) \times B), y \in ((C Func D) \times B) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m N n), g \in (2^{nd} (x) H 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ \underset{˙}{\cdot} 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)))⟩$

Metamath Proof Explorer

Theorem evlfval

Proof