Theorem arwass

Description: Associativity of composition in 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	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
	arwass.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) )
	arwass.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑍 𝐻 𝑊 ) )
Assertion	arwass	⊢ ( 𝜑 → ( ( 𝐾 · 𝐺 ) · 𝐹 ) = ( 𝐾 · ( 𝐺 · 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		arwlid.h	⊢ 𝐻 = ( Homa ‘ 𝐶 )
2		arwlid.o	⊢ · = ( compa ‘ 𝐶 )
3		arwlid.a	⊢ 1 = ( Ida ‘ 𝐶 )
4		arwlid.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
5		arwass.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) )
6		arwass.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑍 𝐻 𝑊 ) )
7		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
8		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
9		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
10	1	homarcl	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → 𝐶 ∈ Cat )
11	4 10	syl	⊢ ( 𝜑 → 𝐶 ∈ Cat )
12	1 7	homarcl2	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) )
13	4 12	syl	⊢ ( 𝜑 → ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) )
14	13	simpld	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
15	13	simprd	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐶 ) )
16	1 7	homarcl2	⊢ ( 𝐾 ∈ ( 𝑍 𝐻 𝑊 ) → ( 𝑍 ∈ ( Base ‘ 𝐶 ) ∧ 𝑊 ∈ ( Base ‘ 𝐶 ) ) )
17	6 16	syl	⊢ ( 𝜑 → ( 𝑍 ∈ ( Base ‘ 𝐶 ) ∧ 𝑊 ∈ ( Base ‘ 𝐶 ) ) )
18	17	simpld	⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ 𝐶 ) )
19	1 8	homahom	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ( 2nd ‘ 𝐹 ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
20	4 19	syl	⊢ ( 𝜑 → ( 2nd ‘ 𝐹 ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
21	1 8	homahom	⊢ ( 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) → ( 2nd ‘ 𝐺 ) ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑍 ) )
22	5 21	syl	⊢ ( 𝜑 → ( 2nd ‘ 𝐺 ) ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑍 ) )
23	17	simprd	⊢ ( 𝜑 → 𝑊 ∈ ( Base ‘ 𝐶 ) )
24	1 8	homahom	⊢ ( 𝐾 ∈ ( 𝑍 𝐻 𝑊 ) → ( 2nd ‘ 𝐾 ) ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑊 ) )
25	6 24	syl	⊢ ( 𝜑 → ( 2nd ‘ 𝐾 ) ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑊 ) )
26	7 8 9 11 14 15 18 20 22 23 25	catass	⊢ ( 𝜑 → ( ( ( 2nd ‘ 𝐾 ) ( ⟨ 𝑌 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) ( 2nd ‘ 𝐺 ) ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) ( 2nd ‘ 𝐹 ) ) = ( ( 2nd ‘ 𝐾 ) ( ⟨ 𝑋 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) ( ( 2nd ‘ 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) ( 2nd ‘ 𝐹 ) ) ) )
27	2 1 5 6 9	coa2	⊢ ( 𝜑 → ( 2nd ‘ ( 𝐾 · 𝐺 ) ) = ( ( 2nd ‘ 𝐾 ) ( ⟨ 𝑌 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) ( 2nd ‘ 𝐺 ) ) )
28	27	oveq1d	⊢ ( 𝜑 → ( ( 2nd ‘ ( 𝐾 · 𝐺 ) ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) ( 2nd ‘ 𝐹 ) ) = ( ( ( 2nd ‘ 𝐾 ) ( ⟨ 𝑌 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) ( 2nd ‘ 𝐺 ) ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) ( 2nd ‘ 𝐹 ) ) )
29	2 1 4 5 9	coa2	⊢ ( 𝜑 → ( 2nd ‘ ( 𝐺 · 𝐹 ) ) = ( ( 2nd ‘ 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) ( 2nd ‘ 𝐹 ) ) )
30	29	oveq2d	⊢ ( 𝜑 → ( ( 2nd ‘ 𝐾 ) ( ⟨ 𝑋 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) ( 2nd ‘ ( 𝐺 · 𝐹 ) ) ) = ( ( 2nd ‘ 𝐾 ) ( ⟨ 𝑋 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) ( ( 2nd ‘ 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) ( 2nd ‘ 𝐹 ) ) ) )
31	26 28 30	3eqtr4d	⊢ ( 𝜑 → ( ( 2nd ‘ ( 𝐾 · 𝐺 ) ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) ( 2nd ‘ 𝐹 ) ) = ( ( 2nd ‘ 𝐾 ) ( ⟨ 𝑋 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) ( 2nd ‘ ( 𝐺 · 𝐹 ) ) ) )
32	31	oteq3d	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑊 , ( ( 2nd ‘ ( 𝐾 · 𝐺 ) ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) ( 2nd ‘ 𝐹 ) ) ⟩ = ⟨ 𝑋 , 𝑊 , ( ( 2nd ‘ 𝐾 ) ( ⟨ 𝑋 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) ( 2nd ‘ ( 𝐺 · 𝐹 ) ) ) ⟩ )
33	2 1 5 6	coahom	⊢ ( 𝜑 → ( 𝐾 · 𝐺 ) ∈ ( 𝑌 𝐻 𝑊 ) )
34	2 1 4 33 9	coaval	⊢ ( 𝜑 → ( ( 𝐾 · 𝐺 ) · 𝐹 ) = ⟨ 𝑋 , 𝑊 , ( ( 2nd ‘ ( 𝐾 · 𝐺 ) ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) ( 2nd ‘ 𝐹 ) ) ⟩ )
35	2 1 4 5	coahom	⊢ ( 𝜑 → ( 𝐺 · 𝐹 ) ∈ ( 𝑋 𝐻 𝑍 ) )
36	2 1 35 6 9	coaval	⊢ ( 𝜑 → ( 𝐾 · ( 𝐺 · 𝐹 ) ) = ⟨ 𝑋 , 𝑊 , ( ( 2nd ‘ 𝐾 ) ( ⟨ 𝑋 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) ( 2nd ‘ ( 𝐺 · 𝐹 ) ) ) ⟩ )
37	32 34 36	3eqtr4d	⊢ ( 𝜑 → ( ( 𝐾 · 𝐺 ) · 𝐹 ) = ( 𝐾 · ( 𝐺 · 𝐹 ) ) )