Metamath Proof Explorer


Theorem pcoass

Description: Order of concatenation does not affect homotopy class. (Contributed by Jeff Madsen, 19-Jun-2010) (Proof shortened by Mario Carneiro, 8-Jun-2014)

Ref Expression
Hypotheses pcoass.2 ( 𝜑𝐹 ∈ ( II Cn 𝐽 ) )
pcoass.3 ( 𝜑𝐺 ∈ ( II Cn 𝐽 ) )
pcoass.4 ( 𝜑𝐻 ∈ ( II Cn 𝐽 ) )
pcoass.5 ( 𝜑 → ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 0 ) )
pcoass.6 ( 𝜑 → ( 𝐺 ‘ 1 ) = ( 𝐻 ‘ 0 ) )
pcoass.7 𝑃 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) , ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) )
Assertion pcoass ( 𝜑 → ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ( *𝑝𝐽 ) 𝐻 ) ( ≃ph𝐽 ) ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) )

Proof

Step Hyp Ref Expression
1 pcoass.2 ( 𝜑𝐹 ∈ ( II Cn 𝐽 ) )
2 pcoass.3 ( 𝜑𝐺 ∈ ( II Cn 𝐽 ) )
3 pcoass.4 ( 𝜑𝐻 ∈ ( II Cn 𝐽 ) )
4 pcoass.5 ( 𝜑 → ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 0 ) )
5 pcoass.6 ( 𝜑 → ( 𝐺 ‘ 1 ) = ( 𝐻 ‘ 0 ) )
6 pcoass.7 𝑃 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) , ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) )
7 iftrue ( 𝑥 ≤ ( 1 / 4 ) → if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) = ( 2 · 𝑥 ) )
8 7 fveq2d ( 𝑥 ≤ ( 1 / 4 ) → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) ) = ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ ( 2 · 𝑥 ) ) )
9 8 adantl ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 4 ) ) → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) ) = ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ ( 2 · 𝑥 ) ) )
10 2cn 2 ∈ ℂ
11 elicc01 ( 𝑥 ∈ ( 0 [,] 1 ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥𝑥 ≤ 1 ) )
12 11 simp1bi ( 𝑥 ∈ ( 0 [,] 1 ) → 𝑥 ∈ ℝ )
13 12 adantr ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑥 ≤ ( 1 / 4 ) ) → 𝑥 ∈ ℝ )
14 13 recnd ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑥 ≤ ( 1 / 4 ) ) → 𝑥 ∈ ℂ )
15 mulcom ( ( 2 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 2 · 𝑥 ) = ( 𝑥 · 2 ) )
16 10 14 15 sylancr ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑥 ≤ ( 1 / 4 ) ) → ( 2 · 𝑥 ) = ( 𝑥 · 2 ) )
17 11 simp2bi ( 𝑥 ∈ ( 0 [,] 1 ) → 0 ≤ 𝑥 )
18 17 adantr ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑥 ≤ ( 1 / 4 ) ) → 0 ≤ 𝑥 )
19 simpr ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑥 ≤ ( 1 / 4 ) ) → 𝑥 ≤ ( 1 / 4 ) )
20 0re 0 ∈ ℝ
21 4nn 4 ∈ ℕ
22 nnrecre ( 4 ∈ ℕ → ( 1 / 4 ) ∈ ℝ )
23 21 22 ax-mp ( 1 / 4 ) ∈ ℝ
24 20 23 elicc2i ( 𝑥 ∈ ( 0 [,] ( 1 / 4 ) ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥𝑥 ≤ ( 1 / 4 ) ) )
25 13 18 19 24 syl3anbrc ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑥 ≤ ( 1 / 4 ) ) → 𝑥 ∈ ( 0 [,] ( 1 / 4 ) ) )
26 2rp 2 ∈ ℝ+
27 10 mul02i ( 0 · 2 ) = 0
28 23 recni ( 1 / 4 ) ∈ ℂ
29 28 2timesi ( 2 · ( 1 / 4 ) ) = ( ( 1 / 4 ) + ( 1 / 4 ) )
30 2ne0 2 ≠ 0
31 recdiv2 ( ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 1 / 2 ) / 2 ) = ( 1 / ( 2 · 2 ) ) )
32 10 30 10 30 31 mp4an ( ( 1 / 2 ) / 2 ) = ( 1 / ( 2 · 2 ) )
33 2t2e4 ( 2 · 2 ) = 4
34 33 oveq2i ( 1 / ( 2 · 2 ) ) = ( 1 / 4 )
35 32 34 eqtri ( ( 1 / 2 ) / 2 ) = ( 1 / 4 )
36 35 35 oveq12i ( ( ( 1 / 2 ) / 2 ) + ( ( 1 / 2 ) / 2 ) ) = ( ( 1 / 4 ) + ( 1 / 4 ) )
37 halfcn ( 1 / 2 ) ∈ ℂ
38 2halves ( ( 1 / 2 ) ∈ ℂ → ( ( ( 1 / 2 ) / 2 ) + ( ( 1 / 2 ) / 2 ) ) = ( 1 / 2 ) )
39 37 38 ax-mp ( ( ( 1 / 2 ) / 2 ) + ( ( 1 / 2 ) / 2 ) ) = ( 1 / 2 )
40 36 39 eqtr3i ( ( 1 / 4 ) + ( 1 / 4 ) ) = ( 1 / 2 )
41 29 40 eqtri ( 2 · ( 1 / 4 ) ) = ( 1 / 2 )
42 10 28 41 mulcomli ( ( 1 / 4 ) · 2 ) = ( 1 / 2 )
43 20 23 26 27 42 iccdili ( 𝑥 ∈ ( 0 [,] ( 1 / 4 ) ) → ( 𝑥 · 2 ) ∈ ( 0 [,] ( 1 / 2 ) ) )
44 25 43 syl ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑥 ≤ ( 1 / 4 ) ) → ( 𝑥 · 2 ) ∈ ( 0 [,] ( 1 / 2 ) ) )
45 16 44 eqeltrd ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑥 ≤ ( 1 / 4 ) ) → ( 2 · 𝑥 ) ∈ ( 0 [,] ( 1 / 2 ) ) )
46 2 3 5 pcocn ( 𝜑 → ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ∈ ( II Cn 𝐽 ) )
47 1 46 pcoval1 ( ( 𝜑 ∧ ( 2 · 𝑥 ) ∈ ( 0 [,] ( 1 / 2 ) ) ) → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ ( 2 · 𝑥 ) ) = ( 𝐹 ‘ ( 2 · ( 2 · 𝑥 ) ) ) )
48 1 2 pcoval1 ( ( 𝜑 ∧ ( 2 · 𝑥 ) ∈ ( 0 [,] ( 1 / 2 ) ) ) → ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ ( 2 · 𝑥 ) ) = ( 𝐹 ‘ ( 2 · ( 2 · 𝑥 ) ) ) )
49 47 48 eqtr4d ( ( 𝜑 ∧ ( 2 · 𝑥 ) ∈ ( 0 [,] ( 1 / 2 ) ) ) → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ ( 2 · 𝑥 ) ) = ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ ( 2 · 𝑥 ) ) )
50 45 49 sylan2 ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑥 ≤ ( 1 / 4 ) ) ) → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ ( 2 · 𝑥 ) ) = ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ ( 2 · 𝑥 ) ) )
51 50 anassrs ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 4 ) ) → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ ( 2 · 𝑥 ) ) = ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ ( 2 · 𝑥 ) ) )
52 9 51 eqtrd ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 4 ) ) → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) ) = ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ ( 2 · 𝑥 ) ) )
53 52 adantlr ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ 𝑥 ≤ ( 1 / 4 ) ) → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) ) = ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ ( 2 · 𝑥 ) ) )
54 simplll ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → 𝜑 )
55 12 ad2antlr ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) → 𝑥 ∈ ℝ )
56 55 adantr ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → 𝑥 ∈ ℝ )
57 letric ( ( 𝑥 ∈ ℝ ∧ ( 1 / 4 ) ∈ ℝ ) → ( 𝑥 ≤ ( 1 / 4 ) ∨ ( 1 / 4 ) ≤ 𝑥 ) )
58 55 23 57 sylancl ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) → ( 𝑥 ≤ ( 1 / 4 ) ∨ ( 1 / 4 ) ≤ 𝑥 ) )
59 58 orcanai ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → ( 1 / 4 ) ≤ 𝑥 )
60 simplr ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → 𝑥 ≤ ( 1 / 2 ) )
61 halfre ( 1 / 2 ) ∈ ℝ
62 23 61 elicc2i ( 𝑥 ∈ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 1 / 4 ) ≤ 𝑥𝑥 ≤ ( 1 / 2 ) ) )
63 56 59 60 62 syl3anbrc ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → 𝑥 ∈ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) )
64 62 simp1bi ( 𝑥 ∈ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) → 𝑥 ∈ ℝ )
65 readdcl ( ( 𝑥 ∈ ℝ ∧ ( 1 / 4 ) ∈ ℝ ) → ( 𝑥 + ( 1 / 4 ) ) ∈ ℝ )
66 64 23 65 sylancl ( 𝑥 ∈ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) → ( 𝑥 + ( 1 / 4 ) ) ∈ ℝ )
67 23 a1i ( 𝑥 ∈ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) → ( 1 / 4 ) ∈ ℝ )
68 62 simp2bi ( 𝑥 ∈ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) → ( 1 / 4 ) ≤ 𝑥 )
69 67 64 67 68 leadd1dd ( 𝑥 ∈ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) → ( ( 1 / 4 ) + ( 1 / 4 ) ) ≤ ( 𝑥 + ( 1 / 4 ) ) )
70 40 69 eqbrtrrid ( 𝑥 ∈ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) → ( 1 / 2 ) ≤ ( 𝑥 + ( 1 / 4 ) ) )
71 61 a1i ( 𝑥 ∈ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) → ( 1 / 2 ) ∈ ℝ )
72 62 simp3bi ( 𝑥 ∈ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) → 𝑥 ≤ ( 1 / 2 ) )
73 2lt4 2 < 4
74 2re 2 ∈ ℝ
75 4re 4 ∈ ℝ
76 2pos 0 < 2
77 4pos 0 < 4
78 74 75 76 77 ltrecii ( 2 < 4 ↔ ( 1 / 4 ) < ( 1 / 2 ) )
79 73 78 mpbi ( 1 / 4 ) < ( 1 / 2 )
80 23 61 79 ltleii ( 1 / 4 ) ≤ ( 1 / 2 )
81 80 a1i ( 𝑥 ∈ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) → ( 1 / 4 ) ≤ ( 1 / 2 ) )
82 64 67 71 71 72 81 le2addd ( 𝑥 ∈ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) → ( 𝑥 + ( 1 / 4 ) ) ≤ ( ( 1 / 2 ) + ( 1 / 2 ) ) )
83 ax-1cn 1 ∈ ℂ
84 2halves ( 1 ∈ ℂ → ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1 )
85 83 84 ax-mp ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1
86 82 85 breqtrdi ( 𝑥 ∈ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) → ( 𝑥 + ( 1 / 4 ) ) ≤ 1 )
87 1re 1 ∈ ℝ
88 61 87 elicc2i ( ( 𝑥 + ( 1 / 4 ) ) ∈ ( ( 1 / 2 ) [,] 1 ) ↔ ( ( 𝑥 + ( 1 / 4 ) ) ∈ ℝ ∧ ( 1 / 2 ) ≤ ( 𝑥 + ( 1 / 4 ) ) ∧ ( 𝑥 + ( 1 / 4 ) ) ≤ 1 ) )
89 66 70 86 88 syl3anbrc ( 𝑥 ∈ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) → ( 𝑥 + ( 1 / 4 ) ) ∈ ( ( 1 / 2 ) [,] 1 ) )
90 63 89 syl ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → ( 𝑥 + ( 1 / 4 ) ) ∈ ( ( 1 / 2 ) [,] 1 ) )
91 2 3 pco0 ( 𝜑 → ( ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ‘ 0 ) = ( 𝐺 ‘ 0 ) )
92 4 91 eqtr4d ( 𝜑 → ( 𝐹 ‘ 1 ) = ( ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ‘ 0 ) )
93 1 46 92 pcoval2 ( ( 𝜑 ∧ ( 𝑥 + ( 1 / 4 ) ) ∈ ( ( 1 / 2 ) [,] 1 ) ) → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ ( 𝑥 + ( 1 / 4 ) ) ) = ( ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ‘ ( ( 2 · ( 𝑥 + ( 1 / 4 ) ) ) − 1 ) ) )
94 54 90 93 syl2anc ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ ( 𝑥 + ( 1 / 4 ) ) ) = ( ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ‘ ( ( 2 · ( 𝑥 + ( 1 / 4 ) ) ) − 1 ) ) )
95 85 oveq2i ( ( 2 · ( 𝑥 + ( 1 / 4 ) ) ) − ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( ( 2 · ( 𝑥 + ( 1 / 4 ) ) ) − 1 )
96 2cnd ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → 2 ∈ ℂ )
97 56 recnd ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → 𝑥 ∈ ℂ )
98 28 a1i ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → ( 1 / 4 ) ∈ ℂ )
99 96 97 98 adddid ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → ( 2 · ( 𝑥 + ( 1 / 4 ) ) ) = ( ( 2 · 𝑥 ) + ( 2 · ( 1 / 4 ) ) ) )
100 41 oveq2i ( ( 2 · 𝑥 ) + ( 2 · ( 1 / 4 ) ) ) = ( ( 2 · 𝑥 ) + ( 1 / 2 ) )
101 99 100 eqtrdi ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → ( 2 · ( 𝑥 + ( 1 / 4 ) ) ) = ( ( 2 · 𝑥 ) + ( 1 / 2 ) ) )
102 101 oveq1d ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → ( ( 2 · ( 𝑥 + ( 1 / 4 ) ) ) − ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( ( ( 2 · 𝑥 ) + ( 1 / 2 ) ) − ( ( 1 / 2 ) + ( 1 / 2 ) ) ) )
103 95 102 eqtr3id ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → ( ( 2 · ( 𝑥 + ( 1 / 4 ) ) ) − 1 ) = ( ( ( 2 · 𝑥 ) + ( 1 / 2 ) ) − ( ( 1 / 2 ) + ( 1 / 2 ) ) ) )
104 remulcl ( ( 2 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 2 · 𝑥 ) ∈ ℝ )
105 74 56 104 sylancr ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → ( 2 · 𝑥 ) ∈ ℝ )
106 105 recnd ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → ( 2 · 𝑥 ) ∈ ℂ )
107 37 a1i ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → ( 1 / 2 ) ∈ ℂ )
108 106 107 107 pnpcan2d ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → ( ( ( 2 · 𝑥 ) + ( 1 / 2 ) ) − ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( ( 2 · 𝑥 ) − ( 1 / 2 ) ) )
109 103 108 eqtrd ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → ( ( 2 · ( 𝑥 + ( 1 / 4 ) ) ) − 1 ) = ( ( 2 · 𝑥 ) − ( 1 / 2 ) ) )
110 109 fveq2d ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → ( ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ‘ ( ( 2 · ( 𝑥 + ( 1 / 4 ) ) ) − 1 ) ) = ( ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ‘ ( ( 2 · 𝑥 ) − ( 1 / 2 ) ) ) )
111 10 97 15 sylancr ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → ( 2 · 𝑥 ) = ( 𝑥 · 2 ) )
112 83 10 30 divcan1i ( ( 1 / 2 ) · 2 ) = 1
113 23 61 26 42 112 iccdili ( 𝑥 ∈ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) → ( 𝑥 · 2 ) ∈ ( ( 1 / 2 ) [,] 1 ) )
114 63 113 syl ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → ( 𝑥 · 2 ) ∈ ( ( 1 / 2 ) [,] 1 ) )
115 111 114 eqeltrd ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → ( 2 · 𝑥 ) ∈ ( ( 1 / 2 ) [,] 1 ) )
116 37 subidi ( ( 1 / 2 ) − ( 1 / 2 ) ) = 0
117 1mhlfehlf ( 1 − ( 1 / 2 ) ) = ( 1 / 2 )
118 61 87 61 116 117 iccshftli ( ( 2 · 𝑥 ) ∈ ( ( 1 / 2 ) [,] 1 ) → ( ( 2 · 𝑥 ) − ( 1 / 2 ) ) ∈ ( 0 [,] ( 1 / 2 ) ) )
119 115 118 syl ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → ( ( 2 · 𝑥 ) − ( 1 / 2 ) ) ∈ ( 0 [,] ( 1 / 2 ) ) )
120 2 3 pcoval1 ( ( 𝜑 ∧ ( ( 2 · 𝑥 ) − ( 1 / 2 ) ) ∈ ( 0 [,] ( 1 / 2 ) ) ) → ( ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ‘ ( ( 2 · 𝑥 ) − ( 1 / 2 ) ) ) = ( 𝐺 ‘ ( 2 · ( ( 2 · 𝑥 ) − ( 1 / 2 ) ) ) ) )
121 54 119 120 syl2anc ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → ( ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ‘ ( ( 2 · 𝑥 ) − ( 1 / 2 ) ) ) = ( 𝐺 ‘ ( 2 · ( ( 2 · 𝑥 ) − ( 1 / 2 ) ) ) ) )
122 96 106 107 subdid ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → ( 2 · ( ( 2 · 𝑥 ) − ( 1 / 2 ) ) ) = ( ( 2 · ( 2 · 𝑥 ) ) − ( 2 · ( 1 / 2 ) ) ) )
123 10 30 recidi ( 2 · ( 1 / 2 ) ) = 1
124 123 oveq2i ( ( 2 · ( 2 · 𝑥 ) ) − ( 2 · ( 1 / 2 ) ) ) = ( ( 2 · ( 2 · 𝑥 ) ) − 1 )
125 122 124 eqtrdi ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → ( 2 · ( ( 2 · 𝑥 ) − ( 1 / 2 ) ) ) = ( ( 2 · ( 2 · 𝑥 ) ) − 1 ) )
126 125 fveq2d ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → ( 𝐺 ‘ ( 2 · ( ( 2 · 𝑥 ) − ( 1 / 2 ) ) ) ) = ( 𝐺 ‘ ( ( 2 · ( 2 · 𝑥 ) ) − 1 ) ) )
127 121 126 eqtrd ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → ( ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ‘ ( ( 2 · 𝑥 ) − ( 1 / 2 ) ) ) = ( 𝐺 ‘ ( ( 2 · ( 2 · 𝑥 ) ) − 1 ) ) )
128 94 110 127 3eqtrd ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ ( 𝑥 + ( 1 / 4 ) ) ) = ( 𝐺 ‘ ( ( 2 · ( 2 · 𝑥 ) ) − 1 ) ) )
129 iffalse ( ¬ 𝑥 ≤ ( 1 / 4 ) → if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) = ( 𝑥 + ( 1 / 4 ) ) )
130 129 fveq2d ( ¬ 𝑥 ≤ ( 1 / 4 ) → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) ) = ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ ( 𝑥 + ( 1 / 4 ) ) ) )
131 130 adantl ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) ) = ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ ( 𝑥 + ( 1 / 4 ) ) ) )
132 1 2 4 pcoval2 ( ( 𝜑 ∧ ( 2 · 𝑥 ) ∈ ( ( 1 / 2 ) [,] 1 ) ) → ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ ( 2 · 𝑥 ) ) = ( 𝐺 ‘ ( ( 2 · ( 2 · 𝑥 ) ) − 1 ) ) )
133 54 115 132 syl2anc ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ ( 2 · 𝑥 ) ) = ( 𝐺 ‘ ( ( 2 · ( 2 · 𝑥 ) ) − 1 ) ) )
134 128 131 133 3eqtr4d ( ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 4 ) ) → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) ) = ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ ( 2 · 𝑥 ) ) )
135 53 134 pm2.61dan ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) ) = ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ ( 2 · 𝑥 ) ) )
136 iftrue ( 𝑥 ≤ ( 1 / 2 ) → if ( 𝑥 ≤ ( 1 / 2 ) , if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) , ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) = if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) )
137 136 fveq2d ( 𝑥 ≤ ( 1 / 2 ) → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ if ( 𝑥 ≤ ( 1 / 2 ) , if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) , ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) ) = ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) ) )
138 137 adantl ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ if ( 𝑥 ≤ ( 1 / 2 ) , if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) , ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) ) = ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) ) )
139 iftrue ( 𝑥 ≤ ( 1 / 2 ) → if ( 𝑥 ≤ ( 1 / 2 ) , ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ ( 2 · 𝑥 ) ) , ( 𝐻 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) = ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ ( 2 · 𝑥 ) ) )
140 139 adantl ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) → if ( 𝑥 ≤ ( 1 / 2 ) , ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ ( 2 · 𝑥 ) ) , ( 𝐻 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) = ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ ( 2 · 𝑥 ) ) )
141 135 138 140 3eqtr4d ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ if ( 𝑥 ≤ ( 1 / 2 ) , if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) , ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) ) = if ( 𝑥 ≤ ( 1 / 2 ) , ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ ( 2 · 𝑥 ) ) , ( 𝐻 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) )
142 elii2 ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑥 ≤ ( 1 / 2 ) ) → 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) )
143 halfge0 0 ≤ ( 1 / 2 )
144 halflt1 ( 1 / 2 ) < 1
145 61 87 144 ltleii ( 1 / 2 ) ≤ 1
146 elicc01 ( ( 1 / 2 ) ∈ ( 0 [,] 1 ) ↔ ( ( 1 / 2 ) ∈ ℝ ∧ 0 ≤ ( 1 / 2 ) ∧ ( 1 / 2 ) ≤ 1 ) )
147 61 143 145 146 mpbir3an ( 1 / 2 ) ∈ ( 0 [,] 1 )
148 1elunit 1 ∈ ( 0 [,] 1 )
149 iccss2 ( ( ( 1 / 2 ) ∈ ( 0 [,] 1 ) ∧ 1 ∈ ( 0 [,] 1 ) ) → ( ( 1 / 2 ) [,] 1 ) ⊆ ( 0 [,] 1 ) )
150 147 148 149 mp2an ( ( 1 / 2 ) [,] 1 ) ⊆ ( 0 [,] 1 )
151 150 sseli ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) → 𝑥 ∈ ( 0 [,] 1 ) )
152 10 30 div0i ( 0 / 2 ) = 0
153 eqid ( 1 / 2 ) = ( 1 / 2 )
154 20 87 26 152 153 icccntri ( 𝑥 ∈ ( 0 [,] 1 ) → ( 𝑥 / 2 ) ∈ ( 0 [,] ( 1 / 2 ) ) )
155 37 addid2i ( 0 + ( 1 / 2 ) ) = ( 1 / 2 )
156 20 61 61 155 85 iccshftri ( ( 𝑥 / 2 ) ∈ ( 0 [,] ( 1 / 2 ) ) → ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ∈ ( ( 1 / 2 ) [,] 1 ) )
157 151 154 156 3syl ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) → ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ∈ ( ( 1 / 2 ) [,] 1 ) )
158 1 46 92 pcoval2 ( ( 𝜑 ∧ ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ∈ ( ( 1 / 2 ) [,] 1 ) ) → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) = ( ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ‘ ( ( 2 · ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) − 1 ) ) )
159 157 158 sylan2 ( ( 𝜑𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) ) → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) = ( ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ‘ ( ( 2 · ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) − 1 ) ) )
160 61 87 elicc2i ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) ↔ ( 𝑥 ∈ ℝ ∧ ( 1 / 2 ) ≤ 𝑥𝑥 ≤ 1 ) )
161 160 simp1bi ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) → 𝑥 ∈ ℝ )
162 161 recnd ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) → 𝑥 ∈ ℂ )
163 1cnd ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) → 1 ∈ ℂ )
164 2cnd ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) → 2 ∈ ℂ )
165 30 a1i ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) → 2 ≠ 0 )
166 162 163 164 165 divdird ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) → ( ( 𝑥 + 1 ) / 2 ) = ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) )
167 166 oveq2d ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) → ( 2 · ( ( 𝑥 + 1 ) / 2 ) ) = ( 2 · ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) )
168 peano2cn ( 𝑥 ∈ ℂ → ( 𝑥 + 1 ) ∈ ℂ )
169 162 168 syl ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) → ( 𝑥 + 1 ) ∈ ℂ )
170 169 164 165 divcan2d ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) → ( 2 · ( ( 𝑥 + 1 ) / 2 ) ) = ( 𝑥 + 1 ) )
171 167 170 eqtr3d ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) → ( 2 · ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) = ( 𝑥 + 1 ) )
172 162 163 171 mvrraddd ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) → ( ( 2 · ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) − 1 ) = 𝑥 )
173 172 fveq2d ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) → ( ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ‘ ( ( 2 · ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) − 1 ) ) = ( ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ‘ 𝑥 ) )
174 173 adantl ( ( 𝜑𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) ) → ( ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ‘ ( ( 2 · ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) − 1 ) ) = ( ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ‘ 𝑥 ) )
175 2 3 5 pcoval2 ( ( 𝜑𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) ) → ( ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ‘ 𝑥 ) = ( 𝐻 ‘ ( ( 2 · 𝑥 ) − 1 ) ) )
176 159 174 175 3eqtrd ( ( 𝜑𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) ) → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) = ( 𝐻 ‘ ( ( 2 · 𝑥 ) − 1 ) ) )
177 142 176 sylan2 ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑥 ≤ ( 1 / 2 ) ) ) → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) = ( 𝐻 ‘ ( ( 2 · 𝑥 ) − 1 ) ) )
178 177 anassrs ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 2 ) ) → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) = ( 𝐻 ‘ ( ( 2 · 𝑥 ) − 1 ) ) )
179 iffalse ( ¬ 𝑥 ≤ ( 1 / 2 ) → if ( 𝑥 ≤ ( 1 / 2 ) , if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) , ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) = ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) )
180 179 fveq2d ( ¬ 𝑥 ≤ ( 1 / 2 ) → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ if ( 𝑥 ≤ ( 1 / 2 ) , if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) , ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) ) = ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) )
181 180 adantl ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 2 ) ) → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ if ( 𝑥 ≤ ( 1 / 2 ) , if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) , ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) ) = ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) )
182 iffalse ( ¬ 𝑥 ≤ ( 1 / 2 ) → if ( 𝑥 ≤ ( 1 / 2 ) , ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ ( 2 · 𝑥 ) ) , ( 𝐻 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) = ( 𝐻 ‘ ( ( 2 · 𝑥 ) − 1 ) ) )
183 182 adantl ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 2 ) ) → if ( 𝑥 ≤ ( 1 / 2 ) , ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ ( 2 · 𝑥 ) ) , ( 𝐻 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) = ( 𝐻 ‘ ( ( 2 · 𝑥 ) − 1 ) ) )
184 178 181 183 3eqtr4d ( ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 2 ) ) → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ if ( 𝑥 ≤ ( 1 / 2 ) , if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) , ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) ) = if ( 𝑥 ≤ ( 1 / 2 ) , ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ ( 2 · 𝑥 ) ) , ( 𝐻 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) )
185 141 184 pm2.61dan ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ if ( 𝑥 ≤ ( 1 / 2 ) , if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) , ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) ) = if ( 𝑥 ≤ ( 1 / 2 ) , ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ ( 2 · 𝑥 ) ) , ( 𝐻 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) )
186 185 mpteq2dva ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ if ( 𝑥 ≤ ( 1 / 2 ) , if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) , ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ ( 2 · 𝑥 ) ) , ( 𝐻 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) )
187 iitopon II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
188 187 a1i ( 𝜑 → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
189 188 cnmptid ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ 𝑥 ) ∈ ( II Cn II ) )
190 0elunit 0 ∈ ( 0 [,] 1 )
191 190 a1i ( 𝜑 → 0 ∈ ( 0 [,] 1 ) )
192 188 188 191 cnmptc ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ 0 ) ∈ ( II Cn II ) )
193 eqid ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
194 eqid ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) )
195 eqid ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) )
196 dfii2 II = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) )
197 0red ( 𝜑 → 0 ∈ ℝ )
198 1red ( 𝜑 → 1 ∈ ℝ )
199 147 a1i ( 𝜑 → ( 1 / 2 ) ∈ ( 0 [,] 1 ) )
200 simprl ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → 𝑦 = ( 1 / 2 ) )
201 200 oveq1d ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → ( 𝑦 + ( 1 / 4 ) ) = ( ( 1 / 2 ) + ( 1 / 4 ) ) )
202 37 28 addcomi ( ( 1 / 2 ) + ( 1 / 4 ) ) = ( ( 1 / 4 ) + ( 1 / 2 ) )
203 201 202 eqtrdi ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → ( 𝑦 + ( 1 / 4 ) ) = ( ( 1 / 4 ) + ( 1 / 2 ) ) )
204 23 61 ltnlei ( ( 1 / 4 ) < ( 1 / 2 ) ↔ ¬ ( 1 / 2 ) ≤ ( 1 / 4 ) )
205 79 204 mpbi ¬ ( 1 / 2 ) ≤ ( 1 / 4 )
206 200 breq1d ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → ( 𝑦 ≤ ( 1 / 4 ) ↔ ( 1 / 2 ) ≤ ( 1 / 4 ) ) )
207 205 206 mtbiri ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → ¬ 𝑦 ≤ ( 1 / 4 ) )
208 207 iffalsed ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → if ( 𝑦 ≤ ( 1 / 4 ) , ( 2 · 𝑦 ) , ( 𝑦 + ( 1 / 4 ) ) ) = ( 𝑦 + ( 1 / 4 ) ) )
209 200 oveq1d ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → ( 𝑦 / 2 ) = ( ( 1 / 2 ) / 2 ) )
210 209 35 eqtrdi ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → ( 𝑦 / 2 ) = ( 1 / 4 ) )
211 210 oveq1d ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑦 / 2 ) + ( 1 / 2 ) ) = ( ( 1 / 4 ) + ( 1 / 2 ) ) )
212 203 208 211 3eqtr4d ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 2 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → if ( 𝑦 ≤ ( 1 / 4 ) , ( 2 · 𝑦 ) , ( 𝑦 + ( 1 / 4 ) ) ) = ( ( 𝑦 / 2 ) + ( 1 / 2 ) ) )
213 eqid ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) )
214 eqid ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) = ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 4 ) [,] ( 1 / 2 ) ) )
215 61 a1i ( 𝜑 → ( 1 / 2 ) ∈ ℝ )
216 75 77 recgt0ii 0 < ( 1 / 4 )
217 20 23 216 ltleii 0 ≤ ( 1 / 4 )
218 20 61 elicc2i ( ( 1 / 4 ) ∈ ( 0 [,] ( 1 / 2 ) ) ↔ ( ( 1 / 4 ) ∈ ℝ ∧ 0 ≤ ( 1 / 4 ) ∧ ( 1 / 4 ) ≤ ( 1 / 2 ) ) )
219 23 217 80 218 mpbir3an ( 1 / 4 ) ∈ ( 0 [,] ( 1 / 2 ) )
220 219 a1i ( 𝜑 → ( 1 / 4 ) ∈ ( 0 [,] ( 1 / 2 ) ) )
221 simprl ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 4 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → 𝑦 = ( 1 / 4 ) )
222 221 oveq2d ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 4 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → ( 2 · 𝑦 ) = ( 2 · ( 1 / 4 ) ) )
223 221 oveq1d ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 4 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → ( 𝑦 + ( 1 / 4 ) ) = ( ( 1 / 4 ) + ( 1 / 4 ) ) )
224 29 222 223 3eqtr4a ( ( 𝜑 ∧ ( 𝑦 = ( 1 / 4 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ) → ( 2 · 𝑦 ) = ( 𝑦 + ( 1 / 4 ) ) )
225 retopon ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
226 0xr 0 ∈ ℝ*
227 61 rexri ( 1 / 2 ) ∈ ℝ*
228 lbicc2 ( ( 0 ∈ ℝ* ∧ ( 1 / 2 ) ∈ ℝ* ∧ 0 ≤ ( 1 / 2 ) ) → 0 ∈ ( 0 [,] ( 1 / 2 ) ) )
229 226 227 143 228 mp3an 0 ∈ ( 0 [,] ( 1 / 2 ) )
230 iccss2 ( ( 0 ∈ ( 0 [,] ( 1 / 2 ) ) ∧ ( 1 / 4 ) ∈ ( 0 [,] ( 1 / 2 ) ) ) → ( 0 [,] ( 1 / 4 ) ) ⊆ ( 0 [,] ( 1 / 2 ) ) )
231 229 219 230 mp2an ( 0 [,] ( 1 / 4 ) ) ⊆ ( 0 [,] ( 1 / 2 ) )
232 iccssre ( ( 0 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ )
233 20 61 232 mp2an ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ
234 231 233 sstri ( 0 [,] ( 1 / 4 ) ) ⊆ ℝ
235 resttopon ( ( ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ∧ ( 0 [,] ( 1 / 4 ) ) ⊆ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) ) ∈ ( TopOn ‘ ( 0 [,] ( 1 / 4 ) ) ) )
236 225 234 235 mp2an ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) ) ∈ ( TopOn ‘ ( 0 [,] ( 1 / 4 ) ) )
237 236 a1i ( 𝜑 → ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) ) ∈ ( TopOn ‘ ( 0 [,] ( 1 / 4 ) ) ) )
238 237 188 cnmpt1st ( 𝜑 → ( 𝑦 ∈ ( 0 [,] ( 1 / 4 ) ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ 𝑦 ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) ) ×t II ) Cn ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) ) ) )
239 retop ( topGen ‘ ran (,) ) ∈ Top
240 ovex ( 0 [,] ( 1 / 2 ) ) ∈ V
241 restabs ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 0 [,] ( 1 / 4 ) ) ⊆ ( 0 [,] ( 1 / 2 ) ) ∧ ( 0 [,] ( 1 / 2 ) ) ∈ V ) → ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ↾t ( 0 [,] ( 1 / 4 ) ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) ) )
242 239 231 240 241 mp3an ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ↾t ( 0 [,] ( 1 / 4 ) ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) )
243 242 eqcomi ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) ) = ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ↾t ( 0 [,] ( 1 / 4 ) ) )
244 resttopon ( ( ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ∧ ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ∈ ( TopOn ‘ ( 0 [,] ( 1 / 2 ) ) ) )
245 225 233 244 mp2an ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ∈ ( TopOn ‘ ( 0 [,] ( 1 / 2 ) ) )
246 245 a1i ( 𝜑 → ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ∈ ( TopOn ‘ ( 0 [,] ( 1 / 2 ) ) ) )
247 231 a1i ( 𝜑 → ( 0 [,] ( 1 / 4 ) ) ⊆ ( 0 [,] ( 1 / 2 ) ) )
248 194 iihalf1cn ( 𝑥 ∈ ( 0 [,] ( 1 / 2 ) ) ↦ ( 2 · 𝑥 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) Cn II )
249 248 a1i ( 𝜑 → ( 𝑥 ∈ ( 0 [,] ( 1 / 2 ) ) ↦ ( 2 · 𝑥 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) Cn II ) )
250 243 246 247 249 cnmpt1res ( 𝜑 → ( 𝑥 ∈ ( 0 [,] ( 1 / 4 ) ) ↦ ( 2 · 𝑥 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) ) Cn II ) )
251 oveq2 ( 𝑥 = 𝑦 → ( 2 · 𝑥 ) = ( 2 · 𝑦 ) )
252 237 188 238 237 250 251 cnmpt21 ( 𝜑 → ( 𝑦 ∈ ( 0 [,] ( 1 / 4 ) ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 2 · 𝑦 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) ) ×t II ) Cn II ) )
253 iccssre ( ( ( 1 / 4 ) ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ⊆ ℝ )
254 23 61 253 mp2an ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ⊆ ℝ
255 resttopon ( ( ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ∧ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ⊆ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) ∈ ( TopOn ‘ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) )
256 225 254 255 mp2an ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) ∈ ( TopOn ‘ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) )
257 256 a1i ( 𝜑 → ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) ∈ ( TopOn ‘ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) )
258 257 188 cnmpt1st ( 𝜑 → ( 𝑦 ∈ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ 𝑦 ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) ×t II ) Cn ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) ) )
259 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
260 254 a1i ( 𝜑 → ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ⊆ ℝ )
261 unitssre ( 0 [,] 1 ) ⊆ ℝ
262 261 a1i ( 𝜑 → ( 0 [,] 1 ) ⊆ ℝ )
263 150 89 sselid ( 𝑥 ∈ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) → ( 𝑥 + ( 1 / 4 ) ) ∈ ( 0 [,] 1 ) )
264 263 adantl ( ( 𝜑𝑥 ∈ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) → ( 𝑥 + ( 1 / 4 ) ) ∈ ( 0 [,] 1 ) )
265 259 cnfldtopon ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
266 265 a1i ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
267 266 cnmptid ( 𝜑 → ( 𝑥 ∈ ℂ ↦ 𝑥 ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
268 23 a1i ( 𝜑 → ( 1 / 4 ) ∈ ℝ )
269 268 recnd ( 𝜑 → ( 1 / 4 ) ∈ ℂ )
270 266 266 269 cnmptc ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( 1 / 4 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
271 259 addcn + ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
272 271 a1i ( 𝜑 → + ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
273 266 267 270 272 cnmpt12f ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 + ( 1 / 4 ) ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
274 259 214 196 260 262 264 273 cnmptre ( 𝜑 → ( 𝑥 ∈ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ↦ ( 𝑥 + ( 1 / 4 ) ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) Cn II ) )
275 oveq1 ( 𝑥 = 𝑦 → ( 𝑥 + ( 1 / 4 ) ) = ( 𝑦 + ( 1 / 4 ) ) )
276 257 188 258 257 274 275 cnmpt21 ( 𝜑 → ( 𝑦 ∈ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑦 + ( 1 / 4 ) ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) ×t II ) Cn II ) )
277 193 213 214 194 197 215 220 188 224 252 276 cnmpopc ( 𝜑 → ( 𝑦 ∈ ( 0 [,] ( 1 / 2 ) ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ if ( 𝑦 ≤ ( 1 / 4 ) , ( 2 · 𝑦 ) , ( 𝑦 + ( 1 / 4 ) ) ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ×t II ) Cn II ) )
278 iccssre ( ( ( 1 / 2 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ )
279 61 87 278 mp2an ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ
280 resttopon ( ( ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ∧ ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ∈ ( TopOn ‘ ( ( 1 / 2 ) [,] 1 ) ) )
281 225 279 280 mp2an ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ∈ ( TopOn ‘ ( ( 1 / 2 ) [,] 1 ) )
282 281 a1i ( 𝜑 → ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ∈ ( TopOn ‘ ( ( 1 / 2 ) [,] 1 ) ) )
283 282 188 cnmpt1st ( 𝜑 → ( 𝑦 ∈ ( ( 1 / 2 ) [,] 1 ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ 𝑦 ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ×t II ) Cn ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ) )
284 279 a1i ( 𝜑 → ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ )
285 150 157 sselid ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) → ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ∈ ( 0 [,] 1 ) )
286 285 adantl ( ( 𝜑𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) ) → ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ∈ ( 0 [,] 1 ) )
287 259 divccn ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 / 2 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
288 10 30 287 mp2an ( 𝑥 ∈ ℂ ↦ ( 𝑥 / 2 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) )
289 288 a1i ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 / 2 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
290 37 a1i ( 𝜑 → ( 1 / 2 ) ∈ ℂ )
291 266 266 290 cnmptc ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( 1 / 2 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
292 266 289 291 272 cnmpt12f ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
293 259 195 196 284 262 286 292 cnmptre ( 𝜑 → ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) ↦ ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) Cn II ) )
294 oveq1 ( 𝑥 = 𝑦 → ( 𝑥 / 2 ) = ( 𝑦 / 2 ) )
295 294 oveq1d ( 𝑥 = 𝑦 → ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) = ( ( 𝑦 / 2 ) + ( 1 / 2 ) ) )
296 282 188 283 282 293 295 cnmpt21 ( 𝜑 → ( 𝑦 ∈ ( ( 1 / 2 ) [,] 1 ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑦 / 2 ) + ( 1 / 2 ) ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ×t II ) Cn II ) )
297 193 194 195 196 197 198 199 188 212 277 296 cnmpopc ( 𝜑 → ( 𝑦 ∈ ( 0 [,] 1 ) , 𝑧 ∈ ( 0 [,] 1 ) ↦ if ( 𝑦 ≤ ( 1 / 2 ) , if ( 𝑦 ≤ ( 1 / 4 ) , ( 2 · 𝑦 ) , ( 𝑦 + ( 1 / 4 ) ) ) , ( ( 𝑦 / 2 ) + ( 1 / 2 ) ) ) ) ∈ ( ( II ×t II ) Cn II ) )
298 breq1 ( 𝑥 = 𝑦 → ( 𝑥 ≤ ( 1 / 2 ) ↔ 𝑦 ≤ ( 1 / 2 ) ) )
299 breq1 ( 𝑥 = 𝑦 → ( 𝑥 ≤ ( 1 / 4 ) ↔ 𝑦 ≤ ( 1 / 4 ) ) )
300 299 251 275 ifbieq12d ( 𝑥 = 𝑦 → if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) = if ( 𝑦 ≤ ( 1 / 4 ) , ( 2 · 𝑦 ) , ( 𝑦 + ( 1 / 4 ) ) ) )
301 298 300 295 ifbieq12d ( 𝑥 = 𝑦 → if ( 𝑥 ≤ ( 1 / 2 ) , if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) , ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) = if ( 𝑦 ≤ ( 1 / 2 ) , if ( 𝑦 ≤ ( 1 / 4 ) , ( 2 · 𝑦 ) , ( 𝑦 + ( 1 / 4 ) ) ) , ( ( 𝑦 / 2 ) + ( 1 / 2 ) ) ) )
302 301 equcoms ( 𝑦 = 𝑥 → if ( 𝑥 ≤ ( 1 / 2 ) , if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) , ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) = if ( 𝑦 ≤ ( 1 / 2 ) , if ( 𝑦 ≤ ( 1 / 4 ) , ( 2 · 𝑦 ) , ( 𝑦 + ( 1 / 4 ) ) ) , ( ( 𝑦 / 2 ) + ( 1 / 2 ) ) ) )
303 302 adantr ( ( 𝑦 = 𝑥𝑧 = 0 ) → if ( 𝑥 ≤ ( 1 / 2 ) , if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) , ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) = if ( 𝑦 ≤ ( 1 / 2 ) , if ( 𝑦 ≤ ( 1 / 4 ) , ( 2 · 𝑦 ) , ( 𝑦 + ( 1 / 4 ) ) ) , ( ( 𝑦 / 2 ) + ( 1 / 2 ) ) ) )
304 303 eqcomd ( ( 𝑦 = 𝑥𝑧 = 0 ) → if ( 𝑦 ≤ ( 1 / 2 ) , if ( 𝑦 ≤ ( 1 / 4 ) , ( 2 · 𝑦 ) , ( 𝑦 + ( 1 / 4 ) ) ) , ( ( 𝑦 / 2 ) + ( 1 / 2 ) ) ) = if ( 𝑥 ≤ ( 1 / 2 ) , if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) , ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) )
305 188 189 192 188 188 297 304 cnmpt12 ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) , ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) ) ∈ ( II Cn II ) )
306 6 305 eqeltrid ( 𝜑𝑃 ∈ ( II Cn II ) )
307 iiuni ( 0 [,] 1 ) = II
308 307 307 cnf ( 𝑃 ∈ ( II Cn II ) → 𝑃 : ( 0 [,] 1 ) ⟶ ( 0 [,] 1 ) )
309 306 308 syl ( 𝜑𝑃 : ( 0 [,] 1 ) ⟶ ( 0 [,] 1 ) )
310 6 fmpt ( ∀ 𝑥 ∈ ( 0 [,] 1 ) if ( 𝑥 ≤ ( 1 / 2 ) , if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) , ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) ∈ ( 0 [,] 1 ) ↔ 𝑃 : ( 0 [,] 1 ) ⟶ ( 0 [,] 1 ) )
311 309 310 sylibr ( 𝜑 → ∀ 𝑥 ∈ ( 0 [,] 1 ) if ( 𝑥 ≤ ( 1 / 2 ) , if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) , ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) ∈ ( 0 [,] 1 ) )
312 6 a1i ( 𝜑𝑃 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) , ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) ) )
313 1 46 92 pcocn ( 𝜑 → ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ∈ ( II Cn 𝐽 ) )
314 eqid 𝐽 = 𝐽
315 307 314 cnf ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ∈ ( II Cn 𝐽 ) → ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) : ( 0 [,] 1 ) ⟶ 𝐽 )
316 313 315 syl ( 𝜑 → ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) : ( 0 [,] 1 ) ⟶ 𝐽 )
317 316 feqmptd ( 𝜑 → ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) = ( 𝑦 ∈ ( 0 [,] 1 ) ↦ ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ 𝑦 ) ) )
318 fveq2 ( 𝑦 = if ( 𝑥 ≤ ( 1 / 2 ) , if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) , ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ 𝑦 ) = ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ if ( 𝑥 ≤ ( 1 / 2 ) , if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) , ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) ) )
319 311 312 317 318 fmptcof ( 𝜑 → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ∘ 𝑃 ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ‘ if ( 𝑥 ≤ ( 1 / 2 ) , if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) , ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) ) ) )
320 1 2 4 pcocn ( 𝜑 → ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ∈ ( II Cn 𝐽 ) )
321 320 3 pcoval ( 𝜑 → ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ( *𝑝𝐽 ) 𝐻 ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ ( 2 · 𝑥 ) ) , ( 𝐻 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) )
322 186 319 321 3eqtr4rd ( 𝜑 → ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ( *𝑝𝐽 ) 𝐻 ) = ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ∘ 𝑃 ) )
323 id ( 𝑥 = 0 → 𝑥 = 0 )
324 323 143 eqbrtrdi ( 𝑥 = 0 → 𝑥 ≤ ( 1 / 2 ) )
325 324 iftrued ( 𝑥 = 0 → if ( 𝑥 ≤ ( 1 / 2 ) , if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) , ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) = if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) )
326 323 217 eqbrtrdi ( 𝑥 = 0 → 𝑥 ≤ ( 1 / 4 ) )
327 326 iftrued ( 𝑥 = 0 → if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) = ( 2 · 𝑥 ) )
328 oveq2 ( 𝑥 = 0 → ( 2 · 𝑥 ) = ( 2 · 0 ) )
329 2t0e0 ( 2 · 0 ) = 0
330 328 329 eqtrdi ( 𝑥 = 0 → ( 2 · 𝑥 ) = 0 )
331 325 327 330 3eqtrd ( 𝑥 = 0 → if ( 𝑥 ≤ ( 1 / 2 ) , if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) , ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) = 0 )
332 c0ex 0 ∈ V
333 331 6 332 fvmpt ( 0 ∈ ( 0 [,] 1 ) → ( 𝑃 ‘ 0 ) = 0 )
334 191 333 syl ( 𝜑 → ( 𝑃 ‘ 0 ) = 0 )
335 148 a1i ( 𝜑 → 1 ∈ ( 0 [,] 1 ) )
336 61 87 ltnlei ( ( 1 / 2 ) < 1 ↔ ¬ 1 ≤ ( 1 / 2 ) )
337 144 336 mpbi ¬ 1 ≤ ( 1 / 2 )
338 breq1 ( 𝑥 = 1 → ( 𝑥 ≤ ( 1 / 2 ) ↔ 1 ≤ ( 1 / 2 ) ) )
339 337 338 mtbiri ( 𝑥 = 1 → ¬ 𝑥 ≤ ( 1 / 2 ) )
340 339 iffalsed ( 𝑥 = 1 → if ( 𝑥 ≤ ( 1 / 2 ) , if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) , ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) = ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) )
341 oveq1 ( 𝑥 = 1 → ( 𝑥 / 2 ) = ( 1 / 2 ) )
342 341 oveq1d ( 𝑥 = 1 → ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) = ( ( 1 / 2 ) + ( 1 / 2 ) ) )
343 342 85 eqtrdi ( 𝑥 = 1 → ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) = 1 )
344 340 343 eqtrd ( 𝑥 = 1 → if ( 𝑥 ≤ ( 1 / 2 ) , if ( 𝑥 ≤ ( 1 / 4 ) , ( 2 · 𝑥 ) , ( 𝑥 + ( 1 / 4 ) ) ) , ( ( 𝑥 / 2 ) + ( 1 / 2 ) ) ) = 1 )
345 1ex 1 ∈ V
346 344 6 345 fvmpt ( 1 ∈ ( 0 [,] 1 ) → ( 𝑃 ‘ 1 ) = 1 )
347 335 346 syl ( 𝜑 → ( 𝑃 ‘ 1 ) = 1 )
348 313 306 334 347 reparpht ( 𝜑 → ( ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) ∘ 𝑃 ) ( ≃ph𝐽 ) ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) )
349 322 348 eqbrtrd ( 𝜑 → ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ( *𝑝𝐽 ) 𝐻 ) ( ≃ph𝐽 ) ( 𝐹 ( *𝑝𝐽 ) ( 𝐺 ( *𝑝𝐽 ) 𝐻 ) ) )