Theorem xpcco1st

Description: Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	xpcco1st.t	$$⊢T=C{\times }_{c}D$$
	xpcco1st.b	$$⊢B={\mathrm{Base}}_T$$
	xpcco1st.k	$$⊢K=\mathrm{Hom}\left(T\right)$$
	xpcco1st.o	$$⊢O=\mathrm{comp}\left(T\right)$$
	xpcco1st.x	$$⊢\phi \to X\in B$$
	xpcco1st.y	$$⊢\phi \to Y\in B$$
	xpcco1st.z	$$⊢\phi \to Z\in B$$
	xpcco1st.f	$$⊢\phi \to F\in \left(XKY\right)$$
	xpcco1st.g	$$⊢\phi \to G\in \left(YKZ\right)$$
	xpcco1st.1	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
Assertion	xpcco1st	$$⊢\phi \to 1^{st}\left(G\left(⟨X,Y⟩OZ\right)F\right)=1^{st}\left(G\right)\left(⟨1^{st}\left(X\right),1^{st}\left(Y\right)⟩\underset{\dot{}}{·}{1}^{st}\left(Z\right)\right)1^{st}\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		xpcco1st.t	$$⊢T=C{\times }_{c}D$$
2		xpcco1st.b	$$⊢B={\mathrm{Base}}_T$$
3		xpcco1st.k	$$⊢K=\mathrm{Hom}\left(T\right)$$
4		xpcco1st.o	$$⊢O=\mathrm{comp}\left(T\right)$$
5		xpcco1st.x	$$⊢\phi \to X\in B$$
6		xpcco1st.y	$$⊢\phi \to Y\in B$$
7		xpcco1st.z	$$⊢\phi \to Z\in B$$
8		xpcco1st.f	$$⊢\phi \to F\in \left(XKY\right)$$
9		xpcco1st.g	$$⊢\phi \to G\in \left(YKZ\right)$$
10		xpcco1st.1	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
11		eqid	$$⊢\mathrm{comp}\left(D\right)=\mathrm{comp}\left(D\right)$$
12	1 2 3 10 11 4 5 6 7 8 9	xpcco	$$⊢\phi \to G\left(⟨X,Y⟩OZ\right)F=⟨1^{st}\left(G\right)\left(⟨1^{st}\left(X\right),1^{st}\left(Y\right)⟩\underset{\dot{}}{·}{1}^{st}\left(Z\right)\right)1^{st}\left(F\right),2^{nd}\left(G\right)\left(⟨2^{nd}\left(X\right),2^{nd}\left(Y\right)⟩\mathrm{comp}\left(D\right)2^{nd}\left(Z\right)\right)2^{nd}\left(F\right)⟩$$
13		ovex	$$⊢1^{st}\left(G\right)\left(⟨1^{st}\left(X\right),1^{st}\left(Y\right)⟩\underset{\dot{}}{·}{1}^{st}\left(Z\right)\right)1^{st}\left(F\right)\in \mathrm{V}$$
14		ovex	$$⊢2^{nd}\left(G\right)\left(⟨2^{nd}\left(X\right),2^{nd}\left(Y\right)⟩\mathrm{comp}\left(D\right)2^{nd}\left(Z\right)\right)2^{nd}\left(F\right)\in \mathrm{V}$$
15	13 14	op1std	$$⊢G\left(⟨X,Y⟩OZ\right)F=⟨1^{st}\left(G\right)\left(⟨1^{st}\left(X\right),1^{st}\left(Y\right)⟩\underset{\dot{}}{·}{1}^{st}\left(Z\right)\right)1^{st}\left(F\right),2^{nd}\left(G\right)\left(⟨2^{nd}\left(X\right),2^{nd}\left(Y\right)⟩\mathrm{comp}\left(D\right)2^{nd}\left(Z\right)\right)2^{nd}\left(F\right)⟩\to 1^{st}\left(G\left(⟨X,Y⟩OZ\right)F\right)=1^{st}\left(G\right)\left(⟨1^{st}\left(X\right),1^{st}\left(Y\right)⟩\underset{\dot{}}{·}{1}^{st}\left(Z\right)\right)1^{st}\left(F\right)$$
16	12 15	syl	$$⊢\phi \to 1^{st}\left(G\left(⟨X,Y⟩OZ\right)F\right)=1^{st}\left(G\right)\left(⟨1^{st}\left(X\right),1^{st}\left(Y\right)⟩\underset{\dot{}}{·}{1}^{st}\left(Z\right)\right)1^{st}\left(F\right)$$