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

Theorem pcoass 23632
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 4434 . . . . . . . . . . 11 (𝑥 ≤ (1 / 4) → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (2 · 𝑥))
21fveq2d 6653 . . . . . . . . . 10 (𝑥 ≤ (1 / 4) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(2 · 𝑥)))
32adantl 485 . . . . . . . . 9 (((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(2 · 𝑥)))
4 2cn 11704 . . . . . . . . . . . . 13 2 ∈ ℂ
5 elicc01 12848 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (0[,]1) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥𝑥 ≤ 1))
65simp1bi 1142 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0[,]1) → 𝑥 ∈ ℝ)
76adantr 484 . . . . . . . . . . . . . 14 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℝ)
87recnd 10662 . . . . . . . . . . . . 13 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℂ)
9 mulcom 10616 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) = (𝑥 · 2))
104, 8, 9sylancr 590 . . . . . . . . . . . 12 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) = (𝑥 · 2))
115simp2bi 1143 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0[,]1) → 0 ≤ 𝑥)
1211adantr 484 . . . . . . . . . . . . . 14 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 0 ≤ 𝑥)
13 simpr 488 . . . . . . . . . . . . . 14 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ≤ (1 / 4))
14 0re 10636 . . . . . . . . . . . . . . 15 0 ∈ ℝ
15 4nn 11712 . . . . . . . . . . . . . . . 16 4 ∈ ℕ
16 nnrecre 11671 . . . . . . . . . . . . . . . 16 (4 ∈ ℕ → (1 / 4) ∈ ℝ)
1715, 16ax-mp 5 . . . . . . . . . . . . . . 15 (1 / 4) ∈ ℝ
1814, 17elicc2i 12795 . . . . . . . . . . . . . 14 (𝑥 ∈ (0[,](1 / 4)) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥𝑥 ≤ (1 / 4)))
197, 12, 13, 18syl3anbrc 1340 . . . . . . . . . . . . 13 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ (0[,](1 / 4)))
20 2rp 12386 . . . . . . . . . . . . . 14 2 ∈ ℝ+
214mul02i 10822 . . . . . . . . . . . . . 14 (0 · 2) = 0
2217recni 10648 . . . . . . . . . . . . . . 15 (1 / 4) ∈ ℂ
23222timesi 11767 . . . . . . . . . . . . . . . 16 (2 · (1 / 4)) = ((1 / 4) + (1 / 4))
24 2ne0 11733 . . . . . . . . . . . . . . . . . . . 20 2 ≠ 0
25 recdiv2 11346 . . . . . . . . . . . . . . . . . . . 20 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((1 / 2) / 2) = (1 / (2 · 2)))
264, 24, 4, 24, 25mp4an 692 . . . . . . . . . . . . . . . . . . 19 ((1 / 2) / 2) = (1 / (2 · 2))
27 2t2e4 11793 . . . . . . . . . . . . . . . . . . . 20 (2 · 2) = 4
2827oveq2i 7150 . . . . . . . . . . . . . . . . . . 19 (1 / (2 · 2)) = (1 / 4)
2926, 28eqtri 2824 . . . . . . . . . . . . . . . . . 18 ((1 / 2) / 2) = (1 / 4)
3029, 29oveq12i 7151 . . . . . . . . . . . . . . . . 17 (((1 / 2) / 2) + ((1 / 2) / 2)) = ((1 / 4) + (1 / 4))
31 halfcn 11844 . . . . . . . . . . . . . . . . . 18 (1 / 2) ∈ ℂ
32 2halves 11857 . . . . . . . . . . . . . . . . . 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 2826 . . . . . . . . . . . . . . . 16 ((1 / 4) + (1 / 4)) = (1 / 2)
3523, 34eqtri 2824 . . . . . . . . . . . . . . 15 (2 · (1 / 4)) = (1 / 2)
364, 22, 35mulcomli 10643 . . . . . . . . . . . . . 14 ((1 / 4) · 2) = (1 / 2)
3714, 17, 20, 21, 36iccdili 12873 . . . . . . . . . . . . 13 (𝑥 ∈ (0[,](1 / 4)) → (𝑥 · 2) ∈ (0[,](1 / 2)))
3819, 37syl 17 . . . . . . . . . . . 12 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → (𝑥 · 2) ∈ (0[,](1 / 2)))
3910, 38eqeltrd 2893 . . . . . . . . . . 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 23625 . . . . . . . . . . . . 13 (𝜑 → (𝐺(*𝑝𝐽)𝐻) ∈ (II Cn 𝐽))
4540, 44pcoval1 23621 . . . . . . . . . . . 12 ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(2 · 𝑥)) = (𝐹‘(2 · (2 · 𝑥))))
4640, 41pcoval1 23621 . . . . . . . . . . . 12 ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) → ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)) = (𝐹‘(2 · (2 · 𝑥))))
4745, 46eqtr4d 2839 . . . . . . . . . . 11 ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
4839, 47sylan2 595 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4))) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
4948anassrs 471 . . . . . . . . 9 (((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
503, 49eqtrd 2836 . . . . . . . 8 (((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
5150adantlr 714 . . . . . . 7 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
52 simplll 774 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝜑)
536ad2antlr 726 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → 𝑥 ∈ ℝ)
5453adantr 484 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℝ)
55 letric 10733 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ (1 / 4) ∈ ℝ) → (𝑥 ≤ (1 / 4) ∨ (1 / 4) ≤ 𝑥))
5653, 17, 55sylancl 589 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → (𝑥 ≤ (1 / 4) ∨ (1 / 4) ≤ 𝑥))
5756orcanai 1000 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (1 / 4) ≤ 𝑥)
58 simplr 768 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ≤ (1 / 2))
59 halfre 11843 . . . . . . . . . . . . 13 (1 / 2) ∈ ℝ
6017, 59elicc2i 12795 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 4)[,](1 / 2)) ↔ (𝑥 ∈ ℝ ∧ (1 / 4) ≤ 𝑥𝑥 ≤ (1 / 2)))
6154, 57, 58, 60syl3anbrc 1340 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ((1 / 4)[,](1 / 2)))
6260simp1bi 1142 . . . . . . . . . . . . 13 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → 𝑥 ∈ ℝ)
63 readdcl 10613 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ (1 / 4) ∈ ℝ) → (𝑥 + (1 / 4)) ∈ ℝ)
6462, 17, 63sylancl 589 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ∈ ℝ)
6517a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 4) ∈ ℝ)
6660simp2bi 1143 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 4) ≤ 𝑥)
6765, 62, 65, 66leadd1dd 11247 . . . . . . . . . . . . 13 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → ((1 / 4) + (1 / 4)) ≤ (𝑥 + (1 / 4)))
6834, 67eqbrtrrid 5069 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 2) ≤ (𝑥 + (1 / 4)))
6959a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 2) ∈ ℝ)
7060simp3bi 1144 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → 𝑥 ≤ (1 / 2))
71 2lt4 11804 . . . . . . . . . . . . . . . . 17 2 < 4
72 2re 11703 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
73 4re 11713 . . . . . . . . . . . . . . . . . 18 4 ∈ ℝ
74 2pos 11732 . . . . . . . . . . . . . . . . . 18 0 < 2
75 4pos 11736 . . . . . . . . . . . . . . . . . 18 0 < 4
7672, 73, 74, 75ltrecii 11549 . . . . . . . . . . . . . . . . 17 (2 < 4 ↔ (1 / 4) < (1 / 2))
7771, 76mpbi 233 . . . . . . . . . . . . . . . 16 (1 / 4) < (1 / 2)
7817, 59, 77ltleii 10756 . . . . . . . . . . . . . . 15 (1 / 4) ≤ (1 / 2)
7978a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 4) ≤ (1 / 2))
8062, 65, 69, 69, 70, 79le2addd 11252 . . . . . . . . . . . . 13 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ≤ ((1 / 2) + (1 / 2)))
81 ax-1cn 10588 . . . . . . . . . . . . . 14 1 ∈ ℂ
82 2halves 11857 . . . . . . . . . . . . . 14 (1 ∈ ℂ → ((1 / 2) + (1 / 2)) = 1)
8381, 82ax-mp 5 . . . . . . . . . . . . 13 ((1 / 2) + (1 / 2)) = 1
8480, 83breqtrdi 5074 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ≤ 1)
85 1re 10634 . . . . . . . . . . . . 13 1 ∈ ℝ
8659, 85elicc2i 12795 . . . . . . . . . . . 12 ((𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1) ↔ ((𝑥 + (1 / 4)) ∈ ℝ ∧ (1 / 2) ≤ (𝑥 + (1 / 4)) ∧ (𝑥 + (1 / 4)) ≤ 1))
8764, 68, 84, 86syl3anbrc 1340 . . . . . . . . . . 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 23622 . . . . . . . . . . . 12 (𝜑 → ((𝐺(*𝑝𝐽)𝐻)‘0) = (𝐺‘0))
9189, 90eqtr4d 2839 . . . . . . . . . . 11 (𝜑 → (𝐹‘1) = ((𝐺(*𝑝𝐽)𝐻)‘0))
9240, 44, 91pcoval2 23624 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(𝑥 + (1 / 4))) = ((𝐺(*𝑝𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)))
9352, 88, 92syl2anc 587 . . . . . . . . 9 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(𝑥 + (1 / 4))) = ((𝐺(*𝑝𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)))
9483oveq2i 7150 . . . . . . . . . . . 12 ((2 · (𝑥 + (1 / 4))) − ((1 / 2) + (1 / 2))) = ((2 · (𝑥 + (1 / 4))) − 1)
95 2cnd 11707 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 2 ∈ ℂ)
9654recnd 10662 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℂ)
9722a1i 11 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (1 / 4) ∈ ℂ)
9895, 96, 97adddid 10658 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · (𝑥 + (1 / 4))) = ((2 · 𝑥) + (2 · (1 / 4))))
9935oveq2i 7150 . . . . . . . . . . . . . 14 ((2 · 𝑥) + (2 · (1 / 4))) = ((2 · 𝑥) + (1 / 2))
10098, 99eqtrdi 2852 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · (𝑥 + (1 / 4))) = ((2 · 𝑥) + (1 / 2)))
101100oveq1d 7154 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − ((1 / 2) + (1 / 2))) = (((2 · 𝑥) + (1 / 2)) − ((1 / 2) + (1 / 2))))
10294, 101syl5eqr 2850 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − 1) = (((2 · 𝑥) + (1 / 2)) − ((1 / 2) + (1 / 2))))
103 remulcl 10615 . . . . . . . . . . . . . 14 ((2 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (2 · 𝑥) ∈ ℝ)
10472, 54, 103sylancr 590 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈ ℝ)
105104recnd 10662 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈ ℂ)
10631a1i 11 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (1 / 2) ∈ ℂ)
107105, 106, 106pnpcan2d 11028 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (((2 · 𝑥) + (1 / 2)) − ((1 / 2) + (1 / 2))) = ((2 · 𝑥) − (1 / 2)))
108102, 107eqtrd 2836 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − 1) = ((2 · 𝑥) − (1 / 2)))
109108fveq2d 6653 . . . . . . . . 9 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(*𝑝𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)) = ((𝐺(*𝑝𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))))
1104, 96, 9sylancr 590 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) = (𝑥 · 2))
11181, 4, 24divcan1i 11377 . . . . . . . . . . . . . . 15 ((1 / 2) · 2) = 1
11217, 59, 20, 36, 111iccdili 12873 . . . . . . . . . . . . . 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 2893 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈ ((1 / 2)[,]1))
11531subidi 10950 . . . . . . . . . . . . 13 ((1 / 2) − (1 / 2)) = 0
116 1mhlfehlf 11848 . . . . . . . . . . . . 13 (1 − (1 / 2)) = (1 / 2)
11759, 85, 59, 115, 116iccshftli 12871 . . . . . . . . . . . 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 23621 . . . . . . . . . . 11 ((𝜑 ∧ ((2 · 𝑥) − (1 / 2)) ∈ (0[,](1 / 2))) → ((𝐺(*𝑝𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))))
12052, 118, 119syl2anc 587 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(*𝑝𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))))
12195, 105, 106subdid 11089 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · ((2 · 𝑥) − (1 / 2))) = ((2 · (2 · 𝑥)) − (2 · (1 / 2))))
1224, 24recidi 11364 . . . . . . . . . . . . 13 (2 · (1 / 2)) = 1
123122oveq2i 7150 . . . . . . . . . . . 12 ((2 · (2 · 𝑥)) − (2 · (1 / 2))) = ((2 · (2 · 𝑥)) − 1)
124121, 123eqtrdi 2852 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · ((2 · 𝑥) − (1 / 2))) = ((2 · (2 · 𝑥)) − 1))
125124fveq2d 6653 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
126120, 125eqtrd 2836 . . . . . . . . 9 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(*𝑝𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
12793, 109, 1263eqtrd 2840 . . . . . . . 8 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(𝑥 + (1 / 4))) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
128 iffalse 4437 . . . . . . . . . 10 𝑥 ≤ (1 / 4) → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (𝑥 + (1 / 4)))
129128fveq2d 6653 . . . . . . . . 9 𝑥 ≤ (1 / 4) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(𝑥 + (1 / 4))))
130129adantl 485 . . . . . . . 8 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(𝑥 + (1 / 4))))
13140, 41, 89pcoval2 23624 . . . . . . . . 9 ((𝜑 ∧ (2 · 𝑥) ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
13252, 114, 131syl2anc 587 . . . . . . . 8 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
133127, 130, 1323eqtr4d 2846 . . . . . . 7 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
13451, 133pm2.61dan 812 . . . . . 6 (((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
135 iftrue 4434 . . . . . . . 8 (𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))))
136135fveq2d 6653 . . . . . . 7 (𝑥 ≤ (1 / 2) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))))
137136adantl 485 . . . . . 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 4434 . . . . . . 7 (𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
139138adantl 485 . . . . . 6 (((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
140134, 137, 1393eqtr4d 2846 . . . . 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 23544 . . . . . . . 8 ((𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 ≤ (1 / 2)) → 𝑥 ∈ ((1 / 2)[,]1))
142 halfge0 11846 . . . . . . . . . . . . . 14 0 ≤ (1 / 2)
143 halflt1 11847 . . . . . . . . . . . . . . 15 (1 / 2) < 1
14459, 85, 143ltleii 10756 . . . . . . . . . . . . . 14 (1 / 2) ≤ 1
145 elicc01 12848 . . . . . . . . . . . . . 14 ((1 / 2) ∈ (0[,]1) ↔ ((1 / 2) ∈ ℝ ∧ 0 ≤ (1 / 2) ∧ (1 / 2) ≤ 1))
14659, 142, 144, 145mpbir3an 1338 . . . . . . . . . . . . 13 (1 / 2) ∈ (0[,]1)
147 1elunit 12852 . . . . . . . . . . . . 13 1 ∈ (0[,]1)
148 iccss2 12800 . . . . . . . . . . . . 13 (((1 / 2) ∈ (0[,]1) ∧ 1 ∈ (0[,]1)) → ((1 / 2)[,]1) ⊆ (0[,]1))
149146, 147, 148mp2an 691 . . . . . . . . . . . 12 ((1 / 2)[,]1) ⊆ (0[,]1)
150149sseli 3914 . . . . . . . . . . 11 (𝑥 ∈ ((1 / 2)[,]1) → 𝑥 ∈ (0[,]1))
1514, 24div0i 11367 . . . . . . . . . . . 12 (0 / 2) = 0
152 eqid 2801 . . . . . . . . . . . 12 (1 / 2) = (1 / 2)
15314, 85, 20, 151, 152icccntri 12875 . . . . . . . . . . 11 (𝑥 ∈ (0[,]1) → (𝑥 / 2) ∈ (0[,](1 / 2)))
15431addid2i 10821 . . . . . . . . . . . 12 (0 + (1 / 2)) = (1 / 2)
15514, 59, 59, 154, 83iccshftri 12869 . . . . . . . . . . 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 23624 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 / 2) + (1 / 2)) ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = ((𝐺(*𝑝𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)))
158156, 157sylan2 595 . . . . . . . . 9 ((𝜑𝑥 ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = ((𝐺(*𝑝𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)))
15959, 85elicc2i 12795 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 2)[,]1) ↔ (𝑥 ∈ ℝ ∧ (1 / 2) ≤ 𝑥𝑥 ≤ 1))
160159simp1bi 1142 . . . . . . . . . . . . 13 (𝑥 ∈ ((1 / 2)[,]1) → 𝑥 ∈ ℝ)
161160recnd 10662 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 2)[,]1) → 𝑥 ∈ ℂ)
162 1cnd 10629 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 2)[,]1) → 1 ∈ ℂ)
163 2cnd 11707 . . . . . . . . . . . . . . 15 (𝑥 ∈ ((1 / 2)[,]1) → 2 ∈ ℂ)
16424a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ ((1 / 2)[,]1) → 2 ≠ 0)
165161, 162, 163, 164divdird 11447 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 2)[,]1) → ((𝑥 + 1) / 2) = ((𝑥 / 2) + (1 / 2)))
166165oveq2d 7155 . . . . . . . . . . . . 13 (𝑥 ∈ ((1 / 2)[,]1) → (2 · ((𝑥 + 1) / 2)) = (2 · ((𝑥 / 2) + (1 / 2))))
167 peano2cn 10805 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℂ → (𝑥 + 1) ∈ ℂ)
168161, 167syl 17 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 2)[,]1) → (𝑥 + 1) ∈ ℂ)
169168, 163, 164divcan2d 11411 . . . . . . . . . . . . 13 (𝑥 ∈ ((1 / 2)[,]1) → (2 · ((𝑥 + 1) / 2)) = (𝑥 + 1))
170166, 169eqtr3d 2838 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 2)[,]1) → (2 · ((𝑥 / 2) + (1 / 2))) = (𝑥 + 1))
171161, 162, 170mvrraddd 11045 . . . . . . . . . . 11 (𝑥 ∈ ((1 / 2)[,]1) → ((2 · ((𝑥 / 2) + (1 / 2))) − 1) = 𝑥)
172171fveq2d 6653 . . . . . . . . . 10 (𝑥 ∈ ((1 / 2)[,]1) → ((𝐺(*𝑝𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)) = ((𝐺(*𝑝𝐽)𝐻)‘𝑥))
173172adantl 485 . . . . . . . . 9 ((𝜑𝑥 ∈ ((1 / 2)[,]1)) → ((𝐺(*𝑝𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)) = ((𝐺(*𝑝𝐽)𝐻)‘𝑥))
17441, 42, 43pcoval2 23624 . . . . . . . . 9 ((𝜑𝑥 ∈ ((1 / 2)[,]1)) → ((𝐺(*𝑝𝐽)𝐻)‘𝑥) = (𝐻‘((2 · 𝑥) − 1)))
175158, 173, 1743eqtrd 2840 . . . . . . . 8 ((𝜑𝑥 ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1)))
176141, 175sylan2 595 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 ≤ (1 / 2))) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1)))
177176anassrs 471 . . . . . 6 (((𝜑𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1)))
178 iffalse 4437 . . . . . . . 8 𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = ((𝑥 / 2) + (1 / 2)))
179178fveq2d 6653 . . . . . . 7 𝑥 ≤ (1 / 2) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))))
180179adantl 485 . . . . . 6 (((𝜑𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))))
181 iffalse 4437 . . . . . . 7 𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = (𝐻‘((2 · 𝑥) − 1)))
182181adantl 485 . . . . . 6 (((𝜑𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = (𝐻‘((2 · 𝑥) − 1)))
183177, 180, 1823eqtr4d 2846 . . . . 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 812 . . . 4 ((𝜑𝑥 ∈ (0[,]1)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))))
185184mpteq2dva 5128 . . 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 23487 . . . . . . . . 9 II ∈ (TopOn‘(0[,]1))
188187a1i 11 . . . . . . . 8 (𝜑 → II ∈ (TopOn‘(0[,]1)))
189188cnmptid 22269 . . . . . . . 8 (𝜑 → (𝑥 ∈ (0[,]1) ↦ 𝑥) ∈ (II Cn II))
190 0elunit 12851 . . . . . . . . . 10 0 ∈ (0[,]1)
191190a1i 11 . . . . . . . . 9 (𝜑 → 0 ∈ (0[,]1))
192188, 188, 191cnmptc 22270 . . . . . . . 8 (𝜑 → (𝑥 ∈ (0[,]1) ↦ 0) ∈ (II Cn II))
193 eqid 2801 . . . . . . . . 9 (topGen‘ran (,)) = (topGen‘ran (,))
194 eqid 2801 . . . . . . . . 9 ((topGen‘ran (,)) ↾t (0[,](1 / 2))) = ((topGen‘ran (,)) ↾t (0[,](1 / 2)))
195 eqid 2801 . . . . . . . . 9 ((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) = ((topGen‘ran (,)) ↾t ((1 / 2)[,]1))
196 dfii2 23490 . . . . . . . . 9 II = ((topGen‘ran (,)) ↾t (0[,]1))
197 0red 10637 . . . . . . . . 9 (𝜑 → 0 ∈ ℝ)
198 1red 10635 . . . . . . . . 9 (𝜑 → 1 ∈ ℝ)
199146a1i 11 . . . . . . . . 9 (𝜑 → (1 / 2) ∈ (0[,]1))
200 simprl 770 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → 𝑦 = (1 / 2))
201200oveq1d 7154 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 2) + (1 / 4)))
20231, 22addcomi 10824 . . . . . . . . . . 11 ((1 / 2) + (1 / 4)) = ((1 / 4) + (1 / 2))
203201, 202eqtrdi 2852 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 4) + (1 / 2)))
20417, 59ltnlei 10754 . . . . . . . . . . . . 13 ((1 / 4) < (1 / 2) ↔ ¬ (1 / 2) ≤ (1 / 4))
20577, 204mpbi 233 . . . . . . . . . . . 12 ¬ (1 / 2) ≤ (1 / 4)
206200breq1d 5043 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 ≤ (1 / 4) ↔ (1 / 2) ≤ (1 / 4)))
207205, 206mtbiri 330 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → ¬ 𝑦 ≤ (1 / 4))
208207iffalsed 4439 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))) = (𝑦 + (1 / 4)))
209200oveq1d 7154 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 / 2) = ((1 / 2) / 2))
210209, 29eqtrdi 2852 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 / 2) = (1 / 4))
211210oveq1d 7154 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → ((𝑦 / 2) + (1 / 2)) = ((1 / 4) + (1 / 2)))
212203, 208, 2113eqtr4d 2846 . . . . . . . . 9 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))) = ((𝑦 / 2) + (1 / 2)))
213 eqid 2801 . . . . . . . . . 10 ((topGen‘ran (,)) ↾t (0[,](1 / 4))) = ((topGen‘ran (,)) ↾t (0[,](1 / 4)))
214 eqid 2801 . . . . . . . . . 10 ((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2))) = ((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2)))
21559a1i 11 . . . . . . . . . 10 (𝜑 → (1 / 2) ∈ ℝ)
21673, 75recgt0ii 11539 . . . . . . . . . . . . 13 0 < (1 / 4)
21714, 17, 216ltleii 10756 . . . . . . . . . . . 12 0 ≤ (1 / 4)
21814, 59elicc2i 12795 . . . . . . . . . . . 12 ((1 / 4) ∈ (0[,](1 / 2)) ↔ ((1 / 4) ∈ ℝ ∧ 0 ≤ (1 / 4) ∧ (1 / 4) ≤ (1 / 2)))
21917, 217, 78, 218mpbir3an 1338 . . . . . . . . . . 11 (1 / 4) ∈ (0[,](1 / 2))
220219a1i 11 . . . . . . . . . 10 (𝜑 → (1 / 4) ∈ (0[,](1 / 2)))
221 simprl 770 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → 𝑦 = (1 / 4))
222221oveq2d 7155 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = (2 · (1 / 4)))
223221oveq1d 7154 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 4) + (1 / 4)))
22423, 222, 2233eqtr4a 2862 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = (𝑦 + (1 / 4)))
225 retopon 23372 . . . . . . . . . . . . 13 (topGen‘ran (,)) ∈ (TopOn‘ℝ)
226 0xr 10681 . . . . . . . . . . . . . . . 16 0 ∈ ℝ*
22759rexri 10692 . . . . . . . . . . . . . . . 16 (1 / 2) ∈ ℝ*
228 lbicc2 12846 . . . . . . . . . . . . . . . 16 ((0 ∈ ℝ* ∧ (1 / 2) ∈ ℝ* ∧ 0 ≤ (1 / 2)) → 0 ∈ (0[,](1 / 2)))
229226, 227, 142, 228mp3an 1458 . . . . . . . . . . . . . . 15 0 ∈ (0[,](1 / 2))
230 iccss2 12800 . . . . . . . . . . . . . . 15 ((0 ∈ (0[,](1 / 2)) ∧ (1 / 4) ∈ (0[,](1 / 2))) → (0[,](1 / 4)) ⊆ (0[,](1 / 2)))
231229, 219, 230mp2an 691 . . . . . . . . . . . . . 14 (0[,](1 / 4)) ⊆ (0[,](1 / 2))
232 iccssre 12811 . . . . . . . . . . . . . . 15 ((0 ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (0[,](1 / 2)) ⊆ ℝ)
23314, 59, 232mp2an 691 . . . . . . . . . . . . . 14 (0[,](1 / 2)) ⊆ ℝ
234231, 233sstri 3927 . . . . . . . . . . . . 13 (0[,](1 / 4)) ⊆ ℝ
235 resttopon 21769 . . . . . . . . . . . . 13 (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 / 4)) ⊆ ℝ) → ((topGen‘ran (,)) ↾t (0[,](1 / 4))) ∈ (TopOn‘(0[,](1 / 4))))
236225, 234, 235mp2an 691 . . . . . . . . . . . 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 22276 . . . . . . . . . . 11 (𝜑 → (𝑦 ∈ (0[,](1 / 4)), 𝑧 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,)) ↾t (0[,](1 / 4))) ×t II) Cn ((topGen‘ran (,)) ↾t (0[,](1 / 4)))))
239 retop 23370 . . . . . . . . . . . . . 14 (topGen‘ran (,)) ∈ Top
240 ovex 7172 . . . . . . . . . . . . . 14 (0[,](1 / 2)) ∈ V
241 restabs 21773 . . . . . . . . . . . . . 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 1458 . . . . . . . . . . . . 13 (((topGen‘ran (,)) ↾t (0[,](1 / 2))) ↾t (0[,](1 / 4))) = ((topGen‘ran (,)) ↾t (0[,](1 / 4)))
243242eqcomi 2810 . . . . . . . . . . . 12 ((topGen‘ran (,)) ↾t (0[,](1 / 4))) = (((topGen‘ran (,)) ↾t (0[,](1 / 2))) ↾t (0[,](1 / 4)))
244 resttopon 21769 . . . . . . . . . . . . . 14 (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 / 2)) ⊆ ℝ) → ((topGen‘ran (,)) ↾t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 / 2))))
245225, 233, 244mp2an 691 . . . . . . . . . . . . 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 23540 . . . . . . . . . . . . 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 22284 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ (0[,](1 / 4)) ↦ (2 · 𝑥)) ∈ (((topGen‘ran (,)) ↾t (0[,](1 / 4))) Cn II))
251 oveq2 7147 . . . . . . . . . . 11 (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
252237, 188, 238, 237, 250, 251cnmpt21 22279 . . . . . . . . . 10 (𝜑 → (𝑦 ∈ (0[,](1 / 4)), 𝑧 ∈ (0[,]1) ↦ (2 · 𝑦)) ∈ ((((topGen‘ran (,)) ↾t (0[,](1 / 4))) ×t II) Cn II))
253 iccssre 12811 . . . . . . . . . . . . . 14 (((1 / 4) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → ((1 / 4)[,](1 / 2)) ⊆ ℝ)
25417, 59, 253mp2an 691 . . . . . . . . . . . . 13 ((1 / 4)[,](1 / 2)) ⊆ ℝ
255 resttopon 21769 . . . . . . . . . . . . 13 (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 / 4)[,](1 / 2)) ⊆ ℝ) → ((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2))) ∈ (TopOn‘((1 / 4)[,](1 / 2))))
256225, 254, 255mp2an 691 . . . . . . . . . . . 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 22276 . . . . . . . . . . 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 2801 . . . . . . . . . . . 12 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
260254a1i 11 . . . . . . . . . . . 12 (𝜑 → ((1 / 4)[,](1 / 2)) ⊆ ℝ)
261 unitssre 12881 . . . . . . . . . . . . 13 (0[,]1) ⊆ ℝ
262261a1i 11 . . . . . . . . . . . 12 (𝜑 → (0[,]1) ⊆ ℝ)
263149, 87sseldi 3916 . . . . . . . . . . . . 13 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ∈ (0[,]1))
264263adantl 485 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((1 / 4)[,](1 / 2))) → (𝑥 + (1 / 4)) ∈ (0[,]1))
265259cnfldtopon 23391 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
266265a1i 11 . . . . . . . . . . . . 13 (𝜑 → (TopOpen‘ℂfld) ∈ (TopOn‘ℂ))
267266cnmptid 22269 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ ℂ ↦ 𝑥) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
26817a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (1 / 4) ∈ ℝ)
269268recnd 10662 . . . . . . . . . . . . . 14 (𝜑 → (1 / 4) ∈ ℂ)
270266, 266, 269cnmptc 22270 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ ℂ ↦ (1 / 4)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
271259addcn 23473 . . . . . . . . . . . . . 14 + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
272271a1i 11 . . . . . . . . . . . . 13 (𝜑 → + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
273266, 267, 270, 272cnmpt12f 22274 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ ℂ ↦ (𝑥 + (1 / 4))) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
274259, 214, 196, 260, 262, 264, 273cnmptre 23535 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ ((1 / 4)[,](1 / 2)) ↦ (𝑥 + (1 / 4))) ∈ (((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2))) Cn II))
275 oveq1 7146 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑥 + (1 / 4)) = (𝑦 + (1 / 4)))
276257, 188, 258, 257, 274, 275cnmpt21 22279 . . . . . . . . . 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 23536 . . . . . . . . 9 (𝜑 → (𝑦 ∈ (0[,](1 / 2)), 𝑧 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4)))) ∈ ((((topGen‘ran (,)) ↾t (0[,](1 / 2))) ×t II) Cn II))
278 iccssre 12811 . . . . . . . . . . . . 13 (((1 / 2) ∈ ℝ ∧ 1 ∈ ℝ) → ((1 / 2)[,]1) ⊆ ℝ)
27959, 85, 278mp2an 691 . . . . . . . . . . . 12 ((1 / 2)[,]1) ⊆ ℝ
280 resttopon 21769 . . . . . . . . . . . 12 (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 / 2)[,]1) ⊆ ℝ) → ((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1)))
281225, 279, 280mp2an 691 . . . . . . . . . . 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 22276 . . . . . . . . . 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 3916 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 2)[,]1) → ((𝑥 / 2) + (1 / 2)) ∈ (0[,]1))
286285adantl 485 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((1 / 2)[,]1)) → ((𝑥 / 2) + (1 / 2)) ∈ (0[,]1))
287259divccn 23481 . . . . . . . . . . . . . 14 ((2 ∈ ℂ ∧ 2 ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
2884, 24, 287mp2an 691 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld))
289288a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
29031a1i 11 . . . . . . . . . . . . 13 (𝜑 → (1 / 2) ∈ ℂ)
291266, 266, 290cnmptc 22270 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ ℂ ↦ (1 / 2)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
292266, 289, 291, 272cnmpt12f 22274 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ ℂ ↦ ((𝑥 / 2) + (1 / 2))) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
293259, 195, 196, 284, 262, 286, 292cnmptre 23535 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ ((1 / 2)[,]1) ↦ ((𝑥 / 2) + (1 / 2))) ∈ (((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) Cn II))
294 oveq1 7146 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑥 / 2) = (𝑦 / 2))
295294oveq1d 7154 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝑥 / 2) + (1 / 2)) = ((𝑦 / 2) + (1 / 2)))
296282, 188, 283, 282, 293, 295cnmpt21 22279 . . . . . . . . 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 23536 . . . . . . . 8 (𝜑 → (𝑦 ∈ (0[,]1), 𝑧 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 2), if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))), ((𝑦 / 2) + (1 / 2)))) ∈ ((II ×t II) Cn II))
298 breq1 5036 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥 ≤ (1 / 2) ↔ 𝑦 ≤ (1 / 2)))
299 breq1 5036 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑥 ≤ (1 / 4) ↔ 𝑦 ≤ (1 / 4)))
300299, 251, 275ifbieq12d 4455 . . . . . . . . . . . 12 (𝑥 = 𝑦 → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))))
301298, 300, 295ifbieq12d 4455 . . . . . . . . . . 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 2027 . . . . . . . . . 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 484 . . . . . . . . 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 2807 . . . . . . . 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 22275 . . . . . . 7 (𝜑 → (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) ∈ (II Cn II))
306186, 305eqeltrid 2897 . . . . . 6 (𝜑𝑃 ∈ (II Cn II))
307 iiuni 23489 . . . . . . 7 (0[,]1) = II
308307, 307cnf 21854 . . . . . 6 (𝑃 ∈ (II Cn II) → 𝑃:(0[,]1)⟶(0[,]1))
309306, 308syl 17 . . . . 5 (𝜑𝑃:(0[,]1)⟶(0[,]1))
310186fmpt 6855 . . . . 5 (∀𝑥 ∈ (0[,]1)if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) ∈ (0[,]1) ↔ 𝑃:(0[,]1)⟶(0[,]1))
311309, 310sylibr 237 . . . 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 23625 . . . . . 6 (𝜑 → (𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)) ∈ (II Cn 𝐽))
314 eqid 2801 . . . . . . 7 𝐽 = 𝐽
315307, 314cnf 21854 . . . . . 6 ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)) ∈ (II Cn 𝐽) → (𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)):(0[,]1)⟶ 𝐽)
316313, 315syl 17 . . . . 5 (𝜑 → (𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)):(0[,]1)⟶ 𝐽)
317316feqmptd 6712 . . . 4 (𝜑 → (𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)) = (𝑦 ∈ (0[,]1) ↦ ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘𝑦)))
318 fveq2 6649 . . . 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 6873 . . 3 (𝜑 → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)) ∘ 𝑃) = (𝑥 ∈ (0[,]1) ↦ ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))))))
32040, 41, 89pcocn 23625 . . . 4 (𝜑 → (𝐹(*𝑝𝐽)𝐺) ∈ (II Cn 𝐽))
321320, 42pcoval 23619 . . 3 (𝜑 → ((𝐹(*𝑝𝐽)𝐺)(*𝑝𝐽)𝐻) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1)))))
322185, 319, 3213eqtr4rd 2847 . 2 (𝜑 → ((𝐹(*𝑝𝐽)𝐺)(*𝑝𝐽)𝐻) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)) ∘ 𝑃))
323 id 22 . . . . . . . 8 (𝑥 = 0 → 𝑥 = 0)
324323, 142eqbrtrdi 5072 . . . . . . 7 (𝑥 = 0 → 𝑥 ≤ (1 / 2))
325324iftrued 4436 . . . . . 6 (𝑥 = 0 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))))
326323, 217eqbrtrdi 5072 . . . . . . 7 (𝑥 = 0 → 𝑥 ≤ (1 / 4))
327326iftrued 4436 . . . . . 6 (𝑥 = 0 → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (2 · 𝑥))
328 oveq2 7147 . . . . . . 7 (𝑥 = 0 → (2 · 𝑥) = (2 · 0))
329 2t0e0 11798 . . . . . . 7 (2 · 0) = 0
330328, 329eqtrdi 2852 . . . . . 6 (𝑥 = 0 → (2 · 𝑥) = 0)
331325, 327, 3303eqtrd 2840 . . . . 5 (𝑥 = 0 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = 0)
332 c0ex 10628 . . . . 5 0 ∈ V
333331, 186, 332fvmpt 6749 . . . 4 (0 ∈ (0[,]1) → (𝑃‘0) = 0)
334191, 333syl 17 . . 3 (𝜑 → (𝑃‘0) = 0)
335147a1i 11 . . . 4 (𝜑 → 1 ∈ (0[,]1))
33659, 85ltnlei 10754 . . . . . . . . 9 ((1 / 2) < 1 ↔ ¬ 1 ≤ (1 / 2))
337143, 336mpbi 233 . . . . . . . 8 ¬ 1 ≤ (1 / 2)
338 breq1 5036 . . . . . . . 8 (𝑥 = 1 → (𝑥 ≤ (1 / 2) ↔ 1 ≤ (1 / 2)))
339337, 338mtbiri 330 . . . . . . 7 (𝑥 = 1 → ¬ 𝑥 ≤ (1 / 2))
340339iffalsed 4439 . . . . . 6 (𝑥 = 1 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = ((𝑥 / 2) + (1 / 2)))
341 oveq1 7146 . . . . . . . 8 (𝑥 = 1 → (𝑥 / 2) = (1 / 2))
342341oveq1d 7154 . . . . . . 7 (𝑥 = 1 → ((𝑥 / 2) + (1 / 2)) = ((1 / 2) + (1 / 2)))
343342, 83eqtrdi 2852 . . . . . 6 (𝑥 = 1 → ((𝑥 / 2) + (1 / 2)) = 1)
344340, 343eqtrd 2836 . . . . 5 (𝑥 = 1 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = 1)
345 1ex 10630 . . . . 5 1 ∈ V
346344, 186, 345fvmpt 6749 . . . 4 (1 ∈ (0[,]1) → (𝑃‘1) = 1)
347335, 346syl 17 . . 3 (𝜑 → (𝑃‘1) = 1)
348313, 306, 334, 347reparpht 23606 . 2 (𝜑 → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)) ∘ 𝑃)( ≃ph𝐽)(𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)))
349322, 348eqbrtrd 5055 1 (𝜑 → ((𝐹(*𝑝𝐽)𝐺)(*𝑝𝐽)𝐻)( ≃ph𝐽)(𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  wo 844   = wceq 1538  wcel 2112  wne 2990  wral 3109  Vcvv 3444  wss 3884  ifcif 4428   cuni 4803   class class class wbr 5033  cmpt 5113  ran crn 5524  ccom 5527  wf 6324  cfv 6328  (class class class)co 7139  cc 10528  cr 10529  0cc0 10530  1c1 10531   + caddc 10533   · cmul 10535  *cxr 10667   < clt 10668  cle 10669  cmin 10863   / cdiv 11290  cn 11629  2c2 11684  4c4 11686  (,)cioo 12730  [,]cicc 12733  t crest 16689  TopOpenctopn 16690  topGenctg 16706  fldccnfld 20094  Topctop 21501  TopOnctopon 21518   Cn ccn 21832   ×t ctx 22168  IIcii 23483  phcphtpc 23577  *𝑝cpco 23608
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607  ax-pre-sup 10608  ax-addf 10609  ax-mulf 10610
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-of 7393  df-om 7565  df-1st 7675  df-2nd 7676  df-supp 7818  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-2o 8090  df-oadd 8093  df-er 8276  df-map 8395  df-ixp 8449  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fsupp 8822  df-fi 8863  df-sup 8894  df-inf 8895  df-oi 8962  df-card 9356  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-div 11291  df-nn 11630  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-q 12341  df-rp 12382  df-xneg 12499  df-xadd 12500  df-xmul 12501  df-ioo 12734  df-icc 12737  df-fz 12890  df-fzo 13033  df-seq 13369  df-exp 13430  df-hash 13691  df-cj 14453  df-re 14454  df-im 14455  df-sqrt 14589  df-abs 14590  df-struct 16480  df-ndx 16481  df-slot 16482  df-base 16484  df-sets 16485  df-ress 16486  df-plusg 16573  df-mulr 16574  df-starv 16575  df-sca 16576  df-vsca 16577  df-ip 16578  df-tset 16579  df-ple 16580  df-ds 16582  df-unif 16583  df-hom 16584  df-cco 16585  df-rest 16691  df-topn 16692  df-0g 16710  df-gsum 16711  df-topgen 16712  df-pt 16713  df-prds 16716  df-xrs 16770  df-qtop 16775  df-imas 16776  df-xps 16778  df-mre 16852  df-mrc 16853  df-acs 16855  df-mgm 17847  df-sgrp 17896  df-mnd 17907  df-submnd 17952  df-mulg 18220  df-cntz 18442  df-cmn 18903  df-psmet 20086  df-xmet 20087  df-met 20088  df-bl 20089  df-mopn 20090  df-cnfld 20095  df-top 21502  df-topon 21519  df-topsp 21541  df-bases 21554  df-cld 21627  df-cn 21835  df-cnp 21836  df-tx 22170  df-hmeo 22363  df-xms 22930  df-ms 22931  df-tms 22932  df-ii 23485  df-htpy 23578  df-phtpy 23579  df-phtpc 23600  df-pco 23613
This theorem is referenced by:  pcophtb  23637  pi1grplem  23657  pi1xfr  23663  pi1xfrcnvlem  23664
  Copyright terms: Public domain W3C validator