hof2fval

Description: The morphism part of the Hom functor, for morphisms <. f , g >. : <. X , Y >. --> <. Z , W >. (which since the first argument is contravariant means morphisms f : Z --> X and g : Y --> W ), yields a function (a morphism of SetCat ) mapping h : X --> Y to g o. h o. f : Z --> W . (Contributed by Mario Carneiro, 15-Jan-2017)

	Ref	Expression
Hypotheses	hofval.m	$⊢ M = {Hom}_{F} (C)$
	hofval.c	$⊢ φ \to C \in Cat$
	hof1.b	$⊢ B = {Base}_{C}$
	hof1.h	$⊢ H = Hom (C)$
	hof1.x	$⊢ φ \to X \in B$
	hof1.y	$⊢ φ \to Y \in B$
	hof2.z	$⊢ φ \to Z \in B$
	hof2.w	$⊢ φ \to W \in B$
	hof2.o	$⊢ \underset{˙}{\cdot} = comp (C)$
Assertion	hof2fval	$⊢ φ \to ⟨X, Y⟩ 2^{nd} (M) ⟨Z, W⟩ = (f \in (Z H X), g \in (Y H W) ⟼ (h \in (X H Y) ⟼ (g (⟨X, Y⟩ \underset{˙}{\cdot} W) h) (⟨Z, X⟩ \underset{˙}{\cdot} W) f))$

Proof

