oppcco

Description: Composition in the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	oppcco.b	$⊢ B = {Base}_{C}$
	oppcco.c	$⊢ \underset{˙}{\cdot} = comp (C)$
	oppcco.o	$⊢ O = oppCat (C)$
	oppcco.x	$⊢ φ \to X \in B$
	oppcco.y	$⊢ φ \to Y \in B$
	oppcco.z	$⊢ φ \to Z \in B$
Assertion	oppcco	$⊢ φ \to G (⟨X, Y⟩ comp (O) Z) F = F (⟨Z, Y⟩ \underset{˙}{\cdot} X) G$

Step	Hyp	Ref	Expression
1		oppcco.b	$⊢ B = {Base}_{C}$
2		oppcco.c	$⊢ \underset{˙}{\cdot} = comp (C)$
3		oppcco.o	$⊢ O = oppCat (C)$
4		oppcco.x	$⊢ φ \to X \in B$
5		oppcco.y	$⊢ φ \to Y \in B$
6		oppcco.z	$⊢ φ \to Z \in B$
7	1 2 3 4 5 6	oppccofval	$⊢ φ \to ⟨X, Y⟩ comp (O) Z = tpos (⟨Z, Y⟩ \underset{˙}{\cdot} X)$
8	7	oveqd	$⊢ φ \to G (⟨X, Y⟩ comp (O) Z) F = G tpos (⟨Z, Y⟩ \underset{˙}{\cdot} X) F$
9		ovtpos	$⊢ G tpos (⟨Z, Y⟩ \underset{˙}{\cdot} X) F = F (⟨Z, Y⟩ \underset{˙}{\cdot} X) G$
10	8 9	eqtrdi	$⊢ φ \to G (⟨X, Y⟩ comp (O) Z) F = F (⟨Z, Y⟩ \underset{˙}{\cdot} X) G$

Metamath Proof Explorer