sectco

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

	Ref	Expression
Hypotheses	sectco.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	sectco.o	⊢ · = ( comp ‘ 𝐶 )
	sectco.s	⊢ 𝑆 = ( Sect ‘ 𝐶 )
	sectco.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	sectco.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	sectco.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	sectco.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	sectco.1	⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 )
	sectco.2	⊢ ( 𝜑 → 𝐻 ( 𝑌 𝑆 𝑍 ) 𝐾 )
Assertion	sectco	⊢ ( 𝜑 → ( 𝐻 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ( 𝑋 𝑆 𝑍 ) ( 𝐺 ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		sectco.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		sectco.o	⊢ · = ( comp ‘ 𝐶 )
3		sectco.s	⊢ 𝑆 = ( Sect ‘ 𝐶 )
4		sectco.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
5		sectco.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		sectco.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7		sectco.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
8		sectco.1	⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 )
9		sectco.2	⊢ ( 𝜑 → 𝐻 ( 𝑌 𝑆 𝑍 ) 𝐾 )
10		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
11		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
12	1 10 2 11 3 4 5 6	issect	⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ) )
13	8 12	mpbid	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) )
14	13	simp1d	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
15	1 10 2 11 3 4 6 7	issect	⊢ ( 𝜑 → ( 𝐻 ( 𝑌 𝑆 𝑍 ) 𝐾 ↔ ( 𝐻 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑍 ) ∧ 𝐾 ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ ( 𝐾 ( ⟨ 𝑌 , 𝑍 ⟩ · 𝑌 ) 𝐻 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) ) )
16	9 15	mpbid	⊢ ( 𝜑 → ( 𝐻 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑍 ) ∧ 𝐾 ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ ( 𝐾 ( ⟨ 𝑌 , 𝑍 ⟩ · 𝑌 ) 𝐻 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) )
17	16	simp1d	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑍 ) )
18	1 10 2 4 5 6 7 14 17	catcocl	⊢ ( 𝜑 → ( 𝐻 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑍 ) )
19	16	simp2d	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑌 ) )
20	13	simp2d	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) )
21	1 10 2 4 5 7 6 18 19 5 20	catass	⊢ ( 𝜑 → ( ( 𝐺 ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) 𝐾 ) ( ⟨ 𝑋 , 𝑍 ⟩ · 𝑋 ) ( 𝐻 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ) = ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) ( 𝐾 ( ⟨ 𝑋 , 𝑍 ⟩ · 𝑌 ) ( 𝐻 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ) ) )
22	16	simp3d	⊢ ( 𝜑 → ( 𝐾 ( ⟨ 𝑌 , 𝑍 ⟩ · 𝑌 ) 𝐻 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) )
23	22	oveq1d	⊢ ( 𝜑 → ( ( 𝐾 ( ⟨ 𝑌 , 𝑍 ⟩ · 𝑌 ) 𝐻 ) ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑌 ) 𝐹 ) = ( ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑌 ) 𝐹 ) )
24	1 10 2 4 5 6 7 14 17 6 19	catass	⊢ ( 𝜑 → ( ( 𝐾 ( ⟨ 𝑌 , 𝑍 ⟩ · 𝑌 ) 𝐻 ) ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑌 ) 𝐹 ) = ( 𝐾 ( ⟨ 𝑋 , 𝑍 ⟩ · 𝑌 ) ( 𝐻 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ) )
25	1 10 11 4 5 2 6 14	catlid	⊢ ( 𝜑 → ( ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑌 ) 𝐹 ) = 𝐹 )
26	23 24 25	3eqtr3d	⊢ ( 𝜑 → ( 𝐾 ( ⟨ 𝑋 , 𝑍 ⟩ · 𝑌 ) ( 𝐻 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ) = 𝐹 )
27	26	oveq2d	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) ( 𝐾 ( ⟨ 𝑋 , 𝑍 ⟩ · 𝑌 ) ( 𝐻 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ) ) = ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) )
28	13	simp3d	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) )
29	21 27 28	3eqtrd	⊢ ( 𝜑 → ( ( 𝐺 ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) 𝐾 ) ( ⟨ 𝑋 , 𝑍 ⟩ · 𝑋 ) ( 𝐻 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) )
30	1 10 2 4 7 6 5 19 20	catcocl	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) 𝐾 ) ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑋 ) )
31	1 10 2 11 3 4 5 7 18 30	issect2	⊢ ( 𝜑 → ( ( 𝐻 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ( 𝑋 𝑆 𝑍 ) ( 𝐺 ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) 𝐾 ) ↔ ( ( 𝐺 ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) 𝐾 ) ( ⟨ 𝑋 , 𝑍 ⟩ · 𝑋 ) ( 𝐻 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) )
32	29 31	mpbird	⊢ ( 𝜑 → ( 𝐻 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ( 𝑋 𝑆 𝑍 ) ( 𝐺 ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) 𝐾 ) )

Metamath Proof Explorer

Theorem sectco

Proof