yon12

Description: Value of the Yoneda embedding at a morphism. The partially evaluated Yoneda embedding is also the contravariant Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017)

	Ref	Expression
Hypotheses	yon11.y	$⊢ Y = Yon (C)$
	yon11.b	$⊢ B = {Base}_{C}$
	yon11.c	$⊢ φ \to C \in Cat$
	yon11.p	$⊢ φ \to X \in B$
	yon11.h	$⊢ H = Hom (C)$
	yon11.z	$⊢ φ \to Z \in B$
	yon12.x	$⊢ \underset{˙}{\cdot} = comp (C)$
	yon12.w	$⊢ φ \to W \in B$
	yon12.f	$⊢ φ \to F \in (W H Z)$
	yon12.g	$⊢ φ \to G \in (Z H X)$
Assertion	yon12	$⊢ φ \to (Z 2^{nd} (1^{st} (Y) (X)) W) (F) (G) = G (⟨W, Z⟩ \underset{˙}{\cdot} X) F$

Proof

Step	Hyp	Ref	Expression
1		yon11.y	$⊢ Y = Yon (C)$
2		yon11.b	$⊢ B = {Base}_{C}$
3		yon11.c	$⊢ φ \to C \in Cat$
4		yon11.p	$⊢ φ \to X \in B$
5		yon11.h	$⊢ H = Hom (C)$
6		yon11.z	$⊢ φ \to Z \in B$
7		yon12.x	$⊢ \underset{˙}{\cdot} = comp (C)$
8		yon12.w	$⊢ φ \to W \in B$
9		yon12.f	$⊢ φ \to F \in (W H Z)$
10		yon12.g	$⊢ φ \to G \in (Z H X)$
11		eqid	$⊢ oppCat (C) = oppCat (C)$
12		eqid	$⊢ {Hom}_{F} (oppCat (C)) = {Hom}_{F} (oppCat (C))$
13	1 3 11 12	yonval	$⊢ φ \to Y = ⟨C, oppCat (C)⟩ {curry}_{F} {Hom}_{F} (oppCat (C))$
14	13	fveq2d	$⊢ φ \to 1^{st} (Y) = 1^{st} (⟨C, oppCat (C)⟩ {curry}_{F} {Hom}_{F} (oppCat (C)))$
15	14	fveq1d	$⊢ φ \to 1^{st} (Y) (X) = 1^{st} (⟨C, oppCat (C)⟩ {curry}_{F} {Hom}_{F} (oppCat (C))) (X)$
16	15	fveq2d	$⊢ φ \to 2^{nd} (1^{st} (Y) (X)) = 2^{nd} (1^{st} (⟨C, oppCat (C)⟩ {curry}_{F} {Hom}_{F} (oppCat (C))) (X))$
17	16	oveqd	$⊢ φ \to Z 2^{nd} (1^{st} (Y) (X)) W = Z 2^{nd} (1^{st} (⟨C, oppCat (C)⟩ {curry}_{F} {Hom}_{F} (oppCat (C))) (X)) W$
18	17	fveq1d	$⊢ φ \to (Z 2^{nd} (1^{st} (Y) (X)) W) (F) = (Z 2^{nd} (1^{st} (⟨C, oppCat (C)⟩ {curry}_{F} {Hom}_{F} (oppCat (C))) (X)) W) (F)$
19		eqid	$⊢ ⟨C, oppCat (C)⟩ {curry}_{F} {Hom}_{F} (oppCat (C)) = ⟨C, oppCat (C)⟩ {curry}_{F} {Hom}_{F} (oppCat (C))$
20	11	oppccat	$⊢ C \in Cat \to oppCat (C) \in Cat$
21	3 20	syl	$⊢ φ \to oppCat (C) \in Cat$
22		eqid	$⊢ SetCat (ran {Hom}_{𝑓} (C)) = SetCat (ran {Hom}_{𝑓} (C))$
23		fvex	$⊢ {Hom}_{𝑓} (C) \in V$
24	23	rnex	$⊢ ran {Hom}_{𝑓} (C) \in V$
25	24	a1i	$⊢ φ \to ran {Hom}_{𝑓} (C) \in V$
26		ssidd	$⊢ φ \to ran {Hom}_{𝑓} (C) \subseteq ran {Hom}_{𝑓} (C)$
27	11 12 22 3 25 26	oppchofcl	$⊢ φ \to {Hom}_{F} (oppCat (C)) \in ((C \times_{c} oppCat (C)) Func SetCat (ran {Hom}_{𝑓} (C)))$
28	11 2	oppcbas	$⊢ B = {Base}_{oppCat (C)}$
29		eqid	$⊢ 1^{st} (⟨C, oppCat (C)⟩ {curry}_{F} {Hom}_{F} (oppCat (C))) (X) = 1^{st} (⟨C, oppCat (C)⟩ {curry}_{F} {Hom}_{F} (oppCat (C))) (X)$
30		eqid	$⊢ Hom (oppCat (C)) = Hom (oppCat (C))$
31		eqid	$⊢ Id (C) = Id (C)$
32	5 11	oppchom	$⊢ Z Hom (oppCat (C)) W = W H Z$
33	9 32	eleqtrrdi	$⊢ φ \to F \in (Z Hom (oppCat (C)) W)$
34	19 2 3 21 27 28 4 29 6 30 31 8 33	curf12	$⊢ φ \to (Z 2^{nd} (1^{st} (⟨C, oppCat (C)⟩ {curry}_{F} {Hom}_{F} (oppCat (C))) (X)) W) (F) = Id (C) (X) (⟨X, Z⟩ 2^{nd} ({Hom}_{F} (oppCat (C))) ⟨X, W⟩) F$
35	18 34	eqtrd	$⊢ φ \to (Z 2^{nd} (1^{st} (Y) (X)) W) (F) = Id (C) (X) (⟨X, Z⟩ 2^{nd} ({Hom}_{F} (oppCat (C))) ⟨X, W⟩) F$
36	35	fveq1d	$⊢ φ \to (Z 2^{nd} (1^{st} (Y) (X)) W) (F) (G) = (Id (C) (X) (⟨X, Z⟩ 2^{nd} ({Hom}_{F} (oppCat (C))) ⟨X, W⟩) F) (G)$
37		eqid	$⊢ comp (oppCat (C)) = comp (oppCat (C))$
38	2 5 31 3 4	catidcl	$⊢ φ \to Id (C) (X) \in (X H X)$
39	5 11	oppchom	$⊢ X Hom (oppCat (C)) X = X H X$
40	38 39	eleqtrrdi	$⊢ φ \to Id (C) (X) \in (X Hom (oppCat (C)) X)$
41	5 11	oppchom	$⊢ X Hom (oppCat (C)) Z = Z H X$
42	10 41	eleqtrrdi	$⊢ φ \to G \in (X Hom (oppCat (C)) Z)$
43	12 21 28 30 4 6 4 8 37 40 33 42	hof2	$⊢ φ \to (Id (C) (X) (⟨X, Z⟩ 2^{nd} ({Hom}_{F} (oppCat (C))) ⟨X, W⟩) F) (G) = (F (⟨X, Z⟩ comp (oppCat (C)) W) G) (⟨X, X⟩ comp (oppCat (C)) W) Id (C) (X)$
44	2 7 11 4 6 8	oppcco	$⊢ φ \to F (⟨X, Z⟩ comp (oppCat (C)) W) G = G (⟨W, Z⟩ \underset{˙}{\cdot} X) F$
45	44	oveq1d	$⊢ φ \to (F (⟨X, Z⟩ comp (oppCat (C)) W) G) (⟨X, X⟩ comp (oppCat (C)) W) Id (C) (X) = (G (⟨W, Z⟩ \underset{˙}{\cdot} X) F) (⟨X, X⟩ comp (oppCat (C)) W) Id (C) (X)$
46	2 7 11 4 4 8	oppcco	$⊢ φ \to (G (⟨W, Z⟩ \underset{˙}{\cdot} X) F) (⟨X, X⟩ comp (oppCat (C)) W) Id (C) (X) = Id (C) (X) (⟨W, X⟩ \underset{˙}{\cdot} X) (G (⟨W, Z⟩ \underset{˙}{\cdot} X) F)$
47	2 5 7 3 8 6 4 9 10	catcocl	$⊢ φ \to G (⟨W, Z⟩ \underset{˙}{\cdot} X) F \in (W H X)$
48	2 5 31 3 8 7 4 47	catlid	$⊢ φ \to Id (C) (X) (⟨W, X⟩ \underset{˙}{\cdot} X) (G (⟨W, Z⟩ \underset{˙}{\cdot} X) F) = G (⟨W, Z⟩ \underset{˙}{\cdot} X) F$
49	45 46 48	3eqtrd	$⊢ φ \to (F (⟨X, Z⟩ comp (oppCat (C)) W) G) (⟨X, X⟩ comp (oppCat (C)) W) Id (C) (X) = G (⟨W, Z⟩ \underset{˙}{\cdot} X) F$
50	36 43 49	3eqtrd	$⊢ φ \to (Z 2^{nd} (1^{st} (Y) (X)) W) (F) (G) = G (⟨W, Z⟩ \underset{˙}{\cdot} X) F$

Metamath Proof Explorer

Theorem yon12

Proof