hofcllem

	Ref	Expression
Hypotheses	hofcl.m	$⊢ M = {Hom}_{F} (C)$
	hofcl.o	$⊢ O = oppCat (C)$
	hofcl.d	$⊢ D = SetCat (U)$
	hofcl.c	$⊢ φ \to C \in Cat$
	hofcl.u	$⊢ φ \to U \in V$
	hofcl.h	$⊢ φ \to ran {Hom}_{𝑓} (C) \subseteq U$
	hofcllem.b	$⊢ B = {Base}_{C}$
	hofcllem.h	$⊢ H = Hom (C)$
	hofcllem.x	$⊢ φ \to X \in B$
	hofcllem.y	$⊢ φ \to Y \in B$
	hofcllem.z	$⊢ φ \to Z \in B$
	hofcllem.w	$⊢ φ \to W \in B$
	hofcllem.s	$⊢ φ \to S \in B$
	hofcllem.t	$⊢ φ \to T \in B$
	hofcllem.m	$⊢ φ \to K \in (Z H X)$
	hofcllem.n	$⊢ φ \to L \in (Y H W)$
	hofcllem.p	$⊢ φ \to P \in (S H Z)$
	hofcllem.q	$⊢ φ \to Q \in (W H T)$
Assertion	hofcllem	$⊢ φ \to (K (⟨S, Z⟩ comp (C) X) P) (⟨X, Y⟩ 2^{nd} (M) ⟨S, T⟩) (Q (⟨Y, W⟩ comp (C) T) L) = (P (⟨Z, W⟩ 2^{nd} (M) ⟨S, T⟩) Q) (⟨X H Y, Z H W⟩ comp (D) (S H T)) (K (⟨X, Y⟩ 2^{nd} (M) ⟨Z, W⟩) L)$

Proof

