Theorem arwrid

Description: Right 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	arwrid	$$⊢\phi \to F\underset{\dot{}}{·}\underset{\dot{}}{1}\left(X\right)=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	simpld	$$⊢\phi \to X\in {\mathrm{Base}}_C$$
12	3 5 7 8 11	ida2	$$⊢\phi \to 2^{nd}\left(\underset{\dot{}}{1}\left(X\right)\right)=\mathrm{Id}\left(C\right)\left(X\right)$$
13	12	oveq2d	$$⊢\phi \to 2^{nd}\left(F\right)\left(⟨X,X⟩\mathrm{comp}\left(C\right)Y\right)2^{nd}\left(\underset{\dot{}}{1}\left(X\right)\right)=2^{nd}\left(F\right)\left(⟨X,X⟩\mathrm{comp}\left(C\right)Y\right)\mathrm{Id}\left(C\right)\left(X\right)$$
14		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
15		eqid	$$⊢\mathrm{comp}\left(C\right)=\mathrm{comp}\left(C\right)$$
16	10	simprd	$$⊢\phi \to Y\in {\mathrm{Base}}_C$$
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 11 15 16 18	catrid	$$⊢\phi \to 2^{nd}\left(F\right)\left(⟨X,X⟩\mathrm{comp}\left(C\right)Y\right)\mathrm{Id}\left(C\right)\left(X\right)=2^{nd}\left(F\right)$$
20	13 19	eqtrd	$$⊢\phi \to 2^{nd}\left(F\right)\left(⟨X,X⟩\mathrm{comp}\left(C\right)Y\right)2^{nd}\left(\underset{\dot{}}{1}\left(X\right)\right)=2^{nd}\left(F\right)$$
21	20	oteq3d	$$⊢\phi \to ⟨X,Y,2^{nd}\left(F\right)\left(⟨X,X⟩\mathrm{comp}\left(C\right)Y\right)2^{nd}\left(\underset{\dot{}}{1}\left(X\right)\right)⟩=⟨X,Y,2^{nd}\left(F\right)⟩$$
22	3 5 7 11 1	idahom	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)\in \left(XHX\right)$$
23	2 1 22 4 15	coaval	$$⊢\phi \to F\underset{\dot{}}{·}\underset{\dot{}}{1}\left(X\right)=⟨X,Y,2^{nd}\left(F\right)\left(⟨X,X⟩\mathrm{comp}\left(C\right)Y\right)2^{nd}\left(\underset{\dot{}}{1}\left(X\right)\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 F\underset{\dot{}}{·}\underset{\dot{}}{1}\left(X\right)=F$$