evlf2

Description: Value of the evaluation functor at a morphism. (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$
	evlf2.f	$⊢ φ \to F \in (C Func D)$
	evlf2.g	$⊢ φ \to G \in (C Func D)$
	evlf2.x	$⊢ φ \to X \in B$
	evlf2.y	$⊢ φ \to Y \in B$
	evlf2.l	$⊢ L = ⟨F, X⟩ 2^{nd} (E) ⟨G, Y⟩$
Assertion	evlf2	$⊢ φ \to L = (a \in (F N G), g \in (X H Y) ⟼ a (Y) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ \underset{˙}{\cdot} 1^{st} (G) (Y)) (X 2^{nd} (F) 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		evlf2.f	$⊢ φ \to F \in (C Func D)$
9		evlf2.g	$⊢ φ \to G \in (C Func D)$
10		evlf2.x	$⊢ φ \to X \in B$
11		evlf2.y	$⊢ φ \to Y \in B$
12		evlf2.l	$⊢ L = ⟨F, X⟩ 2^{nd} (E) ⟨G, Y⟩$
13	1 2 3 4 5 6 7	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)))⟩$
14		ovex	$⊢ C Func D \in V$
15	4	fvexi	$⊢ B \in V$
16	14 15	mpoex	$⊢ (f \in (C Func D), x \in B ⟼ 1^{st} (f) (x)) \in V$
17	14 15	xpex	$⊢ (C Func D) \times B \in V$
18	17 17	mpoex	$⊢ (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$
19	16 18	op2ndd	$⊢ 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)))⟩ \to 2^{nd} (E) = (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)))$
20	13 19	syl	$⊢ φ \to 2^{nd} (E) = (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)))$
21		fvexd	$⊢ (φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \to 1^{st} (x) \in V$
22		simprl	$⊢ (φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \to x = ⟨F, X⟩$
23	22	fveq2d	$⊢ (φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \to 1^{st} (x) = 1^{st} (⟨F, X⟩)$
24		op1stg	$⊢ (F \in (C Func D) \land X \in B) \to 1^{st} (⟨F, X⟩) = F$
25	8 10 24	syl2anc	$⊢ φ \to 1^{st} (⟨F, X⟩) = F$
26	25	adantr	$⊢ (φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \to 1^{st} (⟨F, X⟩) = F$
27	23 26	eqtrd	$⊢ (φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \to 1^{st} (x) = F$
28		fvexd	$⊢ ((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \to 1^{st} (y) \in V$
29		simplrr	$⊢ ((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \to y = ⟨G, Y⟩$
30	29	fveq2d	$⊢ ((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \to 1^{st} (y) = 1^{st} (⟨G, Y⟩)$
31		op1stg	$⊢ (G \in (C Func D) \land Y \in B) \to 1^{st} (⟨G, Y⟩) = G$
32	9 11 31	syl2anc	$⊢ φ \to 1^{st} (⟨G, Y⟩) = G$
33	32	ad2antrr	$⊢ ((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \to 1^{st} (⟨G, Y⟩) = G$
34	30 33	eqtrd	$⊢ ((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \to 1^{st} (y) = G$
35		simplr	$⊢ (((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \land n = G) \to m = F$
36		simpr	$⊢ (((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \land n = G) \to n = G$
37	35 36	oveq12d	$⊢ (((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \land n = G) \to m N n = F N G$
38	22	ad2antrr	$⊢ (((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \land n = G) \to x = ⟨F, X⟩$
39	38	fveq2d	$⊢ (((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \land n = G) \to 2^{nd} (x) = 2^{nd} (⟨F, X⟩)$
40		op2ndg	$⊢ (F \in (C Func D) \land X \in B) \to 2^{nd} (⟨F, X⟩) = X$
41	8 10 40	syl2anc	$⊢ φ \to 2^{nd} (⟨F, X⟩) = X$
42	41	ad3antrrr	$⊢ (((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \land n = G) \to 2^{nd} (⟨F, X⟩) = X$
43	39 42	eqtrd	$⊢ (((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \land n = G) \to 2^{nd} (x) = X$
44	29	adantr	$⊢ (((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \land n = G) \to y = ⟨G, Y⟩$
45	44	fveq2d	$⊢ (((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \land n = G) \to 2^{nd} (y) = 2^{nd} (⟨G, Y⟩)$
46		op2ndg	$⊢ (G \in (C Func D) \land Y \in B) \to 2^{nd} (⟨G, Y⟩) = Y$
47	9 11 46	syl2anc	$⊢ φ \to 2^{nd} (⟨G, Y⟩) = Y$
48	47	ad3antrrr	$⊢ (((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \land n = G) \to 2^{nd} (⟨G, Y⟩) = Y$
49	45 48	eqtrd	$⊢ (((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \land n = G) \to 2^{nd} (y) = Y$
50	43 49	oveq12d	$⊢ (((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \land n = G) \to 2^{nd} (x) H 2^{nd} (y) = X H Y$
51	35	fveq2d	$⊢ (((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \land n = G) \to 1^{st} (m) = 1^{st} (F)$
52	51 43	fveq12d	$⊢ (((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \land n = G) \to 1^{st} (m) (2^{nd} (x)) = 1^{st} (F) (X)$
53	51 49	fveq12d	$⊢ (((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \land n = G) \to 1^{st} (m) (2^{nd} (y)) = 1^{st} (F) (Y)$
54	52 53	opeq12d	$⊢ (((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \land n = G) \to ⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ = ⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩$
55	36	fveq2d	$⊢ (((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \land n = G) \to 1^{st} (n) = 1^{st} (G)$
56	55 49	fveq12d	$⊢ (((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \land n = G) \to 1^{st} (n) (2^{nd} (y)) = 1^{st} (G) (Y)$
57	54 56	oveq12d	$⊢ (((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \land n = G) \to ⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ \underset{˙}{\cdot} 1^{st} (n) (2^{nd} (y)) = ⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ \underset{˙}{\cdot} 1^{st} (G) (Y)$
58	49	fveq2d	$⊢ (((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \land n = G) \to a (2^{nd} (y)) = a (Y)$
59	35	fveq2d	$⊢ (((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \land n = G) \to 2^{nd} (m) = 2^{nd} (F)$
60	59 43 49	oveq123d	$⊢ (((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \land n = G) \to 2^{nd} (x) 2^{nd} (m) 2^{nd} (y) = X 2^{nd} (F) Y$
61	60	fveq1d	$⊢ (((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \land n = G) \to (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g) = (X 2^{nd} (F) Y) (g)$
62	57 58 61	oveq123d	$⊢ (((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \land n = G) \to 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) = a (Y) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ \underset{˙}{\cdot} 1^{st} (G) (Y)) (X 2^{nd} (F) Y) (g)$
63	37 50 62	mpoeq123dv	$⊢ (((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \land n = G) \to (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)) = (a \in (F N G), g \in (X H Y) ⟼ a (Y) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ \underset{˙}{\cdot} 1^{st} (G) (Y)) (X 2^{nd} (F) Y) (g))$
64	28 34 63	csbied2	$⊢ ((φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \land m = F) \to ⦋ 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)) = (a \in (F N G), g \in (X H Y) ⟼ a (Y) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ \underset{˙}{\cdot} 1^{st} (G) (Y)) (X 2^{nd} (F) Y) (g))$
65	21 27 64	csbied2	$⊢ (φ \land (x = ⟨F, X⟩ \land y = ⟨G, Y⟩)) \to ⦋ 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)) = (a \in (F N G), g \in (X H Y) ⟼ a (Y) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ \underset{˙}{\cdot} 1^{st} (G) (Y)) (X 2^{nd} (F) Y) (g))$
66	8 10	opelxpd	$⊢ φ \to ⟨F, X⟩ \in ((C Func D) \times B)$
67	9 11	opelxpd	$⊢ φ \to ⟨G, Y⟩ \in ((C Func D) \times B)$
68		ovex	$⊢ F N G \in V$
69		ovex	$⊢ X H Y \in V$
70	68 69	mpoex	$⊢ (a \in (F N G), g \in (X H Y) ⟼ a (Y) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ \underset{˙}{\cdot} 1^{st} (G) (Y)) (X 2^{nd} (F) Y) (g)) \in V$
71	70	a1i	$⊢ φ \to (a \in (F N G), g \in (X H Y) ⟼ a (Y) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ \underset{˙}{\cdot} 1^{st} (G) (Y)) (X 2^{nd} (F) Y) (g)) \in V$
72	20 65 66 67 71	ovmpod	$⊢ φ \to ⟨F, X⟩ 2^{nd} (E) ⟨G, Y⟩ = (a \in (F N G), g \in (X H Y) ⟼ a (Y) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ \underset{˙}{\cdot} 1^{st} (G) (Y)) (X 2^{nd} (F) Y) (g))$
73	12 72	syl5eq	$⊢ φ \to L = (a \in (F N G), g \in (X H Y) ⟼ a (Y) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ \underset{˙}{\cdot} 1^{st} (G) (Y)) (X 2^{nd} (F) Y) (g))$

Metamath Proof Explorer

Theorem evlf2

Proof