Metamath Proof Explorer


Theorem 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 ∘ ( 1st𝐺 ) ) ( ⟨ 𝐹 , 𝐺 𝐺 ) 𝑅 ) = 𝑅 )

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 𝐷 ) ) → ( 1st𝐺 ) ( 𝐶 Func 𝐷 ) ( 2nd𝐺 ) )
13 8 11 12 sylancr ( 𝜑 → ( 1st𝐺 ) ( 𝐶 Func 𝐷 ) ( 2nd𝐺 ) )
14 6 7 13 funcf1 ( 𝜑 → ( 1st𝐺 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
15 fvco3 ( ( ( 1st𝐺 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1 ∘ ( 1st𝐺 ) ) ‘ 𝑥 ) = ( 1 ‘ ( ( 1st𝐺 ) ‘ 𝑥 ) ) )
16 14 15 sylan ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1 ∘ ( 1st𝐺 ) ) ‘ 𝑥 ) = ( 1 ‘ ( ( 1st𝐺 ) ‘ 𝑥 ) ) )
17 16 oveq1d ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 1 ∘ ( 1st𝐺 ) ) ‘ 𝑥 ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1st𝐺 ) ‘ 𝑥 ) ) ( 𝑅𝑥 ) ) = ( ( 1 ‘ ( ( 1st𝐺 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1st𝐺 ) ‘ 𝑥 ) ) ( 𝑅𝑥 ) ) )
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 𝐷 ) ) → ( 1st𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd𝐹 ) )
25 8 19 24 sylancr ( 𝜑 → ( 1st𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd𝐹 ) )
26 6 7 25 funcf1 ( 𝜑 → ( 1st𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
27 26 ffvelrnda ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1st𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
28 eqid ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
29 14 ffvelrnda ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1st𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
30 2 5 nat1st2nd ( 𝜑𝑅 ∈ ( ⟨ ( 1st𝐹 ) , ( 2nd𝐹 ) ⟩ 𝑁 ⟨ ( 1st𝐺 ) , ( 2nd𝐺 ) ⟩ ) )
31 30 adantr ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑅 ∈ ( ⟨ ( 1st𝐹 ) , ( 2nd𝐹 ) ⟩ 𝑁 ⟨ ( 1st𝐺 ) , ( 2nd𝐺 ) ⟩ ) )
32 simpr ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
33 2 31 6 18 32 natcl ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑅𝑥 ) ∈ ( ( ( 1st𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1st𝐺 ) ‘ 𝑥 ) ) )
34 7 18 4 23 27 28 29 33 catlid ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1 ‘ ( ( 1st𝐺 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1st𝐺 ) ‘ 𝑥 ) ) ( 𝑅𝑥 ) ) = ( 𝑅𝑥 ) )
35 17 34 eqtrd ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 1 ∘ ( 1st𝐺 ) ) ‘ 𝑥 ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1st𝐺 ) ‘ 𝑥 ) ) ( 𝑅𝑥 ) ) = ( 𝑅𝑥 ) )
36 35 mpteq2dva ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 1 ∘ ( 1st𝐺 ) ) ‘ 𝑥 ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1st𝐺 ) ‘ 𝑥 ) ) ( 𝑅𝑥 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑅𝑥 ) ) )
37 1 2 4 11 fucidcl ( 𝜑 → ( 1 ∘ ( 1st𝐺 ) ) ∈ ( 𝐺 𝑁 𝐺 ) )
38 1 2 6 28 3 5 37 fucco ( 𝜑 → ( ( 1 ∘ ( 1st𝐺 ) ) ( ⟨ 𝐹 , 𝐺 𝐺 ) 𝑅 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 1 ∘ ( 1st𝐺 ) ) ‘ 𝑥 ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1st𝐺 ) ‘ 𝑥 ) ) ( 𝑅𝑥 ) ) ) )
39 2 30 6 natfn ( 𝜑𝑅 Fn ( Base ‘ 𝐶 ) )
40 dffn5 ( 𝑅 Fn ( Base ‘ 𝐶 ) ↔ 𝑅 = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑅𝑥 ) ) )
41 39 40 sylib ( 𝜑𝑅 = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑅𝑥 ) ) )
42 36 38 41 3eqtr4d ( 𝜑 → ( ( 1 ∘ ( 1st𝐺 ) ) ( ⟨ 𝐹 , 𝐺 𝐺 ) 𝑅 ) = 𝑅 )