Metamath Proof Explorer


Theorem arwlid

Description: Left identity of a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses arwlid.h H = Hom a C
arwlid.o · ˙ = comp a C
arwlid.a 1 ˙ = Id a C
arwlid.f φ F X H Y
Assertion arwlid φ 1 ˙ Y · ˙ F = F

Proof

Step Hyp Ref Expression
1 arwlid.h H = Hom a C
2 arwlid.o · ˙ = comp a C
3 arwlid.a 1 ˙ = Id a C
4 arwlid.f φ F X H Y
5 eqid Base C = Base C
6 1 homarcl F X H Y C Cat
7 4 6 syl φ C Cat
8 eqid Id C = Id C
9 1 5 homarcl2 F X H Y X Base C Y Base C
10 4 9 syl φ X Base C Y Base C
11 10 simprd φ Y Base C
12 3 5 7 8 11 ida2 φ 2 nd 1 ˙ Y = Id C Y
13 12 oveq1d φ 2 nd 1 ˙ Y X Y comp C Y 2 nd F = Id C Y X Y comp C Y 2 nd F
14 eqid Hom C = Hom C
15 10 simpld φ X Base C
16 eqid comp C = comp C
17 1 14 homahom F X H Y 2 nd F X Hom C Y
18 4 17 syl φ 2 nd F X Hom C Y
19 5 14 8 7 15 16 11 18 catlid φ Id C Y X Y comp C Y 2 nd F = 2 nd F
20 13 19 eqtrd φ 2 nd 1 ˙ Y X Y comp C Y 2 nd F = 2 nd F
21 20 oteq3d φ X Y 2 nd 1 ˙ Y X Y comp C Y 2 nd F = X Y 2 nd F
22 3 5 7 11 1 idahom φ 1 ˙ Y Y H Y
23 2 1 4 22 16 coaval φ 1 ˙ Y · ˙ F = X Y 2 nd 1 ˙ Y X Y comp C Y 2 nd F
24 1 homadmcd F X H Y F = X Y 2 nd F
25 4 24 syl φ F = X Y 2 nd F
26 21 23 25 3eqtr4d φ 1 ˙ Y · ˙ F = F