Step	Hyp	Ref	Expression
1		hofcl.m	$⊢ M = {Hom}_{F} (C)$
2		hofcl.o	$⊢ O = oppCat (C)$
3		hofcl.d	$⊢ D = SetCat (U)$
4		hofcl.c	$⊢ φ \to C \in Cat$
5		hofcl.u	$⊢ φ \to U \in V$
6		hofcl.h	$⊢ φ \to ran {Hom}_{𝑓} (C) \subseteq U$
7		hofcllem.b	$⊢ B = {Base}_{C}$
8		hofcllem.h	$⊢ H = Hom (C)$
9		hofcllem.x	$⊢ φ \to X \in B$
10		hofcllem.y	$⊢ φ \to Y \in B$
11		hofcllem.z	$⊢ φ \to Z \in B$
12		hofcllem.w	$⊢ φ \to W \in B$
13		hofcllem.s	$⊢ φ \to S \in B$
14		hofcllem.t	$⊢ φ \to T \in B$
15		hofcllem.m	$⊢ φ \to K \in (Z H X)$
16		hofcllem.n	$⊢ φ \to L \in (Y H W)$
17		hofcllem.p	$⊢ φ \to P \in (S H Z)$
18		hofcllem.q	$⊢ φ \to Q \in (W H T)$
19		eqid	$⊢ comp (C) = comp (C)$
20	4	adantr	$⊢ (φ \land f \in (X H Y)) \to C \in Cat$
21	13	adantr	$⊢ (φ \land f \in (X H Y)) \to S \in B$
22	11	adantr	$⊢ (φ \land f \in (X H Y)) \to Z \in B$
23	9	adantr	$⊢ (φ \land f \in (X H Y)) \to X \in B$
24	17	adantr	$⊢ (φ \land f \in (X H Y)) \to P \in (S H Z)$
25	15	adantr	$⊢ (φ \land f \in (X H Y)) \to K \in (Z H X)$
26	14	adantr	$⊢ (φ \land f \in (X H Y)) \to T \in B$
27	10	adantr	$⊢ (φ \land f \in (X H Y)) \to Y \in B$
28		simpr	$⊢ (φ \land f \in (X H Y)) \to f \in (X H Y)$
29	7 8 19 4 10 12 14 16 18	catcocl	$⊢ φ \to Q (⟨Y, W⟩ comp (C) T) L \in (Y H T)$
30	29	adantr	$⊢ (φ \land f \in (X H Y)) \to Q (⟨Y, W⟩ comp (C) T) L \in (Y H T)$
31	7 8 19 20 23 27 26 28 30	catcocl	$⊢ (φ \land f \in (X H Y)) \to (Q (⟨Y, W⟩ comp (C) T) L) (⟨X, Y⟩ comp (C) T) f \in (X H T)$
32	7 8 19 20 21 22 23 24 25 26 31	catass	$⊢ (φ \land f \in (X H Y)) \to (((Q (⟨Y, W⟩ comp (C) T) L) (⟨X, Y⟩ comp (C) T) f) (⟨Z, X⟩ comp (C) T) K) (⟨S, Z⟩ comp (C) T) P = ((Q (⟨Y, W⟩ comp (C) T) L) (⟨X, Y⟩ comp (C) T) f) (⟨S, X⟩ comp (C) T) (K (⟨S, Z⟩ comp (C) X) P)$
33	12	adantr	$⊢ (φ \land f \in (X H Y)) \to W \in B$
34	16	adantr	$⊢ (φ \land f \in (X H Y)) \to L \in (Y H W)$
35	18	adantr	$⊢ (φ \land f \in (X H Y)) \to Q \in (W H T)$
36	7 8 19 20 23 27 33 28 34 26 35	catass	$⊢ (φ \land f \in (X H Y)) \to (Q (⟨Y, W⟩ comp (C) T) L) (⟨X, Y⟩ comp (C) T) f = Q (⟨X, W⟩ comp (C) T) (L (⟨X, Y⟩ comp (C) W) f)$
37	36	oveq1d	$⊢ (φ \land f \in (X H Y)) \to ((Q (⟨Y, W⟩ comp (C) T) L) (⟨X, Y⟩ comp (C) T) f) (⟨Z, X⟩ comp (C) T) K = (Q (⟨X, W⟩ comp (C) T) (L (⟨X, Y⟩ comp (C) W) f)) (⟨Z, X⟩ comp (C) T) K$
38	7 8 19 20 23 27 33 28 34	catcocl	$⊢ (φ \land f \in (X H Y)) \to L (⟨X, Y⟩ comp (C) W) f \in (X H W)$
39	7 8 19 20 22 23 33 25 38 26 35	catass	$⊢ (φ \land f \in (X H Y)) \to (Q (⟨X, W⟩ comp (C) T) (L (⟨X, Y⟩ comp (C) W) f)) (⟨Z, X⟩ comp (C) T) K = Q (⟨Z, W⟩ comp (C) T) ((L (⟨X, Y⟩ comp (C) W) f) (⟨Z, X⟩ comp (C) W) K)$
40	37 39	eqtrd	$⊢ (φ \land f \in (X H Y)) \to ((Q (⟨Y, W⟩ comp (C) T) L) (⟨X, Y⟩ comp (C) T) f) (⟨Z, X⟩ comp (C) T) K = Q (⟨Z, W⟩ comp (C) T) ((L (⟨X, Y⟩ comp (C) W) f) (⟨Z, X⟩ comp (C) W) K)$
41	40	oveq1d	$⊢ (φ \land f \in (X H Y)) \to (((Q (⟨Y, W⟩ comp (C) T) L) (⟨X, Y⟩ comp (C) T) f) (⟨Z, X⟩ comp (C) T) K) (⟨S, Z⟩ comp (C) T) P = (Q (⟨Z, W⟩ comp (C) T) ((L (⟨X, Y⟩ comp (C) W) f) (⟨Z, X⟩ comp (C) W) K)) (⟨S, Z⟩ comp (C) T) P$
42	32 41	eqtr3d	$⊢ (φ \land f \in (X H Y)) \to ((Q (⟨Y, W⟩ comp (C) T) L) (⟨X, Y⟩ comp (C) T) f) (⟨S, X⟩ comp (C) T) (K (⟨S, Z⟩ comp (C) X) P) = (Q (⟨Z, W⟩ comp (C) T) ((L (⟨X, Y⟩ comp (C) W) f) (⟨Z, X⟩ comp (C) W) K)) (⟨S, Z⟩ comp (C) T) P$
43	42	mpteq2dva	$⊢ φ \to (f \in (X H Y) ⟼ ((Q (⟨Y, W⟩ comp (C) T) L) (⟨X, Y⟩ comp (C) T) f) (⟨S, X⟩ comp (C) T) (K (⟨S, Z⟩ comp (C) X) P)) = (f \in (X H Y) ⟼ (Q (⟨Z, W⟩ comp (C) T) ((L (⟨X, Y⟩ comp (C) W) f) (⟨Z, X⟩ comp (C) W) K)) (⟨S, Z⟩ comp (C) T) P)$
44	7 8 19 4 13 11 9 17 15	catcocl	$⊢ φ \to K (⟨S, Z⟩ comp (C) X) P \in (S H X)$
45	1 4 7 8 9 10 13 14 19 44 29	hof2val	$⊢ φ \to (K (⟨S, Z⟩ comp (C) X) P) (⟨X, Y⟩ 2^{nd} (M) ⟨S, T⟩) (Q (⟨Y, W⟩ comp (C) T) L) = (f \in (X H Y) ⟼ ((Q (⟨Y, W⟩ comp (C) T) L) (⟨X, Y⟩ comp (C) T) f) (⟨S, X⟩ comp (C) T) (K (⟨S, Z⟩ comp (C) X) P))$
46	1 4 7 8 11 12 13 14 19 17 18	hof2val	$⊢ φ \to P (⟨Z, W⟩ 2^{nd} (M) ⟨S, T⟩) Q = (g \in (Z H W) ⟼ (Q (⟨Z, W⟩ comp (C) T) g) (⟨S, Z⟩ comp (C) T) P)$
47	1 4 7 8 9 10 11 12 19 15 16	hof2val	$⊢ φ \to K (⟨X, Y⟩ 2^{nd} (M) ⟨Z, W⟩) L = (f \in (X H Y) ⟼ (L (⟨X, Y⟩ comp (C) W) f) (⟨Z, X⟩ comp (C) W) K)$
48	46 47	oveq12d	$⊢ φ \to (P (⟨Z, W⟩ 2^{nd} (M) ⟨S, T⟩) Q) (⟨X H Y, Z H W⟩ comp (D) (S H T)) (K (⟨X, Y⟩ 2^{nd} (M) ⟨Z, W⟩) L) = (g \in (Z H W) ⟼ (Q (⟨Z, W⟩ comp (C) T) g) (⟨S, Z⟩ comp (C) T) P) (⟨X H Y, Z H W⟩ comp (D) (S H T)) (f \in (X H Y) ⟼ (L (⟨X, Y⟩ comp (C) W) f) (⟨Z, X⟩ comp (C) W) K)$
49		eqid	$⊢ comp (D) = comp (D)$
50		eqid	$⊢ {Hom}_{𝑓} (C) = {Hom}_{𝑓} (C)$
51	50 7 8 9 10	homfval	$⊢ φ \to X {Hom}_{𝑓} (C) Y = X H Y$
52	50 7	homffn	$⊢ {Hom}_{𝑓} (C) Fn (B \times B)$
53	52	a1i	$⊢ φ \to {Hom}_{𝑓} (C) Fn (B \times B)$
54		df-f	$⊢ {Hom}_{𝑓} (C) : B \times B ⟶ U \leftrightarrow ({Hom}_{𝑓} (C) Fn (B \times B) \land ran {Hom}_{𝑓} (C) \subseteq U)$
55	53 6 54	sylanbrc	$⊢ φ \to {Hom}_{𝑓} (C) : B \times B ⟶ U$
56	55 9 10	fovrnd	$⊢ φ \to X {Hom}_{𝑓} (C) Y \in U$
57	51 56	eqeltrrd	$⊢ φ \to X H Y \in U$
58	50 7 8 11 12	homfval	$⊢ φ \to Z {Hom}_{𝑓} (C) W = Z H W$
59	55 11 12	fovrnd	$⊢ φ \to Z {Hom}_{𝑓} (C) W \in U$
60	58 59	eqeltrrd	$⊢ φ \to Z H W \in U$
61	50 7 8 13 14	homfval	$⊢ φ \to S {Hom}_{𝑓} (C) T = S H T$
62	55 13 14	fovrnd	$⊢ φ \to S {Hom}_{𝑓} (C) T \in U$
63	61 62	eqeltrrd	$⊢ φ \to S H T \in U$
64	7 8 19 20 22 23 33 25 38	catcocl	$⊢ (φ \land f \in (X H Y)) \to (L (⟨X, Y⟩ comp (C) W) f) (⟨Z, X⟩ comp (C) W) K \in (Z H W)$
65	64	fmpttd	$⊢ φ \to (f \in (X H Y) ⟼ (L (⟨X, Y⟩ comp (C) W) f) (⟨Z, X⟩ comp (C) W) K) : X H Y ⟶ Z H W$
66	4	adantr	$⊢ (φ \land g \in (Z H W)) \to C \in Cat$
67	13	adantr	$⊢ (φ \land g \in (Z H W)) \to S \in B$
68	11	adantr	$⊢ (φ \land g \in (Z H W)) \to Z \in B$
69	14	adantr	$⊢ (φ \land g \in (Z H W)) \to T \in B$
70	17	adantr	$⊢ (φ \land g \in (Z H W)) \to P \in (S H Z)$
71	12	adantr	$⊢ (φ \land g \in (Z H W)) \to W \in B$
72		simpr	$⊢ (φ \land g \in (Z H W)) \to g \in (Z H W)$
73	18	adantr	$⊢ (φ \land g \in (Z H W)) \to Q \in (W H T)$
74	7 8 19 66 68 71 69 72 73	catcocl	$⊢ (φ \land g \in (Z H W)) \to Q (⟨Z, W⟩ comp (C) T) g \in (Z H T)$
75	7 8 19 66 67 68 69 70 74	catcocl	$⊢ (φ \land g \in (Z H W)) \to (Q (⟨Z, W⟩ comp (C) T) g) (⟨S, Z⟩ comp (C) T) P \in (S H T)$
76	75	fmpttd	$⊢ φ \to (g \in (Z H W) ⟼ (Q (⟨Z, W⟩ comp (C) T) g) (⟨S, Z⟩ comp (C) T) P) : Z H W ⟶ S H T$
77	3 5 49 57 60 63 65 76	setcco	$⊢ φ \to (g \in (Z H W) ⟼ (Q (⟨Z, W⟩ comp (C) T) g) (⟨S, Z⟩ comp (C) T) P) (⟨X H Y, Z H W⟩ comp (D) (S H T)) (f \in (X H Y) ⟼ (L (⟨X, Y⟩ comp (C) W) f) (⟨Z, X⟩ comp (C) W) K) = (g \in (Z H W) ⟼ (Q (⟨Z, W⟩ comp (C) T) g) (⟨S, Z⟩ comp (C) T) P) \circ (f \in (X H Y) ⟼ (L (⟨X, Y⟩ comp (C) W) f) (⟨Z, X⟩ comp (C) W) K)$
78		eqidd	$⊢ φ \to (f \in (X H Y) ⟼ (L (⟨X, Y⟩ comp (C) W) f) (⟨Z, X⟩ comp (C) W) K) = (f \in (X H Y) ⟼ (L (⟨X, Y⟩ comp (C) W) f) (⟨Z, X⟩ comp (C) W) K)$
79		eqidd	$⊢ φ \to (g \in (Z H W) ⟼ (Q (⟨Z, W⟩ comp (C) T) g) (⟨S, Z⟩ comp (C) T) P) = (g \in (Z H W) ⟼ (Q (⟨Z, W⟩ comp (C) T) g) (⟨S, Z⟩ comp (C) T) P)$
80		oveq2	$⊢ g = (L (⟨X, Y⟩ comp (C) W) f) (⟨Z, X⟩ comp (C) W) K \to Q (⟨Z, W⟩ comp (C) T) g = Q (⟨Z, W⟩ comp (C) T) ((L (⟨X, Y⟩ comp (C) W) f) (⟨Z, X⟩ comp (C) W) K)$
81	80	oveq1d	$⊢ g = (L (⟨X, Y⟩ comp (C) W) f) (⟨Z, X⟩ comp (C) W) K \to (Q (⟨Z, W⟩ comp (C) T) g) (⟨S, Z⟩ comp (C) T) P = (Q (⟨Z, W⟩ comp (C) T) ((L (⟨X, Y⟩ comp (C) W) f) (⟨Z, X⟩ comp (C) W) K)) (⟨S, Z⟩ comp (C) T) P$
82	64 78 79 81	fmptco	$⊢ φ \to (g \in (Z H W) ⟼ (Q (⟨Z, W⟩ comp (C) T) g) (⟨S, Z⟩ comp (C) T) P) \circ (f \in (X H Y) ⟼ (L (⟨X, Y⟩ comp (C) W) f) (⟨Z, X⟩ comp (C) W) K) = (f \in (X H Y) ⟼ (Q (⟨Z, W⟩ comp (C) T) ((L (⟨X, Y⟩ comp (C) W) f) (⟨Z, X⟩ comp (C) W) K)) (⟨S, Z⟩ comp (C) T) P)$
83	48 77 82	3eqtrd	$⊢ φ \to (P (⟨Z, W⟩ 2^{nd} (M) ⟨S, T⟩) Q) (⟨X H Y, Z H W⟩ comp (D) (S H T)) (K (⟨X, Y⟩ 2^{nd} (M) ⟨Z, W⟩) L) = (f \in (X H Y) ⟼ (Q (⟨Z, W⟩ comp (C) T) ((L (⟨X, Y⟩ comp (C) W) f) (⟨Z, X⟩ comp (C) W) K)) (⟨S, Z⟩ comp (C) T) P)$
84	43 45 83	3eqtr4d	$⊢ φ \to (K (⟨S, Z⟩ comp (C) X) P) (⟨X, Y⟩ 2^{nd} (M) ⟨S, T⟩) (Q (⟨Y, W⟩ comp (C) T) L) = (P (⟨Z, W⟩ 2^{nd} (M) ⟨S, T⟩) Q) (⟨X H Y, Z H W⟩ comp (D) (S H T)) (K (⟨X, Y⟩ 2^{nd} (M) ⟨Z, W⟩) L)$

Metamath Proof Explorer

Theorem hofcllem

Proof