Theorem xpcco2nd

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 ) )
	xpcco2nd.1	|- .x. = ( comp ` D )
Assertion	xpcco2nd	|- ( ph -> ( 2nd ` ( G ( <. X , Y >. O Z ) F ) ) = ( ( 2nd ` G ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. .x. ( 2nd ` Z ) ) ( 2nd ` 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		xpcco2nd.1	|- .x. = ( comp ` D )
11		eqid	|- ( comp ` C ) = ( comp ` C )
12	1 2 3 11 10 4 5 6 7 8 9	xpcco	|- ( ph -> ( G ( <. X , Y >. O Z ) F ) = <. ( ( 1st ` G ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. ( comp ` C ) ( 1st ` Z ) ) ( 1st ` F ) ) , ( ( 2nd ` G ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. .x. ( 2nd ` Z ) ) ( 2nd ` F ) ) >. )
13		ovex	|- ( ( 1st ` G ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. ( comp ` C ) ( 1st ` Z ) ) ( 1st ` F ) ) e. _V
14		ovex	|- ( ( 2nd ` G ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. .x. ( 2nd ` Z ) ) ( 2nd ` F ) ) e. _V
15	13 14	op2ndd	|- ( ( G ( <. X , Y >. O Z ) F ) = <. ( ( 1st ` G ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. ( comp ` C ) ( 1st ` Z ) ) ( 1st ` F ) ) , ( ( 2nd ` G ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. .x. ( 2nd ` Z ) ) ( 2nd ` F ) ) >. -> ( 2nd ` ( G ( <. X , Y >. O Z ) F ) ) = ( ( 2nd ` G ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. .x. ( 2nd ` Z ) ) ( 2nd ` F ) ) )
16	12 15	syl	|- ( ph -> ( 2nd ` ( G ( <. X , Y >. O Z ) F ) ) = ( ( 2nd ` G ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. .x. ( 2nd ` Z ) ) ( 2nd ` F ) ) )