Theorem sectco

Description: Composition of two sections. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	sectco.b	$$⊢B={\mathrm{Base}}_C$$
	sectco.o	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
	sectco.s	$$⊢S=\mathrm{Sect}\left(C\right)$$
	sectco.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	sectco.x	$$⊢\phi \to X\in B$$
	sectco.y	$$⊢\phi \to Y\in B$$
	sectco.z	$$⊢\phi \to Z\in B$$
	sectco.1	$$⊢\phi \to F\left(XSY\right)G$$
	sectco.2	$$⊢\phi \to H\left(YSZ\right)K$$
Assertion	sectco	$$⊢\phi \to \left(H\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F\right)\left(XSZ\right)\left(G\left(⟨Z,Y⟩\underset{\dot{}}{·}X\right)K\right)$$

Proof

Step	Hyp	Ref	Expression
1		sectco.b	$$⊢B={\mathrm{Base}}_C$$
2		sectco.o	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
3		sectco.s	$$⊢S=\mathrm{Sect}\left(C\right)$$
4		sectco.c	$$⊢\phi \to C\in \mathrm{Cat}$$
5		sectco.x	$$⊢\phi \to X\in B$$
6		sectco.y	$$⊢\phi \to Y\in B$$
7		sectco.z	$$⊢\phi \to Z\in B$$
8		sectco.1	$$⊢\phi \to F\left(XSY\right)G$$
9		sectco.2	$$⊢\phi \to H\left(YSZ\right)K$$
10		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
11		eqid	$$⊢\mathrm{Id}\left(C\right)=\mathrm{Id}\left(C\right)$$
12	1 10 2 11 3 4 5 6	issect	$$⊢\phi \to \left(F\left(XSY\right)G\leftrightarrow \left(F\in \left(X\mathrm{Hom}\left(C\right)Y\right)\wedge G\in \left(Y\mathrm{Hom}\left(C\right)X\right)\wedge G\left(⟨X,Y⟩\underset{\dot{}}{·}X\right)F=\mathrm{Id}\left(C\right)\left(X\right)\right)\right)$$
13	8 12	mpbid	$$⊢\phi \to \left(F\in \left(X\mathrm{Hom}\left(C\right)Y\right)\wedge G\in \left(Y\mathrm{Hom}\left(C\right)X\right)\wedge G\left(⟨X,Y⟩\underset{\dot{}}{·}X\right)F=\mathrm{Id}\left(C\right)\left(X\right)\right)$$
14	13	simp1d	$$⊢\phi \to F\in \left(X\mathrm{Hom}\left(C\right)Y\right)$$
15	1 10 2 11 3 4 6 7	issect	$$⊢\phi \to \left(H\left(YSZ\right)K\leftrightarrow \left(H\in \left(Y\mathrm{Hom}\left(C\right)Z\right)\wedge K\in \left(Z\mathrm{Hom}\left(C\right)Y\right)\wedge K\left(⟨Y,Z⟩\underset{\dot{}}{·}Y\right)H=\mathrm{Id}\left(C\right)\left(Y\right)\right)\right)$$
16	9 15	mpbid	$$⊢\phi \to \left(H\in \left(Y\mathrm{Hom}\left(C\right)Z\right)\wedge K\in \left(Z\mathrm{Hom}\left(C\right)Y\right)\wedge K\left(⟨Y,Z⟩\underset{\dot{}}{·}Y\right)H=\mathrm{Id}\left(C\right)\left(Y\right)\right)$$
17	16	simp1d	$$⊢\phi \to H\in \left(Y\mathrm{Hom}\left(C\right)Z\right)$$
18	1 10 2 4 5 6 7 14 17	catcocl	$$⊢\phi \to H\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F\in \left(X\mathrm{Hom}\left(C\right)Z\right)$$
19	16	simp2d	$$⊢\phi \to K\in \left(Z\mathrm{Hom}\left(C\right)Y\right)$$
20	13	simp2d	$$⊢\phi \to G\in \left(Y\mathrm{Hom}\left(C\right)X\right)$$
21	1 10 2 4 5 7 6 18 19 5 20	catass	$$⊢\phi \to \left(G\left(⟨Z,Y⟩\underset{\dot{}}{·}X\right)K\right)\left(⟨X,Z⟩\underset{\dot{}}{·}X\right)\left(H\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F\right)=G\left(⟨X,Y⟩\underset{\dot{}}{·}X\right)\left(K\left(⟨X,Z⟩\underset{\dot{}}{·}Y\right)\left(H\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F\right)\right)$$
22	16	simp3d	$$⊢\phi \to K\left(⟨Y,Z⟩\underset{\dot{}}{·}Y\right)H=\mathrm{Id}\left(C\right)\left(Y\right)$$
23	22	oveq1d	$$⊢\phi \to \left(K\left(⟨Y,Z⟩\underset{\dot{}}{·}Y\right)H\right)\left(⟨X,Y⟩\underset{\dot{}}{·}Y\right)F=\mathrm{Id}\left(C\right)\left(Y\right)\left(⟨X,Y⟩\underset{\dot{}}{·}Y\right)F$$
24	1 10 2 4 5 6 7 14 17 6 19	catass	$$⊢\phi \to \left(K\left(⟨Y,Z⟩\underset{\dot{}}{·}Y\right)H\right)\left(⟨X,Y⟩\underset{\dot{}}{·}Y\right)F=K\left(⟨X,Z⟩\underset{\dot{}}{·}Y\right)\left(H\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F\right)$$
25	1 10 11 4 5 2 6 14	catlid	$$⊢\phi \to \mathrm{Id}\left(C\right)\left(Y\right)\left(⟨X,Y⟩\underset{\dot{}}{·}Y\right)F=F$$
26	23 24 25	3eqtr3d	$$⊢\phi \to K\left(⟨X,Z⟩\underset{\dot{}}{·}Y\right)\left(H\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F\right)=F$$
27	26	oveq2d	$$⊢\phi \to G\left(⟨X,Y⟩\underset{\dot{}}{·}X\right)\left(K\left(⟨X,Z⟩\underset{\dot{}}{·}Y\right)\left(H\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F\right)\right)=G\left(⟨X,Y⟩\underset{\dot{}}{·}X\right)F$$
28	13	simp3d	$$⊢\phi \to G\left(⟨X,Y⟩\underset{\dot{}}{·}X\right)F=\mathrm{Id}\left(C\right)\left(X\right)$$
29	21 27 28	3eqtrd	$$⊢\phi \to \left(G\left(⟨Z,Y⟩\underset{\dot{}}{·}X\right)K\right)\left(⟨X,Z⟩\underset{\dot{}}{·}X\right)\left(H\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F\right)=\mathrm{Id}\left(C\right)\left(X\right)$$
30	1 10 2 4 7 6 5 19 20	catcocl	$$⊢\phi \to G\left(⟨Z,Y⟩\underset{\dot{}}{·}X\right)K\in \left(Z\mathrm{Hom}\left(C\right)X\right)$$
31	1 10 2 11 3 4 5 7 18 30	issect2	$$⊢\phi \to \left(\left(H\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F\right)\left(XSZ\right)\left(G\left(⟨Z,Y⟩\underset{\dot{}}{·}X\right)K\right)\leftrightarrow \left(G\left(⟨Z,Y⟩\underset{\dot{}}{·}X\right)K\right)\left(⟨X,Z⟩\underset{\dot{}}{·}X\right)\left(H\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F\right)=\mathrm{Id}\left(C\right)\left(X\right)\right)$$
32	29 31	mpbird	$$⊢\phi \to \left(H\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F\right)\left(XSZ\right)\left(G\left(⟨Z,Y⟩\underset{\dot{}}{·}X\right)K\right)$$