Metamath Proof Explorer

Theorem pcohtpylem

Description: Lemma for pcohtpy . (Contributed by Jeff Madsen, 15-Jun-2010) (Revised by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses pcohtpy.4 ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 0 ) )
pcohtpy.5 ⊢ ( 𝜑 → 𝐹 ( ≃ph ‘ 𝐽 ) 𝐻 )
pcohtpy.6 ⊢ ( 𝜑 → 𝐺 ( ≃ph ‘ 𝐽 ) 𝐾 )
pcohtpylem.7 ⊢ 𝑃 = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( ( 2 · 𝑥 ) 𝑀 𝑦 ) , ( ( ( 2 · 𝑥 ) − 1 ) 𝑁 𝑦 ) ) )
pcohtpylem.8 ⊢ ( 𝜑 → 𝑀 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐻 ) )
pcohtpylem.9 ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐾 ) )
Assertion pcohtpylem ( 𝜑 → 𝑃 ∈ ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ( PHtpy ‘ 𝐽 ) ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 pcohtpy.4 ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 0 ) )
2 pcohtpy.5 ⊢ ( 𝜑 → 𝐹 ( ≃ph ‘ 𝐽 ) 𝐻 )
3 pcohtpy.6 ⊢ ( 𝜑 → 𝐺 ( ≃ph ‘ 𝐽 ) 𝐾 )
4 pcohtpylem.7 ⊢ 𝑃 = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( ( 2 · 𝑥 ) 𝑀 𝑦 ) , ( ( ( 2 · 𝑥 ) − 1 ) 𝑁 𝑦 ) ) )
5 pcohtpylem.8 ⊢ ( 𝜑 → 𝑀 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐻 ) )
6 pcohtpylem.9 ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐾 ) )
7 isphtpc ⊢ ( 𝐹 ( ≃ph ‘ 𝐽 ) 𝐻 ↔ ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ 𝐻 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐻 ) ≠ ∅ ) )
8 2 7 sylib ⊢ ( 𝜑 → ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ 𝐻 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐻 ) ≠ ∅ ) )
9 8 simp1d ⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
10 isphtpc ⊢ ( 𝐺 ( ≃ph ‘ 𝐽 ) 𝐾 ↔ ( 𝐺 ∈ ( II Cn 𝐽 ) ∧ 𝐾 ∈ ( II Cn 𝐽 ) ∧ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐾 ) ≠ ∅ ) )
11 3 10 sylib ⊢ ( 𝜑 → ( 𝐺 ∈ ( II Cn 𝐽 ) ∧ 𝐾 ∈ ( II Cn 𝐽 ) ∧ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐾 ) ≠ ∅ ) )
12 11 simp1d ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
13 9 12 1 pcocn ⊢ ( 𝜑 → ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ∈ ( II Cn 𝐽 ) )
14 8 simp2d ⊢ ( 𝜑 → 𝐻 ∈ ( II Cn 𝐽 ) )
15 11 simp2d ⊢ ( 𝜑 → 𝐾 ∈ ( II Cn 𝐽 ) )
16 9 14 5 phtpy01 ⊢ ( 𝜑 → ( ( 𝐹 ‘ 0 ) = ( 𝐻 ‘ 0 ) ∧ ( 𝐹 ‘ 1 ) = ( 𝐻 ‘ 1 ) ) )
17 16 simprd ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = ( 𝐻 ‘ 1 ) )
18 12 15 6 phtpy01 ⊢ ( 𝜑 → ( ( 𝐺 ‘ 0 ) = ( 𝐾 ‘ 0 ) ∧ ( 𝐺 ‘ 1 ) = ( 𝐾 ‘ 1 ) ) )
19 18 simpld ⊢ ( 𝜑 → ( 𝐺 ‘ 0 ) = ( 𝐾 ‘ 0 ) )
20 1 17 19 3eqtr3d ⊢ ( 𝜑 → ( 𝐻 ‘ 1 ) = ( 𝐾 ‘ 0 ) )
21 14 15 20 pcocn ⊢ ( 𝜑 → ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐾 ) ∈ ( II Cn 𝐽 ) )
22 eqid ⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
23 eqid ⊢ ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) )
24 eqid ⊢ ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) )
25 dfii2 ⊢ II = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) )
26 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
27 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
28 halfre ⊢ ( 1 / 2 ) ∈ ℝ
29 halfge0 ⊢ 0 ≤ ( 1 / 2 )
30 1re ⊢ 1 ∈ ℝ
31 halflt1 ⊢ ( 1 / 2 ) < 1
32 28 30 31 ltleii ⊢ ( 1 / 2 ) ≤ 1
33 elicc01 ⊢ ( ( 1 / 2 ) ∈ ( 0 [,] 1 ) ↔ ( ( 1 / 2 ) ∈ ℝ ∧ 0 ≤ ( 1 / 2 ) ∧ ( 1 / 2 ) ≤ 1 ) )
34 28 29 32 33 mpbir3an ⊢ ( 1 / 2 ) ∈ ( 0 [,] 1 )
35 34 a1i ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ( 0 [,] 1 ) )
36 iitopon ⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
37 36 a1i ⊢ ( 𝜑 → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
38 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 = ( 1 / 2 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 0 ) )
39 9 14 5 phtpyi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 [,] 1 ) ) → ( ( 0 𝑀 𝑦 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 𝑀 𝑦 ) = ( 𝐹 ‘ 1 ) ) )
40 39 simprd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 [,] 1 ) ) → ( 1 𝑀 𝑦 ) = ( 𝐹 ‘ 1 ) )
41 40 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑥 = ( 1 / 2 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ) → ( 1 𝑀 𝑦 ) = ( 𝐹 ‘ 1 ) )
42 12 15 6 phtpyi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 [,] 1 ) ) → ( ( 0 𝑁 𝑦 ) = ( 𝐺 ‘ 0 ) ∧ ( 1 𝑁 𝑦 ) = ( 𝐺 ‘ 1 ) ) )
43 42 simpld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 [,] 1 ) ) → ( 0 𝑁 𝑦 ) = ( 𝐺 ‘ 0 ) )
44 43 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑥 = ( 1 / 2 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ) → ( 0 𝑁 𝑦 ) = ( 𝐺 ‘ 0 ) )
45 38 41 44 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 = ( 1 / 2 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ) → ( 1 𝑀 𝑦 ) = ( 0 𝑁 𝑦 ) )
46 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 = ( 1 / 2 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ) → 𝑥 = ( 1 / 2 ) )
47 46 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 = ( 1 / 2 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ) → ( 2 · 𝑥 ) = ( 2 · ( 1 / 2 ) ) )
48 2cn ⊢ 2 ∈ ℂ
49 2ne0 ⊢ 2 ≠ 0
50 48 49 recidi ⊢ ( 2 · ( 1 / 2 ) ) = 1
51 47 50 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑥 = ( 1 / 2 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ) → ( 2 · 𝑥 ) = 1 )
52 51 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 = ( 1 / 2 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ) → ( ( 2 · 𝑥 ) 𝑀 𝑦 ) = ( 1 𝑀 𝑦 ) )
53 51 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 = ( 1 / 2 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ) → ( ( 2 · 𝑥 ) − 1 ) = ( 1 − 1 ) )
54 1m1e0 ⊢ ( 1 − 1 ) = 0
55 53 54 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑥 = ( 1 / 2 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ) → ( ( 2 · 𝑥 ) − 1 ) = 0 )
56 55 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 = ( 1 / 2 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ) → ( ( ( 2 · 𝑥 ) − 1 ) 𝑁 𝑦 ) = ( 0 𝑁 𝑦 ) )
57 45 52 56 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 = ( 1 / 2 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ) → ( ( 2 · 𝑥 ) 𝑀 𝑦 ) = ( ( ( 2 · 𝑥 ) − 1 ) 𝑁 𝑦 ) )
58 retopon ⊢ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
59 0re ⊢ 0 ∈ ℝ
60 iccssre ⊢ ( ( 0 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ )
61 59 28 60 mp2an ⊢ ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ
62 resttopon ⊢ ( ( ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ∧ ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ∈ ( TopOn ‘ ( 0 [,] ( 1 / 2 ) ) ) )
63 58 61 62 mp2an ⊢ ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ∈ ( TopOn ‘ ( 0 [,] ( 1 / 2 ) ) )
64 63 a1i ⊢ ( 𝜑 → ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ∈ ( TopOn ‘ ( 0 [,] ( 1 / 2 ) ) ) )
65 64 37 cnmpt1st ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] ( 1 / 2 ) ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ 𝑥 ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ×t II ) Cn ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ) )
66 23 iihalf1cn ⊢ ( 𝑧 ∈ ( 0 [,] ( 1 / 2 ) ) ↦ ( 2 · 𝑧 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) Cn II )
67 66 a1i ⊢ ( 𝜑 → ( 𝑧 ∈ ( 0 [,] ( 1 / 2 ) ) ↦ ( 2 · 𝑧 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) Cn II ) )
68 oveq2 ⊢ ( 𝑧 = 𝑥 → ( 2 · 𝑧 ) = ( 2 · 𝑥 ) )
69 64 37 65 64 67 68 cnmpt21 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] ( 1 / 2 ) ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 2 · 𝑥 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ×t II ) Cn II ) )
70 64 37 cnmpt2nd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] ( 1 / 2 ) ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ 𝑦 ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ×t II ) Cn II ) )
71 9 14 phtpycn ⊢ ( 𝜑 → ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐻 ) ⊆ ( ( II ×t II ) Cn 𝐽 ) )
72 71 5 sseldd ⊢ ( 𝜑 → 𝑀 ∈ ( ( II ×t II ) Cn 𝐽 ) )
73 64 37 69 70 72 cnmpt22f ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] ( 1 / 2 ) ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( ( 2 · 𝑥 ) 𝑀 𝑦 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ×t II ) Cn 𝐽 ) )
74 iccssre ⊢ ( ( ( 1 / 2 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ )
75 28 30 74 mp2an ⊢ ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ
76 resttopon ⊢ ( ( ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ∧ ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ∈ ( TopOn ‘ ( ( 1 / 2 ) [,] 1 ) ) )
77 58 75 76 mp2an ⊢ ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ∈ ( TopOn ‘ ( ( 1 / 2 ) [,] 1 ) )
78 77 a1i ⊢ ( 𝜑 → ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ∈ ( TopOn ‘ ( ( 1 / 2 ) [,] 1 ) ) )
79 78 37 cnmpt1st ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ 𝑥 ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ×t II ) Cn ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ) )
80 24 iihalf2cn ⊢ ( 𝑧 ∈ ( ( 1 / 2 ) [,] 1 ) ↦ ( ( 2 · 𝑧 ) − 1 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) Cn II )
81 80 a1i ⊢ ( 𝜑 → ( 𝑧 ∈ ( ( 1 / 2 ) [,] 1 ) ↦ ( ( 2 · 𝑧 ) − 1 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) Cn II ) )
82 68 oveq1d ⊢ ( 𝑧 = 𝑥 → ( ( 2 · 𝑧 ) − 1 ) = ( ( 2 · 𝑥 ) − 1 ) )
83 78 37 79 78 81 82 cnmpt21 ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( ( 2 · 𝑥 ) − 1 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ×t II ) Cn II ) )
84 78 37 cnmpt2nd ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ 𝑦 ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ×t II ) Cn II ) )
85 12 15 phtpycn ⊢ ( 𝜑 → ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐾 ) ⊆ ( ( II ×t II ) Cn 𝐽 ) )
86 85 6 sseldd ⊢ ( 𝜑 → 𝑁 ∈ ( ( II ×t II ) Cn 𝐽 ) )
87 78 37 83 84 86 cnmpt22f ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( ( ( 2 · 𝑥 ) − 1 ) 𝑁 𝑦 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ×t II ) Cn 𝐽 ) )
88 22 23 24 25 26 27 35 37 57 73 87 cnmpopc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( ( 2 · 𝑥 ) 𝑀 𝑦 ) , ( ( ( 2 · 𝑥 ) − 1 ) 𝑁 𝑦 ) ) ) ∈ ( ( II ×t II ) Cn 𝐽 ) )
89 4 88 eqeltrid ⊢ ( 𝜑 → 𝑃 ∈ ( ( II ×t II ) Cn 𝐽 ) )
90 simpll ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑠 ≤ ( 1 / 2 ) ) → 𝜑 )
91 elii1 ⊢ ( 𝑠 ∈ ( 0 [,] ( 1 / 2 ) ) ↔ ( 𝑠 ∈ ( 0 [,] 1 ) ∧ 𝑠 ≤ ( 1 / 2 ) ) )
92 iihalf1 ⊢ ( 𝑠 ∈ ( 0 [,] ( 1 / 2 ) ) → ( 2 · 𝑠 ) ∈ ( 0 [,] 1 ) )
93 91 92 sylbir ⊢ ( ( 𝑠 ∈ ( 0 [,] 1 ) ∧ 𝑠 ≤ ( 1 / 2 ) ) → ( 2 · 𝑠 ) ∈ ( 0 [,] 1 ) )
94 93 adantll ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑠 ≤ ( 1 / 2 ) ) → ( 2 · 𝑠 ) ∈ ( 0 [,] 1 ) )
95 9 14 phtpyhtpy ⊢ ( 𝜑 → ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐻 ) ⊆ ( 𝐹 ( II Htpy 𝐽 ) 𝐻 ) )
96 95 5 sseldd ⊢ ( 𝜑 → 𝑀 ∈ ( 𝐹 ( II Htpy 𝐽 ) 𝐻 ) )
97 37 9 14 96 htpyi ⊢ ( ( 𝜑 ∧ ( 2 · 𝑠 ) ∈ ( 0 [,] 1 ) ) → ( ( ( 2 · 𝑠 ) 𝑀 0 ) = ( 𝐹 ‘ ( 2 · 𝑠 ) ) ∧ ( ( 2 · 𝑠 ) 𝑀 1 ) = ( 𝐻 ‘ ( 2 · 𝑠 ) ) ) )
98 90 94 97 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑠 ≤ ( 1 / 2 ) ) → ( ( ( 2 · 𝑠 ) 𝑀 0 ) = ( 𝐹 ‘ ( 2 · 𝑠 ) ) ∧ ( ( 2 · 𝑠 ) 𝑀 1 ) = ( 𝐻 ‘ ( 2 · 𝑠 ) ) ) )
99 98 simpld ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑠 ≤ ( 1 / 2 ) ) → ( ( 2 · 𝑠 ) 𝑀 0 ) = ( 𝐹 ‘ ( 2 · 𝑠 ) ) )
100 simpll ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ ¬ 𝑠 ≤ ( 1 / 2 ) ) → 𝜑 )
101 elii2 ⊢ ( ( 𝑠 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑠 ≤ ( 1 / 2 ) ) → 𝑠 ∈ ( ( 1 / 2 ) [,] 1 ) )
102 101 adantll ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ ¬ 𝑠 ≤ ( 1 / 2 ) ) → 𝑠 ∈ ( ( 1 / 2 ) [,] 1 ) )
103 iihalf2 ⊢ ( 𝑠 ∈ ( ( 1 / 2 ) [,] 1 ) → ( ( 2 · 𝑠 ) − 1 ) ∈ ( 0 [,] 1 ) )
104 102 103 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ ¬ 𝑠 ≤ ( 1 / 2 ) ) → ( ( 2 · 𝑠 ) − 1 ) ∈ ( 0 [,] 1 ) )
105 12 15 phtpyhtpy ⊢ ( 𝜑 → ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐾 ) ⊆ ( 𝐺 ( II Htpy 𝐽 ) 𝐾 ) )
106 105 6 sseldd ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐺 ( II Htpy 𝐽 ) 𝐾 ) )
107 37 12 15 106 htpyi ⊢ ( ( 𝜑 ∧ ( ( 2 · 𝑠 ) − 1 ) ∈ ( 0 [,] 1 ) ) → ( ( ( ( 2 · 𝑠 ) − 1 ) 𝑁 0 ) = ( 𝐺 ‘ ( ( 2 · 𝑠 ) − 1 ) ) ∧ ( ( ( 2 · 𝑠 ) − 1 ) 𝑁 1 ) = ( 𝐾 ‘ ( ( 2 · 𝑠 ) − 1 ) ) ) )
108 100 104 107 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ ¬ 𝑠 ≤ ( 1 / 2 ) ) → ( ( ( ( 2 · 𝑠 ) − 1 ) 𝑁 0 ) = ( 𝐺 ‘ ( ( 2 · 𝑠 ) − 1 ) ) ∧ ( ( ( 2 · 𝑠 ) − 1 ) 𝑁 1 ) = ( 𝐾 ‘ ( ( 2 · 𝑠 ) − 1 ) ) ) )
109 108 simpld ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ ¬ 𝑠 ≤ ( 1 / 2 ) ) → ( ( ( 2 · 𝑠 ) − 1 ) 𝑁 0 ) = ( 𝐺 ‘ ( ( 2 · 𝑠 ) − 1 ) ) )
110 99 109 ifeq12da ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → if ( 𝑠 ≤ ( 1 / 2 ) , ( ( 2 · 𝑠 ) 𝑀 0 ) , ( ( ( 2 · 𝑠 ) − 1 ) 𝑁 0 ) ) = if ( 𝑠 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑠 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑠 ) − 1 ) ) ) )
111 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → 𝑠 ∈ ( 0 [,] 1 ) )
112 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
113 simpl ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 0 ) → 𝑥 = 𝑠 )
114 113 breq1d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 0 ) → ( 𝑥 ≤ ( 1 / 2 ) ↔ 𝑠 ≤ ( 1 / 2 ) ) )
115 113 oveq2d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 0 ) → ( 2 · 𝑥 ) = ( 2 · 𝑠 ) )
116 simpr ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 0 ) → 𝑦 = 0 )
117 115 116 oveq12d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 0 ) → ( ( 2 · 𝑥 ) 𝑀 𝑦 ) = ( ( 2 · 𝑠 ) 𝑀 0 ) )
118 115 oveq1d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 0 ) → ( ( 2 · 𝑥 ) − 1 ) = ( ( 2 · 𝑠 ) − 1 ) )
119 118 116 oveq12d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 0 ) → ( ( ( 2 · 𝑥 ) − 1 ) 𝑁 𝑦 ) = ( ( ( 2 · 𝑠 ) − 1 ) 𝑁 0 ) )
120 114 117 119 ifbieq12d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 0 ) → if ( 𝑥 ≤ ( 1 / 2 ) , ( ( 2 · 𝑥 ) 𝑀 𝑦 ) , ( ( ( 2 · 𝑥 ) − 1 ) 𝑁 𝑦 ) ) = if ( 𝑠 ≤ ( 1 / 2 ) , ( ( 2 · 𝑠 ) 𝑀 0 ) , ( ( ( 2 · 𝑠 ) − 1 ) 𝑁 0 ) ) )
121 ovex ⊢ ( ( 2 · 𝑠 ) 𝑀 0 ) ∈ V
122 ovex ⊢ ( ( ( 2 · 𝑠 ) − 1 ) 𝑁 0 ) ∈ V
123 121 122 ifex ⊢ if ( 𝑠 ≤ ( 1 / 2 ) , ( ( 2 · 𝑠 ) 𝑀 0 ) , ( ( ( 2 · 𝑠 ) − 1 ) 𝑁 0 ) ) ∈ V
124 120 4 123 ovmpoa ⊢ ( ( 𝑠 ∈ ( 0 [,] 1 ) ∧ 0 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝑃 0 ) = if ( 𝑠 ≤ ( 1 / 2 ) , ( ( 2 · 𝑠 ) 𝑀 0 ) , ( ( ( 2 · 𝑠 ) − 1 ) 𝑁 0 ) ) )
125 111 112 124 sylancl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝑃 0 ) = if ( 𝑠 ≤ ( 1 / 2 ) , ( ( 2 · 𝑠 ) 𝑀 0 ) , ( ( ( 2 · 𝑠 ) − 1 ) 𝑁 0 ) ) )
126 9 12 pcovalg ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ‘ 𝑠 ) = if ( 𝑠 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑠 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑠 ) − 1 ) ) ) )
127 110 125 126 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝑃 0 ) = ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ‘ 𝑠 ) )
128 98 simprd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑠 ≤ ( 1 / 2 ) ) → ( ( 2 · 𝑠 ) 𝑀 1 ) = ( 𝐻 ‘ ( 2 · 𝑠 ) ) )
129 108 simprd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ ¬ 𝑠 ≤ ( 1 / 2 ) ) → ( ( ( 2 · 𝑠 ) − 1 ) 𝑁 1 ) = ( 𝐾 ‘ ( ( 2 · 𝑠 ) − 1 ) ) )
130 128 129 ifeq12da ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → if ( 𝑠 ≤ ( 1 / 2 ) , ( ( 2 · 𝑠 ) 𝑀 1 ) , ( ( ( 2 · 𝑠 ) − 1 ) 𝑁 1 ) ) = if ( 𝑠 ≤ ( 1 / 2 ) , ( 𝐻 ‘ ( 2 · 𝑠 ) ) , ( 𝐾 ‘ ( ( 2 · 𝑠 ) − 1 ) ) ) )
131 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
132 simpl ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → 𝑥 = 𝑠 )
133 132 breq1d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → ( 𝑥 ≤ ( 1 / 2 ) ↔ 𝑠 ≤ ( 1 / 2 ) ) )
134 132 oveq2d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → ( 2 · 𝑥 ) = ( 2 · 𝑠 ) )
135 simpr ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → 𝑦 = 1 )
136 134 135 oveq12d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → ( ( 2 · 𝑥 ) 𝑀 𝑦 ) = ( ( 2 · 𝑠 ) 𝑀 1 ) )
137 134 oveq1d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → ( ( 2 · 𝑥 ) − 1 ) = ( ( 2 · 𝑠 ) − 1 ) )
138 137 135 oveq12d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → ( ( ( 2 · 𝑥 ) − 1 ) 𝑁 𝑦 ) = ( ( ( 2 · 𝑠 ) − 1 ) 𝑁 1 ) )
139 133 136 138 ifbieq12d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 1 ) → if ( 𝑥 ≤ ( 1 / 2 ) , ( ( 2 · 𝑥 ) 𝑀 𝑦 ) , ( ( ( 2 · 𝑥 ) − 1 ) 𝑁 𝑦 ) ) = if ( 𝑠 ≤ ( 1 / 2 ) , ( ( 2 · 𝑠 ) 𝑀 1 ) , ( ( ( 2 · 𝑠 ) − 1 ) 𝑁 1 ) ) )
140 ovex ⊢ ( ( 2 · 𝑠 ) 𝑀 1 ) ∈ V
141 ovex ⊢ ( ( ( 2 · 𝑠 ) − 1 ) 𝑁 1 ) ∈ V
142 140 141 ifex ⊢ if ( 𝑠 ≤ ( 1 / 2 ) , ( ( 2 · 𝑠 ) 𝑀 1 ) , ( ( ( 2 · 𝑠 ) − 1 ) 𝑁 1 ) ) ∈ V
143 139 4 142 ovmpoa ⊢ ( ( 𝑠 ∈ ( 0 [,] 1 ) ∧ 1 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝑃 1 ) = if ( 𝑠 ≤ ( 1 / 2 ) , ( ( 2 · 𝑠 ) 𝑀 1 ) , ( ( ( 2 · 𝑠 ) − 1 ) 𝑁 1 ) ) )
144 111 131 143 sylancl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝑃 1 ) = if ( 𝑠 ≤ ( 1 / 2 ) , ( ( 2 · 𝑠 ) 𝑀 1 ) , ( ( ( 2 · 𝑠 ) − 1 ) 𝑁 1 ) ) )
145 14 15 pcovalg ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐾 ) ‘ 𝑠 ) = if ( 𝑠 ≤ ( 1 / 2 ) , ( 𝐻 ‘ ( 2 · 𝑠 ) ) , ( 𝐾 ‘ ( ( 2 · 𝑠 ) − 1 ) ) ) )
146 130 144 145 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝑃 1 ) = ( ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐾 ) ‘ 𝑠 ) )
147 9 14 5 phtpyi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 0 𝑀 𝑠 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 𝑀 𝑠 ) = ( 𝐹 ‘ 1 ) ) )
148 147 simpld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 𝑀 𝑠 ) = ( 𝐹 ‘ 0 ) )
149 simpl ⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 𝑠 ) → 𝑥 = 0 )
150 149 29 eqbrtrdi ⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 𝑠 ) → 𝑥 ≤ ( 1 / 2 ) )
151 150 iftrued ⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 𝑠 ) → if ( 𝑥 ≤ ( 1 / 2 ) , ( ( 2 · 𝑥 ) 𝑀 𝑦 ) , ( ( ( 2 · 𝑥 ) − 1 ) 𝑁 𝑦 ) ) = ( ( 2 · 𝑥 ) 𝑀 𝑦 ) )
152 149 oveq2d ⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 𝑠 ) → ( 2 · 𝑥 ) = ( 2 · 0 ) )
153 2t0e0 ⊢ ( 2 · 0 ) = 0
154 152 153 eqtrdi ⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 𝑠 ) → ( 2 · 𝑥 ) = 0 )
155 simpr ⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 𝑠 ) → 𝑦 = 𝑠 )
156 154 155 oveq12d ⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 𝑠 ) → ( ( 2 · 𝑥 ) 𝑀 𝑦 ) = ( 0 𝑀 𝑠 ) )
157 151 156 eqtrd ⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 𝑠 ) → if ( 𝑥 ≤ ( 1 / 2 ) , ( ( 2 · 𝑥 ) 𝑀 𝑦 ) , ( ( ( 2 · 𝑥 ) − 1 ) 𝑁 𝑦 ) ) = ( 0 𝑀 𝑠 ) )
158 ovex ⊢ ( 0 𝑀 𝑠 ) ∈ V
159 157 4 158 ovmpoa ⊢ ( ( 0 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 𝑃 𝑠 ) = ( 0 𝑀 𝑠 ) )
160 112 111 159 sylancr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 𝑃 𝑠 ) = ( 0 𝑀 𝑠 ) )
161 9 12 pco0 ⊢ ( 𝜑 → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ‘ 0 ) = ( 𝐹 ‘ 0 ) )
162 161 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ‘ 0 ) = ( 𝐹 ‘ 0 ) )
163 148 160 162 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 𝑃 𝑠 ) = ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ‘ 0 ) )
164 12 15 6 phtpyi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 0 𝑁 𝑠 ) = ( 𝐺 ‘ 0 ) ∧ ( 1 𝑁 𝑠 ) = ( 𝐺 ‘ 1 ) ) )
165 164 simprd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 𝑁 𝑠 ) = ( 𝐺 ‘ 1 ) )
166 28 30 ltnlei ⊢ ( ( 1 / 2 ) < 1 ↔ ¬ 1 ≤ ( 1 / 2 ) )
167 31 166 mpbi ⊢ ¬ 1 ≤ ( 1 / 2 )
168 simpl ⊢ ( ( 𝑥 = 1 ∧ 𝑦 = 𝑠 ) → 𝑥 = 1 )
169 168 breq1d ⊢ ( ( 𝑥 = 1 ∧ 𝑦 = 𝑠 ) → ( 𝑥 ≤ ( 1 / 2 ) ↔ 1 ≤ ( 1 / 2 ) ) )
170 167 169 mtbiri ⊢ ( ( 𝑥 = 1 ∧ 𝑦 = 𝑠 ) → ¬ 𝑥 ≤ ( 1 / 2 ) )
171 170 iffalsed ⊢ ( ( 𝑥 = 1 ∧ 𝑦 = 𝑠 ) → if ( 𝑥 ≤ ( 1 / 2 ) , ( ( 2 · 𝑥 ) 𝑀 𝑦 ) , ( ( ( 2 · 𝑥 ) − 1 ) 𝑁 𝑦 ) ) = ( ( ( 2 · 𝑥 ) − 1 ) 𝑁 𝑦 ) )
172 168 oveq2d ⊢ ( ( 𝑥 = 1 ∧ 𝑦 = 𝑠 ) → ( 2 · 𝑥 ) = ( 2 · 1 ) )
173 2t1e2 ⊢ ( 2 · 1 ) = 2
174 172 173 eqtrdi ⊢ ( ( 𝑥 = 1 ∧ 𝑦 = 𝑠 ) → ( 2 · 𝑥 ) = 2 )
175 174 oveq1d ⊢ ( ( 𝑥 = 1 ∧ 𝑦 = 𝑠 ) → ( ( 2 · 𝑥 ) − 1 ) = ( 2 − 1 ) )
176 2m1e1 ⊢ ( 2 − 1 ) = 1
177 175 176 eqtrdi ⊢ ( ( 𝑥 = 1 ∧ 𝑦 = 𝑠 ) → ( ( 2 · 𝑥 ) − 1 ) = 1 )
178 simpr ⊢ ( ( 𝑥 = 1 ∧ 𝑦 = 𝑠 ) → 𝑦 = 𝑠 )
179 177 178 oveq12d ⊢ ( ( 𝑥 = 1 ∧ 𝑦 = 𝑠 ) → ( ( ( 2 · 𝑥 ) − 1 ) 𝑁 𝑦 ) = ( 1 𝑁 𝑠 ) )
180 171 179 eqtrd ⊢ ( ( 𝑥 = 1 ∧ 𝑦 = 𝑠 ) → if ( 𝑥 ≤ ( 1 / 2 ) , ( ( 2 · 𝑥 ) 𝑀 𝑦 ) , ( ( ( 2 · 𝑥 ) − 1 ) 𝑁 𝑦 ) ) = ( 1 𝑁 𝑠 ) )
181 ovex ⊢ ( 1 𝑁 𝑠 ) ∈ V
182 180 4 181 ovmpoa ⊢ ( ( 1 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 𝑃 𝑠 ) = ( 1 𝑁 𝑠 ) )
183 131 111 182 sylancr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 𝑃 𝑠 ) = ( 1 𝑁 𝑠 ) )
184 9 12 pco1 ⊢ ( 𝜑 → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ‘ 1 ) = ( 𝐺 ‘ 1 ) )
185 184 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ‘ 1 ) = ( 𝐺 ‘ 1 ) )
186 165 183 185 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 𝑃 𝑠 ) = ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ‘ 1 ) )
187 13 21 89 127 146 163 186 isphtpy2d ⊢ ( 𝜑 → 𝑃 ∈ ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ( PHtpy ‘ 𝐽 ) ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐾 ) ) )