Metamath Proof Explorer

Theorem xpcco1st

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

		Ref	Expression
	Hypotheses	xpcco1st.t	⊢ 𝑇 = ( 𝐶 ×_c 𝐷 )
		xpcco1st.b	⊢ 𝐵 = ( Base ‘ 𝑇 )
		xpcco1st.k	⊢ 𝐾 = ( Hom ‘ 𝑇 )
		xpcco1st.o	⊢ 𝑂 = ( comp ‘ 𝑇 )
		xpcco1st.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
		xpcco1st.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
		xpcco1st.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
		xpcco1st.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐾 𝑌 ) )
		xpcco1st.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐾 𝑍 ) )
		xpcco1st.1	⊢ · = ( comp ‘ 𝐶 )
	Assertion	xpcco1st	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ 𝑂 𝑍 ) 𝐹 ) ) = ( ( 1^st ‘ 𝐺 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ · ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		xpcco1st.t	⊢ 𝑇 = ( 𝐶 ×_c 𝐷 )
2		xpcco1st.b	⊢ 𝐵 = ( Base ‘ 𝑇 )
3		xpcco1st.k	⊢ 𝐾 = ( Hom ‘ 𝑇 )
4		xpcco1st.o	⊢ 𝑂 = ( comp ‘ 𝑇 )
5		xpcco1st.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		xpcco1st.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7		xpcco1st.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
8		xpcco1st.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐾 𝑌 ) )
9		xpcco1st.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐾 𝑍 ) )
10		xpcco1st.1	⊢ · = ( comp ‘ 𝐶 )
11		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
12	1 2 3 10 11 4 5 6 7 8 9	xpcco	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ 𝑂 𝑍 ) 𝐹 ) = ⟨ ( ( 1^st ‘ 𝐺 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ · ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝐹 ) ) , ( ( 2^nd ‘ 𝐺 ) ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑍 ) ) ( 2^nd ‘ 𝐹 ) ) ⟩ )
13		ovex	⊢ ( ( 1^st ‘ 𝐺 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ · ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝐹 ) ) ∈ V
14		ovex	⊢ ( ( 2^nd ‘ 𝐺 ) ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑍 ) ) ( 2^nd ‘ 𝐹 ) ) ∈ V
15	13 14	op1std	⊢ ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ 𝑂 𝑍 ) 𝐹 ) = ⟨ ( ( 1^st ‘ 𝐺 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ · ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝐹 ) ) , ( ( 2^nd ‘ 𝐺 ) ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑍 ) ) ( 2^nd ‘ 𝐹 ) ) ⟩ → ( 1^st ‘ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ 𝑂 𝑍 ) 𝐹 ) ) = ( ( 1^st ‘ 𝐺 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ · ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝐹 ) ) )
16	12 15	syl	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ 𝑂 𝑍 ) 𝐹 ) ) = ( ( 1^st ‘ 𝐺 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ · ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝐹 ) ) )