fucrid

Description: Right identity of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	fuclid.q	$⊢ Q = C FuncCat D$
	fuclid.n	$⊢ N = C Nat D$
	fuclid.x	$⊢ \underset{˙}{∙} = comp (Q)$
	fuclid.1	$⊢ \underset{˙}{1} = Id (D)$
	fuclid.r	$⊢ φ \to R \in (F N G)$
Assertion	fucrid	$⊢ φ \to R (⟨F, F⟩ \underset{˙}{∙} G) (\underset{˙}{1} \circ 1^{st} (F)) = R$

Proof

Step	Hyp	Ref	Expression
1		fuclid.q	$⊢ Q = C FuncCat D$
2		fuclid.n	$⊢ N = C Nat D$
3		fuclid.x	$⊢ \underset{˙}{∙} = comp (Q)$
4		fuclid.1	$⊢ \underset{˙}{1} = Id (D)$
5		fuclid.r	$⊢ φ \to R \in (F N G)$
6		eqid	$⊢ {Base}_{C} = {Base}_{C}$
7		eqid	$⊢ {Base}_{D} = {Base}_{D}$
8		relfunc	$⊢ Rel (C Func D)$
9	2	natrcl	$⊢ R \in (F N G) \to (F \in (C Func D) \land G \in (C Func D))$
10	5 9	syl	$⊢ φ \to (F \in (C Func D) \land G \in (C Func D))$
11	10	simpld	$⊢ φ \to F \in (C Func D)$
12		1st2ndbr	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
13	8 11 12	sylancr	$⊢ φ \to 1^{st} (F) (C Func D) 2^{nd} (F)$
14	6 7 13	funcf1	$⊢ φ \to 1^{st} (F) : {Base}_{C} ⟶ {Base}_{D}$
15		fvco3	$⊢ (1^{st} (F) : {Base}_{C} ⟶ {Base}_{D} \land x \in {Base}_{C}) \to (\underset{˙}{1} \circ 1^{st} (F)) (x) = \underset{˙}{1} (1^{st} (F) (x))$
16	14 15	sylan	$⊢ (φ \land x \in {Base}_{C}) \to (\underset{˙}{1} \circ 1^{st} (F)) (x) = \underset{˙}{1} (1^{st} (F) (x))$
17	16	oveq2d	$⊢ (φ \land x \in {Base}_{C}) \to R (x) (⟨1^{st} (F) (x), 1^{st} (F) (x)⟩ comp (D) 1^{st} (G) (x)) (\underset{˙}{1} \circ 1^{st} (F)) (x) = R (x) (⟨1^{st} (F) (x), 1^{st} (F) (x)⟩ comp (D) 1^{st} (G) (x)) \underset{˙}{1} (1^{st} (F) (x))$
18		eqid	$⊢ Hom (D) = Hom (D)$
19		funcrcl	$⊢ F \in (C Func D) \to (C \in Cat \land D \in Cat)$
20	11 19	syl	$⊢ φ \to (C \in Cat \land D \in Cat)$
21	20	simprd	$⊢ φ \to D \in Cat$
22	21	adantr	$⊢ (φ \land x \in {Base}_{C}) \to D \in Cat$
23	14	ffvelrnda	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (F) (x) \in {Base}_{D}$
24		eqid	$⊢ comp (D) = comp (D)$
25	10	simprd	$⊢ φ \to G \in (C Func D)$
26		1st2ndbr	$⊢ (Rel (C Func D) \land G \in (C Func D)) \to 1^{st} (G) (C Func D) 2^{nd} (G)$
27	8 25 26	sylancr	$⊢ φ \to 1^{st} (G) (C Func D) 2^{nd} (G)$
28	6 7 27	funcf1	$⊢ φ \to 1^{st} (G) : {Base}_{C} ⟶ {Base}_{D}$
29	28	ffvelrnda	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (G) (x) \in {Base}_{D}$
30	2 5	nat1st2nd	$⊢ φ \to R \in (⟨1^{st} (F), 2^{nd} (F)⟩ N ⟨1^{st} (G), 2^{nd} (G)⟩)$
31	30	adantr	$⊢ (φ \land x \in {Base}_{C}) \to R \in (⟨1^{st} (F), 2^{nd} (F)⟩ N ⟨1^{st} (G), 2^{nd} (G)⟩)$
32		simpr	$⊢ (φ \land x \in {Base}_{C}) \to x \in {Base}_{C}$
33	2 31 6 18 32	natcl	$⊢ (φ \land x \in {Base}_{C}) \to R (x) \in (1^{st} (F) (x) Hom (D) 1^{st} (G) (x))$
34	7 18 4 22 23 24 29 33	catrid	$⊢ (φ \land x \in {Base}_{C}) \to R (x) (⟨1^{st} (F) (x), 1^{st} (F) (x)⟩ comp (D) 1^{st} (G) (x)) \underset{˙}{1} (1^{st} (F) (x)) = R (x)$
35	17 34	eqtrd	$⊢ (φ \land x \in {Base}_{C}) \to R (x) (⟨1^{st} (F) (x), 1^{st} (F) (x)⟩ comp (D) 1^{st} (G) (x)) (\underset{˙}{1} \circ 1^{st} (F)) (x) = R (x)$
36	35	mpteq2dva	$⊢ φ \to (x \in {Base}_{C} ⟼ R (x) (⟨1^{st} (F) (x), 1^{st} (F) (x)⟩ comp (D) 1^{st} (G) (x)) (\underset{˙}{1} \circ 1^{st} (F)) (x)) = (x \in {Base}_{C} ⟼ R (x))$
37	1 2 4 11	fucidcl	$⊢ φ \to \underset{˙}{1} \circ 1^{st} (F) \in (F N F)$
38	1 2 6 24 3 37 5	fucco	$⊢ φ \to R (⟨F, F⟩ \underset{˙}{∙} G) (\underset{˙}{1} \circ 1^{st} (F)) = (x \in {Base}_{C} ⟼ R (x) (⟨1^{st} (F) (x), 1^{st} (F) (x)⟩ comp (D) 1^{st} (G) (x)) (\underset{˙}{1} \circ 1^{st} (F)) (x))$
39	2 30 6	natfn	$⊢ φ \to R Fn {Base}_{C}$
40		dffn5	$⊢ R Fn {Base}_{C} \leftrightarrow R = (x \in {Base}_{C} ⟼ R (x))$
41	39 40	sylib	$⊢ φ \to R = (x \in {Base}_{C} ⟼ R (x))$
42	36 38 41	3eqtr4d	$⊢ φ \to R (⟨F, F⟩ \underset{˙}{∙} G) (\underset{˙}{1} \circ 1^{st} (F)) = R$

Metamath Proof Explorer

Theorem fucrid

Proof