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