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

Theorem pcoass 23331
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 4356 . . . . . . . . . . 11 (𝑥 ≤ (1 / 4) → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (2 · 𝑥))
21fveq2d 6503 . . . . . . . . . 10 (𝑥 ≤ (1 / 4) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(2 · 𝑥)))
32adantl 474 . . . . . . . . 9 (((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(2 · 𝑥)))
4 2cn 11515 . . . . . . . . . . . . 13 2 ∈ ℂ
5 elicc01 12670 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (0[,]1) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥𝑥 ≤ 1))
65simp1bi 1125 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0[,]1) → 𝑥 ∈ ℝ)
76adantr 473 . . . . . . . . . . . . . 14 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℝ)
87recnd 10468 . . . . . . . . . . . . 13 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℂ)
9 mulcom 10421 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) = (𝑥 · 2))
104, 8, 9sylancr 578 . . . . . . . . . . . 12 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) = (𝑥 · 2))
115simp2bi 1126 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0[,]1) → 0 ≤ 𝑥)
1211adantr 473 . . . . . . . . . . . . . 14 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 0 ≤ 𝑥)
13 simpr 477 . . . . . . . . . . . . . 14 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ≤ (1 / 4))
14 0re 10441 . . . . . . . . . . . . . . 15 0 ∈ ℝ
15 4nn 11524 . . . . . . . . . . . . . . . 16 4 ∈ ℕ
16 nnrecre 11482 . . . . . . . . . . . . . . . 16 (4 ∈ ℕ → (1 / 4) ∈ ℝ)
1715, 16ax-mp 5 . . . . . . . . . . . . . . 15 (1 / 4) ∈ ℝ
1814, 17elicc2i 12618 . . . . . . . . . . . . . 14 (𝑥 ∈ (0[,](1 / 4)) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥𝑥 ≤ (1 / 4)))
197, 12, 13, 18syl3anbrc 1323 . . . . . . . . . . . . 13 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ (0[,](1 / 4)))
20 2rp 12209 . . . . . . . . . . . . . 14 2 ∈ ℝ+
214mul02i 10629 . . . . . . . . . . . . . 14 (0 · 2) = 0
2217recni 10454 . . . . . . . . . . . . . . 15 (1 / 4) ∈ ℂ
23222timesi 11585 . . . . . . . . . . . . . . . 16 (2 · (1 / 4)) = ((1 / 4) + (1 / 4))
24 2ne0 11551 . . . . . . . . . . . . . . . . . . . 20 2 ≠ 0
25 recdiv2 11154 . . . . . . . . . . . . . . . . . . . 20 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((1 / 2) / 2) = (1 / (2 · 2)))
264, 24, 4, 24, 25mp4an 680 . . . . . . . . . . . . . . . . . . 19 ((1 / 2) / 2) = (1 / (2 · 2))
27 2t2e4 11611 . . . . . . . . . . . . . . . . . . . 20 (2 · 2) = 4
2827oveq2i 6987 . . . . . . . . . . . . . . . . . . 19 (1 / (2 · 2)) = (1 / 4)
2926, 28eqtri 2803 . . . . . . . . . . . . . . . . . 18 ((1 / 2) / 2) = (1 / 4)
3029, 29oveq12i 6988 . . . . . . . . . . . . . . . . 17 (((1 / 2) / 2) + ((1 / 2) / 2)) = ((1 / 4) + (1 / 4))
31 halfcn 11662 . . . . . . . . . . . . . . . . . 18 (1 / 2) ∈ ℂ
32 2halves 11675 . . . . . . . . . . . . . . . . . 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 2805 . . . . . . . . . . . . . . . 16 ((1 / 4) + (1 / 4)) = (1 / 2)
3523, 34eqtri 2803 . . . . . . . . . . . . . . 15 (2 · (1 / 4)) = (1 / 2)
364, 22, 35mulcomli 10449 . . . . . . . . . . . . . 14 ((1 / 4) · 2) = (1 / 2)
3714, 17, 20, 21, 36iccdili 12693 . . . . . . . . . . . . 13 (𝑥 ∈ (0[,](1 / 4)) → (𝑥 · 2) ∈ (0[,](1 / 2)))
3819, 37syl 17 . . . . . . . . . . . 12 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → (𝑥 · 2) ∈ (0[,](1 / 2)))
3910, 38eqeltrd 2867 . . . . . . . . . . 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 23324 . . . . . . . . . . . . 13 (𝜑 → (𝐺(*𝑝𝐽)𝐻) ∈ (II Cn 𝐽))
4540, 44pcoval1 23320 . . . . . . . . . . . 12 ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(2 · 𝑥)) = (𝐹‘(2 · (2 · 𝑥))))
4640, 41pcoval1 23320 . . . . . . . . . . . 12 ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) → ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)) = (𝐹‘(2 · (2 · 𝑥))))
4745, 46eqtr4d 2818 . . . . . . . . . . 11 ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
4839, 47sylan2 583 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4))) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
4948anassrs 460 . . . . . . . . 9 (((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
503, 49eqtrd 2815 . . . . . . . 8 (((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
5150adantlr 702 . . . . . . 7 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
52 simplll 762 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝜑)
536ad2antlr 714 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → 𝑥 ∈ ℝ)
5453adantr 473 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℝ)
55 letric 10540 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ (1 / 4) ∈ ℝ) → (𝑥 ≤ (1 / 4) ∨ (1 / 4) ≤ 𝑥))
5653, 17, 55sylancl 577 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → (𝑥 ≤ (1 / 4) ∨ (1 / 4) ≤ 𝑥))
5756orcanai 985 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (1 / 4) ≤ 𝑥)
58 simplr 756 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ≤ (1 / 2))
59 halfre 11661 . . . . . . . . . . . . 13 (1 / 2) ∈ ℝ
6017, 59elicc2i 12618 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 4)[,](1 / 2)) ↔ (𝑥 ∈ ℝ ∧ (1 / 4) ≤ 𝑥𝑥 ≤ (1 / 2)))
6154, 57, 58, 60syl3anbrc 1323 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ((1 / 4)[,](1 / 2)))
6260simp1bi 1125 . . . . . . . . . . . . 13 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → 𝑥 ∈ ℝ)
63 readdcl 10418 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ (1 / 4) ∈ ℝ) → (𝑥 + (1 / 4)) ∈ ℝ)
6462, 17, 63sylancl 577 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ∈ ℝ)
6517a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 4) ∈ ℝ)
6660simp2bi 1126 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 4) ≤ 𝑥)
6765, 62, 65, 66leadd1dd 11055 . . . . . . . . . . . . 13 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → ((1 / 4) + (1 / 4)) ≤ (𝑥 + (1 / 4)))
6834, 67syl5eqbrr 4965 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 2) ≤ (𝑥 + (1 / 4)))
6959a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 2) ∈ ℝ)
7060simp3bi 1127 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → 𝑥 ≤ (1 / 2))
71 2lt4 11622 . . . . . . . . . . . . . . . . 17 2 < 4
72 2re 11514 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
73 4re 11525 . . . . . . . . . . . . . . . . . 18 4 ∈ ℝ
74 2pos 11550 . . . . . . . . . . . . . . . . . 18 0 < 2
75 4pos 11554 . . . . . . . . . . . . . . . . . 18 0 < 4
7672, 73, 74, 75ltrecii 11357 . . . . . . . . . . . . . . . . 17 (2 < 4 ↔ (1 / 4) < (1 / 2))
7771, 76mpbi 222 . . . . . . . . . . . . . . . 16 (1 / 4) < (1 / 2)
7817, 59, 77ltleii 10563 . . . . . . . . . . . . . . 15 (1 / 4) ≤ (1 / 2)
7978a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 4) ≤ (1 / 2))
8062, 65, 69, 69, 70, 79le2addd 11060 . . . . . . . . . . . . 13 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ≤ ((1 / 2) + (1 / 2)))
81 ax-1cn 10393 . . . . . . . . . . . . . 14 1 ∈ ℂ
82 2halves 11675 . . . . . . . . . . . . . 14 (1 ∈ ℂ → ((1 / 2) + (1 / 2)) = 1)
8381, 82ax-mp 5 . . . . . . . . . . . . 13 ((1 / 2) + (1 / 2)) = 1
8480, 83syl6breq 4970 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ≤ 1)
85 1re 10439 . . . . . . . . . . . . 13 1 ∈ ℝ
8659, 85elicc2i 12618 . . . . . . . . . . . 12 ((𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1) ↔ ((𝑥 + (1 / 4)) ∈ ℝ ∧ (1 / 2) ≤ (𝑥 + (1 / 4)) ∧ (𝑥 + (1 / 4)) ≤ 1))
8764, 68, 84, 86syl3anbrc 1323 . . . . . . . . . . 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 23321 . . . . . . . . . . . 12 (𝜑 → ((𝐺(*𝑝𝐽)𝐻)‘0) = (𝐺‘0))
9189, 90eqtr4d 2818 . . . . . . . . . . 11 (𝜑 → (𝐹‘1) = ((𝐺(*𝑝𝐽)𝐻)‘0))
9240, 44, 91pcoval2 23323 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(𝑥 + (1 / 4))) = ((𝐺(*𝑝𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)))
9352, 88, 92syl2anc 576 . . . . . . . . 9 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(𝑥 + (1 / 4))) = ((𝐺(*𝑝𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)))
9483oveq2i 6987 . . . . . . . . . . . 12 ((2 · (𝑥 + (1 / 4))) − ((1 / 2) + (1 / 2))) = ((2 · (𝑥 + (1 / 4))) − 1)
95 2cnd 11518 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 2 ∈ ℂ)
9654recnd 10468 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℂ)
9722a1i 11 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (1 / 4) ∈ ℂ)
9895, 96, 97adddid 10464 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · (𝑥 + (1 / 4))) = ((2 · 𝑥) + (2 · (1 / 4))))
9935oveq2i 6987 . . . . . . . . . . . . . 14 ((2 · 𝑥) + (2 · (1 / 4))) = ((2 · 𝑥) + (1 / 2))
10098, 99syl6eq 2831 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · (𝑥 + (1 / 4))) = ((2 · 𝑥) + (1 / 2)))
101100oveq1d 6991 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − ((1 / 2) + (1 / 2))) = (((2 · 𝑥) + (1 / 2)) − ((1 / 2) + (1 / 2))))
10294, 101syl5eqr 2829 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − 1) = (((2 · 𝑥) + (1 / 2)) − ((1 / 2) + (1 / 2))))
103 remulcl 10420 . . . . . . . . . . . . . 14 ((2 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (2 · 𝑥) ∈ ℝ)
10472, 54, 103sylancr 578 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈ ℝ)
105104recnd 10468 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈ ℂ)
10631a1i 11 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (1 / 2) ∈ ℂ)
107105, 106, 106pnpcan2d 10836 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (((2 · 𝑥) + (1 / 2)) − ((1 / 2) + (1 / 2))) = ((2 · 𝑥) − (1 / 2)))
108102, 107eqtrd 2815 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − 1) = ((2 · 𝑥) − (1 / 2)))
109108fveq2d 6503 . . . . . . . . 9 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(*𝑝𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)) = ((𝐺(*𝑝𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))))
1104, 96, 9sylancr 578 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) = (𝑥 · 2))
11181, 4, 24divcan1i 11185 . . . . . . . . . . . . . . 15 ((1 / 2) · 2) = 1
11217, 59, 20, 36, 111iccdili 12693 . . . . . . . . . . . . . 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 2867 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈ ((1 / 2)[,]1))
11531subidi 10758 . . . . . . . . . . . . 13 ((1 / 2) − (1 / 2)) = 0
116 1mhlfehlf 11666 . . . . . . . . . . . . 13 (1 − (1 / 2)) = (1 / 2)
11759, 85, 59, 115, 116iccshftli 12691 . . . . . . . . . . . 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 23320 . . . . . . . . . . 11 ((𝜑 ∧ ((2 · 𝑥) − (1 / 2)) ∈ (0[,](1 / 2))) → ((𝐺(*𝑝𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))))
12052, 118, 119syl2anc 576 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(*𝑝𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))))
12195, 105, 106subdid 10897 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · ((2 · 𝑥) − (1 / 2))) = ((2 · (2 · 𝑥)) − (2 · (1 / 2))))
1224, 24recidi 11172 . . . . . . . . . . . . 13 (2 · (1 / 2)) = 1
123122oveq2i 6987 . . . . . . . . . . . 12 ((2 · (2 · 𝑥)) − (2 · (1 / 2))) = ((2 · (2 · 𝑥)) − 1)
124121, 123syl6eq 2831 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · ((2 · 𝑥) − (1 / 2))) = ((2 · (2 · 𝑥)) − 1))
125124fveq2d 6503 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
126120, 125eqtrd 2815 . . . . . . . . 9 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(*𝑝𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
12793, 109, 1263eqtrd 2819 . . . . . . . 8 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(𝑥 + (1 / 4))) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
128 iffalse 4359 . . . . . . . . . 10 𝑥 ≤ (1 / 4) → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (𝑥 + (1 / 4)))
129128fveq2d 6503 . . . . . . . . 9 𝑥 ≤ (1 / 4) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(𝑥 + (1 / 4))))
130129adantl 474 . . . . . . . 8 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(𝑥 + (1 / 4))))
13140, 41, 89pcoval2 23323 . . . . . . . . 9 ((𝜑 ∧ (2 · 𝑥) ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
13252, 114, 131syl2anc 576 . . . . . . . 8 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
133127, 130, 1323eqtr4d 2825 . . . . . . 7 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
13451, 133pm2.61dan 800 . . . . . 6 (((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
135 iftrue 4356 . . . . . . . 8 (𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))))
136135fveq2d 6503 . . . . . . 7 (𝑥 ≤ (1 / 2) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))))
137136adantl 474 . . . . . 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 4356 . . . . . . 7 (𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
139138adantl 474 . . . . . 6 (((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
140134, 137, 1393eqtr4d 2825 . . . . 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 23243 . . . . . . . 8 ((𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 ≤ (1 / 2)) → 𝑥 ∈ ((1 / 2)[,]1))
142 halfge0 11664 . . . . . . . . . . . . . 14 0 ≤ (1 / 2)
143 halflt1 11665 . . . . . . . . . . . . . . 15 (1 / 2) < 1
14459, 85, 143ltleii 10563 . . . . . . . . . . . . . 14 (1 / 2) ≤ 1
145 elicc01 12670 . . . . . . . . . . . . . 14 ((1 / 2) ∈ (0[,]1) ↔ ((1 / 2) ∈ ℝ ∧ 0 ≤ (1 / 2) ∧ (1 / 2) ≤ 1))
14659, 142, 144, 145mpbir3an 1321 . . . . . . . . . . . . 13 (1 / 2) ∈ (0[,]1)
147 1elunit 12672 . . . . . . . . . . . . 13 1 ∈ (0[,]1)
148 iccss2 12623 . . . . . . . . . . . . 13 (((1 / 2) ∈ (0[,]1) ∧ 1 ∈ (0[,]1)) → ((1 / 2)[,]1) ⊆ (0[,]1))
149146, 147, 148mp2an 679 . . . . . . . . . . . 12 ((1 / 2)[,]1) ⊆ (0[,]1)
150149sseli 3855 . . . . . . . . . . 11 (𝑥 ∈ ((1 / 2)[,]1) → 𝑥 ∈ (0[,]1))
1514, 24div0i 11175 . . . . . . . . . . . 12 (0 / 2) = 0
152 eqid 2779 . . . . . . . . . . . 12 (1 / 2) = (1 / 2)
15314, 85, 20, 151, 152icccntri 12695 . . . . . . . . . . 11 (𝑥 ∈ (0[,]1) → (𝑥 / 2) ∈ (0[,](1 / 2)))
15431addid2i 10628 . . . . . . . . . . . 12 (0 + (1 / 2)) = (1 / 2)
15514, 59, 59, 154, 83iccshftri 12689 . . . . . . . . . . 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 23323 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 / 2) + (1 / 2)) ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = ((𝐺(*𝑝𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)))
158156, 157sylan2 583 . . . . . . . . 9 ((𝜑𝑥 ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = ((𝐺(*𝑝𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)))
15959, 85elicc2i 12618 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 2)[,]1) ↔ (𝑥 ∈ ℝ ∧ (1 / 2) ≤ 𝑥𝑥 ≤ 1))
160159simp1bi 1125 . . . . . . . . . . . . 13 (𝑥 ∈ ((1 / 2)[,]1) → 𝑥 ∈ ℝ)
161160recnd 10468 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 2)[,]1) → 𝑥 ∈ ℂ)
162 1cnd 10434 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 2)[,]1) → 1 ∈ ℂ)
163 2cnd 11518 . . . . . . . . . . . . . . 15 (𝑥 ∈ ((1 / 2)[,]1) → 2 ∈ ℂ)
16424a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ ((1 / 2)[,]1) → 2 ≠ 0)
165161, 162, 163, 164divdird 11255 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 2)[,]1) → ((𝑥 + 1) / 2) = ((𝑥 / 2) + (1 / 2)))
166165oveq2d 6992 . . . . . . . . . . . . 13 (𝑥 ∈ ((1 / 2)[,]1) → (2 · ((𝑥 + 1) / 2)) = (2 · ((𝑥 / 2) + (1 / 2))))
167 peano2cn 10612 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℂ → (𝑥 + 1) ∈ ℂ)
168161, 167syl 17 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 2)[,]1) → (𝑥 + 1) ∈ ℂ)
169168, 163, 164divcan2d 11219 . . . . . . . . . . . . 13 (𝑥 ∈ ((1 / 2)[,]1) → (2 · ((𝑥 + 1) / 2)) = (𝑥 + 1))
170166, 169eqtr3d 2817 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 2)[,]1) → (2 · ((𝑥 / 2) + (1 / 2))) = (𝑥 + 1))
171161, 162, 170mvrraddd 10853 . . . . . . . . . . 11 (𝑥 ∈ ((1 / 2)[,]1) → ((2 · ((𝑥 / 2) + (1 / 2))) − 1) = 𝑥)
172171fveq2d 6503 . . . . . . . . . 10 (𝑥 ∈ ((1 / 2)[,]1) → ((𝐺(*𝑝𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)) = ((𝐺(*𝑝𝐽)𝐻)‘𝑥))
173172adantl 474 . . . . . . . . 9 ((𝜑𝑥 ∈ ((1 / 2)[,]1)) → ((𝐺(*𝑝𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)) = ((𝐺(*𝑝𝐽)𝐻)‘𝑥))
17441, 42, 43pcoval2 23323 . . . . . . . . 9 ((𝜑𝑥 ∈ ((1 / 2)[,]1)) → ((𝐺(*𝑝𝐽)𝐻)‘𝑥) = (𝐻‘((2 · 𝑥) − 1)))
175158, 173, 1743eqtrd 2819 . . . . . . . 8 ((𝜑𝑥 ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1)))
176141, 175sylan2 583 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 ≤ (1 / 2))) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1)))
177176anassrs 460 . . . . . 6 (((𝜑𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1)))
178 iffalse 4359 . . . . . . . 8 𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = ((𝑥 / 2) + (1 / 2)))
179178fveq2d 6503 . . . . . . 7 𝑥 ≤ (1 / 2) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))))
180179adantl 474 . . . . . 6 (((𝜑𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))))
181 iffalse 4359 . . . . . . 7 𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = (𝐻‘((2 · 𝑥) − 1)))
182181adantl 474 . . . . . 6 (((𝜑𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = (𝐻‘((2 · 𝑥) − 1)))
183177, 180, 1823eqtr4d 2825 . . . . 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 800 . . . 4 ((𝜑𝑥 ∈ (0[,]1)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))))
185184mpteq2dva 5022 . . 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 23190 . . . . . . . . 9 II ∈ (TopOn‘(0[,]1))
188187a1i 11 . . . . . . . 8 (𝜑 → II ∈ (TopOn‘(0[,]1)))
189188cnmptid 21973 . . . . . . . 8 (𝜑 → (𝑥 ∈ (0[,]1) ↦ 𝑥) ∈ (II Cn II))
190 0elunit 12671 . . . . . . . . . 10 0 ∈ (0[,]1)
191190a1i 11 . . . . . . . . 9 (𝜑 → 0 ∈ (0[,]1))
192188, 188, 191cnmptc 21974 . . . . . . . 8 (𝜑 → (𝑥 ∈ (0[,]1) ↦ 0) ∈ (II Cn II))
193 eqid 2779 . . . . . . . . 9 (topGen‘ran (,)) = (topGen‘ran (,))
194 eqid 2779 . . . . . . . . 9 ((topGen‘ran (,)) ↾t (0[,](1 / 2))) = ((topGen‘ran (,)) ↾t (0[,](1 / 2)))
195 eqid 2779 . . . . . . . . 9 ((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) = ((topGen‘ran (,)) ↾t ((1 / 2)[,]1))
196 dfii2 23193 . . . . . . . . 9 II = ((topGen‘ran (,)) ↾t (0[,]1))
197 0red 10443 . . . . . . . . 9 (𝜑 → 0 ∈ ℝ)
198 1red 10440 . . . . . . . . 9 (𝜑 → 1 ∈ ℝ)
199146a1i 11 . . . . . . . . 9 (𝜑 → (1 / 2) ∈ (0[,]1))
200 simprl 758 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → 𝑦 = (1 / 2))
201200oveq1d 6991 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 2) + (1 / 4)))
20231, 22addcomi 10631 . . . . . . . . . . 11 ((1 / 2) + (1 / 4)) = ((1 / 4) + (1 / 2))
203201, 202syl6eq 2831 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 4) + (1 / 2)))
20417, 59ltnlei 10561 . . . . . . . . . . . . 13 ((1 / 4) < (1 / 2) ↔ ¬ (1 / 2) ≤ (1 / 4))
20577, 204mpbi 222 . . . . . . . . . . . 12 ¬ (1 / 2) ≤ (1 / 4)
206200breq1d 4939 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 ≤ (1 / 4) ↔ (1 / 2) ≤ (1 / 4)))
207205, 206mtbiri 319 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → ¬ 𝑦 ≤ (1 / 4))
208207iffalsed 4361 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))) = (𝑦 + (1 / 4)))
209200oveq1d 6991 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 / 2) = ((1 / 2) / 2))
210209, 29syl6eq 2831 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 / 2) = (1 / 4))
211210oveq1d 6991 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → ((𝑦 / 2) + (1 / 2)) = ((1 / 4) + (1 / 2)))
212203, 208, 2113eqtr4d 2825 . . . . . . . . 9 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))) = ((𝑦 / 2) + (1 / 2)))
213 eqid 2779 . . . . . . . . . 10 ((topGen‘ran (,)) ↾t (0[,](1 / 4))) = ((topGen‘ran (,)) ↾t (0[,](1 / 4)))
214 eqid 2779 . . . . . . . . . 10 ((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2))) = ((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2)))
21559a1i 11 . . . . . . . . . 10 (𝜑 → (1 / 2) ∈ ℝ)
21673, 75recgt0ii 11347 . . . . . . . . . . . . 13 0 < (1 / 4)
21714, 17, 216ltleii 10563 . . . . . . . . . . . 12 0 ≤ (1 / 4)
21814, 59elicc2i 12618 . . . . . . . . . . . 12 ((1 / 4) ∈ (0[,](1 / 2)) ↔ ((1 / 4) ∈ ℝ ∧ 0 ≤ (1 / 4) ∧ (1 / 4) ≤ (1 / 2)))
21917, 217, 78, 218mpbir3an 1321 . . . . . . . . . . 11 (1 / 4) ∈ (0[,](1 / 2))
220219a1i 11 . . . . . . . . . 10 (𝜑 → (1 / 4) ∈ (0[,](1 / 2)))
221 simprl 758 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → 𝑦 = (1 / 4))
222221oveq2d 6992 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = (2 · (1 / 4)))
223221oveq1d 6991 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 4) + (1 / 4)))
22423, 222, 2233eqtr4a 2841 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = (𝑦 + (1 / 4)))
225 retopon 23075 . . . . . . . . . . . . 13 (topGen‘ran (,)) ∈ (TopOn‘ℝ)
226 0xr 10487 . . . . . . . . . . . . . . . 16 0 ∈ ℝ*
22759rexri 10499 . . . . . . . . . . . . . . . 16 (1 / 2) ∈ ℝ*
228 lbicc2 12668 . . . . . . . . . . . . . . . 16 ((0 ∈ ℝ* ∧ (1 / 2) ∈ ℝ* ∧ 0 ≤ (1 / 2)) → 0 ∈ (0[,](1 / 2)))
229226, 227, 142, 228mp3an 1440 . . . . . . . . . . . . . . 15 0 ∈ (0[,](1 / 2))
230 iccss2 12623 . . . . . . . . . . . . . . 15 ((0 ∈ (0[,](1 / 2)) ∧ (1 / 4) ∈ (0[,](1 / 2))) → (0[,](1 / 4)) ⊆ (0[,](1 / 2)))
231229, 219, 230mp2an 679 . . . . . . . . . . . . . 14 (0[,](1 / 4)) ⊆ (0[,](1 / 2))
232 iccssre 12634 . . . . . . . . . . . . . . 15 ((0 ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (0[,](1 / 2)) ⊆ ℝ)
23314, 59, 232mp2an 679 . . . . . . . . . . . . . 14 (0[,](1 / 2)) ⊆ ℝ
234231, 233sstri 3868 . . . . . . . . . . . . 13 (0[,](1 / 4)) ⊆ ℝ
235 resttopon 21473 . . . . . . . . . . . . 13 (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 / 4)) ⊆ ℝ) → ((topGen‘ran (,)) ↾t (0[,](1 / 4))) ∈ (TopOn‘(0[,](1 / 4))))
236225, 234, 235mp2an 679 . . . . . . . . . . . 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 21980 . . . . . . . . . . 11 (𝜑 → (𝑦 ∈ (0[,](1 / 4)), 𝑧 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,)) ↾t (0[,](1 / 4))) ×t II) Cn ((topGen‘ran (,)) ↾t (0[,](1 / 4)))))
239 retop 23073 . . . . . . . . . . . . . 14 (topGen‘ran (,)) ∈ Top
240 ovex 7008 . . . . . . . . . . . . . 14 (0[,](1 / 2)) ∈ V
241 restabs 21477 . . . . . . . . . . . . . 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 1440 . . . . . . . . . . . . 13 (((topGen‘ran (,)) ↾t (0[,](1 / 2))) ↾t (0[,](1 / 4))) = ((topGen‘ran (,)) ↾t (0[,](1 / 4)))
243242eqcomi 2788 . . . . . . . . . . . 12 ((topGen‘ran (,)) ↾t (0[,](1 / 4))) = (((topGen‘ran (,)) ↾t (0[,](1 / 2))) ↾t (0[,](1 / 4)))
244 resttopon 21473 . . . . . . . . . . . . . 14 (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 / 2)) ⊆ ℝ) → ((topGen‘ran (,)) ↾t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 / 2))))
245225, 233, 244mp2an 679 . . . . . . . . . . . . 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 23239 . . . . . . . . . . . . 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 21988 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ (0[,](1 / 4)) ↦ (2 · 𝑥)) ∈ (((topGen‘ran (,)) ↾t (0[,](1 / 4))) Cn II))
251 oveq2 6984 . . . . . . . . . . 11 (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
252237, 188, 238, 237, 250, 251cnmpt21 21983 . . . . . . . . . 10 (𝜑 → (𝑦 ∈ (0[,](1 / 4)), 𝑧 ∈ (0[,]1) ↦ (2 · 𝑦)) ∈ ((((topGen‘ran (,)) ↾t (0[,](1 / 4))) ×t II) Cn II))
253 iccssre 12634 . . . . . . . . . . . . . 14 (((1 / 4) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → ((1 / 4)[,](1 / 2)) ⊆ ℝ)
25417, 59, 253mp2an 679 . . . . . . . . . . . . 13 ((1 / 4)[,](1 / 2)) ⊆ ℝ
255 resttopon 21473 . . . . . . . . . . . . 13 (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 / 4)[,](1 / 2)) ⊆ ℝ) → ((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2))) ∈ (TopOn‘((1 / 4)[,](1 / 2))))
256225, 254, 255mp2an 679 . . . . . . . . . . . 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 21980 . . . . . . . . . . 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 2779 . . . . . . . . . . . 12 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
260254a1i 11 . . . . . . . . . . . 12 (𝜑 → ((1 / 4)[,](1 / 2)) ⊆ ℝ)
261 unitssre 12701 . . . . . . . . . . . . 13 (0[,]1) ⊆ ℝ
262261a1i 11 . . . . . . . . . . . 12 (𝜑 → (0[,]1) ⊆ ℝ)
263149, 87sseldi 3857 . . . . . . . . . . . . 13 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ∈ (0[,]1))
264263adantl 474 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((1 / 4)[,](1 / 2))) → (𝑥 + (1 / 4)) ∈ (0[,]1))
265259cnfldtopon 23094 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
266265a1i 11 . . . . . . . . . . . . 13 (𝜑 → (TopOpen‘ℂfld) ∈ (TopOn‘ℂ))
267266cnmptid 21973 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ ℂ ↦ 𝑥) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
26817a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (1 / 4) ∈ ℝ)
269268recnd 10468 . . . . . . . . . . . . . 14 (𝜑 → (1 / 4) ∈ ℂ)
270266, 266, 269cnmptc 21974 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ ℂ ↦ (1 / 4)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
271259addcn 23176 . . . . . . . . . . . . . 14 + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
272271a1i 11 . . . . . . . . . . . . 13 (𝜑 → + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
273266, 267, 270, 272cnmpt12f 21978 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ ℂ ↦ (𝑥 + (1 / 4))) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
274259, 214, 196, 260, 262, 264, 273cnmptre 23234 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ ((1 / 4)[,](1 / 2)) ↦ (𝑥 + (1 / 4))) ∈ (((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2))) Cn II))
275 oveq1 6983 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑥 + (1 / 4)) = (𝑦 + (1 / 4)))
276257, 188, 258, 257, 274, 275cnmpt21 21983 . . . . . . . . . 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 23235 . . . . . . . . 9 (𝜑 → (𝑦 ∈ (0[,](1 / 2)), 𝑧 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4)))) ∈ ((((topGen‘ran (,)) ↾t (0[,](1 / 2))) ×t II) Cn II))
278 iccssre 12634 . . . . . . . . . . . . 13 (((1 / 2) ∈ ℝ ∧ 1 ∈ ℝ) → ((1 / 2)[,]1) ⊆ ℝ)
27959, 85, 278mp2an 679 . . . . . . . . . . . 12 ((1 / 2)[,]1) ⊆ ℝ
280 resttopon 21473 . . . . . . . . . . . 12 (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 / 2)[,]1) ⊆ ℝ) → ((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1)))
281225, 279, 280mp2an 679 . . . . . . . . . . 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 21980 . . . . . . . . . 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, 156sseldi 3857 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 2)[,]1) → ((𝑥 / 2) + (1 / 2)) ∈ (0[,]1))
286285adantl 474 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((1 / 2)[,]1)) → ((𝑥 / 2) + (1 / 2)) ∈ (0[,]1))
287259divccn 23184 . . . . . . . . . . . . . 14 ((2 ∈ ℂ ∧ 2 ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
2884, 24, 287mp2an 679 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld))
289288a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
29031a1i 11 . . . . . . . . . . . . 13 (𝜑 → (1 / 2) ∈ ℂ)
291266, 266, 290cnmptc 21974 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ ℂ ↦ (1 / 2)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
292266, 289, 291, 272cnmpt12f 21978 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ ℂ ↦ ((𝑥 / 2) + (1 / 2))) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
293259, 195, 196, 284, 262, 286, 292cnmptre 23234 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ ((1 / 2)[,]1) ↦ ((𝑥 / 2) + (1 / 2))) ∈ (((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) Cn II))
294 oveq1 6983 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑥 / 2) = (𝑦 / 2))
295294oveq1d 6991 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝑥 / 2) + (1 / 2)) = ((𝑦 / 2) + (1 / 2)))
296282, 188, 283, 282, 293, 295cnmpt21 21983 . . . . . . . . 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 23235 . . . . . . . 8 (𝜑 → (𝑦 ∈ (0[,]1), 𝑧 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 2), if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))), ((𝑦 / 2) + (1 / 2)))) ∈ ((II ×t II) Cn II))
298 breq1 4932 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥 ≤ (1 / 2) ↔ 𝑦 ≤ (1 / 2)))
299 breq1 4932 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑥 ≤ (1 / 4) ↔ 𝑦 ≤ (1 / 4)))
300299, 251, 275ifbieq12d 4377 . . . . . . . . . . . 12 (𝑥 = 𝑦 → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))))
301298, 300, 295ifbieq12d 4377 . . . . . . . . . . 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 1977 . . . . . . . . . 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 473 . . . . . . . . 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 2785 . . . . . . . 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 21979 . . . . . . 7 (𝜑 → (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) ∈ (II Cn II))
306186, 305syl5eqel 2871 . . . . . 6 (𝜑𝑃 ∈ (II Cn II))
307 iiuni 23192 . . . . . . 7 (0[,]1) = II
308307, 307cnf 21558 . . . . . 6 (𝑃 ∈ (II Cn II) → 𝑃:(0[,]1)⟶(0[,]1))
309306, 308syl 17 . . . . 5 (𝜑𝑃:(0[,]1)⟶(0[,]1))
310186fmpt 6697 . . . . 5 (∀𝑥 ∈ (0[,]1)if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) ∈ (0[,]1) ↔ 𝑃:(0[,]1)⟶(0[,]1))
311309, 310sylibr 226 . . . 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 23324 . . . . . 6 (𝜑 → (𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)) ∈ (II Cn 𝐽))
314 eqid 2779 . . . . . . 7 𝐽 = 𝐽
315307, 314cnf 21558 . . . . . 6 ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)) ∈ (II Cn 𝐽) → (𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)):(0[,]1)⟶ 𝐽)
316313, 315syl 17 . . . . 5 (𝜑 → (𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)):(0[,]1)⟶ 𝐽)
317316feqmptd 6562 . . . 4 (𝜑 → (𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)) = (𝑦 ∈ (0[,]1) ↦ ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘𝑦)))
318 fveq2 6499 . . . 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 6715 . . 3 (𝜑 → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)) ∘ 𝑃) = (𝑥 ∈ (0[,]1) ↦ ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))))))
32040, 41, 89pcocn 23324 . . . 4 (𝜑 → (𝐹(*𝑝𝐽)𝐺) ∈ (II Cn 𝐽))
321320, 42pcoval 23318 . . 3 (𝜑 → ((𝐹(*𝑝𝐽)𝐺)(*𝑝𝐽)𝐻) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1)))))
322185, 319, 3213eqtr4rd 2826 . 2 (𝜑 → ((𝐹(*𝑝𝐽)𝐺)(*𝑝𝐽)𝐻) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)) ∘ 𝑃))
323 id 22 . . . . . . . 8 (𝑥 = 0 → 𝑥 = 0)
324323, 142syl6eqbr 4968 . . . . . . 7 (𝑥 = 0 → 𝑥 ≤ (1 / 2))
325324iftrued 4358 . . . . . 6 (𝑥 = 0 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))))
326323, 217syl6eqbr 4968 . . . . . . 7 (𝑥 = 0 → 𝑥 ≤ (1 / 4))
327326iftrued 4358 . . . . . 6 (𝑥 = 0 → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (2 · 𝑥))
328 oveq2 6984 . . . . . . 7 (𝑥 = 0 → (2 · 𝑥) = (2 · 0))
329 2t0e0 11616 . . . . . . 7 (2 · 0) = 0
330328, 329syl6eq 2831 . . . . . 6 (𝑥 = 0 → (2 · 𝑥) = 0)
331325, 327, 3303eqtrd 2819 . . . . 5 (𝑥 = 0 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = 0)
332 c0ex 10433 . . . . 5 0 ∈ V
333331, 186, 332fvmpt 6595 . . . 4 (0 ∈ (0[,]1) → (𝑃‘0) = 0)
334191, 333syl 17 . . 3 (𝜑 → (𝑃‘0) = 0)
335147a1i 11 . . . 4 (𝜑 → 1 ∈ (0[,]1))
33659, 85ltnlei 10561 . . . . . . . . 9 ((1 / 2) < 1 ↔ ¬ 1 ≤ (1 / 2))
337143, 336mpbi 222 . . . . . . . 8 ¬ 1 ≤ (1 / 2)
338 breq1 4932 . . . . . . . 8 (𝑥 = 1 → (𝑥 ≤ (1 / 2) ↔ 1 ≤ (1 / 2)))
339337, 338mtbiri 319 . . . . . . 7 (𝑥 = 1 → ¬ 𝑥 ≤ (1 / 2))
340339iffalsed 4361 . . . . . 6 (𝑥 = 1 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = ((𝑥 / 2) + (1 / 2)))
341 oveq1 6983 . . . . . . . 8 (𝑥 = 1 → (𝑥 / 2) = (1 / 2))
342341oveq1d 6991 . . . . . . 7 (𝑥 = 1 → ((𝑥 / 2) + (1 / 2)) = ((1 / 2) + (1 / 2)))
343342, 83syl6eq 2831 . . . . . 6 (𝑥 = 1 → ((𝑥 / 2) + (1 / 2)) = 1)
344340, 343eqtrd 2815 . . . . 5 (𝑥 = 1 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = 1)
345 1ex 10435 . . . . 5 1 ∈ V
346344, 186, 345fvmpt 6595 . . . 4 (1 ∈ (0[,]1) → (𝑃‘1) = 1)
347335, 346syl 17 . . 3 (𝜑 → (𝑃‘1) = 1)
348313, 306, 334, 347reparpht 23305 . 2 (𝜑 → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)) ∘ 𝑃)( ≃ph𝐽)(𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)))
349322, 348eqbrtrd 4951 1 (𝜑 → ((𝐹(*𝑝𝐽)𝐺)(*𝑝𝐽)𝐻)( ≃ph𝐽)(𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 387  wo 833   = wceq 1507  wcel 2050  wne 2968  wral 3089  Vcvv 3416  wss 3830  ifcif 4350   cuni 4712   class class class wbr 4929  cmpt 5008  ran crn 5408  ccom 5411  wf 6184  cfv 6188  (class class class)co 6976  cc 10333  cr 10334  0cc0 10335  1c1 10336   + caddc 10338   · cmul 10340  *cxr 10473   < clt 10474  cle 10475  cmin 10670   / cdiv 11098  cn 11439  2c2 11495  4c4 11497  (,)cioo 12554  [,]cicc 12557  t crest 16550  TopOpenctopn 16551  topGenctg 16567  fldccnfld 20247  Topctop 21205  TopOnctopon 21222   Cn ccn 21536   ×t ctx 21872  IIcii 23186  phcphtpc 23276  *𝑝cpco 23307
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2751  ax-rep 5049  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279  ax-cnex 10391  ax-resscn 10392  ax-1cn 10393  ax-icn 10394  ax-addcl 10395  ax-addrcl 10396  ax-mulcl 10397  ax-mulrcl 10398  ax-mulcom 10399  ax-addass 10400  ax-mulass 10401  ax-distr 10402  ax-i2m1 10403  ax-1ne0 10404  ax-1rid 10405  ax-rnegex 10406  ax-rrecex 10407  ax-cnre 10408  ax-pre-lttri 10409  ax-pre-lttrn 10410  ax-pre-ltadd 10411  ax-pre-mulgt0 10412  ax-pre-sup 10413  ax-addf 10414  ax-mulf 10415
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rmo 3097  df-rab 3098  df-v 3418  df-sbc 3683  df-csb 3788  df-dif 3833  df-un 3835  df-in 3837  df-ss 3844  df-pss 3846  df-nul 4180  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-tp 4446  df-op 4448  df-uni 4713  df-int 4750  df-iun 4794  df-iin 4795  df-br 4930  df-opab 4992  df-mpt 5009  df-tr 5031  df-id 5312  df-eprel 5317  df-po 5326  df-so 5327  df-fr 5366  df-se 5367  df-we 5368  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-pred 5986  df-ord 6032  df-on 6033  df-lim 6034  df-suc 6035  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-isom 6197  df-riota 6937  df-ov 6979  df-oprab 6980  df-mpo 6981  df-of 7227  df-om 7397  df-1st 7501  df-2nd 7502  df-supp 7634  df-wrecs 7750  df-recs 7812  df-rdg 7850  df-1o 7905  df-2o 7906  df-oadd 7909  df-er 8089  df-map 8208  df-ixp 8260  df-en 8307  df-dom 8308  df-sdom 8309  df-fin 8310  df-fsupp 8629  df-fi 8670  df-sup 8701  df-inf 8702  df-oi 8769  df-card 9162  df-cda 9388  df-pnf 10476  df-mnf 10477  df-xr 10478  df-ltxr 10479  df-le 10480  df-sub 10672  df-neg 10673  df-div 11099  df-nn 11440  df-2 11503  df-3 11504  df-4 11505  df-5 11506  df-6 11507  df-7 11508  df-8 11509  df-9 11510  df-n0 11708  df-z 11794  df-dec 11912  df-uz 12059  df-q 12163  df-rp 12205  df-xneg 12324  df-xadd 12325  df-xmul 12326  df-ioo 12558  df-icc 12561  df-fz 12709  df-fzo 12850  df-seq 13185  df-exp 13245  df-hash 13506  df-cj 14319  df-re 14320  df-im 14321  df-sqrt 14455  df-abs 14456  df-struct 16341  df-ndx 16342  df-slot 16343  df-base 16345  df-sets 16346  df-ress 16347  df-plusg 16434  df-mulr 16435  df-starv 16436  df-sca 16437  df-vsca 16438  df-ip 16439  df-tset 16440  df-ple 16441  df-ds 16443  df-unif 16444  df-hom 16445  df-cco 16446  df-rest 16552  df-topn 16553  df-0g 16571  df-gsum 16572  df-topgen 16573  df-pt 16574  df-prds 16577  df-xrs 16631  df-qtop 16636  df-imas 16637  df-xps 16639  df-mre 16715  df-mrc 16716  df-acs 16718  df-mgm 17710  df-sgrp 17752  df-mnd 17763  df-submnd 17804  df-mulg 18012  df-cntz 18218  df-cmn 18668  df-psmet 20239  df-xmet 20240  df-met 20241  df-bl 20242  df-mopn 20243  df-cnfld 20248  df-top 21206  df-topon 21223  df-topsp 21245  df-bases 21258  df-cld 21331  df-cn 21539  df-cnp 21540  df-tx 21874  df-hmeo 22067  df-xms 22633  df-ms 22634  df-tms 22635  df-ii 23188  df-htpy 23277  df-phtpy 23278  df-phtpc 23299  df-pco 23312
This theorem is referenced by:  pcophtb  23336  pi1grplem  23356  pi1xfr  23362  pi1xfrcnvlem  23363
  Copyright terms: Public domain W3C validator