Metamath Proof Explorer

Theorem htpyco1

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

Ref Expression
Hypotheses htpyco1.n ⊢ 𝑁 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑃 ‘ 𝑥 ) 𝐻 𝑦 ) )
htpyco1.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
htpyco1.p ⊢ ( 𝜑 → 𝑃 ∈ ( 𝐽 Cn 𝐾 ) )
htpyco1.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐾 Cn 𝐿 ) )
htpyco1.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐾 Cn 𝐿 ) )
htpyco1.h ⊢ ( 𝜑 → 𝐻 ∈ ( 𝐹 ( 𝐾 Htpy 𝐿 ) 𝐺 ) )
Assertion htpyco1 ( 𝜑 → 𝑁 ∈ ( ( 𝐹 ∘ 𝑃 ) ( 𝐽 Htpy 𝐿 ) ( 𝐺 ∘ 𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 htpyco1.n ⊢ 𝑁 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑃 ‘ 𝑥 ) 𝐻 𝑦 ) )
2 htpyco1.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3 htpyco1.p ⊢ ( 𝜑 → 𝑃 ∈ ( 𝐽 Cn 𝐾 ) )
4 htpyco1.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐾 Cn 𝐿 ) )
5 htpyco1.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐾 Cn 𝐿 ) )
6 htpyco1.h ⊢ ( 𝜑 → 𝐻 ∈ ( 𝐹 ( 𝐾 Htpy 𝐿 ) 𝐺 ) )
7 cnco ⊢ ( ( 𝑃 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐹 ∈ ( 𝐾 Cn 𝐿 ) ) → ( 𝐹 ∘ 𝑃 ) ∈ ( 𝐽 Cn 𝐿 ) )
8 3 4 7 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∘ 𝑃 ) ∈ ( 𝐽 Cn 𝐿 ) )
9 cnco ⊢ ( ( 𝑃 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐺 ∈ ( 𝐾 Cn 𝐿 ) ) → ( 𝐺 ∘ 𝑃 ) ∈ ( 𝐽 Cn 𝐿 ) )
10 3 5 9 syl2anc ⊢ ( 𝜑 → ( 𝐺 ∘ 𝑃 ) ∈ ( 𝐽 Cn 𝐿 ) )
11 iitopon ⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
12 11 a1i ⊢ ( 𝜑 → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
13 2 12 cnmpt1st ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 0 [,] 1 ) ↦ 𝑥 ) ∈ ( ( 𝐽 ×t II ) Cn 𝐽 ) )
14 2 12 13 3 cnmpt21f ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑃 ‘ 𝑥 ) ) ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) )
15 2 12 cnmpt2nd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 0 [,] 1 ) ↦ 𝑦 ) ∈ ( ( 𝐽 ×t II ) Cn II ) )
16 cntop2 ⊢ ( 𝑃 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
17 3 16 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
18 toptopon2 ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
19 17 18 sylib ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
20 19 4 5 htpycn ⊢ ( 𝜑 → ( 𝐹 ( 𝐾 Htpy 𝐿 ) 𝐺 ) ⊆ ( ( 𝐾 ×t II ) Cn 𝐿 ) )
21 20 6 sseldd ⊢ ( 𝜑 → 𝐻 ∈ ( ( 𝐾 ×t II ) Cn 𝐿 ) )
22 2 12 14 15 21 cnmpt22f ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑃 ‘ 𝑥 ) 𝐻 𝑦 ) ) ∈ ( ( 𝐽 ×t II ) Cn 𝐿 ) )
23 1 22 eqeltrid ⊢ ( 𝜑 → 𝑁 ∈ ( ( 𝐽 ×t II ) Cn 𝐿 ) )
24 cnf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ∧ 𝑃 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝑃 : 𝑋 ⟶ ∪ 𝐾 )
25 2 19 3 24 syl3anc ⊢ ( 𝜑 → 𝑃 : 𝑋 ⟶ ∪ 𝐾 )
26 25 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑃 ‘ 𝑠 ) ∈ ∪ 𝐾 )
27 19 4 5 6 htpyi ⊢ ( ( 𝜑 ∧ ( 𝑃 ‘ 𝑠 ) ∈ ∪ 𝐾 ) → ( ( ( 𝑃 ‘ 𝑠 ) 𝐻 0 ) = ( 𝐹 ‘ ( 𝑃 ‘ 𝑠 ) ) ∧ ( ( 𝑃 ‘ 𝑠 ) 𝐻 1 ) = ( 𝐺 ‘ ( 𝑃 ‘ 𝑠 ) ) ) )
28 26 27 syldan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( ( ( 𝑃 ‘ 𝑠 ) 𝐻 0 ) = ( 𝐹 ‘ ( 𝑃 ‘ 𝑠 ) ) ∧ ( ( 𝑃 ‘ 𝑠 ) 𝐻 1 ) = ( 𝐺 ‘ ( 𝑃 ‘ 𝑠 ) ) ) )
29 28 simpld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( ( 𝑃 ‘ 𝑠 ) 𝐻 0 ) = ( 𝐹 ‘ ( 𝑃 ‘ 𝑠 ) ) )
30 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → 𝑠 ∈ 𝑋 )
31 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
32 fveq2 ⊢ ( 𝑥 = 𝑠 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑠 ) )
33 id ⊢ ( 𝑦 = 0 → 𝑦 = 0 )
34 32 33 oveqan12d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 0 ) → ( ( 𝑃 ‘ 𝑥 ) 𝐻 𝑦 ) = ( ( 𝑃 ‘ 𝑠 ) 𝐻 0 ) )
35 ovex ⊢ ( ( 𝑃 ‘ 𝑠 ) 𝐻 0 ) ∈ V
36 34 1 35 ovmpoa ⊢ ( ( 𝑠 ∈ 𝑋 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝑁 0 ) = ( ( 𝑃 ‘ 𝑠 ) 𝐻 0 ) )
37 30 31 36 sylancl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑠 𝑁 0 ) = ( ( 𝑃 ‘ 𝑠 ) 𝐻 0 ) )
38 fvco3 ⊢ ( ( 𝑃 : 𝑋 ⟶ ∪ 𝐾 ∧ 𝑠 ∈ 𝑋 ) → ( ( 𝐹 ∘ 𝑃 ) ‘ 𝑠 ) = ( 𝐹 ‘ ( 𝑃 ‘ 𝑠 ) ) )
39 25 38 sylan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( ( 𝐹 ∘ 𝑃 ) ‘ 𝑠 ) = ( 𝐹 ‘ ( 𝑃 ‘ 𝑠 ) ) )
40 29 37 39 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑠 𝑁 0 ) = ( ( 𝐹 ∘ 𝑃 ) ‘ 𝑠 ) )
41 28 simprd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( ( 𝑃 ‘ 𝑠 ) 𝐻 1 ) = ( 𝐺 ‘ ( 𝑃 ‘ 𝑠 ) ) )
42 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
43 id ⊢ ( 𝑦 = 1 → 𝑦 = 1 )
44 32 43 oveqan12d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → ( ( 𝑃 ‘ 𝑥 ) 𝐻 𝑦 ) = ( ( 𝑃 ‘ 𝑠 ) 𝐻 1 ) )
45 ovex ⊢ ( ( 𝑃 ‘ 𝑠 ) 𝐻 1 ) ∈ V
46 44 1 45 ovmpoa ⊢ ( ( 𝑠 ∈ 𝑋 ∧ 1 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝑁 1 ) = ( ( 𝑃 ‘ 𝑠 ) 𝐻 1 ) )
47 30 42 46 sylancl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑠 𝑁 1 ) = ( ( 𝑃 ‘ 𝑠 ) 𝐻 1 ) )
48 fvco3 ⊢ ( ( 𝑃 : 𝑋 ⟶ ∪ 𝐾 ∧ 𝑠 ∈ 𝑋 ) → ( ( 𝐺 ∘ 𝑃 ) ‘ 𝑠 ) = ( 𝐺 ‘ ( 𝑃 ‘ 𝑠 ) ) )
49 25 48 sylan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( ( 𝐺 ∘ 𝑃 ) ‘ 𝑠 ) = ( 𝐺 ‘ ( 𝑃 ‘ 𝑠 ) ) )
50 41 47 49 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑠 𝑁 1 ) = ( ( 𝐺 ∘ 𝑃 ) ‘ 𝑠 ) )
51 2 8 10 23 40 50 ishtpyd ⊢ ( 𝜑 → 𝑁 ∈ ( ( 𝐹 ∘ 𝑃 ) ( 𝐽 Htpy 𝐿 ) ( 𝐺 ∘ 𝑃 ) ) )