Metamath Proof Explorer

Theorem phtpyco2

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

Ref Expression
Hypotheses phtpyco2.f ⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
phtpyco2.g ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
phtpyco2.p ⊢ ( 𝜑 → 𝑃 ∈ ( 𝐽 Cn 𝐾 ) )
phtpyco2.h ⊢ ( 𝜑 → 𝐻 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) )
Assertion phtpyco2 ( 𝜑 → ( 𝑃 ∘ 𝐻 ) ∈ ( ( 𝑃 ∘ 𝐹 ) ( PHtpy ‘ 𝐾 ) ( 𝑃 ∘ 𝐺 ) ) )

Proof

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