fuclid

Description: Left 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	fuclid	$⊢ φ \to (\underset{˙}{1} \circ 1^{st} (G)) (⟨F, G⟩ \underset{˙}{∙} G) R = 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	simprd	$⊢ φ \to G \in (C Func D)$
12		1st2ndbr	$⊢ (Rel (C Func D) \land G \in (C Func D)) \to 1^{st} (G) (C Func D) 2^{nd} (G)$
13	8 11 12	sylancr	$⊢ φ \to 1^{st} (G) (C Func D) 2^{nd} (G)$
14	6 7 13	funcf1	$⊢ φ \to 1^{st} (G) : {Base}_{C} ⟶ {Base}_{D}$
15		fvco3	$⊢ (1^{st} (G) : {Base}_{C} ⟶ {Base}_{D} \land x \in {Base}_{C}) \to (\underset{˙}{1} \circ 1^{st} (G)) (x) = \underset{˙}{1} (1^{st} (G) (x))$
16	14 15	sylan	$⊢ (φ \land x \in {Base}_{C}) \to (\underset{˙}{1} \circ 1^{st} (G)) (x) = \underset{˙}{1} (1^{st} (G) (x))$
17	16	oveq1d	$⊢ (φ \land x \in {Base}_{C}) \to (\underset{˙}{1} \circ 1^{st} (G)) (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (G) (x)) R (x) = \underset{˙}{1} (1^{st} (G) (x)) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (G) (x)) R (x)$
18		eqid	$⊢ Hom (D) = Hom (D)$
19	10	simpld	$⊢ φ \to F \in (C Func D)$
20		funcrcl	$⊢ F \in (C Func D) \to (C \in Cat \land D \in Cat)$
21	19 20	syl	$⊢ φ \to (C \in Cat \land D \in Cat)$
22	21	simprd	$⊢ φ \to D \in Cat$
23	22	adantr	$⊢ (φ \land x \in {Base}_{C}) \to D \in Cat$
24		1st2ndbr	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
25	8 19 24	sylancr	$⊢ φ \to 1^{st} (F) (C Func D) 2^{nd} (F)$
26	6 7 25	funcf1	$⊢ φ \to 1^{st} (F) : {Base}_{C} ⟶ {Base}_{D}$
27	26	ffvelcdmda	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (F) (x) \in {Base}_{D}$
28		eqid	$⊢ comp (D) = comp (D)$
29	14	ffvelcdmda	$⊢ (φ \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 23 27 28 29 33	catlid	$⊢ (φ \land x \in {Base}_{C}) \to \underset{˙}{1} (1^{st} (G) (x)) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (G) (x)) R (x) = R (x)$
35	17 34	eqtrd	$⊢ (φ \land x \in {Base}_{C}) \to (\underset{˙}{1} \circ 1^{st} (G)) (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (G) (x)) R (x) = R (x)$
36	35	mpteq2dva	$⊢ φ \to (x \in {Base}_{C} ⟼ (\underset{˙}{1} \circ 1^{st} (G)) (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (G) (x)) R (x)) = (x \in {Base}_{C} ⟼ R (x))$
37	1 2 4 11	fucidcl	$⊢ φ \to \underset{˙}{1} \circ 1^{st} (G) \in (G N G)$
38	1 2 6 28 3 5 37	fucco	$⊢ φ \to (\underset{˙}{1} \circ 1^{st} (G)) (⟨F, G⟩ \underset{˙}{∙} G) R = (x \in {Base}_{C} ⟼ (\underset{˙}{1} \circ 1^{st} (G)) (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (G) (x)) R (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 (\underset{˙}{1} \circ 1^{st} (G)) (⟨F, G⟩ \underset{˙}{∙} G) R = R$

Metamath Proof Explorer

Theorem fuclid

Proof