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 ⊢ φ → F ∈ J Cn K
htpyco2.g ⊢ φ → G ∈ J Cn K
htpyco2.p ⊢ φ → P ∈ K Cn L
htpyco2.h ⊢ φ → H ∈ F J Htpy K G
Assertion htpyco2 ⊢ φ → P ∘ H ∈ P ∘ F J Htpy L P ∘ G

Proof

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