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 ⊢ φ → F ∈ II Cn J
phtpyco2.g ⊢ φ → G ∈ II Cn J
phtpyco2.p ⊢ φ → P ∈ J Cn K
phtpyco2.h ⊢ φ → H ∈ F PHtpy ⁡ J G
Assertion phtpyco2 ⊢ φ → P ∘ H ∈ P ∘ F PHtpy ⁡ K P ∘ G

Proof

Step Hyp Ref Expression
1 phtpyco2.f ⊢ φ → F ∈ II Cn J
2 phtpyco2.g ⊢ φ → G ∈ II Cn J
3 phtpyco2.p ⊢ φ → P ∈ J Cn K
4 phtpyco2.h ⊢ φ → H ∈ F PHtpy ⁡ J G
5 cnco ⊢ F ∈ II Cn J ∧ P ∈ J Cn K → P ∘ F ∈ II Cn K
6 1 3 5 syl2anc ⊢ φ → P ∘ F ∈ II Cn K
7 cnco ⊢ G ∈ II Cn J ∧ P ∈ J Cn K → P ∘ G ∈ II Cn K
8 2 3 7 syl2anc ⊢ φ → P ∘ G ∈ II Cn K
9 1 2 phtpyhtpy ⊢ φ → F PHtpy ⁡ J G ⊆ F II Htpy J G
10 9 4 sseldd ⊢ φ → H ∈ F II Htpy J G
11 1 2 3 10 htpyco2 ⊢ φ → P ∘ H ∈ P ∘ F II Htpy K P ∘ G
12 1 2 4 phtpyi ⊢ φ ∧ s ∈ 0 1 → 0 H s = F ⁡ 0 ∧ 1 H s = F ⁡ 1
13 12 simpld ⊢ φ ∧ s ∈ 0 1 → 0 H s = F ⁡ 0
14 13 fveq2d ⊢ φ ∧ s ∈ 0 1 → P ⁡ 0 H s = P ⁡ F ⁡ 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 ⊢ F ∈ II Cn J → J ∈ Top
19 1 18 syl ⊢ φ → J ∈ Top
20 toptopon2 ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ ⋃ J
21 19 20 sylib ⊢ φ → J ∈ TopOn ⁡ ⋃ J
22 1 2 phtpycn ⊢ φ → F PHtpy ⁡ J G ⊆ II × t II Cn J
23 22 4 sseldd ⊢ φ → H ∈ II × t II Cn J
24 cnf2 ⊢ II × t II ∈ TopOn ⁡ 0 1 × 0 1 ∧ J ∈ TopOn ⁡ ⋃ J ∧ H ∈ II × t II Cn J → H : 0 1 × 0 1 ⟶ ⋃ J
25 17 21 23 24 mp3an2i ⊢ φ → H : 0 1 × 0 1 ⟶ ⋃ J
26 0elunit ⊢ 0 ∈ 0 1
27 simpr ⊢ φ ∧ s ∈ 0 1 → s ∈ 0 1
28 opelxpi ⊢ 0 ∈ 0 1 ∧ s ∈ 0 1 → 0 s ∈ 0 1 × 0 1
29 26 27 28 sylancr ⊢ φ ∧ s ∈ 0 1 → 0 s ∈ 0 1 × 0 1
30 fvco3 ⊢ H : 0 1 × 0 1 ⟶ ⋃ J ∧ 0 s ∈ 0 1 × 0 1 → P ∘ H ⁡ 0 s = P ⁡ H ⁡ 0 s
31 25 29 30 syl2an2r ⊢ φ ∧ s ∈ 0 1 → P ∘ H ⁡ 0 s = P ⁡ H ⁡ 0 s
32 df-ov ⊢ 0 P ∘ H s = P ∘ H ⁡ 0 s
33 df-ov ⊢ 0 H s = H ⁡ 0 s
34 33 fveq2i ⊢ P ⁡ 0 H s = P ⁡ H ⁡ 0 s
35 31 32 34 3eqtr4g ⊢ φ ∧ s ∈ 0 1 → 0 P ∘ H s = P ⁡ 0 H s
36 iiuni ⊢ 0 1 = ⋃ II
37 eqid ⊢ ⋃ J = ⋃ J
38 36 37 cnf ⊢ F ∈ II Cn J → F : 0 1 ⟶ ⋃ J
39 1 38 syl ⊢ φ → F : 0 1 ⟶ ⋃ J
40 39 adantr ⊢ φ ∧ s ∈ 0 1 → F : 0 1 ⟶ ⋃ J
41 fvco3 ⊢ F : 0 1 ⟶ ⋃ J ∧ 0 ∈ 0 1 → P ∘ F ⁡ 0 = P ⁡ F ⁡ 0
42 40 26 41 sylancl ⊢ φ ∧ s ∈ 0 1 → P ∘ F ⁡ 0 = P ⁡ F ⁡ 0
43 14 35 42 3eqtr4d ⊢ φ ∧ s ∈ 0 1 → 0 P ∘ H s = P ∘ F ⁡ 0
44 12 simprd ⊢ φ ∧ s ∈ 0 1 → 1 H s = F ⁡ 1
45 44 fveq2d ⊢ φ ∧ s ∈ 0 1 → P ⁡ 1 H s = P ⁡ F ⁡ 1
46 1elunit ⊢ 1 ∈ 0 1
47 opelxpi ⊢ 1 ∈ 0 1 ∧ s ∈ 0 1 → 1 s ∈ 0 1 × 0 1
48 46 27 47 sylancr ⊢ φ ∧ s ∈ 0 1 → 1 s ∈ 0 1 × 0 1
49 fvco3 ⊢ H : 0 1 × 0 1 ⟶ ⋃ J ∧ 1 s ∈ 0 1 × 0 1 → P ∘ H ⁡ 1 s = P ⁡ H ⁡ 1 s
50 25 48 49 syl2an2r ⊢ φ ∧ s ∈ 0 1 → P ∘ H ⁡ 1 s = P ⁡ H ⁡ 1 s
51 df-ov ⊢ 1 P ∘ H s = P ∘ H ⁡ 1 s
52 df-ov ⊢ 1 H s = H ⁡ 1 s
53 52 fveq2i ⊢ P ⁡ 1 H s = P ⁡ H ⁡ 1 s
54 50 51 53 3eqtr4g ⊢ φ ∧ s ∈ 0 1 → 1 P ∘ H s = P ⁡ 1 H s
55 fvco3 ⊢ F : 0 1 ⟶ ⋃ J ∧ 1 ∈ 0 1 → P ∘ F ⁡ 1 = P ⁡ F ⁡ 1
56 40 46 55 sylancl ⊢ φ ∧ s ∈ 0 1 → P ∘ F ⁡ 1 = P ⁡ F ⁡ 1
57 45 54 56 3eqtr4d ⊢ φ ∧ s ∈ 0 1 → 1 P ∘ H s = P ∘ F ⁡ 1
58 6 8 11 43 57 isphtpyd ⊢ φ → P ∘ H ∈ P ∘ F PHtpy ⁡ K P ∘ G