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 = {Base}_{T}$
	xpcco1st.k	$⊢ K = Hom (T)$
	xpcco1st.o	$⊢ O = comp (T)$
	xpcco1st.x	$⊢ φ \to X \in B$
	xpcco1st.y	$⊢ φ \to Y \in B$
	xpcco1st.z	$⊢ φ \to Z \in B$
	xpcco1st.f	$⊢ φ \to F \in (X K Y)$
	xpcco1st.g	$⊢ φ \to G \in (Y K Z)$
	xpcco1st.1	$⊢ \underset{˙}{\cdot} = comp (C)$
Assertion	xpcco1st	$⊢ φ \to 1^{st} (G (⟨X, Y⟩ O Z) F) = 1^{st} (G) (⟨1^{st} (X), 1^{st} (Y)⟩ \underset{˙}{\cdot} 1^{st} (Z)) 1^{st} (F)$

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

Metamath Proof Explorer