MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pcoass Structured version   Visualization version   GIF version

Theorem pcoass 25057
Description: Order of concatenation does not affect homotopy class. (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof shortened by Mario Carneiro, 8-Jun-2014.)
Hypotheses
Ref Expression
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
Ref Expression
pcoass (𝜑 → ((𝐹(*𝑝𝐽)𝐺)(*𝑝𝐽)𝐻)( ≃ph𝐽)(𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)))
Distinct variable groups:   𝑥,𝐹   𝑥,𝐺   𝑥,𝐻   𝑥,𝐽   𝜑,𝑥
Allowed substitution hint:   𝑃(𝑥)

Proof of Theorem pcoass
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 iftrue 4531 . . . . . . . . . . 11 (𝑥 ≤ (1 / 4) → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (2 · 𝑥))
21fveq2d 6910 . . . . . . . . . 10 (𝑥 ≤ (1 / 4) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(2 · 𝑥)))
32adantl 481 . . . . . . . . 9 (((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(2 · 𝑥)))
4 2cn 12341 . . . . . . . . . . . . 13 2 ∈ ℂ
5 elicc01 13506 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (0[,]1) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥𝑥 ≤ 1))
65simp1bi 1146 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0[,]1) → 𝑥 ∈ ℝ)
76adantr 480 . . . . . . . . . . . . . 14 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℝ)
87recnd 11289 . . . . . . . . . . . . 13 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℂ)
9 mulcom 11241 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) = (𝑥 · 2))
104, 8, 9sylancr 587 . . . . . . . . . . . 12 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) = (𝑥 · 2))
115simp2bi 1147 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0[,]1) → 0 ≤ 𝑥)
1211adantr 480 . . . . . . . . . . . . . 14 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 0 ≤ 𝑥)
13 simpr 484 . . . . . . . . . . . . . 14 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ≤ (1 / 4))
14 0re 11263 . . . . . . . . . . . . . . 15 0 ∈ ℝ
15 4nn 12349 . . . . . . . . . . . . . . . 16 4 ∈ ℕ
16 nnrecre 12308 . . . . . . . . . . . . . . . 16 (4 ∈ ℕ → (1 / 4) ∈ ℝ)
1715, 16ax-mp 5 . . . . . . . . . . . . . . 15 (1 / 4) ∈ ℝ
1814, 17elicc2i 13453 . . . . . . . . . . . . . 14 (𝑥 ∈ (0[,](1 / 4)) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥𝑥 ≤ (1 / 4)))
197, 12, 13, 18syl3anbrc 1344 . . . . . . . . . . . . 13 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ (0[,](1 / 4)))
20 2rp 13039 . . . . . . . . . . . . . 14 2 ∈ ℝ+
214mul02i 11450 . . . . . . . . . . . . . 14 (0 · 2) = 0
2217recni 11275 . . . . . . . . . . . . . . 15 (1 / 4) ∈ ℂ
23222timesi 12404 . . . . . . . . . . . . . . . 16 (2 · (1 / 4)) = ((1 / 4) + (1 / 4))
24 2ne0 12370 . . . . . . . . . . . . . . . . . . . 20 2 ≠ 0
25 recdiv2 11980 . . . . . . . . . . . . . . . . . . . 20 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((1 / 2) / 2) = (1 / (2 · 2)))
264, 24, 4, 24, 25mp4an 693 . . . . . . . . . . . . . . . . . . 19 ((1 / 2) / 2) = (1 / (2 · 2))
27 2t2e4 12430 . . . . . . . . . . . . . . . . . . . 20 (2 · 2) = 4
2827oveq2i 7442 . . . . . . . . . . . . . . . . . . 19 (1 / (2 · 2)) = (1 / 4)
2926, 28eqtri 2765 . . . . . . . . . . . . . . . . . 18 ((1 / 2) / 2) = (1 / 4)
3029, 29oveq12i 7443 . . . . . . . . . . . . . . . . 17 (((1 / 2) / 2) + ((1 / 2) / 2)) = ((1 / 4) + (1 / 4))
31 halfcn 12481 . . . . . . . . . . . . . . . . . 18 (1 / 2) ∈ ℂ
32 2halves 12494 . . . . . . . . . . . . . . . . . 18 ((1 / 2) ∈ ℂ → (((1 / 2) / 2) + ((1 / 2) / 2)) = (1 / 2))
3331, 32ax-mp 5 . . . . . . . . . . . . . . . . 17 (((1 / 2) / 2) + ((1 / 2) / 2)) = (1 / 2)
3430, 33eqtr3i 2767 . . . . . . . . . . . . . . . 16 ((1 / 4) + (1 / 4)) = (1 / 2)
3523, 34eqtri 2765 . . . . . . . . . . . . . . 15 (2 · (1 / 4)) = (1 / 2)
364, 22, 35mulcomli 11270 . . . . . . . . . . . . . 14 ((1 / 4) · 2) = (1 / 2)
3714, 17, 20, 21, 36iccdili 13531 . . . . . . . . . . . . 13 (𝑥 ∈ (0[,](1 / 4)) → (𝑥 · 2) ∈ (0[,](1 / 2)))
3819, 37syl 17 . . . . . . . . . . . 12 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → (𝑥 · 2) ∈ (0[,](1 / 2)))
3910, 38eqeltrd 2841 . . . . . . . . . . 11 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈ (0[,](1 / 2)))
40 pcoass.2 . . . . . . . . . . . . 13 (𝜑𝐹 ∈ (II Cn 𝐽))
41 pcoass.3 . . . . . . . . . . . . . 14 (𝜑𝐺 ∈ (II Cn 𝐽))
42 pcoass.4 . . . . . . . . . . . . . 14 (𝜑𝐻 ∈ (II Cn 𝐽))
43 pcoass.6 . . . . . . . . . . . . . 14 (𝜑 → (𝐺‘1) = (𝐻‘0))
4441, 42, 43pcocn 25050 . . . . . . . . . . . . 13 (𝜑 → (𝐺(*𝑝𝐽)𝐻) ∈ (II Cn 𝐽))
4540, 44pcoval1 25046 . . . . . . . . . . . 12 ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(2 · 𝑥)) = (𝐹‘(2 · (2 · 𝑥))))
4640, 41pcoval1 25046 . . . . . . . . . . . 12 ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) → ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)) = (𝐹‘(2 · (2 · 𝑥))))
4745, 46eqtr4d 2780 . . . . . . . . . . 11 ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
4839, 47sylan2 593 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4))) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
4948anassrs 467 . . . . . . . . 9 (((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
503, 49eqtrd 2777 . . . . . . . 8 (((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
5150adantlr 715 . . . . . . 7 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
52 simplll 775 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝜑)
536ad2antlr 727 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → 𝑥 ∈ ℝ)
5453adantr 480 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℝ)
55 letric 11361 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ (1 / 4) ∈ ℝ) → (𝑥 ≤ (1 / 4) ∨ (1 / 4) ≤ 𝑥))
5653, 17, 55sylancl 586 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → (𝑥 ≤ (1 / 4) ∨ (1 / 4) ≤ 𝑥))
5756orcanai 1005 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (1 / 4) ≤ 𝑥)
58 simplr 769 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ≤ (1 / 2))
59 halfre 12480 . . . . . . . . . . . . 13 (1 / 2) ∈ ℝ
6017, 59elicc2i 13453 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 4)[,](1 / 2)) ↔ (𝑥 ∈ ℝ ∧ (1 / 4) ≤ 𝑥𝑥 ≤ (1 / 2)))
6154, 57, 58, 60syl3anbrc 1344 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ((1 / 4)[,](1 / 2)))
6260simp1bi 1146 . . . . . . . . . . . . 13 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → 𝑥 ∈ ℝ)
63 readdcl 11238 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ (1 / 4) ∈ ℝ) → (𝑥 + (1 / 4)) ∈ ℝ)
6462, 17, 63sylancl 586 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ∈ ℝ)
6517a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 4) ∈ ℝ)
6660simp2bi 1147 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 4) ≤ 𝑥)
6765, 62, 65, 66leadd1dd 11877 . . . . . . . . . . . . 13 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → ((1 / 4) + (1 / 4)) ≤ (𝑥 + (1 / 4)))
6834, 67eqbrtrrid 5179 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 2) ≤ (𝑥 + (1 / 4)))
6959a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 2) ∈ ℝ)
7060simp3bi 1148 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → 𝑥 ≤ (1 / 2))
71 2lt4 12441 . . . . . . . . . . . . . . . . 17 2 < 4
72 2re 12340 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
73 4re 12350 . . . . . . . . . . . . . . . . . 18 4 ∈ ℝ
74 2pos 12369 . . . . . . . . . . . . . . . . . 18 0 < 2
75 4pos 12373 . . . . . . . . . . . . . . . . . 18 0 < 4
7672, 73, 74, 75ltrecii 12184 . . . . . . . . . . . . . . . . 17 (2 < 4 ↔ (1 / 4) < (1 / 2))
7771, 76mpbi 230 . . . . . . . . . . . . . . . 16 (1 / 4) < (1 / 2)
7817, 59, 77ltleii 11384 . . . . . . . . . . . . . . 15 (1 / 4) ≤ (1 / 2)
7978a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 4) ≤ (1 / 2))
8062, 65, 69, 69, 70, 79le2addd 11882 . . . . . . . . . . . . 13 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ≤ ((1 / 2) + (1 / 2)))
81 ax-1cn 11213 . . . . . . . . . . . . . 14 1 ∈ ℂ
82 2halves 12494 . . . . . . . . . . . . . 14 (1 ∈ ℂ → ((1 / 2) + (1 / 2)) = 1)
8381, 82ax-mp 5 . . . . . . . . . . . . 13 ((1 / 2) + (1 / 2)) = 1
8480, 83breqtrdi 5184 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ≤ 1)
85 1re 11261 . . . . . . . . . . . . 13 1 ∈ ℝ
8659, 85elicc2i 13453 . . . . . . . . . . . 12 ((𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1) ↔ ((𝑥 + (1 / 4)) ∈ ℝ ∧ (1 / 2) ≤ (𝑥 + (1 / 4)) ∧ (𝑥 + (1 / 4)) ≤ 1))
8764, 68, 84, 86syl3anbrc 1344 . . . . . . . . . . 11 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1))
8861, 87syl 17 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1))
89 pcoass.5 . . . . . . . . . . . 12 (𝜑 → (𝐹‘1) = (𝐺‘0))
9041, 42pco0 25047 . . . . . . . . . . . 12 (𝜑 → ((𝐺(*𝑝𝐽)𝐻)‘0) = (𝐺‘0))
9189, 90eqtr4d 2780 . . . . . . . . . . 11 (𝜑 → (𝐹‘1) = ((𝐺(*𝑝𝐽)𝐻)‘0))
9240, 44, 91pcoval2 25049 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(𝑥 + (1 / 4))) = ((𝐺(*𝑝𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)))
9352, 88, 92syl2anc 584 . . . . . . . . 9 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(𝑥 + (1 / 4))) = ((𝐺(*𝑝𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)))
9483oveq2i 7442 . . . . . . . . . . . 12 ((2 · (𝑥 + (1 / 4))) − ((1 / 2) + (1 / 2))) = ((2 · (𝑥 + (1 / 4))) − 1)
95 2cnd 12344 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 2 ∈ ℂ)
9654recnd 11289 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℂ)
9722a1i 11 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (1 / 4) ∈ ℂ)
9895, 96, 97adddid 11285 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · (𝑥 + (1 / 4))) = ((2 · 𝑥) + (2 · (1 / 4))))
9935oveq2i 7442 . . . . . . . . . . . . . 14 ((2 · 𝑥) + (2 · (1 / 4))) = ((2 · 𝑥) + (1 / 2))
10098, 99eqtrdi 2793 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · (𝑥 + (1 / 4))) = ((2 · 𝑥) + (1 / 2)))
101100oveq1d 7446 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − ((1 / 2) + (1 / 2))) = (((2 · 𝑥) + (1 / 2)) − ((1 / 2) + (1 / 2))))
10294, 101eqtr3id 2791 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − 1) = (((2 · 𝑥) + (1 / 2)) − ((1 / 2) + (1 / 2))))
103 remulcl 11240 . . . . . . . . . . . . . 14 ((2 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (2 · 𝑥) ∈ ℝ)
10472, 54, 103sylancr 587 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈ ℝ)
105104recnd 11289 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈ ℂ)
10631a1i 11 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (1 / 2) ∈ ℂ)
107105, 106, 106pnpcan2d 11658 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (((2 · 𝑥) + (1 / 2)) − ((1 / 2) + (1 / 2))) = ((2 · 𝑥) − (1 / 2)))
108102, 107eqtrd 2777 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − 1) = ((2 · 𝑥) − (1 / 2)))
109108fveq2d 6910 . . . . . . . . 9 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(*𝑝𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)) = ((𝐺(*𝑝𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))))
1104, 96, 9sylancr 587 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) = (𝑥 · 2))
11181, 4, 24divcan1i 12011 . . . . . . . . . . . . . . 15 ((1 / 2) · 2) = 1
11217, 59, 20, 36, 111iccdili 13531 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 · 2) ∈ ((1 / 2)[,]1))
11361, 112syl 17 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (𝑥 · 2) ∈ ((1 / 2)[,]1))
114110, 113eqeltrd 2841 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈ ((1 / 2)[,]1))
11531subidi 11580 . . . . . . . . . . . . 13 ((1 / 2) − (1 / 2)) = 0
116 1mhlfehlf 12485 . . . . . . . . . . . . 13 (1 − (1 / 2)) = (1 / 2)
11759, 85, 59, 115, 116iccshftli 13529 . . . . . . . . . . . 12 ((2 · 𝑥) ∈ ((1 / 2)[,]1) → ((2 · 𝑥) − (1 / 2)) ∈ (0[,](1 / 2)))
118114, 117syl 17 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · 𝑥) − (1 / 2)) ∈ (0[,](1 / 2)))
11941, 42pcoval1 25046 . . . . . . . . . . 11 ((𝜑 ∧ ((2 · 𝑥) − (1 / 2)) ∈ (0[,](1 / 2))) → ((𝐺(*𝑝𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))))
12052, 118, 119syl2anc 584 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(*𝑝𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))))
12195, 105, 106subdid 11719 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · ((2 · 𝑥) − (1 / 2))) = ((2 · (2 · 𝑥)) − (2 · (1 / 2))))
1224, 24recidi 11998 . . . . . . . . . . . . 13 (2 · (1 / 2)) = 1
123122oveq2i 7442 . . . . . . . . . . . 12 ((2 · (2 · 𝑥)) − (2 · (1 / 2))) = ((2 · (2 · 𝑥)) − 1)
124121, 123eqtrdi 2793 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · ((2 · 𝑥) − (1 / 2))) = ((2 · (2 · 𝑥)) − 1))
125124fveq2d 6910 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
126120, 125eqtrd 2777 . . . . . . . . 9 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(*𝑝𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
12793, 109, 1263eqtrd 2781 . . . . . . . 8 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(𝑥 + (1 / 4))) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
128 iffalse 4534 . . . . . . . . . 10 𝑥 ≤ (1 / 4) → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (𝑥 + (1 / 4)))
129128fveq2d 6910 . . . . . . . . 9 𝑥 ≤ (1 / 4) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(𝑥 + (1 / 4))))
130129adantl 481 . . . . . . . 8 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(𝑥 + (1 / 4))))
13140, 41, 89pcoval2 25049 . . . . . . . . 9 ((𝜑 ∧ (2 · 𝑥) ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
13252, 114, 131syl2anc 584 . . . . . . . 8 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
133127, 130, 1323eqtr4d 2787 . . . . . . 7 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
13451, 133pm2.61dan 813 . . . . . 6 (((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
135 iftrue 4531 . . . . . . . 8 (𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))))
136135fveq2d 6910 . . . . . . 7 (𝑥 ≤ (1 / 2) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))))
137136adantl 481 . . . . . 6 (((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))))
138 iftrue 4531 . . . . . . 7 (𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
139138adantl 481 . . . . . 6 (((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
140134, 137, 1393eqtr4d 2787 . . . . 5 (((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))))
141 elii2 24965 . . . . . . . 8 ((𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 ≤ (1 / 2)) → 𝑥 ∈ ((1 / 2)[,]1))
142 halfge0 12483 . . . . . . . . . . . . . 14 0 ≤ (1 / 2)
143 halflt1 12484 . . . . . . . . . . . . . . 15 (1 / 2) < 1
14459, 85, 143ltleii 11384 . . . . . . . . . . . . . 14 (1 / 2) ≤ 1
145 elicc01 13506 . . . . . . . . . . . . . 14 ((1 / 2) ∈ (0[,]1) ↔ ((1 / 2) ∈ ℝ ∧ 0 ≤ (1 / 2) ∧ (1 / 2) ≤ 1))
14659, 142, 144, 145mpbir3an 1342 . . . . . . . . . . . . 13 (1 / 2) ∈ (0[,]1)
147 1elunit 13510 . . . . . . . . . . . . 13 1 ∈ (0[,]1)
148 iccss2 13458 . . . . . . . . . . . . 13 (((1 / 2) ∈ (0[,]1) ∧ 1 ∈ (0[,]1)) → ((1 / 2)[,]1) ⊆ (0[,]1))
149146, 147, 148mp2an 692 . . . . . . . . . . . 12 ((1 / 2)[,]1) ⊆ (0[,]1)
150149sseli 3979 . . . . . . . . . . 11 (𝑥 ∈ ((1 / 2)[,]1) → 𝑥 ∈ (0[,]1))
1514, 24div0i 12001 . . . . . . . . . . . 12 (0 / 2) = 0
152 eqid 2737 . . . . . . . . . . . 12 (1 / 2) = (1 / 2)
15314, 85, 20, 151, 152icccntri 13533 . . . . . . . . . . 11 (𝑥 ∈ (0[,]1) → (𝑥 / 2) ∈ (0[,](1 / 2)))
15431addlidi 11449 . . . . . . . . . . . 12 (0 + (1 / 2)) = (1 / 2)
15514, 59, 59, 154, 83iccshftri 13527 . . . . . . . . . . 11 ((𝑥 / 2) ∈ (0[,](1 / 2)) → ((𝑥 / 2) + (1 / 2)) ∈ ((1 / 2)[,]1))
156150, 153, 1553syl 18 . . . . . . . . . 10 (𝑥 ∈ ((1 / 2)[,]1) → ((𝑥 / 2) + (1 / 2)) ∈ ((1 / 2)[,]1))
15740, 44, 91pcoval2 25049 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 / 2) + (1 / 2)) ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = ((𝐺(*𝑝𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)))
158156, 157sylan2 593 . . . . . . . . 9 ((𝜑𝑥 ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = ((𝐺(*𝑝𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)))
15959, 85elicc2i 13453 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 2)[,]1) ↔ (𝑥 ∈ ℝ ∧ (1 / 2) ≤ 𝑥𝑥 ≤ 1))
160159simp1bi 1146 . . . . . . . . . . . . 13 (𝑥 ∈ ((1 / 2)[,]1) → 𝑥 ∈ ℝ)
161160recnd 11289 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 2)[,]1) → 𝑥 ∈ ℂ)
162 1cnd 11256 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 2)[,]1) → 1 ∈ ℂ)
163 2cnd 12344 . . . . . . . . . . . . . . 15 (𝑥 ∈ ((1 / 2)[,]1) → 2 ∈ ℂ)
16424a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ ((1 / 2)[,]1) → 2 ≠ 0)
165161, 162, 163, 164divdird 12081 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 2)[,]1) → ((𝑥 + 1) / 2) = ((𝑥 / 2) + (1 / 2)))
166165oveq2d 7447 . . . . . . . . . . . . 13 (𝑥 ∈ ((1 / 2)[,]1) → (2 · ((𝑥 + 1) / 2)) = (2 · ((𝑥 / 2) + (1 / 2))))
167 peano2cn 11433 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℂ → (𝑥 + 1) ∈ ℂ)
168161, 167syl 17 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 2)[,]1) → (𝑥 + 1) ∈ ℂ)
169168, 163, 164divcan2d 12045 . . . . . . . . . . . . 13 (𝑥 ∈ ((1 / 2)[,]1) → (2 · ((𝑥 + 1) / 2)) = (𝑥 + 1))
170166, 169eqtr3d 2779 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 2)[,]1) → (2 · ((𝑥 / 2) + (1 / 2))) = (𝑥 + 1))
171161, 162, 170mvrraddd 11675 . . . . . . . . . . 11 (𝑥 ∈ ((1 / 2)[,]1) → ((2 · ((𝑥 / 2) + (1 / 2))) − 1) = 𝑥)
172171fveq2d 6910 . . . . . . . . . 10 (𝑥 ∈ ((1 / 2)[,]1) → ((𝐺(*𝑝𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)) = ((𝐺(*𝑝𝐽)𝐻)‘𝑥))
173172adantl 481 . . . . . . . . 9 ((𝜑𝑥 ∈ ((1 / 2)[,]1)) → ((𝐺(*𝑝𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)) = ((𝐺(*𝑝𝐽)𝐻)‘𝑥))
17441, 42, 43pcoval2 25049 . . . . . . . . 9 ((𝜑𝑥 ∈ ((1 / 2)[,]1)) → ((𝐺(*𝑝𝐽)𝐻)‘𝑥) = (𝐻‘((2 · 𝑥) − 1)))
175158, 173, 1743eqtrd 2781 . . . . . . . 8 ((𝜑𝑥 ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1)))
176141, 175sylan2 593 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 ≤ (1 / 2))) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1)))
177176anassrs 467 . . . . . 6 (((𝜑𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1)))
178 iffalse 4534 . . . . . . . 8 𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = ((𝑥 / 2) + (1 / 2)))
179178fveq2d 6910 . . . . . . 7 𝑥 ≤ (1 / 2) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))))
180179adantl 481 . . . . . 6 (((𝜑𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))))
181 iffalse 4534 . . . . . . 7 𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = (𝐻‘((2 · 𝑥) − 1)))
182181adantl 481 . . . . . 6 (((𝜑𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = (𝐻‘((2 · 𝑥) − 1)))
183177, 180, 1823eqtr4d 2787 . . . . 5 (((𝜑𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))))
184140, 183pm2.61dan 813 . . . 4 ((𝜑𝑥 ∈ (0[,]1)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))))
185184mpteq2dva 5242 . . 3 (𝜑 → (𝑥 ∈ (0[,]1) ↦ ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))))) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1)))))
186 pcoass.7 . . . . . . 7 𝑃 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))))
187 iitopon 24905 . . . . . . . . 9 II ∈ (TopOn‘(0[,]1))
188187a1i 11 . . . . . . . 8 (𝜑 → II ∈ (TopOn‘(0[,]1)))
189188cnmptid 23669 . . . . . . . 8 (𝜑 → (𝑥 ∈ (0[,]1) ↦ 𝑥) ∈ (II Cn II))
190 0elunit 13509 . . . . . . . . . 10 0 ∈ (0[,]1)
191190a1i 11 . . . . . . . . 9 (𝜑 → 0 ∈ (0[,]1))
192188, 188, 191cnmptc 23670 . . . . . . . 8 (𝜑 → (𝑥 ∈ (0[,]1) ↦ 0) ∈ (II Cn II))
193 eqid 2737 . . . . . . . . 9 (topGen‘ran (,)) = (topGen‘ran (,))
194 eqid 2737 . . . . . . . . 9 ((topGen‘ran (,)) ↾t (0[,](1 / 2))) = ((topGen‘ran (,)) ↾t (0[,](1 / 2)))
195 eqid 2737 . . . . . . . . 9 ((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) = ((topGen‘ran (,)) ↾t ((1 / 2)[,]1))
196 dfii2 24908 . . . . . . . . 9 II = ((topGen‘ran (,)) ↾t (0[,]1))
197 0red 11264 . . . . . . . . 9 (𝜑 → 0 ∈ ℝ)
198 1red 11262 . . . . . . . . 9 (𝜑 → 1 ∈ ℝ)
199146a1i 11 . . . . . . . . 9 (𝜑 → (1 / 2) ∈ (0[,]1))
200 simprl 771 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → 𝑦 = (1 / 2))
201200oveq1d 7446 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 2) + (1 / 4)))
20231, 22addcomi 11452 . . . . . . . . . . 11 ((1 / 2) + (1 / 4)) = ((1 / 4) + (1 / 2))
203201, 202eqtrdi 2793 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 4) + (1 / 2)))
20417, 59ltnlei 11382 . . . . . . . . . . . . 13 ((1 / 4) < (1 / 2) ↔ ¬ (1 / 2) ≤ (1 / 4))
20577, 204mpbi 230 . . . . . . . . . . . 12 ¬ (1 / 2) ≤ (1 / 4)
206200breq1d 5153 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 ≤ (1 / 4) ↔ (1 / 2) ≤ (1 / 4)))
207205, 206mtbiri 327 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → ¬ 𝑦 ≤ (1 / 4))
208207iffalsed 4536 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))) = (𝑦 + (1 / 4)))
209200oveq1d 7446 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 / 2) = ((1 / 2) / 2))
210209, 29eqtrdi 2793 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 / 2) = (1 / 4))
211210oveq1d 7446 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → ((𝑦 / 2) + (1 / 2)) = ((1 / 4) + (1 / 2)))
212203, 208, 2113eqtr4d 2787 . . . . . . . . 9 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))) = ((𝑦 / 2) + (1 / 2)))
213 eqid 2737 . . . . . . . . . 10 ((topGen‘ran (,)) ↾t (0[,](1 / 4))) = ((topGen‘ran (,)) ↾t (0[,](1 / 4)))
214 eqid 2737 . . . . . . . . . 10 ((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2))) = ((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2)))
21559a1i 11 . . . . . . . . . 10 (𝜑 → (1 / 2) ∈ ℝ)
21673, 75recgt0ii 12174 . . . . . . . . . . . . 13 0 < (1 / 4)
21714, 17, 216ltleii 11384 . . . . . . . . . . . 12 0 ≤ (1 / 4)
21814, 59elicc2i 13453 . . . . . . . . . . . 12 ((1 / 4) ∈ (0[,](1 / 2)) ↔ ((1 / 4) ∈ ℝ ∧ 0 ≤ (1 / 4) ∧ (1 / 4) ≤ (1 / 2)))
21917, 217, 78, 218mpbir3an 1342 . . . . . . . . . . 11 (1 / 4) ∈ (0[,](1 / 2))
220219a1i 11 . . . . . . . . . 10 (𝜑 → (1 / 4) ∈ (0[,](1 / 2)))
221 simprl 771 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → 𝑦 = (1 / 4))
222221oveq2d 7447 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = (2 · (1 / 4)))
223221oveq1d 7446 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 4) + (1 / 4)))
22423, 222, 2233eqtr4a 2803 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = (𝑦 + (1 / 4)))
225 retopon 24784 . . . . . . . . . . . . 13 (topGen‘ran (,)) ∈ (TopOn‘ℝ)
226 0xr 11308 . . . . . . . . . . . . . . . 16 0 ∈ ℝ*
22759rexri 11319 . . . . . . . . . . . . . . . 16 (1 / 2) ∈ ℝ*
228 lbicc2 13504 . . . . . . . . . . . . . . . 16 ((0 ∈ ℝ* ∧ (1 / 2) ∈ ℝ* ∧ 0 ≤ (1 / 2)) → 0 ∈ (0[,](1 / 2)))
229226, 227, 142, 228mp3an 1463 . . . . . . . . . . . . . . 15 0 ∈ (0[,](1 / 2))
230 iccss2 13458 . . . . . . . . . . . . . . 15 ((0 ∈ (0[,](1 / 2)) ∧ (1 / 4) ∈ (0[,](1 / 2))) → (0[,](1 / 4)) ⊆ (0[,](1 / 2)))
231229, 219, 230mp2an 692 . . . . . . . . . . . . . 14 (0[,](1 / 4)) ⊆ (0[,](1 / 2))
232 iccssre 13469 . . . . . . . . . . . . . . 15 ((0 ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (0[,](1 / 2)) ⊆ ℝ)
23314, 59, 232mp2an 692 . . . . . . . . . . . . . 14 (0[,](1 / 2)) ⊆ ℝ
234231, 233sstri 3993 . . . . . . . . . . . . 13 (0[,](1 / 4)) ⊆ ℝ
235 resttopon 23169 . . . . . . . . . . . . 13 (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 / 4)) ⊆ ℝ) → ((topGen‘ran (,)) ↾t (0[,](1 / 4))) ∈ (TopOn‘(0[,](1 / 4))))
236225, 234, 235mp2an 692 . . . . . . . . . . . 12 ((topGen‘ran (,)) ↾t (0[,](1 / 4))) ∈ (TopOn‘(0[,](1 / 4)))
237236a1i 11 . . . . . . . . . . 11 (𝜑 → ((topGen‘ran (,)) ↾t (0[,](1 / 4))) ∈ (TopOn‘(0[,](1 / 4))))
238237, 188cnmpt1st 23676 . . . . . . . . . . 11 (𝜑 → (𝑦 ∈ (0[,](1 / 4)), 𝑧 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,)) ↾t (0[,](1 / 4))) ×t II) Cn ((topGen‘ran (,)) ↾t (0[,](1 / 4)))))
239 retop 24782 . . . . . . . . . . . . . 14 (topGen‘ran (,)) ∈ Top
240 ovex 7464 . . . . . . . . . . . . . 14 (0[,](1 / 2)) ∈ V
241 restabs 23173 . . . . . . . . . . . . . 14 (((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))))
242239, 231, 240, 241mp3an 1463 . . . . . . . . . . . . 13 (((topGen‘ran (,)) ↾t (0[,](1 / 2))) ↾t (0[,](1 / 4))) = ((topGen‘ran (,)) ↾t (0[,](1 / 4)))
243242eqcomi 2746 . . . . . . . . . . . 12 ((topGen‘ran (,)) ↾t (0[,](1 / 4))) = (((topGen‘ran (,)) ↾t (0[,](1 / 2))) ↾t (0[,](1 / 4)))
244 resttopon 23169 . . . . . . . . . . . . . 14 (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 / 2)) ⊆ ℝ) → ((topGen‘ran (,)) ↾t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 / 2))))
245225, 233, 244mp2an 692 . . . . . . . . . . . . 13 ((topGen‘ran (,)) ↾t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 / 2)))
246245a1i 11 . . . . . . . . . . . 12 (𝜑 → ((topGen‘ran (,)) ↾t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 / 2))))
247231a1i 11 . . . . . . . . . . . 12 (𝜑 → (0[,](1 / 4)) ⊆ (0[,](1 / 2)))
248194iihalf1cn 24959 . . . . . . . . . . . . 13 (𝑥 ∈ (0[,](1 / 2)) ↦ (2 · 𝑥)) ∈ (((topGen‘ran (,)) ↾t (0[,](1 / 2))) Cn II)
249248a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ (0[,](1 / 2)) ↦ (2 · 𝑥)) ∈ (((topGen‘ran (,)) ↾t (0[,](1 / 2))) Cn II))
250243, 246, 247, 249cnmpt1res 23684 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ (0[,](1 / 4)) ↦ (2 · 𝑥)) ∈ (((topGen‘ran (,)) ↾t (0[,](1 / 4))) Cn II))
251 oveq2 7439 . . . . . . . . . . 11 (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
252237, 188, 238, 237, 250, 251cnmpt21 23679 . . . . . . . . . 10 (𝜑 → (𝑦 ∈ (0[,](1 / 4)), 𝑧 ∈ (0[,]1) ↦ (2 · 𝑦)) ∈ ((((topGen‘ran (,)) ↾t (0[,](1 / 4))) ×t II) Cn II))
253 iccssre 13469 . . . . . . . . . . . . . 14 (((1 / 4) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → ((1 / 4)[,](1 / 2)) ⊆ ℝ)
25417, 59, 253mp2an 692 . . . . . . . . . . . . 13 ((1 / 4)[,](1 / 2)) ⊆ ℝ
255 resttopon 23169 . . . . . . . . . . . . 13 (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 / 4)[,](1 / 2)) ⊆ ℝ) → ((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2))) ∈ (TopOn‘((1 / 4)[,](1 / 2))))
256225, 254, 255mp2an 692 . . . . . . . . . . . 12 ((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2))) ∈ (TopOn‘((1 / 4)[,](1 / 2)))
257256a1i 11 . . . . . . . . . . 11 (𝜑 → ((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2))) ∈ (TopOn‘((1 / 4)[,](1 / 2))))
258257, 188cnmpt1st 23676 . . . . . . . . . . 11 (𝜑 → (𝑦 ∈ ((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 2737 . . . . . . . . . . . 12 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
260254a1i 11 . . . . . . . . . . . 12 (𝜑 → ((1 / 4)[,](1 / 2)) ⊆ ℝ)
261 unitssre 13539 . . . . . . . . . . . . 13 (0[,]1) ⊆ ℝ
262261a1i 11 . . . . . . . . . . . 12 (𝜑 → (0[,]1) ⊆ ℝ)
263149, 87sselid 3981 . . . . . . . . . . . . 13 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ∈ (0[,]1))
264263adantl 481 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((1 / 4)[,](1 / 2))) → (𝑥 + (1 / 4)) ∈ (0[,]1))
265259cnfldtopon 24803 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
266265a1i 11 . . . . . . . . . . . . 13 (𝜑 → (TopOpen‘ℂfld) ∈ (TopOn‘ℂ))
267266cnmptid 23669 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ ℂ ↦ 𝑥) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
26817a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (1 / 4) ∈ ℝ)
269268recnd 11289 . . . . . . . . . . . . . 14 (𝜑 → (1 / 4) ∈ ℂ)
270266, 266, 269cnmptc 23670 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ ℂ ↦ (1 / 4)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
271259addcn 24887 . . . . . . . . . . . . . 14 + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
272271a1i 11 . . . . . . . . . . . . 13 (𝜑 → + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
273266, 267, 270, 272cnmpt12f 23674 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ ℂ ↦ (𝑥 + (1 / 4))) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
274259, 214, 196, 260, 262, 264, 273cnmptre 24954 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ ((1 / 4)[,](1 / 2)) ↦ (𝑥 + (1 / 4))) ∈ (((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2))) Cn II))
275 oveq1 7438 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑥 + (1 / 4)) = (𝑦 + (1 / 4)))
276257, 188, 258, 257, 274, 275cnmpt21 23679 . . . . . . . . . 10 (𝜑 → (𝑦 ∈ ((1 / 4)[,](1 / 2)), 𝑧 ∈ (0[,]1) ↦ (𝑦 + (1 / 4))) ∈ ((((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2))) ×t II) Cn II))
277193, 213, 214, 194, 197, 215, 220, 188, 224, 252, 276cnmpopc 24955 . . . . . . . . 9 (𝜑 → (𝑦 ∈ (0[,](1 / 2)), 𝑧 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4)))) ∈ ((((topGen‘ran (,)) ↾t (0[,](1 / 2))) ×t II) Cn II))
278 iccssre 13469 . . . . . . . . . . . . 13 (((1 / 2) ∈ ℝ ∧ 1 ∈ ℝ) → ((1 / 2)[,]1) ⊆ ℝ)
27959, 85, 278mp2an 692 . . . . . . . . . . . 12 ((1 / 2)[,]1) ⊆ ℝ
280 resttopon 23169 . . . . . . . . . . . 12 (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 / 2)[,]1) ⊆ ℝ) → ((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1)))
281225, 279, 280mp2an 692 . . . . . . . . . . 11 ((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1))
282281a1i 11 . . . . . . . . . 10 (𝜑 → ((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1)))
283282, 188cnmpt1st 23676 . . . . . . . . . 10 (𝜑 → (𝑦 ∈ ((1 / 2)[,]1), 𝑧 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ×t II) Cn ((topGen‘ran (,)) ↾t ((1 / 2)[,]1))))
284279a1i 11 . . . . . . . . . . 11 (𝜑 → ((1 / 2)[,]1) ⊆ ℝ)
285149, 156sselid 3981 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 2)[,]1) → ((𝑥 / 2) + (1 / 2)) ∈ (0[,]1))
286285adantl 481 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((1 / 2)[,]1)) → ((𝑥 / 2) + (1 / 2)) ∈ (0[,]1))
287259divccn 24897 . . . . . . . . . . . . . 14 ((2 ∈ ℂ ∧ 2 ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
2884, 24, 287mp2an 692 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld))
289288a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
29031a1i 11 . . . . . . . . . . . . 13 (𝜑 → (1 / 2) ∈ ℂ)
291266, 266, 290cnmptc 23670 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ ℂ ↦ (1 / 2)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
292266, 289, 291, 272cnmpt12f 23674 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ ℂ ↦ ((𝑥 / 2) + (1 / 2))) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
293259, 195, 196, 284, 262, 286, 292cnmptre 24954 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ ((1 / 2)[,]1) ↦ ((𝑥 / 2) + (1 / 2))) ∈ (((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) Cn II))
294 oveq1 7438 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑥 / 2) = (𝑦 / 2))
295294oveq1d 7446 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝑥 / 2) + (1 / 2)) = ((𝑦 / 2) + (1 / 2)))
296282, 188, 283, 282, 293, 295cnmpt21 23679 . . . . . . . . 9 (𝜑 → (𝑦 ∈ ((1 / 2)[,]1), 𝑧 ∈ (0[,]1) ↦ ((𝑦 / 2) + (1 / 2))) ∈ ((((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ×t II) Cn II))
297193, 194, 195, 196, 197, 198, 199, 188, 212, 277, 296cnmpopc 24955 . . . . . . . 8 (𝜑 → (𝑦 ∈ (0[,]1), 𝑧 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 2), if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))), ((𝑦 / 2) + (1 / 2)))) ∈ ((II ×t II) Cn II))
298 breq1 5146 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥 ≤ (1 / 2) ↔ 𝑦 ≤ (1 / 2)))
299 breq1 5146 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑥 ≤ (1 / 4) ↔ 𝑦 ≤ (1 / 4)))
300299, 251, 275ifbieq12d 4554 . . . . . . . . . . . 12 (𝑥 = 𝑦 → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))))
301298, 300, 295ifbieq12d 4554 . . . . . . . . . . 11 (𝑥 = 𝑦 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑦 ≤ (1 / 2), if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))), ((𝑦 / 2) + (1 / 2))))
302301equcoms 2019 . . . . . . . . . 10 (𝑦 = 𝑥 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑦 ≤ (1 / 2), if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))), ((𝑦 / 2) + (1 / 2))))
303302adantr 480 . . . . . . . . 9 ((𝑦 = 𝑥𝑧 = 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))))
304303eqcomd 2743 . . . . . . . 8 ((𝑦 = 𝑥𝑧 = 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))))
305188, 189, 192, 188, 188, 297, 304cnmpt12 23675 . . . . . . 7 (𝜑 → (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) ∈ (II Cn II))
306186, 305eqeltrid 2845 . . . . . 6 (𝜑𝑃 ∈ (II Cn II))
307 iiuni 24907 . . . . . . 7 (0[,]1) = II
308307, 307cnf 23254 . . . . . 6 (𝑃 ∈ (II Cn II) → 𝑃:(0[,]1)⟶(0[,]1))
309306, 308syl 17 . . . . 5 (𝜑𝑃:(0[,]1)⟶(0[,]1))
310186fmpt 7130 . . . . 5 (∀𝑥 ∈ (0[,]1)if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) ∈ (0[,]1) ↔ 𝑃:(0[,]1)⟶(0[,]1))
311309, 310sylibr 234 . . . 4 (𝜑 → ∀𝑥 ∈ (0[,]1)if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) ∈ (0[,]1))
312186a1i 11 . . . 4 (𝜑𝑃 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))))
31340, 44, 91pcocn 25050 . . . . . 6 (𝜑 → (𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)) ∈ (II Cn 𝐽))
314 eqid 2737 . . . . . . 7 𝐽 = 𝐽
315307, 314cnf 23254 . . . . . 6 ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)) ∈ (II Cn 𝐽) → (𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)):(0[,]1)⟶ 𝐽)
316313, 315syl 17 . . . . 5 (𝜑 → (𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)):(0[,]1)⟶ 𝐽)
317316feqmptd 6977 . . . 4 (𝜑 → (𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)) = (𝑦 ∈ (0[,]1) ↦ ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘𝑦)))
318 fveq2 6906 . . . 4 (𝑦 = if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘𝑦) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))))
319311, 312, 317, 318fmptcof 7150 . . 3 (𝜑 → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)) ∘ 𝑃) = (𝑥 ∈ (0[,]1) ↦ ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))))))
32040, 41, 89pcocn 25050 . . . 4 (𝜑 → (𝐹(*𝑝𝐽)𝐺) ∈ (II Cn 𝐽))
321320, 42pcoval 25044 . . 3 (𝜑 → ((𝐹(*𝑝𝐽)𝐺)(*𝑝𝐽)𝐻) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1)))))
322185, 319, 3213eqtr4rd 2788 . 2 (𝜑 → ((𝐹(*𝑝𝐽)𝐺)(*𝑝𝐽)𝐻) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)) ∘ 𝑃))
323 id 22 . . . . . . . 8 (𝑥 = 0 → 𝑥 = 0)
324323, 142eqbrtrdi 5182 . . . . . . 7 (𝑥 = 0 → 𝑥 ≤ (1 / 2))
325324iftrued 4533 . . . . . 6 (𝑥 = 0 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))))
326323, 217eqbrtrdi 5182 . . . . . . 7 (𝑥 = 0 → 𝑥 ≤ (1 / 4))
327326iftrued 4533 . . . . . 6 (𝑥 = 0 → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (2 · 𝑥))
328 oveq2 7439 . . . . . . 7 (𝑥 = 0 → (2 · 𝑥) = (2 · 0))
329 2t0e0 12435 . . . . . . 7 (2 · 0) = 0
330328, 329eqtrdi 2793 . . . . . 6 (𝑥 = 0 → (2 · 𝑥) = 0)
331325, 327, 3303eqtrd 2781 . . . . 5 (𝑥 = 0 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = 0)
332 c0ex 11255 . . . . 5 0 ∈ V
333331, 186, 332fvmpt 7016 . . . 4 (0 ∈ (0[,]1) → (𝑃‘0) = 0)
334191, 333syl 17 . . 3 (𝜑 → (𝑃‘0) = 0)
335147a1i 11 . . . 4 (𝜑 → 1 ∈ (0[,]1))
33659, 85ltnlei 11382 . . . . . . . . 9 ((1 / 2) < 1 ↔ ¬ 1 ≤ (1 / 2))
337143, 336mpbi 230 . . . . . . . 8 ¬ 1 ≤ (1 / 2)
338 breq1 5146 . . . . . . . 8 (𝑥 = 1 → (𝑥 ≤ (1 / 2) ↔ 1 ≤ (1 / 2)))
339337, 338mtbiri 327 . . . . . . 7 (𝑥 = 1 → ¬ 𝑥 ≤ (1 / 2))
340339iffalsed 4536 . . . . . 6 (𝑥 = 1 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = ((𝑥 / 2) + (1 / 2)))
341 oveq1 7438 . . . . . . . 8 (𝑥 = 1 → (𝑥 / 2) = (1 / 2))
342341oveq1d 7446 . . . . . . 7 (𝑥 = 1 → ((𝑥 / 2) + (1 / 2)) = ((1 / 2) + (1 / 2)))
343342, 83eqtrdi 2793 . . . . . 6 (𝑥 = 1 → ((𝑥 / 2) + (1 / 2)) = 1)
344340, 343eqtrd 2777 . . . . 5 (𝑥 = 1 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = 1)
345 1ex 11257 . . . . 5 1 ∈ V
346344, 186, 345fvmpt 7016 . . . 4 (1 ∈ (0[,]1) → (𝑃‘1) = 1)
347335, 346syl 17 . . 3 (𝜑 → (𝑃‘1) = 1)
348313, 306, 334, 347reparpht 25031 . 2 (𝜑 → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)) ∘ 𝑃)( ≃ph𝐽)(𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)))
349322, 348eqbrtrd 5165 1 (𝜑 → ((𝐹(*𝑝𝐽)𝐺)(*𝑝𝐽)𝐻)( ≃ph𝐽)(𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wo 848   = wceq 1540  wcel 2108  wne 2940  wral 3061  Vcvv 3480  wss 3951  ifcif 4525   cuni 4907   class class class wbr 5143  cmpt 5225  ran crn 5686  ccom 5689  wf 6557  cfv 6561  (class class class)co 7431  cc 11153  cr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160  *cxr 11294   < clt 11295  cle 11296  cmin 11492   / cdiv 11920  cn 12266  2c2 12321  4c4 12323  (,)cioo 13387  [,]cicc 13390  t crest 17465  TopOpenctopn 17466  topGenctg 17482  fldccnfld 21364  Topctop 22899  TopOnctopon 22916   Cn ccn 23232   ×t ctx 23568  IIcii 24901  phcphtpc 25001  *𝑝cpco 25033
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233  ax-addf 11234
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-er 8745  df-map 8868  df-ixp 8938  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-fi 9451  df-sup 9482  df-inf 9483  df-oi 9550  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-z 12614  df-dec 12734  df-uz 12879  df-q 12991  df-rp 13035  df-xneg 13154  df-xadd 13155  df-xmul 13156  df-ioo 13391  df-icc 13394  df-fz 13548  df-fzo 13695  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-struct 17184  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-mulr 17311  df-starv 17312  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-hom 17321  df-cco 17322  df-rest 17467  df-topn 17468  df-0g 17486  df-gsum 17487  df-topgen 17488  df-pt 17489  df-prds 17492  df-xrs 17547  df-qtop 17552  df-imas 17553  df-xps 17555  df-mre 17629  df-mrc 17630  df-acs 17632  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-submnd 18797  df-mulg 19086  df-cntz 19335  df-cmn 19800  df-psmet 21356  df-xmet 21357  df-met 21358  df-bl 21359  df-mopn 21360  df-cnfld 21365  df-top 22900  df-topon 22917  df-topsp 22939  df-bases 22953  df-cld 23027  df-cn 23235  df-cnp 23236  df-tx 23570  df-hmeo 23763  df-xms 24330  df-ms 24331  df-tms 24332  df-ii 24903  df-htpy 25002  df-phtpy 25003  df-phtpc 25024  df-pco 25038
This theorem is referenced by:  pcophtb  25062  pi1grplem  25082  pi1xfr  25088  pi1xfrcnvlem  25089
  Copyright terms: Public domain W3C validator