fuclid

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

	Ref	Expression
Hypotheses	fuclid.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
	fuclid.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
	fuclid.x	⊢ ∙ = ( comp ‘ 𝑄 )
	fuclid.1	⊢ 1 = ( Id ‘ 𝐷 )
	fuclid.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 𝑁 𝐺 ) )
Assertion	fuclid	⊢ ( 𝜑 → ( ( 1 ∘ ( 1^st ‘ 𝐺 ) ) ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐺 ) 𝑅 ) = 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		fuclid.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
2		fuclid.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
3		fuclid.x	⊢ ∙ = ( comp ‘ 𝑄 )
4		fuclid.1	⊢ 1 = ( Id ‘ 𝐷 )
5		fuclid.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 𝑁 𝐺 ) )
6		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
7		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
8		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
9	2	natrcl	⊢ ( 𝑅 ∈ ( 𝐹 𝑁 𝐺 ) → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) )
10	5 9	syl	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) )
11	10	simprd	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐷 ) )
12		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
13	8 11 12	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
14	6 7 13	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
15		fvco3	⊢ ( ( ( 1^st ‘ 𝐺 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1 ∘ ( 1^st ‘ 𝐺 ) ) ‘ 𝑥 ) = ( 1 ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) )
16	14 15	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1 ∘ ( 1^st ‘ 𝐺 ) ) ‘ 𝑥 ) = ( 1 ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) )
17	16	oveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 1 ∘ ( 1^st ‘ 𝐺 ) ) ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) = ( ( 1 ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) )
18		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
19	10	simpld	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
20		funcrcl	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
21	19 20	syl	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
22	21	simprd	⊢ ( 𝜑 → 𝐷 ∈ Cat )
23	22	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐷 ∈ Cat )
24		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
25	8 19 24	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
26	6 7 25	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
27	26	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
28		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
29	14	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
30	2 5	nat1st2nd	⊢ ( 𝜑 → 𝑅 ∈ ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ 𝑁 ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ) )
31	30	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑅 ∈ ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ 𝑁 ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ) )
32		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
33	2 31 6 18 32	natcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑅 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) )
34	7 18 4 23 27 28 29 33	catlid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1 ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) = ( 𝑅 ‘ 𝑥 ) )
35	17 34	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 1 ∘ ( 1^st ‘ 𝐺 ) ) ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) = ( 𝑅 ‘ 𝑥 ) )
36	35	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 1 ∘ ( 1^st ‘ 𝐺 ) ) ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑅 ‘ 𝑥 ) ) )
37	1 2 4 11	fucidcl	⊢ ( 𝜑 → ( 1 ∘ ( 1^st ‘ 𝐺 ) ) ∈ ( 𝐺 𝑁 𝐺 ) )
38	1 2 6 28 3 5 37	fucco	⊢ ( 𝜑 → ( ( 1 ∘ ( 1^st ‘ 𝐺 ) ) ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐺 ) 𝑅 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 1 ∘ ( 1^st ‘ 𝐺 ) ) ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) ) )
39	2 30 6	natfn	⊢ ( 𝜑 → 𝑅 Fn ( Base ‘ 𝐶 ) )
40		dffn5	⊢ ( 𝑅 Fn ( Base ‘ 𝐶 ) ↔ 𝑅 = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑅 ‘ 𝑥 ) ) )
41	39 40	sylib	⊢ ( 𝜑 → 𝑅 = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑅 ‘ 𝑥 ) ) )
42	36 38 41	3eqtr4d	⊢ ( 𝜑 → ( ( 1 ∘ ( 1^st ‘ 𝐺 ) ) ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐺 ) 𝑅 ) = 𝑅 )

Metamath Proof Explorer

Theorem fuclid

Proof