evlf2val

Description: Value of the evaluation natural transformation at an object. (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⟩$
	evlf2val.a	$⊢ φ \to A \in (F N G)$
	evlf2val.k	$⊢ φ \to K \in (X H Y)$
Assertion	evlf2val	$⊢ φ \to A L K = A (Y) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ \underset{˙}{\cdot} 1^{st} (G) (Y)) (X 2^{nd} (F) Y) (K)$

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		evlf2val.a	$⊢ φ \to A \in (F N G)$
14		evlf2val.k	$⊢ φ \to K \in (X H Y)$
15	1 2 3 4 5 6 7 8 9 10 11 12	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))$
16		simprl	$⊢ (φ \land (a = A \land g = K)) \to a = A$
17	16	fveq1d	$⊢ (φ \land (a = A \land g = K)) \to a (Y) = A (Y)$
18		simprr	$⊢ (φ \land (a = A \land g = K)) \to g = K$
19	18	fveq2d	$⊢ (φ \land (a = A \land g = K)) \to (X 2^{nd} (F) Y) (g) = (X 2^{nd} (F) Y) (K)$
20	17 19	oveq12d	$⊢ (φ \land (a = A \land g = K)) \to a (Y) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ \underset{˙}{\cdot} 1^{st} (G) (Y)) (X 2^{nd} (F) Y) (g) = A (Y) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ \underset{˙}{\cdot} 1^{st} (G) (Y)) (X 2^{nd} (F) Y) (K)$
21		ovexd	$⊢ φ \to A (Y) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ \underset{˙}{\cdot} 1^{st} (G) (Y)) (X 2^{nd} (F) Y) (K) \in V$
22	15 20 13 14 21	ovmpod	$⊢ φ \to A L K = A (Y) (⟨1^{st} (F) (X), 1^{st} (F) (Y)⟩ \underset{˙}{\cdot} 1^{st} (G) (Y)) (X 2^{nd} (F) Y) (K)$

Metamath Proof Explorer