cofuval

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

	Ref	Expression
Hypotheses	cofuval.b	$⊢ B = {Base}_{C}$
	cofuval.f	$⊢ φ \to F \in (C Func D)$
	cofuval.g	$⊢ φ \to G \in (D Func E)$
Assertion	cofuval	$⊢ φ \to G \circ_{func} F = ⟨1^{st} (G) \circ 1^{st} (F), (x \in B, y \in B ⟼ (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y))⟩$

Proof

Step	Hyp	Ref	Expression
1		cofuval.b	$⊢ B = {Base}_{C}$
2		cofuval.f	$⊢ φ \to F \in (C Func D)$
3		cofuval.g	$⊢ φ \to G \in (D Func E)$
4		df-cofu	$⊢ \circ_{func} = (g \in V, f \in V ⟼ ⟨1^{st} (g) \circ 1^{st} (f), (x \in dom dom 2^{nd} (f), y \in dom dom 2^{nd} (f) ⟼ (1^{st} (f) (x) 2^{nd} (g) 1^{st} (f) (y)) \circ (x 2^{nd} (f) y))⟩)$
5	4	a1i	$⊢ φ \to \circ_{func} = (g \in V, f \in V ⟼ ⟨1^{st} (g) \circ 1^{st} (f), (x \in dom dom 2^{nd} (f), y \in dom dom 2^{nd} (f) ⟼ (1^{st} (f) (x) 2^{nd} (g) 1^{st} (f) (y)) \circ (x 2^{nd} (f) y))⟩)$
6		simprl	$⊢ (φ \land (g = G \land f = F)) \to g = G$
7	6	fveq2d	$⊢ (φ \land (g = G \land f = F)) \to 1^{st} (g) = 1^{st} (G)$
8		simprr	$⊢ (φ \land (g = G \land f = F)) \to f = F$
9	8	fveq2d	$⊢ (φ \land (g = G \land f = F)) \to 1^{st} (f) = 1^{st} (F)$
10	7 9	coeq12d	$⊢ (φ \land (g = G \land f = F)) \to 1^{st} (g) \circ 1^{st} (f) = 1^{st} (G) \circ 1^{st} (F)$
11	8	fveq2d	$⊢ (φ \land (g = G \land f = F)) \to 2^{nd} (f) = 2^{nd} (F)$
12	11	dmeqd	$⊢ (φ \land (g = G \land f = F)) \to dom 2^{nd} (f) = dom 2^{nd} (F)$
13		relfunc	$⊢ Rel (C Func D)$
14		1st2ndbr	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
15	13 2 14	sylancr	$⊢ φ \to 1^{st} (F) (C Func D) 2^{nd} (F)$
16	1 15	funcfn2	$⊢ φ \to 2^{nd} (F) Fn (B \times B)$
17	16	fndmd	$⊢ φ \to dom 2^{nd} (F) = B \times B$
18	17	adantr	$⊢ (φ \land (g = G \land f = F)) \to dom 2^{nd} (F) = B \times B$
19	12 18	eqtrd	$⊢ (φ \land (g = G \land f = F)) \to dom 2^{nd} (f) = B \times B$
20	19	dmeqd	$⊢ (φ \land (g = G \land f = F)) \to dom dom 2^{nd} (f) = dom (B \times B)$
21		dmxpid	$⊢ dom (B \times B) = B$
22	20 21	syl6eq	$⊢ (φ \land (g = G \land f = F)) \to dom dom 2^{nd} (f) = B$
23	6	fveq2d	$⊢ (φ \land (g = G \land f = F)) \to 2^{nd} (g) = 2^{nd} (G)$
24	9	fveq1d	$⊢ (φ \land (g = G \land f = F)) \to 1^{st} (f) (x) = 1^{st} (F) (x)$
25	9	fveq1d	$⊢ (φ \land (g = G \land f = F)) \to 1^{st} (f) (y) = 1^{st} (F) (y)$
26	23 24 25	oveq123d	$⊢ (φ \land (g = G \land f = F)) \to 1^{st} (f) (x) 2^{nd} (g) 1^{st} (f) (y) = 1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)$
27	11	oveqd	$⊢ (φ \land (g = G \land f = F)) \to x 2^{nd} (f) y = x 2^{nd} (F) y$
28	26 27	coeq12d	$⊢ (φ \land (g = G \land f = F)) \to (1^{st} (f) (x) 2^{nd} (g) 1^{st} (f) (y)) \circ (x 2^{nd} (f) y) = (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y)$
29	22 22 28	mpoeq123dv	$⊢ (φ \land (g = G \land f = F)) \to (x \in dom dom 2^{nd} (f), y \in dom dom 2^{nd} (f) ⟼ (1^{st} (f) (x) 2^{nd} (g) 1^{st} (f) (y)) \circ (x 2^{nd} (f) y)) = (x \in B, y \in B ⟼ (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y))$
30	10 29	opeq12d	$⊢ (φ \land (g = G \land f = F)) \to ⟨1^{st} (g) \circ 1^{st} (f), (x \in dom dom 2^{nd} (f), y \in dom dom 2^{nd} (f) ⟼ (1^{st} (f) (x) 2^{nd} (g) 1^{st} (f) (y)) \circ (x 2^{nd} (f) y))⟩ = ⟨1^{st} (G) \circ 1^{st} (F), (x \in B, y \in B ⟼ (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y))⟩$
31	3	elexd	$⊢ φ \to G \in V$
32	2	elexd	$⊢ φ \to F \in V$
33		opex	$⊢ ⟨1^{st} (G) \circ 1^{st} (F), (x \in B, y \in B ⟼ (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y))⟩ \in V$
34	33	a1i	$⊢ φ \to ⟨1^{st} (G) \circ 1^{st} (F), (x \in B, y \in B ⟼ (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y))⟩ \in V$
35	5 30 31 32 34	ovmpod	$⊢ φ \to G \circ_{func} F = ⟨1^{st} (G) \circ 1^{st} (F), (x \in B, y \in B ⟼ (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y))⟩$

Metamath Proof Explorer

Theorem cofuval

Proof