fucrid

Description: Right 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	fucrid	⊢ ( 𝜑 → ( 𝑅 ( ⟨ 𝐹 , 𝐹 ⟩ ∙ 𝐺 ) ( 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	simpld	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 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	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑅 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( ( 1 ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑥 ) ) = ( ( 𝑅 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 1 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
18		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
19		funcrcl	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
20	11 19	syl	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
21	20	simprd	⊢ ( 𝜑 → 𝐷 ∈ Cat )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐷 ∈ Cat )
23	14	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
24		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
25	10	simprd	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐷 ) )
26		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
27	8 25 26	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
28	6 7 27	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
29	28	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 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 22 23 24 29 33	catrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑅 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 1 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) = ( 𝑅 ‘ 𝑥 ) )
35	17 34	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑅 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( ( 1 ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑥 ) ) = ( 𝑅 ‘ 𝑥 ) )
36	35	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑅 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( ( 1 ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑅 ‘ 𝑥 ) ) )
37	1 2 4 11	fucidcl	⊢ ( 𝜑 → ( 1 ∘ ( 1^st ‘ 𝐹 ) ) ∈ ( 𝐹 𝑁 𝐹 ) )
38	1 2 6 24 3 37 5	fucco	⊢ ( 𝜑 → ( 𝑅 ( ⟨ 𝐹 , 𝐹 ⟩ ∙ 𝐺 ) ( 1 ∘ ( 1^st ‘ 𝐹 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑅 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( ( 1 ∘ ( 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 fucrid

Proof