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