This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → ( 𝐻 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ( 𝑋 𝑆 𝑍 ) ( 𝐺 ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) 𝐾 ) )