curf12

Description: The partially evaluated curry functor at a morphism. (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Hypotheses	curfval.g	$⊢ G = ⟨C, D⟩ {curry}_{F} F$
	curfval.a	$⊢ A = {Base}_{C}$
	curfval.c	$⊢ φ \to C \in Cat$
	curfval.d	$⊢ φ \to D \in Cat$
	curfval.f	$⊢ φ \to F \in ((C \times_{c} D) Func E)$
	curfval.b	$⊢ B = {Base}_{D}$
	curf1.x	$⊢ φ \to X \in A$
	curf1.k	$⊢ K = 1^{st} (G) (X)$
	curf11.y	$⊢ φ \to Y \in B$
	curf12.j	$⊢ J = Hom (D)$
	curf12.1	$⊢ \underset{˙}{1} = Id (C)$
	curf12.y	$⊢ φ \to Z \in B$
	curf12.g	$⊢ φ \to H \in (Y J Z)$
Assertion	curf12	$⊢ φ \to (Y 2^{nd} (K) Z) (H) = \underset{˙}{1} (X) (⟨X, Y⟩ 2^{nd} (F) ⟨X, Z⟩) H$

Proof

Step	Hyp	Ref	Expression
1		curfval.g	$⊢ G = ⟨C, D⟩ {curry}_{F} F$
2		curfval.a	$⊢ A = {Base}_{C}$
3		curfval.c	$⊢ φ \to C \in Cat$
4		curfval.d	$⊢ φ \to D \in Cat$
5		curfval.f	$⊢ φ \to F \in ((C \times_{c} D) Func E)$
6		curfval.b	$⊢ B = {Base}_{D}$
7		curf1.x	$⊢ φ \to X \in A$
8		curf1.k	$⊢ K = 1^{st} (G) (X)$
9		curf11.y	$⊢ φ \to Y \in B$
10		curf12.j	$⊢ J = Hom (D)$
11		curf12.1	$⊢ \underset{˙}{1} = Id (C)$
12		curf12.y	$⊢ φ \to Z \in B$
13		curf12.g	$⊢ φ \to H \in (Y J Z)$
14	1 2 3 4 5 6 7 8 10 11	curf1	$⊢ φ \to K = ⟨(y \in B ⟼ X 1^{st} (F) y), (y \in B, z \in B ⟼ (g \in (y J z) ⟼ \underset{˙}{1} (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g))⟩$
15	6	fvexi	$⊢ B \in V$
16	15	mptex	$⊢ (y \in B ⟼ X 1^{st} (F) y) \in V$
17	15 15	mpoex	$⊢ (y \in B, z \in B ⟼ (g \in (y J z) ⟼ \underset{˙}{1} (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g)) \in V$
18	16 17	op2ndd	$⊢ K = ⟨(y \in B ⟼ X 1^{st} (F) y), (y \in B, z \in B ⟼ (g \in (y J z) ⟼ \underset{˙}{1} (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g))⟩ \to 2^{nd} (K) = (y \in B, z \in B ⟼ (g \in (y J z) ⟼ \underset{˙}{1} (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g))$
19	14 18	syl	$⊢ φ \to 2^{nd} (K) = (y \in B, z \in B ⟼ (g \in (y J z) ⟼ \underset{˙}{1} (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g))$
20	12	adantr	$⊢ (φ \land y = Y) \to Z \in B$
21		ovex	$⊢ y J z \in V$
22	21	mptex	$⊢ (g \in (y J z) ⟼ \underset{˙}{1} (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g) \in V$
23	22	a1i	$⊢ (φ \land (y = Y \land z = Z)) \to (g \in (y J z) ⟼ \underset{˙}{1} (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g) \in V$
24	13	adantr	$⊢ (φ \land (y = Y \land z = Z)) \to H \in (Y J Z)$
25		simprl	$⊢ (φ \land (y = Y \land z = Z)) \to y = Y$
26		simprr	$⊢ (φ \land (y = Y \land z = Z)) \to z = Z$
27	25 26	oveq12d	$⊢ (φ \land (y = Y \land z = Z)) \to y J z = Y J Z$
28	24 27	eleqtrrd	$⊢ (φ \land (y = Y \land z = Z)) \to H \in (y J z)$
29		ovexd	$⊢ ((φ \land (y = Y \land z = Z)) \land g = H) \to \underset{˙}{1} (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g \in V$
30		simplrl	$⊢ ((φ \land (y = Y \land z = Z)) \land g = H) \to y = Y$
31	30	opeq2d	$⊢ ((φ \land (y = Y \land z = Z)) \land g = H) \to ⟨X, y⟩ = ⟨X, Y⟩$
32		simplrr	$⊢ ((φ \land (y = Y \land z = Z)) \land g = H) \to z = Z$
33	32	opeq2d	$⊢ ((φ \land (y = Y \land z = Z)) \land g = H) \to ⟨X, z⟩ = ⟨X, Z⟩$
34	31 33	oveq12d	$⊢ ((φ \land (y = Y \land z = Z)) \land g = H) \to ⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩ = ⟨X, Y⟩ 2^{nd} (F) ⟨X, Z⟩$
35		eqidd	$⊢ ((φ \land (y = Y \land z = Z)) \land g = H) \to \underset{˙}{1} (X) = \underset{˙}{1} (X)$
36		simpr	$⊢ ((φ \land (y = Y \land z = Z)) \land g = H) \to g = H$
37	34 35 36	oveq123d	$⊢ ((φ \land (y = Y \land z = Z)) \land g = H) \to \underset{˙}{1} (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g = \underset{˙}{1} (X) (⟨X, Y⟩ 2^{nd} (F) ⟨X, Z⟩) H$
38	28 29 37	fvmptdv2	$⊢ (φ \land (y = Y \land z = Z)) \to (Y 2^{nd} (K) Z = (g \in (y J z) ⟼ \underset{˙}{1} (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g) \to (Y 2^{nd} (K) Z) (H) = \underset{˙}{1} (X) (⟨X, Y⟩ 2^{nd} (F) ⟨X, Z⟩) H)$
39	9 20 23 38	ovmpodv	$⊢ φ \to (2^{nd} (K) = (y \in B, z \in B ⟼ (g \in (y J z) ⟼ \underset{˙}{1} (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g)) \to (Y 2^{nd} (K) Z) (H) = \underset{˙}{1} (X) (⟨X, Y⟩ 2^{nd} (F) ⟨X, Z⟩) H)$
40	19 39	mpd	$⊢ φ \to (Y 2^{nd} (K) Z) (H) = \underset{˙}{1} (X) (⟨X, Y⟩ 2^{nd} (F) ⟨X, Z⟩) H$

Metamath Proof Explorer

Theorem curf12

Proof