cofuval2

Description: Value of the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	cofuval2.b	$⊢ B = {Base}_{C}$
	cofuval2.f	$⊢ φ \to F (C Func D) G$
	cofuval2.x	$⊢ φ \to H (D Func E) K$
Assertion	cofuval2	$⊢ φ \to ⟨H, K⟩ \circ_{func} ⟨F, G⟩ = ⟨H \circ F, (x \in B, y \in B ⟼ (F (x) K F (y)) \circ (x G y))⟩$

Proof

Step	Hyp	Ref	Expression
1		cofuval2.b	$⊢ B = {Base}_{C}$
2		cofuval2.f	$⊢ φ \to F (C Func D) G$
3		cofuval2.x	$⊢ φ \to H (D Func E) K$
4		df-br	$⊢ F (C Func D) G \leftrightarrow ⟨F, G⟩ \in (C Func D)$
5	2 4	sylib	$⊢ φ \to ⟨F, G⟩ \in (C Func D)$
6		df-br	$⊢ H (D Func E) K \leftrightarrow ⟨H, K⟩ \in (D Func E)$
7	3 6	sylib	$⊢ φ \to ⟨H, K⟩ \in (D Func E)$
8	1 5 7	cofuval	$⊢ φ \to ⟨H, K⟩ \circ_{func} ⟨F, G⟩ = ⟨1^{st} (⟨H, K⟩) \circ 1^{st} (⟨F, G⟩), (x \in B, y \in B ⟼ (1^{st} (⟨F, G⟩) (x) 2^{nd} (⟨H, K⟩) 1^{st} (⟨F, G⟩) (y)) \circ (x 2^{nd} (⟨F, G⟩) y))⟩$
9		relfunc	$⊢ Rel (D Func E)$
10		brrelex12	$⊢ (Rel (D Func E) \land H (D Func E) K) \to (H \in V \land K \in V)$
11	9 3 10	sylancr	$⊢ φ \to (H \in V \land K \in V)$
12		op1stg	$⊢ (H \in V \land K \in V) \to 1^{st} (⟨H, K⟩) = H$
13	11 12	syl	$⊢ φ \to 1^{st} (⟨H, K⟩) = H$
14		relfunc	$⊢ Rel (C Func D)$
15		brrelex12	$⊢ (Rel (C Func D) \land F (C Func D) G) \to (F \in V \land G \in V)$
16	14 2 15	sylancr	$⊢ φ \to (F \in V \land G \in V)$
17		op1stg	$⊢ (F \in V \land G \in V) \to 1^{st} (⟨F, G⟩) = F$
18	16 17	syl	$⊢ φ \to 1^{st} (⟨F, G⟩) = F$
19	13 18	coeq12d	$⊢ φ \to 1^{st} (⟨H, K⟩) \circ 1^{st} (⟨F, G⟩) = H \circ F$
20		op2ndg	$⊢ (H \in V \land K \in V) \to 2^{nd} (⟨H, K⟩) = K$
21	11 20	syl	$⊢ φ \to 2^{nd} (⟨H, K⟩) = K$
22	21	3ad2ant1	$⊢ (φ \land x \in B \land y \in B) \to 2^{nd} (⟨H, K⟩) = K$
23	18	3ad2ant1	$⊢ (φ \land x \in B \land y \in B) \to 1^{st} (⟨F, G⟩) = F$
24	23	fveq1d	$⊢ (φ \land x \in B \land y \in B) \to 1^{st} (⟨F, G⟩) (x) = F (x)$
25	23	fveq1d	$⊢ (φ \land x \in B \land y \in B) \to 1^{st} (⟨F, G⟩) (y) = F (y)$
26	22 24 25	oveq123d	$⊢ (φ \land x \in B \land y \in B) \to 1^{st} (⟨F, G⟩) (x) 2^{nd} (⟨H, K⟩) 1^{st} (⟨F, G⟩) (y) = F (x) K F (y)$
27		op2ndg	$⊢ (F \in V \land G \in V) \to 2^{nd} (⟨F, G⟩) = G$
28	16 27	syl	$⊢ φ \to 2^{nd} (⟨F, G⟩) = G$
29	28	3ad2ant1	$⊢ (φ \land x \in B \land y \in B) \to 2^{nd} (⟨F, G⟩) = G$
30	29	oveqd	$⊢ (φ \land x \in B \land y \in B) \to x 2^{nd} (⟨F, G⟩) y = x G y$
31	26 30	coeq12d	$⊢ (φ \land x \in B \land y \in B) \to (1^{st} (⟨F, G⟩) (x) 2^{nd} (⟨H, K⟩) 1^{st} (⟨F, G⟩) (y)) \circ (x 2^{nd} (⟨F, G⟩) y) = (F (x) K F (y)) \circ (x G y)$
32	31	mpoeq3dva	$⊢ φ \to (x \in B, y \in B ⟼ (1^{st} (⟨F, G⟩) (x) 2^{nd} (⟨H, K⟩) 1^{st} (⟨F, G⟩) (y)) \circ (x 2^{nd} (⟨F, G⟩) y)) = (x \in B, y \in B ⟼ (F (x) K F (y)) \circ (x G y))$
33	19 32	opeq12d	$⊢ φ \to ⟨1^{st} (⟨H, K⟩) \circ 1^{st} (⟨F, G⟩), (x \in B, y \in B ⟼ (1^{st} (⟨F, G⟩) (x) 2^{nd} (⟨H, K⟩) 1^{st} (⟨F, G⟩) (y)) \circ (x 2^{nd} (⟨F, G⟩) y))⟩ = ⟨H \circ F, (x \in B, y \in B ⟼ (F (x) K F (y)) \circ (x G y))⟩$
34	8 33	eqtrd	$⊢ φ \to ⟨H, K⟩ \circ_{func} ⟨F, G⟩ = ⟨H \circ F, (x \in B, y \in B ⟼ (F (x) K F (y)) \circ (x G y))⟩$

Metamath Proof Explorer

Theorem cofuval2

Proof