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\left(C\right)$$
	arwlid.o	$$⊢\underset{\dot{}}{·}={comp}_a\left(C\right)$$
	arwlid.a	$$⊢\underset{\dot{}}{1}={Id}_a\left(C\right)$$
	arwlid.f	$$⊢\phi \to F\in \left(XHY\right)$$
Assertion	arwlid	$$⊢\phi \to \underset{\dot{}}{1}\left(Y\right)\underset{\dot{}}{·}F=F$$

Proof

Step	Hyp	Ref	Expression
1		arwlid.h	$$⊢H={Hom}_a\left(C\right)$$
2		arwlid.o	$$⊢\underset{\dot{}}{·}={comp}_a\left(C\right)$$
3		arwlid.a	$$⊢\underset{\dot{}}{1}={Id}_a\left(C\right)$$
4		arwlid.f	$$⊢\phi \to F\in \left(XHY\right)$$
5		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
6	1	homarcl	$$⊢F\in \left(XHY\right)\to C\in \mathrm{Cat}$$
7	4 6	syl	$$⊢\phi \to C\in \mathrm{Cat}$$
8		eqid	$$⊢\mathrm{Id}\left(C\right)=\mathrm{Id}\left(C\right)$$
9	1 5	homarcl2	$$⊢F\in \left(XHY\right)\to \left(X\in {\mathrm{Base}}_C\wedge Y\in {\mathrm{Base}}_C\right)$$
10	4 9	syl	$$⊢\phi \to \left(X\in {\mathrm{Base}}_C\wedge Y\in {\mathrm{Base}}_C\right)$$
11	10	simprd	$$⊢\phi \to Y\in {\mathrm{Base}}_C$$
12	3 5 7 8 11	ida2	$$⊢\phi \to 2^{nd}\left(\underset{\dot{}}{1}\left(Y\right)\right)=\mathrm{Id}\left(C\right)\left(Y\right)$$
13	12	oveq1d	$$⊢\phi \to 2^{nd}\left(\underset{\dot{}}{1}\left(Y\right)\right)\left(⟨X,Y⟩\mathrm{comp}\left(C\right)Y\right)2^{nd}\left(F\right)=\mathrm{Id}\left(C\right)\left(Y\right)\left(⟨X,Y⟩\mathrm{comp}\left(C\right)Y\right)2^{nd}\left(F\right)$$
14		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
15	10	simpld	$$⊢\phi \to X\in {\mathrm{Base}}_C$$
16		eqid	$$⊢\mathrm{comp}\left(C\right)=\mathrm{comp}\left(C\right)$$
17	1 14	homahom	$$⊢F\in \left(XHY\right)\to 2^{nd}\left(F\right)\in \left(X\mathrm{Hom}\left(C\right)Y\right)$$
18	4 17	syl	$$⊢\phi \to 2^{nd}\left(F\right)\in \left(X\mathrm{Hom}\left(C\right)Y\right)$$
19	5 14 8 7 15 16 11 18	catlid	$$⊢\phi \to \mathrm{Id}\left(C\right)\left(Y\right)\left(⟨X,Y⟩\mathrm{comp}\left(C\right)Y\right)2^{nd}\left(F\right)=2^{nd}\left(F\right)$$
20	13 19	eqtrd	$$⊢\phi \to 2^{nd}\left(\underset{\dot{}}{1}\left(Y\right)\right)\left(⟨X,Y⟩\mathrm{comp}\left(C\right)Y\right)2^{nd}\left(F\right)=2^{nd}\left(F\right)$$
21	20	oteq3d	$$⊢\phi \to ⟨X,Y,2^{nd}\left(\underset{\dot{}}{1}\left(Y\right)\right)\left(⟨X,Y⟩\mathrm{comp}\left(C\right)Y\right)2^{nd}\left(F\right)⟩=⟨X,Y,2^{nd}\left(F\right)⟩$$
22	3 5 7 11 1	idahom	$$⊢\phi \to \underset{\dot{}}{1}\left(Y\right)\in \left(YHY\right)$$
23	2 1 4 22 16	coaval	$$⊢\phi \to \underset{\dot{}}{1}\left(Y\right)\underset{\dot{}}{·}F=⟨X,Y,2^{nd}\left(\underset{\dot{}}{1}\left(Y\right)\right)\left(⟨X,Y⟩\mathrm{comp}\left(C\right)Y\right)2^{nd}\left(F\right)⟩$$
24	1	homadmcd	$$⊢F\in \left(XHY\right)\to F=⟨X,Y,2^{nd}\left(F\right)⟩$$
25	4 24	syl	$$⊢\phi \to F=⟨X,Y,2^{nd}\left(F\right)⟩$$
26	21 23 25	3eqtr4d	$$⊢\phi \to \underset{\dot{}}{1}\left(Y\right)\underset{\dot{}}{·}F=F$$