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 addlidi ⊢ ( 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 ‘ 𝐽 ) ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝐺 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ) )