Theorem hof2

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\left(C\right)$$
	hofval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	hof1.b	$$⊢B={\mathrm{Base}}_C$$
	hof1.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	hof1.x	$$⊢\phi \to X\in B$$
	hof1.y	$$⊢\phi \to Y\in B$$
	hof2.z	$$⊢\phi \to Z\in B$$
	hof2.w	$$⊢\phi \to W\in B$$
	hof2.o	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
	hof2.f	$$⊢\phi \to F\in \left(ZHX\right)$$
	hof2.g	$$⊢\phi \to G\in \left(YHW\right)$$
	hof2.k	$$⊢\phi \to K\in \left(XHY\right)$$
Assertion	hof2	$$⊢\phi \to \left(F\left(⟨X,Y⟩2^{nd}\left(M\right)⟨Z,W⟩\right)G\right)\left(K\right)=\left(G\left(⟨X,Y⟩\underset{\dot{}}{·}W\right)K\right)\left(⟨Z,X⟩\underset{\dot{}}{·}W\right)F$$

Proof

Step	Hyp	Ref	Expression
1		hofval.m	$$⊢M={Hom}_F\left(C\right)$$
2		hofval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
3		hof1.b	$$⊢B={\mathrm{Base}}_C$$
4		hof1.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
5		hof1.x	$$⊢\phi \to X\in B$$
6		hof1.y	$$⊢\phi \to Y\in B$$
7		hof2.z	$$⊢\phi \to Z\in B$$
8		hof2.w	$$⊢\phi \to W\in B$$
9		hof2.o	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
10		hof2.f	$$⊢\phi \to F\in \left(ZHX\right)$$
11		hof2.g	$$⊢\phi \to G\in \left(YHW\right)$$
12		hof2.k	$$⊢\phi \to K\in \left(XHY\right)$$
13	1 2 3 4 5 6 7 8 9 10 11	hof2val	$$⊢\phi \to F\left(⟨X,Y⟩2^{nd}\left(M\right)⟨Z,W⟩\right)G=\left(h\in \left(XHY\right)⟼\left(G\left(⟨X,Y⟩\underset{\dot{}}{·}W\right)h\right)\left(⟨Z,X⟩\underset{\dot{}}{·}W\right)F\right)$$
14		simpr	$$⊢\left(\phi \wedge h=K\right)\to h=K$$
15	14	oveq2d	$$⊢\left(\phi \wedge h=K\right)\to G\left(⟨X,Y⟩\underset{\dot{}}{·}W\right)h=G\left(⟨X,Y⟩\underset{\dot{}}{·}W\right)K$$
16	15	oveq1d	$$⊢\left(\phi \wedge h=K\right)\to \left(G\left(⟨X,Y⟩\underset{\dot{}}{·}W\right)h\right)\left(⟨Z,X⟩\underset{\dot{}}{·}W\right)F=\left(G\left(⟨X,Y⟩\underset{\dot{}}{·}W\right)K\right)\left(⟨Z,X⟩\underset{\dot{}}{·}W\right)F$$
17		ovexd	$$⊢\phi \to \left(G\left(⟨X,Y⟩\underset{\dot{}}{·}W\right)K\right)\left(⟨Z,X⟩\underset{\dot{}}{·}W\right)F\in \mathrm{V}$$
18	13 16 12 17	fvmptd	$$⊢\phi \to \left(F\left(⟨X,Y⟩2^{nd}\left(M\right)⟨Z,W⟩\right)G\right)\left(K\right)=\left(G\left(⟨X,Y⟩\underset{\dot{}}{·}W\right)K\right)\left(⟨Z,X⟩\underset{\dot{}}{·}W\right)F$$