cofurid

Description: The identity functor is a right identity for composition. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	cofulid.g	$⊢ φ \to F \in (C Func D)$
	cofurid.1	$⊢ I = {id}_{func} (C)$
Assertion	cofurid	$⊢ φ \to F \circ_{func} I = F$

Proof

Step	Hyp	Ref	Expression
1		cofulid.g	$⊢ φ \to F \in (C Func D)$
2		cofurid.1	$⊢ I = {id}_{func} (C)$
3		eqid	$⊢ {Base}_{C} = {Base}_{C}$
4		funcrcl	$⊢ F \in (C Func D) \to (C \in Cat \land D \in Cat)$
5	1 4	syl	$⊢ φ \to (C \in Cat \land D \in Cat)$
6	5	simpld	$⊢ φ \to C \in Cat$
7	2 3 6	idfu1st	$⊢ φ \to 1^{st} (I) = {I ↾}_{{Base}_{C}}$
8	7	coeq2d	$⊢ φ \to 1^{st} (F) \circ 1^{st} (I) = 1^{st} (F) \circ ({I ↾}_{{Base}_{C}})$
9		eqid	$⊢ {Base}_{D} = {Base}_{D}$
10		relfunc	$⊢ Rel (C Func D)$
11		1st2ndbr	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
12	10 1 11	sylancr	$⊢ φ \to 1^{st} (F) (C Func D) 2^{nd} (F)$
13	3 9 12	funcf1	$⊢ φ \to 1^{st} (F) : {Base}_{C} ⟶ {Base}_{D}$
14		fcoi1	$⊢ 1^{st} (F) : {Base}_{C} ⟶ {Base}_{D} \to 1^{st} (F) \circ ({I ↾}_{{Base}_{C}}) = 1^{st} (F)$
15	13 14	syl	$⊢ φ \to 1^{st} (F) \circ ({I ↾}_{{Base}_{C}}) = 1^{st} (F)$
16	8 15	eqtrd	$⊢ φ \to 1^{st} (F) \circ 1^{st} (I) = 1^{st} (F)$
17	7	3ad2ant1	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to 1^{st} (I) = {I ↾}_{{Base}_{C}}$
18	17	fveq1d	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to 1^{st} (I) (x) = ({I ↾}_{{Base}_{C}}) (x)$
19		fvresi	$⊢ x \in {Base}_{C} \to ({I ↾}_{{Base}_{C}}) (x) = x$
20	19	3ad2ant2	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to ({I ↾}_{{Base}_{C}}) (x) = x$
21	18 20	eqtrd	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to 1^{st} (I) (x) = x$
22	17	fveq1d	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to 1^{st} (I) (y) = ({I ↾}_{{Base}_{C}}) (y)$
23		fvresi	$⊢ y \in {Base}_{C} \to ({I ↾}_{{Base}_{C}}) (y) = y$
24	23	3ad2ant3	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to ({I ↾}_{{Base}_{C}}) (y) = y$
25	22 24	eqtrd	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to 1^{st} (I) (y) = y$
26	21 25	oveq12d	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to 1^{st} (I) (x) 2^{nd} (F) 1^{st} (I) (y) = x 2^{nd} (F) y$
27	6	3ad2ant1	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to C \in Cat$
28		eqid	$⊢ Hom (C) = Hom (C)$
29		simp2	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to x \in {Base}_{C}$
30		simp3	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to y \in {Base}_{C}$
31	2 3 27 28 29 30	idfu2nd	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to x 2^{nd} (I) y = {I ↾}_{(x Hom (C) y)}$
32	26 31	coeq12d	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to (1^{st} (I) (x) 2^{nd} (F) 1^{st} (I) (y)) \circ (x 2^{nd} (I) y) = (x 2^{nd} (F) y) \circ ({I ↾}_{(x Hom (C) y)})$
33		eqid	$⊢ Hom (D) = Hom (D)$
34	12	3ad2ant1	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
35	3 28 33 34 29 30	funcf2	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to (x 2^{nd} (F) y) : x Hom (C) y ⟶ 1^{st} (F) (x) Hom (D) 1^{st} (F) (y)$
36		fcoi1	$⊢ (x 2^{nd} (F) y) : x Hom (C) y ⟶ 1^{st} (F) (x) Hom (D) 1^{st} (F) (y) \to (x 2^{nd} (F) y) \circ ({I ↾}_{(x Hom (C) y)}) = x 2^{nd} (F) y$
37	35 36	syl	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to (x 2^{nd} (F) y) \circ ({I ↾}_{(x Hom (C) y)}) = x 2^{nd} (F) y$
38	32 37	eqtrd	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to (1^{st} (I) (x) 2^{nd} (F) 1^{st} (I) (y)) \circ (x 2^{nd} (I) y) = x 2^{nd} (F) y$
39	38	mpoeq3dva	$⊢ φ \to (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (1^{st} (I) (x) 2^{nd} (F) 1^{st} (I) (y)) \circ (x 2^{nd} (I) y)) = (x \in {Base}_{C}, y \in {Base}_{C} ⟼ x 2^{nd} (F) y)$
40	3 12	funcfn2	$⊢ φ \to 2^{nd} (F) Fn ({Base}_{C} \times {Base}_{C})$
41		fnov	$⊢ 2^{nd} (F) Fn ({Base}_{C} \times {Base}_{C}) \leftrightarrow 2^{nd} (F) = (x \in {Base}_{C}, y \in {Base}_{C} ⟼ x 2^{nd} (F) y)$
42	40 41	sylib	$⊢ φ \to 2^{nd} (F) = (x \in {Base}_{C}, y \in {Base}_{C} ⟼ x 2^{nd} (F) y)$
43	39 42	eqtr4d	$⊢ φ \to (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (1^{st} (I) (x) 2^{nd} (F) 1^{st} (I) (y)) \circ (x 2^{nd} (I) y)) = 2^{nd} (F)$
44	16 43	opeq12d	$⊢ φ \to ⟨1^{st} (F) \circ 1^{st} (I), (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (1^{st} (I) (x) 2^{nd} (F) 1^{st} (I) (y)) \circ (x 2^{nd} (I) y))⟩ = ⟨1^{st} (F), 2^{nd} (F)⟩$
45	2	idfucl	$⊢ C \in Cat \to I \in (C Func C)$
46	6 45	syl	$⊢ φ \to I \in (C Func C)$
47	3 46 1	cofuval	$⊢ φ \to F \circ_{func} I = ⟨1^{st} (F) \circ 1^{st} (I), (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (1^{st} (I) (x) 2^{nd} (F) 1^{st} (I) (y)) \circ (x 2^{nd} (I) y))⟩$
48		1st2nd	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
49	10 1 48	sylancr	$⊢ φ \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
50	44 47 49	3eqtr4d	$⊢ φ \to F \circ_{func} I = F$

Metamath Proof Explorer

Theorem cofurid

Proof