Step	Hyp	Ref	Expression
1		hofval.m	$⊢ M = {Hom}_{F} (C)$
2		hofval.c	$⊢ φ \to C \in Cat$
3		hof1.b	$⊢ B = {Base}_{C}$
4		hof1.h	$⊢ H = Hom (C)$
5		hof1.x	$⊢ φ \to X \in B$
6		hof1.y	$⊢ φ \to Y \in B$
7		hof2.z	$⊢ φ \to Z \in B$
8		hof2.w	$⊢ φ \to W \in B$
9		hof2.o	$⊢ \underset{˙}{\cdot} = comp (C)$
10	1 2 3 4 9	hofval	$⊢ φ \to M = ⟨{Hom}_{𝑓} (C), (x \in (B \times B), y \in (B \times B) ⟼ (f \in (1^{st} (y) H 1^{st} (x)), g \in (2^{nd} (x) H 2^{nd} (y)) ⟼ (h \in H (x) ⟼ (g (x \underset{˙}{\cdot} 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ \underset{˙}{\cdot} 2^{nd} (y)) f)))⟩$
11		fvex	$⊢ {Hom}_{𝑓} (C) \in V$
12	3	fvexi	$⊢ B \in V$
13	12 12	xpex	$⊢ B \times B \in V$
14	13 13	mpoex	$⊢ (x \in (B \times B), y \in (B \times B) ⟼ (f \in (1^{st} (y) H 1^{st} (x)), g \in (2^{nd} (x) H 2^{nd} (y)) ⟼ (h \in H (x) ⟼ (g (x \underset{˙}{\cdot} 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ \underset{˙}{\cdot} 2^{nd} (y)) f))) \in V$
15	11 14	op2ndd	$⊢ M = ⟨{Hom}_{𝑓} (C), (x \in (B \times B), y \in (B \times B) ⟼ (f \in (1^{st} (y) H 1^{st} (x)), g \in (2^{nd} (x) H 2^{nd} (y)) ⟼ (h \in H (x) ⟼ (g (x \underset{˙}{\cdot} 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ \underset{˙}{\cdot} 2^{nd} (y)) f)))⟩ \to 2^{nd} (M) = (x \in (B \times B), y \in (B \times B) ⟼ (f \in (1^{st} (y) H 1^{st} (x)), g \in (2^{nd} (x) H 2^{nd} (y)) ⟼ (h \in H (x) ⟼ (g (x \underset{˙}{\cdot} 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ \underset{˙}{\cdot} 2^{nd} (y)) f)))$
16	10 15	syl	$⊢ φ \to 2^{nd} (M) = (x \in (B \times B), y \in (B \times B) ⟼ (f \in (1^{st} (y) H 1^{st} (x)), g \in (2^{nd} (x) H 2^{nd} (y)) ⟼ (h \in H (x) ⟼ (g (x \underset{˙}{\cdot} 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ \underset{˙}{\cdot} 2^{nd} (y)) f)))$
17		simprr	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = ⟨Z, W⟩)) \to y = ⟨Z, W⟩$
18	17	fveq2d	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = ⟨Z, W⟩)) \to 1^{st} (y) = 1^{st} (⟨Z, W⟩)$
19		op1stg	$⊢ (Z \in B \land W \in B) \to 1^{st} (⟨Z, W⟩) = Z$
20	7 8 19	syl2anc	$⊢ φ \to 1^{st} (⟨Z, W⟩) = Z$
21	20	adantr	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = ⟨Z, W⟩)) \to 1^{st} (⟨Z, W⟩) = Z$
22	18 21	eqtrd	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = ⟨Z, W⟩)) \to 1^{st} (y) = Z$
23		simprl	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = ⟨Z, W⟩)) \to x = ⟨X, Y⟩$
24	23	fveq2d	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = ⟨Z, W⟩)) \to 1^{st} (x) = 1^{st} (⟨X, Y⟩)$
25		op1stg	$⊢ (X \in B \land Y \in B) \to 1^{st} (⟨X, Y⟩) = X$
26	5 6 25	syl2anc	$⊢ φ \to 1^{st} (⟨X, Y⟩) = X$
27	26	adantr	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = ⟨Z, W⟩)) \to 1^{st} (⟨X, Y⟩) = X$
28	24 27	eqtrd	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = ⟨Z, W⟩)) \to 1^{st} (x) = X$
29	22 28	oveq12d	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = ⟨Z, W⟩)) \to 1^{st} (y) H 1^{st} (x) = Z H X$
30	23	fveq2d	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = ⟨Z, W⟩)) \to 2^{nd} (x) = 2^{nd} (⟨X, Y⟩)$
31		op2ndg	$⊢ (X \in B \land Y \in B) \to 2^{nd} (⟨X, Y⟩) = Y$
32	5 6 31	syl2anc	$⊢ φ \to 2^{nd} (⟨X, Y⟩) = Y$
33	32	adantr	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = ⟨Z, W⟩)) \to 2^{nd} (⟨X, Y⟩) = Y$
34	30 33	eqtrd	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = ⟨Z, W⟩)) \to 2^{nd} (x) = Y$
35	17	fveq2d	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = ⟨Z, W⟩)) \to 2^{nd} (y) = 2^{nd} (⟨Z, W⟩)$
36		op2ndg	$⊢ (Z \in B \land W \in B) \to 2^{nd} (⟨Z, W⟩) = W$
37	7 8 36	syl2anc	$⊢ φ \to 2^{nd} (⟨Z, W⟩) = W$
38	37	adantr	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = ⟨Z, W⟩)) \to 2^{nd} (⟨Z, W⟩) = W$
39	35 38	eqtrd	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = ⟨Z, W⟩)) \to 2^{nd} (y) = W$
40	34 39	oveq12d	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = ⟨Z, W⟩)) \to 2^{nd} (x) H 2^{nd} (y) = Y H W$
41	23	fveq2d	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = ⟨Z, W⟩)) \to H (x) = H (⟨X, Y⟩)$
42		df-ov	$⊢ X H Y = H (⟨X, Y⟩)$
43	41 42	eqtr4di	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = ⟨Z, W⟩)) \to H (x) = X H Y$
44	22 28	opeq12d	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = ⟨Z, W⟩)) \to ⟨1^{st} (y), 1^{st} (x)⟩ = ⟨Z, X⟩$
45	44 39	oveq12d	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = ⟨Z, W⟩)) \to ⟨1^{st} (y), 1^{st} (x)⟩ \underset{˙}{\cdot} 2^{nd} (y) = ⟨Z, X⟩ \underset{˙}{\cdot} W$
46	23 39	oveq12d	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = ⟨Z, W⟩)) \to x \underset{˙}{\cdot} 2^{nd} (y) = ⟨X, Y⟩ \underset{˙}{\cdot} W$
47	46	oveqd	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = ⟨Z, W⟩)) \to g (x \underset{˙}{\cdot} 2^{nd} (y)) h = g (⟨X, Y⟩ \underset{˙}{\cdot} W) h$
48		eqidd	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = ⟨Z, W⟩)) \to f = f$
49	45 47 48	oveq123d	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = ⟨Z, W⟩)) \to (g (x \underset{˙}{\cdot} 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ \underset{˙}{\cdot} 2^{nd} (y)) f = (g (⟨X, Y⟩ \underset{˙}{\cdot} W) h) (⟨Z, X⟩ \underset{˙}{\cdot} W) f$
50	43 49	mpteq12dv	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = ⟨Z, W⟩)) \to (h \in H (x) ⟼ (g (x \underset{˙}{\cdot} 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ \underset{˙}{\cdot} 2^{nd} (y)) f) = (h \in (X H Y) ⟼ (g (⟨X, Y⟩ \underset{˙}{\cdot} W) h) (⟨Z, X⟩ \underset{˙}{\cdot} W) f)$
51	29 40 50	mpoeq123dv	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = ⟨Z, W⟩)) \to (f \in (1^{st} (y) H 1^{st} (x)), g \in (2^{nd} (x) H 2^{nd} (y)) ⟼ (h \in H (x) ⟼ (g (x \underset{˙}{\cdot} 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ \underset{˙}{\cdot} 2^{nd} (y)) f)) = (f \in (Z H X), g \in (Y H W) ⟼ (h \in (X H Y) ⟼ (g (⟨X, Y⟩ \underset{˙}{\cdot} W) h) (⟨Z, X⟩ \underset{˙}{\cdot} W) f))$
52	5 6	opelxpd	$⊢ φ \to ⟨X, Y⟩ \in (B \times B)$
53	7 8	opelxpd	$⊢ φ \to ⟨Z, W⟩ \in (B \times B)$
54		ovex	$⊢ Z H X \in V$
55		ovex	$⊢ Y H W \in V$
56	54 55	mpoex	$⊢ (f \in (Z H X), g \in (Y H W) ⟼ (h \in (X H Y) ⟼ (g (⟨X, Y⟩ \underset{˙}{\cdot} W) h) (⟨Z, X⟩ \underset{˙}{\cdot} W) f)) \in V$
57	56	a1i	$⊢ φ \to (f \in (Z H X), g \in (Y H W) ⟼ (h \in (X H Y) ⟼ (g (⟨X, Y⟩ \underset{˙}{\cdot} W) h) (⟨Z, X⟩ \underset{˙}{\cdot} W) f)) \in V$
58	16 51 52 53 57	ovmpod	$⊢ φ \to ⟨X, Y⟩ 2^{nd} (M) ⟨Z, W⟩ = (f \in (Z H X), g \in (Y H W) ⟼ (h \in (X H Y) ⟼ (g (⟨X, Y⟩ \underset{˙}{\cdot} W) h) (⟨Z, X⟩ \underset{˙}{\cdot} W) f))$

Metamath Proof Explorer

Theorem hof2fval

Proof