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 Xc. D )
	xpcco1st.b	|- B = ( Base ` T )
	xpcco1st.k	|- K = ( Hom ` T )
	xpcco1st.o	|- O = ( comp ` T )
	xpcco1st.x	|- ( ph -> X e. B )
	xpcco1st.y	|- ( ph -> Y e. B )
	xpcco1st.z	|- ( ph -> Z e. B )
	xpcco1st.f	|- ( ph -> F e. ( X K Y ) )
	xpcco1st.g	|- ( ph -> G e. ( Y K Z ) )
	xpcco1st.1	|- .x. = ( comp ` C )
Assertion	xpcco1st	|- ( ph -> ( 1st ` ( G ( <. X , Y >. O Z ) F ) ) = ( ( 1st ` G ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. .x. ( 1st ` Z ) ) ( 1st ` F ) ) )

Proof

Step	Hyp	Ref	Expression
1		xpcco1st.t	|- T = ( C Xc. D )
2		xpcco1st.b	|- B = ( Base ` T )
3		xpcco1st.k	|- K = ( Hom ` T )
4		xpcco1st.o	|- O = ( comp ` T )
5		xpcco1st.x	|- ( ph -> X e. B )
6		xpcco1st.y	|- ( ph -> Y e. B )
7		xpcco1st.z	|- ( ph -> Z e. B )
8		xpcco1st.f	|- ( ph -> F e. ( X K Y ) )
9		xpcco1st.g	|- ( ph -> G e. ( Y K Z ) )
10		xpcco1st.1	|- .x. = ( comp ` C )
11		eqid	|- ( comp ` D ) = ( comp ` D )
12	1 2 3 10 11 4 5 6 7 8 9	xpcco	|- ( ph -> ( G ( <. X , Y >. O Z ) F ) = <. ( ( 1st ` G ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. .x. ( 1st ` Z ) ) ( 1st ` F ) ) , ( ( 2nd ` G ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. ( comp ` D ) ( 2nd ` Z ) ) ( 2nd ` F ) ) >. )
13		ovex	|- ( ( 1st ` G ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. .x. ( 1st ` Z ) ) ( 1st ` F ) ) e. _V
14		ovex	|- ( ( 2nd ` G ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. ( comp ` D ) ( 2nd ` Z ) ) ( 2nd ` F ) ) e. _V
15	13 14	op1std	|- ( ( G ( <. X , Y >. O Z ) F ) = <. ( ( 1st ` G ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. .x. ( 1st ` Z ) ) ( 1st ` F ) ) , ( ( 2nd ` G ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. ( comp ` D ) ( 2nd ` Z ) ) ( 2nd ` F ) ) >. -> ( 1st ` ( G ( <. X , Y >. O Z ) F ) ) = ( ( 1st ` G ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. .x. ( 1st ` Z ) ) ( 1st ` F ) ) )
16	12 15	syl	|- ( ph -> ( 1st ` ( G ( <. X , Y >. O Z ) F ) ) = ( ( 1st ` G ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. .x. ( 1st ` Z ) ) ( 1st ` F ) ) )