Theorem arwlid

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

	Ref	Expression
Hypotheses	arwlid.h	⊢ 𝐻 = ( Homa ‘ 𝐶 )
	arwlid.o	⊢ · = ( compa ‘ 𝐶 )
	arwlid.a	⊢ 1 = ( Ida ‘ 𝐶 )
	arwlid.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
Assertion	arwlid	⊢ ( 𝜑 → ( ( 1 ‘ 𝑌 ) · 𝐹 ) = 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		arwlid.h	⊢ 𝐻 = ( Homa ‘ 𝐶 )
2		arwlid.o	⊢ · = ( compa ‘ 𝐶 )
3		arwlid.a	⊢ 1 = ( Ida ‘ 𝐶 )
4		arwlid.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
5		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
6	1	homarcl	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → 𝐶 ∈ Cat )
7	4 6	syl	⊢ ( 𝜑 → 𝐶 ∈ Cat )
8		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
9	1 5	homarcl2	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) )
10	4 9	syl	⊢ ( 𝜑 → ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) )
11	10	simprd	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐶 ) )
12	3 5 7 8 11	ida2	⊢ ( 𝜑 → ( 2nd ‘ ( 1 ‘ 𝑌 ) ) = ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) )
13	12	oveq1d	⊢ ( 𝜑 → ( ( 2nd ‘ ( 1 ‘ 𝑌 ) ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( 2nd ‘ 𝐹 ) ) = ( ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( 2nd ‘ 𝐹 ) ) )
14		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
15	10	simpld	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
16		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
17	1 14	homahom	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ( 2nd ‘ 𝐹 ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
18	4 17	syl	⊢ ( 𝜑 → ( 2nd ‘ 𝐹 ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
19	5 14 8 7 15 16 11 18	catlid	⊢ ( 𝜑 → ( ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( 2nd ‘ 𝐹 ) ) = ( 2nd ‘ 𝐹 ) )
20	13 19	eqtrd	⊢ ( 𝜑 → ( ( 2nd ‘ ( 1 ‘ 𝑌 ) ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( 2nd ‘ 𝐹 ) ) = ( 2nd ‘ 𝐹 ) )
21	20	oteq3d	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 , ( ( 2nd ‘ ( 1 ‘ 𝑌 ) ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( 2nd ‘ 𝐹 ) ) ⟩ = ⟨ 𝑋 , 𝑌 , ( 2nd ‘ 𝐹 ) ⟩ )
22	3 5 7 11 1	idahom	⊢ ( 𝜑 → ( 1 ‘ 𝑌 ) ∈ ( 𝑌 𝐻 𝑌 ) )
23	2 1 4 22 16	coaval	⊢ ( 𝜑 → ( ( 1 ‘ 𝑌 ) · 𝐹 ) = ⟨ 𝑋 , 𝑌 , ( ( 2nd ‘ ( 1 ‘ 𝑌 ) ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( 2nd ‘ 𝐹 ) ) ⟩ )
24	1	homadmcd	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → 𝐹 = ⟨ 𝑋 , 𝑌 , ( 2nd ‘ 𝐹 ) ⟩ )
25	4 24	syl	⊢ ( 𝜑 → 𝐹 = ⟨ 𝑋 , 𝑌 , ( 2nd ‘ 𝐹 ) ⟩ )
26	21 23 25	3eqtr4d	⊢ ( 𝜑 → ( ( 1 ‘ 𝑌 ) · 𝐹 ) = 𝐹 )