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

Theorem pcoass 22870
 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 4125 . . . . . . . . . . 11 (𝑥 ≤ (1 / 4) → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (2 · 𝑥))
21fveq2d 6233 . . . . . . . . . 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 11129 . . . . . . . . . . . . 13 2 ∈ ℂ
5 0re 10078 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ
6 1re 10077 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ
75, 6elicc2i 12277 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (0[,]1) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥𝑥 ≤ 1))
87simp1bi 1096 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0[,]1) → 𝑥 ∈ ℝ)
98adantr 480 . . . . . . . . . . . . . 14 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℝ)
109recnd 10106 . . . . . . . . . . . . 13 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℂ)
11 mulcom 10060 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) = (𝑥 · 2))
124, 10, 11sylancr 696 . . . . . . . . . . . 12 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) = (𝑥 · 2))
137simp2bi 1097 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0[,]1) → 0 ≤ 𝑥)
1413adantr 480 . . . . . . . . . . . . . 14 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 0 ≤ 𝑥)
15 simpr 476 . . . . . . . . . . . . . 14 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ≤ (1 / 4))
16 4nn 11225 . . . . . . . . . . . . . . . 16 4 ∈ ℕ
17 nnrecre 11095 . . . . . . . . . . . . . . . 16 (4 ∈ ℕ → (1 / 4) ∈ ℝ)
1816, 17ax-mp 5 . . . . . . . . . . . . . . 15 (1 / 4) ∈ ℝ
195, 18elicc2i 12277 . . . . . . . . . . . . . 14 (𝑥 ∈ (0[,](1 / 4)) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥𝑥 ≤ (1 / 4)))
209, 14, 15, 19syl3anbrc 1265 . . . . . . . . . . . . 13 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ (0[,](1 / 4)))
21 2rp 11875 . . . . . . . . . . . . . 14 2 ∈ ℝ+
224mul02i 10263 . . . . . . . . . . . . . 14 (0 · 2) = 0
2318recni 10090 . . . . . . . . . . . . . . 15 (1 / 4) ∈ ℂ
24232timesi 11185 . . . . . . . . . . . . . . . 16 (2 · (1 / 4)) = ((1 / 4) + (1 / 4))
25 2ne0 11151 . . . . . . . . . . . . . . . . . . . 20 2 ≠ 0
26 recdiv2 10776 . . . . . . . . . . . . . . . . . . . 20 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((1 / 2) / 2) = (1 / (2 · 2)))
274, 25, 4, 25, 26mp4an 709 . . . . . . . . . . . . . . . . . . 19 ((1 / 2) / 2) = (1 / (2 · 2))
28 2t2e4 11215 . . . . . . . . . . . . . . . . . . . 20 (2 · 2) = 4
2928oveq2i 6701 . . . . . . . . . . . . . . . . . . 19 (1 / (2 · 2)) = (1 / 4)
3027, 29eqtri 2673 . . . . . . . . . . . . . . . . . 18 ((1 / 2) / 2) = (1 / 4)
3130, 30oveq12i 6702 . . . . . . . . . . . . . . . . 17 (((1 / 2) / 2) + ((1 / 2) / 2)) = ((1 / 4) + (1 / 4))
32 halfcn 11285 . . . . . . . . . . . . . . . . . 18 (1 / 2) ∈ ℂ
33 2halves 11298 . . . . . . . . . . . . . . . . . 18 ((1 / 2) ∈ ℂ → (((1 / 2) / 2) + ((1 / 2) / 2)) = (1 / 2))
3432, 33ax-mp 5 . . . . . . . . . . . . . . . . 17 (((1 / 2) / 2) + ((1 / 2) / 2)) = (1 / 2)
3531, 34eqtr3i 2675 . . . . . . . . . . . . . . . 16 ((1 / 4) + (1 / 4)) = (1 / 2)
3624, 35eqtri 2673 . . . . . . . . . . . . . . 15 (2 · (1 / 4)) = (1 / 2)
374, 23, 36mulcomli 10085 . . . . . . . . . . . . . 14 ((1 / 4) · 2) = (1 / 2)
385, 18, 21, 22, 37iccdili 12349 . . . . . . . . . . . . 13 (𝑥 ∈ (0[,](1 / 4)) → (𝑥 · 2) ∈ (0[,](1 / 2)))
3920, 38syl 17 . . . . . . . . . . . 12 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → (𝑥 · 2) ∈ (0[,](1 / 2)))
4012, 39eqeltrd 2730 . . . . . . . . . . 11 ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈ (0[,](1 / 2)))
41 pcoass.2 . . . . . . . . . . . . 13 (𝜑𝐹 ∈ (II Cn 𝐽))
42 pcoass.3 . . . . . . . . . . . . . 14 (𝜑𝐺 ∈ (II Cn 𝐽))
43 pcoass.4 . . . . . . . . . . . . . 14 (𝜑𝐻 ∈ (II Cn 𝐽))
44 pcoass.6 . . . . . . . . . . . . . 14 (𝜑 → (𝐺‘1) = (𝐻‘0))
4542, 43, 44pcocn 22863 . . . . . . . . . . . . 13 (𝜑 → (𝐺(*𝑝𝐽)𝐻) ∈ (II Cn 𝐽))
4641, 45pcoval1 22859 . . . . . . . . . . . 12 ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(2 · 𝑥)) = (𝐹‘(2 · (2 · 𝑥))))
4741, 42pcoval1 22859 . . . . . . . . . . . 12 ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) → ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)) = (𝐹‘(2 · (2 · 𝑥))))
4846, 47eqtr4d 2688 . . . . . . . . . . 11 ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
4940, 48sylan2 490 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4))) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
5049anassrs 681 . . . . . . . . 9 (((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
513, 50eqtrd 2685 . . . . . . . 8 (((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
5251adantlr 751 . . . . . . 7 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
53 simplll 813 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝜑)
548ad2antlr 763 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → 𝑥 ∈ ℝ)
5554adantr 480 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℝ)
56 letric 10175 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ (1 / 4) ∈ ℝ) → (𝑥 ≤ (1 / 4) ∨ (1 / 4) ≤ 𝑥))
5754, 18, 56sylancl 695 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → (𝑥 ≤ (1 / 4) ∨ (1 / 4) ≤ 𝑥))
5857orcanai 972 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (1 / 4) ≤ 𝑥)
59 simplr 807 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ≤ (1 / 2))
60 halfre 11284 . . . . . . . . . . . . 13 (1 / 2) ∈ ℝ
6118, 60elicc2i 12277 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 4)[,](1 / 2)) ↔ (𝑥 ∈ ℝ ∧ (1 / 4) ≤ 𝑥𝑥 ≤ (1 / 2)))
6255, 58, 59, 61syl3anbrc 1265 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ((1 / 4)[,](1 / 2)))
6361simp1bi 1096 . . . . . . . . . . . . 13 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → 𝑥 ∈ ℝ)
64 readdcl 10057 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ (1 / 4) ∈ ℝ) → (𝑥 + (1 / 4)) ∈ ℝ)
6563, 18, 64sylancl 695 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ∈ ℝ)
6618a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 4) ∈ ℝ)
6761simp2bi 1097 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 4) ≤ 𝑥)
6866, 63, 66, 67leadd1dd 10679 . . . . . . . . . . . . 13 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → ((1 / 4) + (1 / 4)) ≤ (𝑥 + (1 / 4)))
6935, 68syl5eqbrr 4721 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 2) ≤ (𝑥 + (1 / 4)))
7060a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 2) ∈ ℝ)
7161simp3bi 1098 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → 𝑥 ≤ (1 / 2))
72 2lt4 11236 . . . . . . . . . . . . . . . . 17 2 < 4
73 2re 11128 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
74 4re 11135 . . . . . . . . . . . . . . . . . 18 4 ∈ ℝ
75 2pos 11150 . . . . . . . . . . . . . . . . . 18 0 < 2
76 4pos 11154 . . . . . . . . . . . . . . . . . 18 0 < 4
7773, 74, 75, 76ltrecii 10978 . . . . . . . . . . . . . . . . 17 (2 < 4 ↔ (1 / 4) < (1 / 2))
7872, 77mpbi 220 . . . . . . . . . . . . . . . 16 (1 / 4) < (1 / 2)
7918, 60, 78ltleii 10198 . . . . . . . . . . . . . . 15 (1 / 4) ≤ (1 / 2)
8079a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 4) ≤ (1 / 2))
8163, 66, 70, 70, 71, 80le2addd 10684 . . . . . . . . . . . . 13 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ≤ ((1 / 2) + (1 / 2)))
82 ax-1cn 10032 . . . . . . . . . . . . . 14 1 ∈ ℂ
83 2halves 11298 . . . . . . . . . . . . . 14 (1 ∈ ℂ → ((1 / 2) + (1 / 2)) = 1)
8482, 83ax-mp 5 . . . . . . . . . . . . 13 ((1 / 2) + (1 / 2)) = 1
8581, 84syl6breq 4726 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ≤ 1)
8660, 6elicc2i 12277 . . . . . . . . . . . 12 ((𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1) ↔ ((𝑥 + (1 / 4)) ∈ ℝ ∧ (1 / 2) ≤ (𝑥 + (1 / 4)) ∧ (𝑥 + (1 / 4)) ≤ 1))
8765, 69, 85, 86syl3anbrc 1265 . . . . . . . . . . 11 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1))
8862, 87syl 17 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1))
89 pcoass.5 . . . . . . . . . . . 12 (𝜑 → (𝐹‘1) = (𝐺‘0))
9042, 43pco0 22860 . . . . . . . . . . . 12 (𝜑 → ((𝐺(*𝑝𝐽)𝐻)‘0) = (𝐺‘0))
9189, 90eqtr4d 2688 . . . . . . . . . . 11 (𝜑 → (𝐹‘1) = ((𝐺(*𝑝𝐽)𝐻)‘0))
9241, 45, 91pcoval2 22862 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(𝑥 + (1 / 4))) = ((𝐺(*𝑝𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)))
9353, 88, 92syl2anc 694 . . . . . . . . 9 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(𝑥 + (1 / 4))) = ((𝐺(*𝑝𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)))
9484oveq2i 6701 . . . . . . . . . . . 12 ((2 · (𝑥 + (1 / 4))) − ((1 / 2) + (1 / 2))) = ((2 · (𝑥 + (1 / 4))) − 1)
95 2cnd 11131 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 2 ∈ ℂ)
9655recnd 10106 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℂ)
9723a1i 11 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (1 / 4) ∈ ℂ)
9895, 96, 97adddid 10102 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · (𝑥 + (1 / 4))) = ((2 · 𝑥) + (2 · (1 / 4))))
9936oveq2i 6701 . . . . . . . . . . . . . 14 ((2 · 𝑥) + (2 · (1 / 4))) = ((2 · 𝑥) + (1 / 2))
10098, 99syl6eq 2701 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · (𝑥 + (1 / 4))) = ((2 · 𝑥) + (1 / 2)))
101100oveq1d 6705 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − ((1 / 2) + (1 / 2))) = (((2 · 𝑥) + (1 / 2)) − ((1 / 2) + (1 / 2))))
10294, 101syl5eqr 2699 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − 1) = (((2 · 𝑥) + (1 / 2)) − ((1 / 2) + (1 / 2))))
103 remulcl 10059 . . . . . . . . . . . . . 14 ((2 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (2 · 𝑥) ∈ ℝ)
10473, 55, 103sylancr 696 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈ ℝ)
105104recnd 10106 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈ ℂ)
10632a1i 11 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (1 / 2) ∈ ℂ)
107105, 106, 106pnpcan2d 10468 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (((2 · 𝑥) + (1 / 2)) − ((1 / 2) + (1 / 2))) = ((2 · 𝑥) − (1 / 2)))
108102, 107eqtrd 2685 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − 1) = ((2 · 𝑥) − (1 / 2)))
109108fveq2d 6233 . . . . . . . . 9 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(*𝑝𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)) = ((𝐺(*𝑝𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))))
1104, 96, 11sylancr 696 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) = (𝑥 · 2))
11182, 4, 25divcan1i 10807 . . . . . . . . . . . . . . 15 ((1 / 2) · 2) = 1
11218, 60, 21, 37, 111iccdili 12349 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 · 2) ∈ ((1 / 2)[,]1))
11362, 112syl 17 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (𝑥 · 2) ∈ ((1 / 2)[,]1))
114110, 113eqeltrd 2730 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈ ((1 / 2)[,]1))
11532subidi 10390 . . . . . . . . . . . . 13 ((1 / 2) − (1 / 2)) = 0
116 1mhlfehlf 11289 . . . . . . . . . . . . 13 (1 − (1 / 2)) = (1 / 2)
11760, 6, 60, 115, 116iccshftli 12347 . . . . . . . . . . . 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)))
11942, 43pcoval1 22859 . . . . . . . . . . 11 ((𝜑 ∧ ((2 · 𝑥) − (1 / 2)) ∈ (0[,](1 / 2))) → ((𝐺(*𝑝𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))))
12053, 118, 119syl2anc 694 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(*𝑝𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))))
12195, 105, 106subdid 10524 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · ((2 · 𝑥) − (1 / 2))) = ((2 · (2 · 𝑥)) − (2 · (1 / 2))))
1224, 25recidi 10794 . . . . . . . . . . . . 13 (2 · (1 / 2)) = 1
123122oveq2i 6701 . . . . . . . . . . . 12 ((2 · (2 · 𝑥)) − (2 · (1 / 2))) = ((2 · (2 · 𝑥)) − 1)
124121, 123syl6eq 2701 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · ((2 · 𝑥) − (1 / 2))) = ((2 · (2 · 𝑥)) − 1))
125124fveq2d 6233 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
126120, 125eqtrd 2685 . . . . . . . . 9 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(*𝑝𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
12793, 109, 1263eqtrd 2689 . . . . . . . 8 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘(𝑥 + (1 / 4))) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
128 iffalse 4128 . . . . . . . . . 10 𝑥 ≤ (1 / 4) → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (𝑥 + (1 / 4)))
129128fveq2d 6233 . . . . . . . . 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))))
13141, 42, 89pcoval2 22862 . . . . . . . . 9 ((𝜑 ∧ (2 · 𝑥) ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
13253, 114, 131syl2anc 694 . . . . . . . 8 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
133127, 130, 1323eqtr4d 2695 . . . . . . 7 ((((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
13452, 133pm2.61dan 849 . . . . . 6 (((𝜑𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)))
135 iftrue 4125 . . . . . . . 8 (𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))))
136135fveq2d 6233 . . . . . . 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 4125 . . . . . . 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 2695 . . . . 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 22782 . . . . . . . 8 ((𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 ≤ (1 / 2)) → 𝑥 ∈ ((1 / 2)[,]1))
142 halfgt0 11286 . . . . . . . . . . . . . . 15 0 < (1 / 2)
1435, 60, 142ltleii 10198 . . . . . . . . . . . . . 14 0 ≤ (1 / 2)
144 halflt1 11288 . . . . . . . . . . . . . . 15 (1 / 2) < 1
14560, 6, 144ltleii 10198 . . . . . . . . . . . . . 14 (1 / 2) ≤ 1
1465, 6elicc2i 12277 . . . . . . . . . . . . . 14 ((1 / 2) ∈ (0[,]1) ↔ ((1 / 2) ∈ ℝ ∧ 0 ≤ (1 / 2) ∧ (1 / 2) ≤ 1))
14760, 143, 145, 146mpbir3an 1263 . . . . . . . . . . . . 13 (1 / 2) ∈ (0[,]1)
148 1elunit 12329 . . . . . . . . . . . . 13 1 ∈ (0[,]1)
149 iccss2 12282 . . . . . . . . . . . . 13 (((1 / 2) ∈ (0[,]1) ∧ 1 ∈ (0[,]1)) → ((1 / 2)[,]1) ⊆ (0[,]1))
150147, 148, 149mp2an 708 . . . . . . . . . . . 12 ((1 / 2)[,]1) ⊆ (0[,]1)
151150sseli 3632 . . . . . . . . . . 11 (𝑥 ∈ ((1 / 2)[,]1) → 𝑥 ∈ (0[,]1))
1524, 25div0i 10797 . . . . . . . . . . . 12 (0 / 2) = 0
153 eqid 2651 . . . . . . . . . . . 12 (1 / 2) = (1 / 2)
1545, 6, 21, 152, 153icccntri 12351 . . . . . . . . . . 11 (𝑥 ∈ (0[,]1) → (𝑥 / 2) ∈ (0[,](1 / 2)))
15532addid2i 10262 . . . . . . . . . . . 12 (0 + (1 / 2)) = (1 / 2)
1565, 60, 60, 155, 84iccshftri 12345 . . . . . . . . . . 11 ((𝑥 / 2) ∈ (0[,](1 / 2)) → ((𝑥 / 2) + (1 / 2)) ∈ ((1 / 2)[,]1))
157151, 154, 1563syl 18 . . . . . . . . . 10 (𝑥 ∈ ((1 / 2)[,]1) → ((𝑥 / 2) + (1 / 2)) ∈ ((1 / 2)[,]1))
15841, 45, 91pcoval2 22862 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 / 2) + (1 / 2)) ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = ((𝐺(*𝑝𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)))
159157, 158sylan2 490 . . . . . . . . 9 ((𝜑𝑥 ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = ((𝐺(*𝑝𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)))
16060, 6elicc2i 12277 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((1 / 2)[,]1) ↔ (𝑥 ∈ ℝ ∧ (1 / 2) ≤ 𝑥𝑥 ≤ 1))
161160simp1bi 1096 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((1 / 2)[,]1) → 𝑥 ∈ ℝ)
162161recnd 10106 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((1 / 2)[,]1) → 𝑥 ∈ ℂ)
16382a1i 11 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((1 / 2)[,]1) → 1 ∈ ℂ)
164 2cnd 11131 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((1 / 2)[,]1) → 2 ∈ ℂ)
16525a1i 11 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((1 / 2)[,]1) → 2 ≠ 0)
166162, 163, 164, 165divdird 10877 . . . . . . . . . . . . . . 15 (𝑥 ∈ ((1 / 2)[,]1) → ((𝑥 + 1) / 2) = ((𝑥 / 2) + (1 / 2)))
167166oveq2d 6706 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 2)[,]1) → (2 · ((𝑥 + 1) / 2)) = (2 · ((𝑥 / 2) + (1 / 2))))
168 peano2cn 10246 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℂ → (𝑥 + 1) ∈ ℂ)
169162, 168syl 17 . . . . . . . . . . . . . . 15 (𝑥 ∈ ((1 / 2)[,]1) → (𝑥 + 1) ∈ ℂ)
170169, 164, 165divcan2d 10841 . . . . . . . . . . . . . 14 (𝑥 ∈ ((1 / 2)[,]1) → (2 · ((𝑥 + 1) / 2)) = (𝑥 + 1))
171167, 170eqtr3d 2687 . . . . . . . . . . . . 13 (𝑥 ∈ ((1 / 2)[,]1) → (2 · ((𝑥 / 2) + (1 / 2))) = (𝑥 + 1))
172171oveq1d 6705 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 2)[,]1) → ((2 · ((𝑥 / 2) + (1 / 2))) − 1) = ((𝑥 + 1) − 1))
173 pncan 10325 . . . . . . . . . . . . 13 ((𝑥 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑥 + 1) − 1) = 𝑥)
174162, 82, 173sylancl 695 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 2)[,]1) → ((𝑥 + 1) − 1) = 𝑥)
175172, 174eqtrd 2685 . . . . . . . . . . 11 (𝑥 ∈ ((1 / 2)[,]1) → ((2 · ((𝑥 / 2) + (1 / 2))) − 1) = 𝑥)
176175fveq2d 6233 . . . . . . . . . 10 (𝑥 ∈ ((1 / 2)[,]1) → ((𝐺(*𝑝𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)) = ((𝐺(*𝑝𝐽)𝐻)‘𝑥))
177176adantl 481 . . . . . . . . 9 ((𝜑𝑥 ∈ ((1 / 2)[,]1)) → ((𝐺(*𝑝𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)) = ((𝐺(*𝑝𝐽)𝐻)‘𝑥))
17842, 43, 44pcoval2 22862 . . . . . . . . 9 ((𝜑𝑥 ∈ ((1 / 2)[,]1)) → ((𝐺(*𝑝𝐽)𝐻)‘𝑥) = (𝐻‘((2 · 𝑥) − 1)))
179159, 177, 1783eqtrd 2689 . . . . . . . 8 ((𝜑𝑥 ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1)))
180141, 179sylan2 490 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 ≤ (1 / 2))) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1)))
181180anassrs 681 . . . . . 6 (((𝜑𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1)))
182 iffalse 4128 . . . . . . . 8 𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = ((𝑥 / 2) + (1 / 2)))
183182fveq2d 6233 . . . . . . 7 𝑥 ≤ (1 / 2) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))))
184183adantl 481 . . . . . 6 (((𝜑𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))))
185 iffalse 4128 . . . . . . 7 𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = (𝐻‘((2 · 𝑥) − 1)))
186185adantl 481 . . . . . 6 (((𝜑𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = (𝐻‘((2 · 𝑥) − 1)))
187181, 184, 1863eqtr4d 2695 . . . . 5 (((𝜑𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))))
188140, 187pm2.61dan 849 . . . 4 ((𝜑𝑥 ∈ (0[,]1)) → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))))
189188mpteq2dva 4777 . . 3 (𝜑 → (𝑥 ∈ (0[,]1) ↦ ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))))) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1)))))
190 pcoass.7 . . . . . . 7 𝑃 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))))
191 iitopon 22729 . . . . . . . . 9 II ∈ (TopOn‘(0[,]1))
192191a1i 11 . . . . . . . 8 (𝜑 → II ∈ (TopOn‘(0[,]1)))
193192cnmptid 21512 . . . . . . . 8 (𝜑 → (𝑥 ∈ (0[,]1) ↦ 𝑥) ∈ (II Cn II))
194 0elunit 12328 . . . . . . . . . 10 0 ∈ (0[,]1)
195194a1i 11 . . . . . . . . 9 (𝜑 → 0 ∈ (0[,]1))
196192, 192, 195cnmptc 21513 . . . . . . . 8 (𝜑 → (𝑥 ∈ (0[,]1) ↦ 0) ∈ (II Cn II))
197 eqid 2651 . . . . . . . . 9 (topGen‘ran (,)) = (topGen‘ran (,))
198 eqid 2651 . . . . . . . . 9 ((topGen‘ran (,)) ↾t (0[,](1 / 2))) = ((topGen‘ran (,)) ↾t (0[,](1 / 2)))
199 eqid 2651 . . . . . . . . 9 ((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) = ((topGen‘ran (,)) ↾t ((1 / 2)[,]1))
200 dfii2 22732 . . . . . . . . 9 II = ((topGen‘ran (,)) ↾t (0[,]1))
201 0red 10079 . . . . . . . . 9 (𝜑 → 0 ∈ ℝ)
202 1red 10093 . . . . . . . . 9 (𝜑 → 1 ∈ ℝ)
203147a1i 11 . . . . . . . . 9 (𝜑 → (1 / 2) ∈ (0[,]1))
204 simprl 809 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → 𝑦 = (1 / 2))
205204oveq1d 6705 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 2) + (1 / 4)))
20632, 23addcomi 10265 . . . . . . . . . . 11 ((1 / 2) + (1 / 4)) = ((1 / 4) + (1 / 2))
207205, 206syl6eq 2701 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 4) + (1 / 2)))
20818, 60ltnlei 10196 . . . . . . . . . . . . 13 ((1 / 4) < (1 / 2) ↔ ¬ (1 / 2) ≤ (1 / 4))
20978, 208mpbi 220 . . . . . . . . . . . 12 ¬ (1 / 2) ≤ (1 / 4)
210204breq1d 4695 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 ≤ (1 / 4) ↔ (1 / 2) ≤ (1 / 4)))
211209, 210mtbiri 316 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → ¬ 𝑦 ≤ (1 / 4))
212211iffalsed 4130 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))) = (𝑦 + (1 / 4)))
213204oveq1d 6705 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 / 2) = ((1 / 2) / 2))
214213, 30syl6eq 2701 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 / 2) = (1 / 4))
215214oveq1d 6705 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → ((𝑦 / 2) + (1 / 2)) = ((1 / 4) + (1 / 2)))
216207, 212, 2153eqtr4d 2695 . . . . . . . . 9 ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))) = ((𝑦 / 2) + (1 / 2)))
217 eqid 2651 . . . . . . . . . 10 ((topGen‘ran (,)) ↾t (0[,](1 / 4))) = ((topGen‘ran (,)) ↾t (0[,](1 / 4)))
218 eqid 2651 . . . . . . . . . 10 ((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2))) = ((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2)))
21960a1i 11 . . . . . . . . . 10 (𝜑 → (1 / 2) ∈ ℝ)
22074, 76recgt0ii 10967 . . . . . . . . . . . . 13 0 < (1 / 4)
2215, 18, 220ltleii 10198 . . . . . . . . . . . 12 0 ≤ (1 / 4)
2225, 60elicc2i 12277 . . . . . . . . . . . 12 ((1 / 4) ∈ (0[,](1 / 2)) ↔ ((1 / 4) ∈ ℝ ∧ 0 ≤ (1 / 4) ∧ (1 / 4) ≤ (1 / 2)))
22318, 221, 79, 222mpbir3an 1263 . . . . . . . . . . 11 (1 / 4) ∈ (0[,](1 / 2))
224223a1i 11 . . . . . . . . . 10 (𝜑 → (1 / 4) ∈ (0[,](1 / 2)))
225 simprl 809 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → 𝑦 = (1 / 4))
226225oveq2d 6706 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = (2 · (1 / 4)))
227225oveq1d 6705 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 4) + (1 / 4)))
22824, 226, 2273eqtr4a 2711 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = (𝑦 + (1 / 4)))
229 retopon 22614 . . . . . . . . . . . . 13 (topGen‘ran (,)) ∈ (TopOn‘ℝ)
230 0xr 10124 . . . . . . . . . . . . . . . 16 0 ∈ ℝ*
23160rexri 10135 . . . . . . . . . . . . . . . 16 (1 / 2) ∈ ℝ*
232 lbicc2 12326 . . . . . . . . . . . . . . . 16 ((0 ∈ ℝ* ∧ (1 / 2) ∈ ℝ* ∧ 0 ≤ (1 / 2)) → 0 ∈ (0[,](1 / 2)))
233230, 231, 143, 232mp3an 1464 . . . . . . . . . . . . . . 15 0 ∈ (0[,](1 / 2))
234 iccss2 12282 . . . . . . . . . . . . . . 15 ((0 ∈ (0[,](1 / 2)) ∧ (1 / 4) ∈ (0[,](1 / 2))) → (0[,](1 / 4)) ⊆ (0[,](1 / 2)))
235233, 223, 234mp2an 708 . . . . . . . . . . . . . 14 (0[,](1 / 4)) ⊆ (0[,](1 / 2))
236 iccssre 12293 . . . . . . . . . . . . . . 15 ((0 ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (0[,](1 / 2)) ⊆ ℝ)
2375, 60, 236mp2an 708 . . . . . . . . . . . . . 14 (0[,](1 / 2)) ⊆ ℝ
238235, 237sstri 3645 . . . . . . . . . . . . 13 (0[,](1 / 4)) ⊆ ℝ
239 resttopon 21013 . . . . . . . . . . . . 13 (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 / 4)) ⊆ ℝ) → ((topGen‘ran (,)) ↾t (0[,](1 / 4))) ∈ (TopOn‘(0[,](1 / 4))))
240229, 238, 239mp2an 708 . . . . . . . . . . . 12 ((topGen‘ran (,)) ↾t (0[,](1 / 4))) ∈ (TopOn‘(0[,](1 / 4)))
241240a1i 11 . . . . . . . . . . 11 (𝜑 → ((topGen‘ran (,)) ↾t (0[,](1 / 4))) ∈ (TopOn‘(0[,](1 / 4))))
242241, 192cnmpt1st 21519 . . . . . . . . . . 11 (𝜑 → (𝑦 ∈ (0[,](1 / 4)), 𝑧 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,)) ↾t (0[,](1 / 4))) ×t II) Cn ((topGen‘ran (,)) ↾t (0[,](1 / 4)))))
243 retop 22612 . . . . . . . . . . . . . 14 (topGen‘ran (,)) ∈ Top
244 ovex 6718 . . . . . . . . . . . . . 14 (0[,](1 / 2)) ∈ V
245 restabs 21017 . . . . . . . . . . . . . 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))))
246243, 235, 244, 245mp3an 1464 . . . . . . . . . . . . 13 (((topGen‘ran (,)) ↾t (0[,](1 / 2))) ↾t (0[,](1 / 4))) = ((topGen‘ran (,)) ↾t (0[,](1 / 4)))
247246eqcomi 2660 . . . . . . . . . . . 12 ((topGen‘ran (,)) ↾t (0[,](1 / 4))) = (((topGen‘ran (,)) ↾t (0[,](1 / 2))) ↾t (0[,](1 / 4)))
248 resttopon 21013 . . . . . . . . . . . . . 14 (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 / 2)) ⊆ ℝ) → ((topGen‘ran (,)) ↾t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 / 2))))
249229, 237, 248mp2an 708 . . . . . . . . . . . . 13 ((topGen‘ran (,)) ↾t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 / 2)))
250249a1i 11 . . . . . . . . . . . 12 (𝜑 → ((topGen‘ran (,)) ↾t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 / 2))))
251235a1i 11 . . . . . . . . . . . 12 (𝜑 → (0[,](1 / 4)) ⊆ (0[,](1 / 2)))
252198iihalf1cn 22778 . . . . . . . . . . . . 13 (𝑥 ∈ (0[,](1 / 2)) ↦ (2 · 𝑥)) ∈ (((topGen‘ran (,)) ↾t (0[,](1 / 2))) Cn II)
253252a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ (0[,](1 / 2)) ↦ (2 · 𝑥)) ∈ (((topGen‘ran (,)) ↾t (0[,](1 / 2))) Cn II))
254247, 250, 251, 253cnmpt1res 21527 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ (0[,](1 / 4)) ↦ (2 · 𝑥)) ∈ (((topGen‘ran (,)) ↾t (0[,](1 / 4))) Cn II))
255 oveq2 6698 . . . . . . . . . . 11 (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
256241, 192, 242, 241, 254, 255cnmpt21 21522 . . . . . . . . . 10 (𝜑 → (𝑦 ∈ (0[,](1 / 4)), 𝑧 ∈ (0[,]1) ↦ (2 · 𝑦)) ∈ ((((topGen‘ran (,)) ↾t (0[,](1 / 4))) ×t II) Cn II))
257 iccssre 12293 . . . . . . . . . . . . . 14 (((1 / 4) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → ((1 / 4)[,](1 / 2)) ⊆ ℝ)
25818, 60, 257mp2an 708 . . . . . . . . . . . . 13 ((1 / 4)[,](1 / 2)) ⊆ ℝ
259 resttopon 21013 . . . . . . . . . . . . 13 (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 / 4)[,](1 / 2)) ⊆ ℝ) → ((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2))) ∈ (TopOn‘((1 / 4)[,](1 / 2))))
260229, 258, 259mp2an 708 . . . . . . . . . . . 12 ((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2))) ∈ (TopOn‘((1 / 4)[,](1 / 2)))
261260a1i 11 . . . . . . . . . . 11 (𝜑 → ((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2))) ∈ (TopOn‘((1 / 4)[,](1 / 2))))
262261, 192cnmpt1st 21519 . . . . . . . . . . 11 (𝜑 → (𝑦 ∈ ((1 / 4)[,](1 / 2)), 𝑧 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2))) ×t II) Cn ((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2)))))
263 eqid 2651 . . . . . . . . . . . 12 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
264258a1i 11 . . . . . . . . . . . 12 (𝜑 → ((1 / 4)[,](1 / 2)) ⊆ ℝ)
265 unitssre 12357 . . . . . . . . . . . . 13 (0[,]1) ⊆ ℝ
266265a1i 11 . . . . . . . . . . . 12 (𝜑 → (0[,]1) ⊆ ℝ)
267150, 87sseldi 3634 . . . . . . . . . . . . 13 (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ∈ (0[,]1))
268267adantl 481 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((1 / 4)[,](1 / 2))) → (𝑥 + (1 / 4)) ∈ (0[,]1))
269263cnfldtopon 22633 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
270269a1i 11 . . . . . . . . . . . . 13 (𝜑 → (TopOpen‘ℂfld) ∈ (TopOn‘ℂ))
271270cnmptid 21512 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ ℂ ↦ 𝑥) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
27218a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (1 / 4) ∈ ℝ)
273272recnd 10106 . . . . . . . . . . . . . 14 (𝜑 → (1 / 4) ∈ ℂ)
274270, 270, 273cnmptc 21513 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ ℂ ↦ (1 / 4)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
275263addcn 22715 . . . . . . . . . . . . . 14 + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
276275a1i 11 . . . . . . . . . . . . 13 (𝜑 → + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
277270, 271, 274, 276cnmpt12f 21517 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ ℂ ↦ (𝑥 + (1 / 4))) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
278263, 218, 200, 264, 266, 268, 277cnmptre 22773 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ ((1 / 4)[,](1 / 2)) ↦ (𝑥 + (1 / 4))) ∈ (((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2))) Cn II))
279 oveq1 6697 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑥 + (1 / 4)) = (𝑦 + (1 / 4)))
280261, 192, 262, 261, 278, 279cnmpt21 21522 . . . . . . . . . 10 (𝜑 → (𝑦 ∈ ((1 / 4)[,](1 / 2)), 𝑧 ∈ (0[,]1) ↦ (𝑦 + (1 / 4))) ∈ ((((topGen‘ran (,)) ↾t ((1 / 4)[,](1 / 2))) ×t II) Cn II))
281197, 217, 218, 198, 201, 219, 224, 192, 228, 256, 280cnmpt2pc 22774 . . . . . . . . 9 (𝜑 → (𝑦 ∈ (0[,](1 / 2)), 𝑧 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4)))) ∈ ((((topGen‘ran (,)) ↾t (0[,](1 / 2))) ×t II) Cn II))
282 iccssre 12293 . . . . . . . . . . . . 13 (((1 / 2) ∈ ℝ ∧ 1 ∈ ℝ) → ((1 / 2)[,]1) ⊆ ℝ)
28360, 6, 282mp2an 708 . . . . . . . . . . . 12 ((1 / 2)[,]1) ⊆ ℝ
284 resttopon 21013 . . . . . . . . . . . 12 (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 / 2)[,]1) ⊆ ℝ) → ((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1)))
285229, 283, 284mp2an 708 . . . . . . . . . . 11 ((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1))
286285a1i 11 . . . . . . . . . 10 (𝜑 → ((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1)))
287286, 192cnmpt1st 21519 . . . . . . . . . 10 (𝜑 → (𝑦 ∈ ((1 / 2)[,]1), 𝑧 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ×t II) Cn ((topGen‘ran (,)) ↾t ((1 / 2)[,]1))))
288283a1i 11 . . . . . . . . . . 11 (𝜑 → ((1 / 2)[,]1) ⊆ ℝ)
289150, 157sseldi 3634 . . . . . . . . . . . 12 (𝑥 ∈ ((1 / 2)[,]1) → ((𝑥 / 2) + (1 / 2)) ∈ (0[,]1))
290289adantl 481 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((1 / 2)[,]1)) → ((𝑥 / 2) + (1 / 2)) ∈ (0[,]1))
291263divccn 22723 . . . . . . . . . . . . . 14 ((2 ∈ ℂ ∧ 2 ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
2924, 25, 291mp2an 708 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld))
293292a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
29432a1i 11 . . . . . . . . . . . . 13 (𝜑 → (1 / 2) ∈ ℂ)
295270, 270, 294cnmptc 21513 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ ℂ ↦ (1 / 2)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
296270, 293, 295, 276cnmpt12f 21517 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ ℂ ↦ ((𝑥 / 2) + (1 / 2))) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
297263, 199, 200, 288, 266, 290, 296cnmptre 22773 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ ((1 / 2)[,]1) ↦ ((𝑥 / 2) + (1 / 2))) ∈ (((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) Cn II))
298 oveq1 6697 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑥 / 2) = (𝑦 / 2))
299298oveq1d 6705 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝑥 / 2) + (1 / 2)) = ((𝑦 / 2) + (1 / 2)))
300286, 192, 287, 286, 297, 299cnmpt21 21522 . . . . . . . . 9 (𝜑 → (𝑦 ∈ ((1 / 2)[,]1), 𝑧 ∈ (0[,]1) ↦ ((𝑦 / 2) + (1 / 2))) ∈ ((((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ×t II) Cn II))
301197, 198, 199, 200, 201, 202, 203, 192, 216, 281, 300cnmpt2pc 22774 . . . . . . . 8 (𝜑 → (𝑦 ∈ (0[,]1), 𝑧 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 2), if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))), ((𝑦 / 2) + (1 / 2)))) ∈ ((II ×t II) Cn II))
302 breq1 4688 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥 ≤ (1 / 2) ↔ 𝑦 ≤ (1 / 2)))
303 breq1 4688 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑥 ≤ (1 / 4) ↔ 𝑦 ≤ (1 / 4)))
304303, 255, 279ifbieq12d 4146 . . . . . . . . . . . 12 (𝑥 = 𝑦 → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))))
305302, 304, 299ifbieq12d 4146 . . . . . . . . . . 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))))
306305equcoms 1993 . . . . . . . . . 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))))
307306adantr 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))))
308307eqcomd 2657 . . . . . . . 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))))
309192, 193, 196, 192, 192, 301, 308cnmpt12 21518 . . . . . . 7 (𝜑 → (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) ∈ (II Cn II))
310190, 309syl5eqel 2734 . . . . . 6 (𝜑𝑃 ∈ (II Cn II))
311 iiuni 22731 . . . . . . 7 (0[,]1) = II
312311, 311cnf 21098 . . . . . 6 (𝑃 ∈ (II Cn II) → 𝑃:(0[,]1)⟶(0[,]1))
313310, 312syl 17 . . . . 5 (𝜑𝑃:(0[,]1)⟶(0[,]1))
314190fmpt 6421 . . . . 5 (∀𝑥 ∈ (0[,]1)if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) ∈ (0[,]1) ↔ 𝑃:(0[,]1)⟶(0[,]1))
315313, 314sylibr 224 . . . 4 (𝜑 → ∀𝑥 ∈ (0[,]1)if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) ∈ (0[,]1))
316190a1i 11 . . . 4 (𝜑𝑃 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))))
31741, 45, 91pcocn 22863 . . . . . 6 (𝜑 → (𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)) ∈ (II Cn 𝐽))
318 eqid 2651 . . . . . . 7 𝐽 = 𝐽
319311, 318cnf 21098 . . . . . 6 ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)) ∈ (II Cn 𝐽) → (𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)):(0[,]1)⟶ 𝐽)
320317, 319syl 17 . . . . 5 (𝜑 → (𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)):(0[,]1)⟶ 𝐽)
321320feqmptd 6288 . . . 4 (𝜑 → (𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)) = (𝑦 ∈ (0[,]1) ↦ ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘𝑦)))
322 fveq2 6229 . . . 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)))))
323315, 316, 321, 322fmptcof 6437 . . 3 (𝜑 → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)) ∘ 𝑃) = (𝑥 ∈ (0[,]1) ↦ ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))))))
32441, 42, 89pcocn 22863 . . . 4 (𝜑 → (𝐹(*𝑝𝐽)𝐺) ∈ (II Cn 𝐽))
325324, 43pcoval 22857 . . 3 (𝜑 → ((𝐹(*𝑝𝐽)𝐺)(*𝑝𝐽)𝐻) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), ((𝐹(*𝑝𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1)))))
326189, 323, 3253eqtr4rd 2696 . 2 (𝜑 → ((𝐹(*𝑝𝐽)𝐺)(*𝑝𝐽)𝐻) = ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)) ∘ 𝑃))
327 id 22 . . . . . . . 8 (𝑥 = 0 → 𝑥 = 0)
328327, 143syl6eqbr 4724 . . . . . . 7 (𝑥 = 0 → 𝑥 ≤ (1 / 2))
329328iftrued 4127 . . . . . 6 (𝑥 = 0 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))))
330327, 221syl6eqbr 4724 . . . . . . 7 (𝑥 = 0 → 𝑥 ≤ (1 / 4))
331330iftrued 4127 . . . . . 6 (𝑥 = 0 → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (2 · 𝑥))
332 oveq2 6698 . . . . . . 7 (𝑥 = 0 → (2 · 𝑥) = (2 · 0))
333 2t0e0 11221 . . . . . . 7 (2 · 0) = 0
334332, 333syl6eq 2701 . . . . . 6 (𝑥 = 0 → (2 · 𝑥) = 0)
335329, 331, 3343eqtrd 2689 . . . . 5 (𝑥 = 0 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = 0)
336 c0ex 10072 . . . . 5 0 ∈ V
337335, 190, 336fvmpt 6321 . . . 4 (0 ∈ (0[,]1) → (𝑃‘0) = 0)
338195, 337syl 17 . . 3 (𝜑 → (𝑃‘0) = 0)
339148a1i 11 . . . 4 (𝜑 → 1 ∈ (0[,]1))
34060, 6ltnlei 10196 . . . . . . . . 9 ((1 / 2) < 1 ↔ ¬ 1 ≤ (1 / 2))
341144, 340mpbi 220 . . . . . . . 8 ¬ 1 ≤ (1 / 2)
342 breq1 4688 . . . . . . . 8 (𝑥 = 1 → (𝑥 ≤ (1 / 2) ↔ 1 ≤ (1 / 2)))
343341, 342mtbiri 316 . . . . . . 7 (𝑥 = 1 → ¬ 𝑥 ≤ (1 / 2))
344343iffalsed 4130 . . . . . 6 (𝑥 = 1 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = ((𝑥 / 2) + (1 / 2)))
345 oveq1 6697 . . . . . . . 8 (𝑥 = 1 → (𝑥 / 2) = (1 / 2))
346345oveq1d 6705 . . . . . . 7 (𝑥 = 1 → ((𝑥 / 2) + (1 / 2)) = ((1 / 2) + (1 / 2)))
347346, 84syl6eq 2701 . . . . . 6 (𝑥 = 1 → ((𝑥 / 2) + (1 / 2)) = 1)
348344, 347eqtrd 2685 . . . . 5 (𝑥 = 1 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = 1)
349 1ex 10073 . . . . 5 1 ∈ V
350348, 190, 349fvmpt 6321 . . . 4 (1 ∈ (0[,]1) → (𝑃‘1) = 1)
351339, 350syl 17 . . 3 (𝜑 → (𝑃‘1) = 1)
352317, 310, 338, 351reparpht 22844 . 2 (𝜑 → ((𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)) ∘ 𝑃)( ≃ph𝐽)(𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)))
353326, 352eqbrtrd 4707 1 (𝜑 → ((𝐹(*𝑝𝐽)𝐺)(*𝑝𝐽)𝐻)( ≃ph𝐽)(𝐹(*𝑝𝐽)(𝐺(*𝑝𝐽)𝐻)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 382   ∧ wa 383   = wceq 1523   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  Vcvv 3231   ⊆ wss 3607  ifcif 4119  ∪ cuni 4468   class class class wbr 4685   ↦ cmpt 4762  ran crn 5144   ∘ ccom 5147  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979  ℝ*cxr 10111   < clt 10112   ≤ cle 10113   − cmin 10304   / cdiv 10722  ℕcn 11058  2c2 11108  4c4 11110  (,)cioo 12213  [,]cicc 12216   ↾t crest 16128  TopOpenctopn 16129  topGenctg 16145  ℂfldccnfld 19794  Topctop 20746  TopOnctopon 20763   Cn ccn 21076   ×t ctx 21411  IIcii 22725   ≃phcphtpc 22815  *𝑝cpco 22846 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053  ax-mulf 10054 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-icc 12220  df-fz 12365  df-fzo 12505  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-mulr 16002  df-starv 16003  df-sca 16004  df-vsca 16005  df-ip 16006  df-tset 16007  df-ple 16008  df-ds 16011  df-unif 16012  df-hom 16013  df-cco 16014  df-rest 16130  df-topn 16131  df-0g 16149  df-gsum 16150  df-topgen 16151  df-pt 16152  df-prds 16155  df-xrs 16209  df-qtop 16214  df-imas 16215  df-xps 16217  df-mre 16293  df-mrc 16294  df-acs 16296  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-submnd 17383  df-mulg 17588  df-cntz 17796  df-cmn 18241  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-cnfld 19795  df-top 20747  df-topon 20764  df-topsp 20785  df-bases 20798  df-cld 20871  df-cn 21079  df-cnp 21080  df-tx 21413  df-hmeo 21606  df-xms 22172  df-ms 22173  df-tms 22174  df-ii 22727  df-htpy 22816  df-phtpy 22817  df-phtpc 22838  df-pco 22851 This theorem is referenced by:  pcophtb  22875  pi1grplem  22895  pi1xfr  22901  pi1xfrcnvlem  22902
 Copyright terms: Public domain W3C validator