Metamath Proof Explorer

Theorem htpyco2

Description: Compose a homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015)

Ref Expression
Hypotheses htpyco2.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
htpyco2.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐽 Cn 𝐾 ) )
htpyco2.p ⊢ ( 𝜑 → 𝑃 ∈ ( 𝐾 Cn 𝐿 ) )
htpyco2.h ⊢ ( 𝜑 → 𝐻 ∈ ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐺 ) )
Assertion htpyco2 ( 𝜑 → ( 𝑃 ∘ 𝐻 ) ∈ ( ( 𝑃 ∘ 𝐹 ) ( 𝐽 Htpy 𝐿 ) ( 𝑃 ∘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 htpyco2.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
2 htpyco2.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐽 Cn 𝐾 ) )
3 htpyco2.p ⊢ ( 𝜑 → 𝑃 ∈ ( 𝐾 Cn 𝐿 ) )
4 htpyco2.h ⊢ ( 𝜑 → 𝐻 ∈ ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐺 ) )
5 cntop1 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top )
6 1 5 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
7 toptopon2 ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
8 6 7 sylib ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
9 cnco ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑃 ∈ ( 𝐾 Cn 𝐿 ) ) → ( 𝑃 ∘ 𝐹 ) ∈ ( 𝐽 Cn 𝐿 ) )
10 1 3 9 syl2anc ⊢ ( 𝜑 → ( 𝑃 ∘ 𝐹 ) ∈ ( 𝐽 Cn 𝐿 ) )
11 cnco ⊢ ( ( 𝐺 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑃 ∈ ( 𝐾 Cn 𝐿 ) ) → ( 𝑃 ∘ 𝐺 ) ∈ ( 𝐽 Cn 𝐿 ) )
12 2 3 11 syl2anc ⊢ ( 𝜑 → ( 𝑃 ∘ 𝐺 ) ∈ ( 𝐽 Cn 𝐿 ) )
13 8 1 2 htpycn ⊢ ( 𝜑 → ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐺 ) ⊆ ( ( 𝐽 ×t II ) Cn 𝐾 ) )
14 13 4 sseldd ⊢ ( 𝜑 → 𝐻 ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) )
15 cnco ⊢ ( ( 𝐻 ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∧ 𝑃 ∈ ( 𝐾 Cn 𝐿 ) ) → ( 𝑃 ∘ 𝐻 ) ∈ ( ( 𝐽 ×t II ) Cn 𝐿 ) )
16 14 3 15 syl2anc ⊢ ( 𝜑 → ( 𝑃 ∘ 𝐻 ) ∈ ( ( 𝐽 ×t II ) Cn 𝐿 ) )
17 8 1 2 4 htpyi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ 𝐽 ) → ( ( 𝑠 𝐻 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 𝐻 1 ) = ( 𝐺 ‘ 𝑠 ) ) )
18 17 simpld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ 𝐽 ) → ( 𝑠 𝐻 0 ) = ( 𝐹 ‘ 𝑠 ) )
19 18 fveq2d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ 𝐽 ) → ( 𝑃 ‘ ( 𝑠 𝐻 0 ) ) = ( 𝑃 ‘ ( 𝐹 ‘ 𝑠 ) ) )
20 iitopon ⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
21 txtopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) ) → ( 𝐽 ×t II ) ∈ ( TopOn ‘ ( ∪ 𝐽 × ( 0 [,] 1 ) ) ) )
22 8 20 21 sylancl ⊢ ( 𝜑 → ( 𝐽 ×t II ) ∈ ( TopOn ‘ ( ∪ 𝐽 × ( 0 [,] 1 ) ) ) )
23 cntop2 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
24 1 23 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
25 toptopon2 ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
26 24 25 sylib ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
27 cnf2 ⊢ ( ( ( 𝐽 ×t II ) ∈ ( TopOn ‘ ( ∪ 𝐽 × ( 0 [,] 1 ) ) ) ∧ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ∧ 𝐻 ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ) → 𝐻 : ( ∪ 𝐽 × ( 0 [,] 1 ) ) ⟶ ∪ 𝐾 )
28 22 26 14 27 syl3anc ⊢ ( 𝜑 → 𝐻 : ( ∪ 𝐽 × ( 0 [,] 1 ) ) ⟶ ∪ 𝐾 )
29 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ 𝐽 ) → 𝑠 ∈ ∪ 𝐽 )
30 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
31 opelxpi ⊢ ( ( 𝑠 ∈ ∪ 𝐽 ∧ 0 ∈ ( 0 [,] 1 ) ) → ⟨ 𝑠 , 0 ⟩ ∈ ( ∪ 𝐽 × ( 0 [,] 1 ) ) )
32 29 30 31 sylancl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ 𝐽 ) → ⟨ 𝑠 , 0 ⟩ ∈ ( ∪ 𝐽 × ( 0 [,] 1 ) ) )
33 fvco3 ⊢ ( ( 𝐻 : ( ∪ 𝐽 × ( 0 [,] 1 ) ) ⟶ ∪ 𝐾 ∧ ⟨ 𝑠 , 0 ⟩ ∈ ( ∪ 𝐽 × ( 0 [,] 1 ) ) ) → ( ( 𝑃 ∘ 𝐻 ) ‘ ⟨ 𝑠 , 0 ⟩ ) = ( 𝑃 ‘ ( 𝐻 ‘ ⟨ 𝑠 , 0 ⟩ ) ) )
34 28 32 33 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ 𝐽 ) → ( ( 𝑃 ∘ 𝐻 ) ‘ ⟨ 𝑠 , 0 ⟩ ) = ( 𝑃 ‘ ( 𝐻 ‘ ⟨ 𝑠 , 0 ⟩ ) ) )
35 df-ov ⊢ ( 𝑠 ( 𝑃 ∘ 𝐻 ) 0 ) = ( ( 𝑃 ∘ 𝐻 ) ‘ ⟨ 𝑠 , 0 ⟩ )
36 df-ov ⊢ ( 𝑠 𝐻 0 ) = ( 𝐻 ‘ ⟨ 𝑠 , 0 ⟩ )
37 36 fveq2i ⊢ ( 𝑃 ‘ ( 𝑠 𝐻 0 ) ) = ( 𝑃 ‘ ( 𝐻 ‘ ⟨ 𝑠 , 0 ⟩ ) )
38 34 35 37 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ 𝐽 ) → ( 𝑠 ( 𝑃 ∘ 𝐻 ) 0 ) = ( 𝑃 ‘ ( 𝑠 𝐻 0 ) ) )
39 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
40 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
41 39 40 cnf ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 )
42 1 41 syl ⊢ ( 𝜑 → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 )
43 fvco3 ⊢ ( ( 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 ∧ 𝑠 ∈ ∪ 𝐽 ) → ( ( 𝑃 ∘ 𝐹 ) ‘ 𝑠 ) = ( 𝑃 ‘ ( 𝐹 ‘ 𝑠 ) ) )
44 42 43 sylan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ 𝐽 ) → ( ( 𝑃 ∘ 𝐹 ) ‘ 𝑠 ) = ( 𝑃 ‘ ( 𝐹 ‘ 𝑠 ) ) )
45 19 38 44 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ 𝐽 ) → ( 𝑠 ( 𝑃 ∘ 𝐻 ) 0 ) = ( ( 𝑃 ∘ 𝐹 ) ‘ 𝑠 ) )
46 17 simprd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ 𝐽 ) → ( 𝑠 𝐻 1 ) = ( 𝐺 ‘ 𝑠 ) )
47 46 fveq2d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ 𝐽 ) → ( 𝑃 ‘ ( 𝑠 𝐻 1 ) ) = ( 𝑃 ‘ ( 𝐺 ‘ 𝑠 ) ) )
48 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
49 opelxpi ⊢ ( ( 𝑠 ∈ ∪ 𝐽 ∧ 1 ∈ ( 0 [,] 1 ) ) → ⟨ 𝑠 , 1 ⟩ ∈ ( ∪ 𝐽 × ( 0 [,] 1 ) ) )
50 29 48 49 sylancl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ 𝐽 ) → ⟨ 𝑠 , 1 ⟩ ∈ ( ∪ 𝐽 × ( 0 [,] 1 ) ) )
51 fvco3 ⊢ ( ( 𝐻 : ( ∪ 𝐽 × ( 0 [,] 1 ) ) ⟶ ∪ 𝐾 ∧ ⟨ 𝑠 , 1 ⟩ ∈ ( ∪ 𝐽 × ( 0 [,] 1 ) ) ) → ( ( 𝑃 ∘ 𝐻 ) ‘ ⟨ 𝑠 , 1 ⟩ ) = ( 𝑃 ‘ ( 𝐻 ‘ ⟨ 𝑠 , 1 ⟩ ) ) )
52 28 50 51 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ 𝐽 ) → ( ( 𝑃 ∘ 𝐻 ) ‘ ⟨ 𝑠 , 1 ⟩ ) = ( 𝑃 ‘ ( 𝐻 ‘ ⟨ 𝑠 , 1 ⟩ ) ) )
53 df-ov ⊢ ( 𝑠 ( 𝑃 ∘ 𝐻 ) 1 ) = ( ( 𝑃 ∘ 𝐻 ) ‘ ⟨ 𝑠 , 1 ⟩ )
54 df-ov ⊢ ( 𝑠 𝐻 1 ) = ( 𝐻 ‘ ⟨ 𝑠 , 1 ⟩ )
55 54 fveq2i ⊢ ( 𝑃 ‘ ( 𝑠 𝐻 1 ) ) = ( 𝑃 ‘ ( 𝐻 ‘ ⟨ 𝑠 , 1 ⟩ ) )
56 52 53 55 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ 𝐽 ) → ( 𝑠 ( 𝑃 ∘ 𝐻 ) 1 ) = ( 𝑃 ‘ ( 𝑠 𝐻 1 ) ) )
57 39 40 cnf ⊢ ( 𝐺 ∈ ( 𝐽 Cn 𝐾 ) → 𝐺 : ∪ 𝐽 ⟶ ∪ 𝐾 )
58 2 57 syl ⊢ ( 𝜑 → 𝐺 : ∪ 𝐽 ⟶ ∪ 𝐾 )
59 fvco3 ⊢ ( ( 𝐺 : ∪ 𝐽 ⟶ ∪ 𝐾 ∧ 𝑠 ∈ ∪ 𝐽 ) → ( ( 𝑃 ∘ 𝐺 ) ‘ 𝑠 ) = ( 𝑃 ‘ ( 𝐺 ‘ 𝑠 ) ) )
60 58 59 sylan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ 𝐽 ) → ( ( 𝑃 ∘ 𝐺 ) ‘ 𝑠 ) = ( 𝑃 ‘ ( 𝐺 ‘ 𝑠 ) ) )
61 47 56 60 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ 𝐽 ) → ( 𝑠 ( 𝑃 ∘ 𝐻 ) 1 ) = ( ( 𝑃 ∘ 𝐺 ) ‘ 𝑠 ) )
62 8 10 12 16 45 61 ishtpyd ⊢ ( 𝜑 → ( 𝑃 ∘ 𝐻 ) ∈ ( ( 𝑃 ∘ 𝐹 ) ( 𝐽 Htpy 𝐿 ) ( 𝑃 ∘ 𝐺 ) ) )