Metamath Proof Explorer

Theorem htpycc

Description: Concatenate two homotopies. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses htpycc.1 ⊢ 𝑁 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 0 [,] 1 ) ↦ if ( 𝑦 ≤ ( 1 / 2 ) , ( 𝑥 𝐿 ( 2 · 𝑦 ) ) , ( 𝑥 𝑀 ( ( 2 · 𝑦 ) − 1 ) ) ) )
htpycc.2 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
htpycc.4 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
htpycc.5 ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐽 Cn 𝐾 ) )
htpycc.6 ⊢ ( 𝜑 → 𝐻 ∈ ( 𝐽 Cn 𝐾 ) )
htpycc.7 ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐺 ) )
htpycc.8 ⊢ ( 𝜑 → 𝑀 ∈ ( 𝐺 ( 𝐽 Htpy 𝐾 ) 𝐻 ) )
Assertion htpycc ( 𝜑 → 𝑁 ∈ ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐻 ) )

Proof

Step Hyp Ref Expression
1 htpycc.1 ⊢ 𝑁 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 0 [,] 1 ) ↦ if ( 𝑦 ≤ ( 1 / 2 ) , ( 𝑥 𝐿 ( 2 · 𝑦 ) ) , ( 𝑥 𝑀 ( ( 2 · 𝑦 ) − 1 ) ) ) )
2 htpycc.2 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3 htpycc.4 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
4 htpycc.5 ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐽 Cn 𝐾 ) )
5 htpycc.6 ⊢ ( 𝜑 → 𝐻 ∈ ( 𝐽 Cn 𝐾 ) )
6 htpycc.7 ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐺 ) )
7 htpycc.8 ⊢ ( 𝜑 → 𝑀 ∈ ( 𝐺 ( 𝐽 Htpy 𝐾 ) 𝐻 ) )
8 iitopon ⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
9 8 a1i ⊢ ( 𝜑 → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
10 eqid ⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
11 eqid ⊢ ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) )
12 eqid ⊢ ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) )
13 dfii2 ⊢ II = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) )
14 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
15 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
16 halfre ⊢ ( 1 / 2 ) ∈ ℝ
17 halfge0 ⊢ 0 ≤ ( 1 / 2 )
18 1re ⊢ 1 ∈ ℝ
19 halflt1 ⊢ ( 1 / 2 ) < 1
20 16 18 19 ltleii ⊢ ( 1 / 2 ) ≤ 1
21 elicc01 ⊢ ( ( 1 / 2 ) ∈ ( 0 [,] 1 ) ↔ ( ( 1 / 2 ) ∈ ℝ ∧ 0 ≤ ( 1 / 2 ) ∧ ( 1 / 2 ) ≤ 1 ) )
22 16 17 20 21 mpbir3an ⊢ ( 1 / 2 ) ∈ ( 0 [,] 1 )
23 22 a1i ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ( 0 [,] 1 ) )
24 2 3 4 6 htpyi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( ( 𝑠 𝐿 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 𝐿 1 ) = ( 𝐺 ‘ 𝑠 ) ) )
25 24 simprd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑠 𝐿 1 ) = ( 𝐺 ‘ 𝑠 ) )
26 2 4 5 7 htpyi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( ( 𝑠 𝑀 0 ) = ( 𝐺 ‘ 𝑠 ) ∧ ( 𝑠 𝑀 1 ) = ( 𝐻 ‘ 𝑠 ) ) )
27 26 simpld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑠 𝑀 0 ) = ( 𝐺 ‘ 𝑠 ) )
28 25 27 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑠 𝐿 1 ) = ( 𝑠 𝑀 0 ) )
29 28 ralrimiva ⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝑋 ( 𝑠 𝐿 1 ) = ( 𝑠 𝑀 0 ) )
30 oveq1 ⊢ ( 𝑠 = 𝑥 → ( 𝑠 𝐿 1 ) = ( 𝑥 𝐿 1 ) )
31 oveq1 ⊢ ( 𝑠 = 𝑥 → ( 𝑠 𝑀 0 ) = ( 𝑥 𝑀 0 ) )
32 30 31 eqeq12d ⊢ ( 𝑠 = 𝑥 → ( ( 𝑠 𝐿 1 ) = ( 𝑠 𝑀 0 ) ↔ ( 𝑥 𝐿 1 ) = ( 𝑥 𝑀 0 ) ) )
33 32 rspccva ⊢ ( ( ∀ 𝑠 ∈ 𝑋 ( 𝑠 𝐿 1 ) = ( 𝑠 𝑀 0 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 𝐿 1 ) = ( 𝑥 𝑀 0 ) )
34 29 33 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 𝐿 1 ) = ( 𝑥 𝑀 0 ) )
35 34 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑥 𝐿 1 ) = ( 𝑥 𝑀 0 ) )
36 simprl ⊢ ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑥 ∈ 𝑋 ) ) → 𝑦 = ( 1 / 2 ) )
37 36 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑥 ∈ 𝑋 ) ) → ( 2 · 𝑦 ) = ( 2 · ( 1 / 2 ) ) )
38 2cn ⊢ 2 ∈ ℂ
39 2ne0 ⊢ 2 ≠ 0
40 38 39 recidi ⊢ ( 2 · ( 1 / 2 ) ) = 1
41 37 40 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑥 ∈ 𝑋 ) ) → ( 2 · 𝑦 ) = 1 )
42 41 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑥 𝐿 ( 2 · 𝑦 ) ) = ( 𝑥 𝐿 1 ) )
43 41 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑥 ∈ 𝑋 ) ) → ( ( 2 · 𝑦 ) − 1 ) = ( 1 − 1 ) )
44 1m1e0 ⊢ ( 1 − 1 ) = 0
45 43 44 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑥 ∈ 𝑋 ) ) → ( ( 2 · 𝑦 ) − 1 ) = 0 )
46 45 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑥 𝑀 ( ( 2 · 𝑦 ) − 1 ) ) = ( 𝑥 𝑀 0 ) )
47 35 42 46 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑥 𝐿 ( 2 · 𝑦 ) ) = ( 𝑥 𝑀 ( ( 2 · 𝑦 ) − 1 ) ) )
48 retopon ⊢ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
49 0re ⊢ 0 ∈ ℝ
50 iccssre ⊢ ( ( 0 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ )
51 49 16 50 mp2an ⊢ ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ
52 resttopon ⊢ ( ( ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ∧ ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ∈ ( TopOn ‘ ( 0 [,] ( 1 / 2 ) ) ) )
53 48 51 52 mp2an ⊢ ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ∈ ( TopOn ‘ ( 0 [,] ( 1 / 2 ) ) )
54 53 a1i ⊢ ( 𝜑 → ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ∈ ( TopOn ‘ ( 0 [,] ( 1 / 2 ) ) ) )
55 54 2 cnmpt2nd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 0 [,] ( 1 / 2 ) ) , 𝑥 ∈ 𝑋 ↦ 𝑥 ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ×t 𝐽 ) Cn 𝐽 ) )
56 54 2 cnmpt1st ⊢ ( 𝜑 → ( 𝑦 ∈ ( 0 [,] ( 1 / 2 ) ) , 𝑥 ∈ 𝑋 ↦ 𝑦 ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ×t 𝐽 ) Cn ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ) )
57 11 iihalf1cn ⊢ ( 𝑧 ∈ ( 0 [,] ( 1 / 2 ) ) ↦ ( 2 · 𝑧 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) Cn II )
58 57 a1i ⊢ ( 𝜑 → ( 𝑧 ∈ ( 0 [,] ( 1 / 2 ) ) ↦ ( 2 · 𝑧 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) Cn II ) )
59 oveq2 ⊢ ( 𝑧 = 𝑦 → ( 2 · 𝑧 ) = ( 2 · 𝑦 ) )
60 54 2 56 54 58 59 cnmpt21 ⊢ ( 𝜑 → ( 𝑦 ∈ ( 0 [,] ( 1 / 2 ) ) , 𝑥 ∈ 𝑋 ↦ ( 2 · 𝑦 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ×t 𝐽 ) Cn II ) )
61 2 3 4 htpycn ⊢ ( 𝜑 → ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐺 ) ⊆ ( ( 𝐽 ×t II ) Cn 𝐾 ) )
62 61 6 sseldd ⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) )
63 54 2 55 60 62 cnmpt22f ⊢ ( 𝜑 → ( 𝑦 ∈ ( 0 [,] ( 1 / 2 ) ) , 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝐿 ( 2 · 𝑦 ) ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ×t 𝐽 ) Cn 𝐾 ) )
64 iccssre ⊢ ( ( ( 1 / 2 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ )
65 16 18 64 mp2an ⊢ ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ
66 resttopon ⊢ ( ( ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ∧ ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ∈ ( TopOn ‘ ( ( 1 / 2 ) [,] 1 ) ) )
67 48 65 66 mp2an ⊢ ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ∈ ( TopOn ‘ ( ( 1 / 2 ) [,] 1 ) )
68 67 a1i ⊢ ( 𝜑 → ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ∈ ( TopOn ‘ ( ( 1 / 2 ) [,] 1 ) ) )
69 68 2 cnmpt2nd ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 1 / 2 ) [,] 1 ) , 𝑥 ∈ 𝑋 ↦ 𝑥 ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ×t 𝐽 ) Cn 𝐽 ) )
70 68 2 cnmpt1st ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 1 / 2 ) [,] 1 ) , 𝑥 ∈ 𝑋 ↦ 𝑦 ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ×t 𝐽 ) Cn ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ) )
71 12 iihalf2cn ⊢ ( 𝑧 ∈ ( ( 1 / 2 ) [,] 1 ) ↦ ( ( 2 · 𝑧 ) − 1 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) Cn II )
72 71 a1i ⊢ ( 𝜑 → ( 𝑧 ∈ ( ( 1 / 2 ) [,] 1 ) ↦ ( ( 2 · 𝑧 ) − 1 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) Cn II ) )
73 59 oveq1d ⊢ ( 𝑧 = 𝑦 → ( ( 2 · 𝑧 ) − 1 ) = ( ( 2 · 𝑦 ) − 1 ) )
74 68 2 70 68 72 73 cnmpt21 ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 1 / 2 ) [,] 1 ) , 𝑥 ∈ 𝑋 ↦ ( ( 2 · 𝑦 ) − 1 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ×t 𝐽 ) Cn II ) )
75 2 4 5 htpycn ⊢ ( 𝜑 → ( 𝐺 ( 𝐽 Htpy 𝐾 ) 𝐻 ) ⊆ ( ( 𝐽 ×t II ) Cn 𝐾 ) )
76 75 7 sseldd ⊢ ( 𝜑 → 𝑀 ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) )
77 68 2 69 74 76 cnmpt22f ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 1 / 2 ) [,] 1 ) , 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝑀 ( ( 2 · 𝑦 ) − 1 ) ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ×t 𝐽 ) Cn 𝐾 ) )
78 10 11 12 13 14 15 23 2 47 63 77 cnmpopc ⊢ ( 𝜑 → ( 𝑦 ∈ ( 0 [,] 1 ) , 𝑥 ∈ 𝑋 ↦ if ( 𝑦 ≤ ( 1 / 2 ) , ( 𝑥 𝐿 ( 2 · 𝑦 ) ) , ( 𝑥 𝑀 ( ( 2 · 𝑦 ) − 1 ) ) ) ) ∈ ( ( II ×t 𝐽 ) Cn 𝐾 ) )
79 9 2 78 cnmptcom ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 0 [,] 1 ) ↦ if ( 𝑦 ≤ ( 1 / 2 ) , ( 𝑥 𝐿 ( 2 · 𝑦 ) ) , ( 𝑥 𝑀 ( ( 2 · 𝑦 ) − 1 ) ) ) ) ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) )
80 1 79 eqeltrid ⊢ ( 𝜑 → 𝑁 ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) )
81 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → 𝑠 ∈ 𝑋 )
82 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
83 simpr ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 0 ) → 𝑦 = 0 )
84 83 17 eqbrtrdi ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 0 ) → 𝑦 ≤ ( 1 / 2 ) )
85 84 iftrued ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 0 ) → if ( 𝑦 ≤ ( 1 / 2 ) , ( 𝑥 𝐿 ( 2 · 𝑦 ) ) , ( 𝑥 𝑀 ( ( 2 · 𝑦 ) − 1 ) ) ) = ( 𝑥 𝐿 ( 2 · 𝑦 ) ) )
86 simpl ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 0 ) → 𝑥 = 𝑠 )
87 83 oveq2d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 0 ) → ( 2 · 𝑦 ) = ( 2 · 0 ) )
88 2t0e0 ⊢ ( 2 · 0 ) = 0
89 87 88 eqtrdi ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 0 ) → ( 2 · 𝑦 ) = 0 )
90 86 89 oveq12d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 0 ) → ( 𝑥 𝐿 ( 2 · 𝑦 ) ) = ( 𝑠 𝐿 0 ) )
91 85 90 eqtrd ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 0 ) → if ( 𝑦 ≤ ( 1 / 2 ) , ( 𝑥 𝐿 ( 2 · 𝑦 ) ) , ( 𝑥 𝑀 ( ( 2 · 𝑦 ) − 1 ) ) ) = ( 𝑠 𝐿 0 ) )
92 ovex ⊢ ( 𝑠 𝐿 0 ) ∈ V
93 91 1 92 ovmpoa ⊢ ( ( 𝑠 ∈ 𝑋 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝑁 0 ) = ( 𝑠 𝐿 0 ) )
94 81 82 93 sylancl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑠 𝑁 0 ) = ( 𝑠 𝐿 0 ) )
95 24 simpld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑠 𝐿 0 ) = ( 𝐹 ‘ 𝑠 ) )
96 94 95 eqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑠 𝑁 0 ) = ( 𝐹 ‘ 𝑠 ) )
97 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
98 16 18 ltnlei ⊢ ( ( 1 / 2 ) < 1 ↔ ¬ 1 ≤ ( 1 / 2 ) )
99 19 98 mpbi ⊢ ¬ 1 ≤ ( 1 / 2 )
100 simpr ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → 𝑦 = 1 )
101 100 breq1d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → ( 𝑦 ≤ ( 1 / 2 ) ↔ 1 ≤ ( 1 / 2 ) ) )
102 99 101 mtbiri ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → ¬ 𝑦 ≤ ( 1 / 2 ) )
103 102 iffalsed ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → if ( 𝑦 ≤ ( 1 / 2 ) , ( 𝑥 𝐿 ( 2 · 𝑦 ) ) , ( 𝑥 𝑀 ( ( 2 · 𝑦 ) − 1 ) ) ) = ( 𝑥 𝑀 ( ( 2 · 𝑦 ) − 1 ) ) )
104 simpl ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → 𝑥 = 𝑠 )
105 100 oveq2d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → ( 2 · 𝑦 ) = ( 2 · 1 ) )
106 2t1e2 ⊢ ( 2 · 1 ) = 2
107 105 106 eqtrdi ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → ( 2 · 𝑦 ) = 2 )
108 107 oveq1d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → ( ( 2 · 𝑦 ) − 1 ) = ( 2 − 1 ) )
109 2m1e1 ⊢ ( 2 − 1 ) = 1
110 108 109 eqtrdi ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → ( ( 2 · 𝑦 ) − 1 ) = 1 )
111 104 110 oveq12d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → ( 𝑥 𝑀 ( ( 2 · 𝑦 ) − 1 ) ) = ( 𝑠 𝑀 1 ) )
112 103 111 eqtrd ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → if ( 𝑦 ≤ ( 1 / 2 ) , ( 𝑥 𝐿 ( 2 · 𝑦 ) ) , ( 𝑥 𝑀 ( ( 2 · 𝑦 ) − 1 ) ) ) = ( 𝑠 𝑀 1 ) )
113 ovex ⊢ ( 𝑠 𝑀 1 ) ∈ V
114 112 1 113 ovmpoa ⊢ ( ( 𝑠 ∈ 𝑋 ∧ 1 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝑁 1 ) = ( 𝑠 𝑀 1 ) )
115 81 97 114 sylancl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑠 𝑁 1 ) = ( 𝑠 𝑀 1 ) )
116 26 simprd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑠 𝑀 1 ) = ( 𝐻 ‘ 𝑠 ) )
117 115 116 eqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑠 𝑁 1 ) = ( 𝐻 ‘ 𝑠 ) )
118 2 3 5 80 96 117 ishtpyd ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐻 ) )