pcoass - Metamath Proof Explorer

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

Theorem pcoass 25151

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.

Step	Hyp	Ref	Expression
1		iftrue 4498	. . . . . . . . . . 11 ⊢ (𝑥 ≤ (1 / 4) → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (2 · 𝑥))
2	1	fveq2d 6886	. . . . . . . . . 10 ⊢ (𝑥 ≤ (1 / 4) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(2 · 𝑥)))
3	2	adantl 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(2 · 𝑥)))
4		2cn 12315	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℂ
5		elicc01 13492	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (0[,]1) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1))
6	5	simp1bi 1161	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0[,]1) → 𝑥 ∈ ℝ)
7	6	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℝ)
8	7	recnd 11236	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℂ)
9		mulcom 11185	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) = (𝑥 · 2))
10	4, 8, 9	sylancr 598	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) = (𝑥 · 2))
11	5	simp2bi 1162	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0[,]1) → 0 ≤ 𝑥)
12	11	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 0 ≤ 𝑥)
13		simpr 489	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ≤ (1 / 4))
14		0re 11209	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℝ
15		4nn 12323	. . . . . . . . . . . . . . . 16 ⊢ 4 ∈ ℕ
16		nnrecre 12277	. . . . . . . . . . . . . . . 16 ⊢ (4 ∈ ℕ → (1 / 4) ∈ ℝ)
17	15, 16	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (1 / 4) ∈ ℝ
18	14, 17	elicc2i 13438	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (0[,](1 / 4)) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ (1 / 4)))
19	7, 12, 13, 18	syl3anbrc 1360	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ (0[,](1 / 4)))
20		2rp 13020	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℝ⁺
21	4	mul02i 11398	. . . . . . . . . . . . . 14 ⊢ (0 · 2) = 0
22	17	recni 11222	. . . . . . . . . . . . . . 15 ⊢ (1 / 4) ∈ ℂ
23	22	2timesi 12377	. . . . . . . . . . . . . . . 16 ⊢ (2 · (1 / 4)) = ((1 / 4) + (1 / 4))
24		2ne0 12346	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ≠ 0
25		recdiv2 11927	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((1 / 2) / 2) = (1 / (2 · 2)))
26	4, 24, 4, 24, 25	mp4an 705	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 / 2) / 2) = (1 / (2 · 2))
27		2t2e4 12403	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2 · 2) = 4
28	27	oveq2i 7422	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 / (2 · 2)) = (1 / 4)
29	26, 28	eqtri 2792	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 / 2) / 2) = (1 / 4)
30	29, 29	oveq12i 7423	. . . . . . . . . . . . . . . . 17 ⊢ (((1 / 2) / 2) + ((1 / 2) / 2)) = ((1 / 4) + (1 / 4))
31		halfcn 12457	. . . . . . . . . . . . . . . . . 18 ⊢ (1 / 2) ∈ ℂ
32		2halves 12461	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 / 2) ∈ ℂ → (((1 / 2) / 2) + ((1 / 2) / 2)) = (1 / 2))
33	31, 32	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (((1 / 2) / 2) + ((1 / 2) / 2)) = (1 / 2)
34	30, 33	eqtr3i 2794	. . . . . . . . . . . . . . . 16 ⊢ ((1 / 4) + (1 / 4)) = (1 / 2)
35	23, 34	eqtri 2792	. . . . . . . . . . . . . . 15 ⊢ (2 · (1 / 4)) = (1 / 2)
36	4, 22, 35	mulcomli 11217	. . . . . . . . . . . . . 14 ⊢ ((1 / 4) · 2) = (1 / 2)
37	14, 17, 20, 21, 36	iccdili 13517	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (0[,](1 / 4)) → (𝑥 · 2) ∈ (0[,](1 / 2)))
38	19, 37	syl 18	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → (𝑥 · 2) ∈ (0[,](1 / 2)))
39	10, 38	eqeltrd 2869	. . . . . . . . . . 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))
44	41, 42, 43	pcocn 25144	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺(*_𝑝‘𝐽)𝐻) ∈ (II Cn 𝐽))
45	40, 44	pcoval1 25140	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(2 · 𝑥)) = (𝐹‘(2 · (2 · 𝑥))))
46	40, 41	pcoval1 25140	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) → ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)) = (𝐹‘(2 · (2 · 𝑥))))
47	45, 46	eqtr4d 2807	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
48	39, 47	sylan2 604	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4))) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
49	48	anassrs 472	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
50	3, 49	eqtrd 2804	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
51	50	adantlr 727	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
52		simplll 786	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝜑)
53	6	ad2antlr 739	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → 𝑥 ∈ ℝ)
54	53	adantr 485	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℝ)
55		letric 11309	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ ∧ (1 / 4) ∈ ℝ) → (𝑥 ≤ (1 / 4) ∨ (1 / 4) ≤ 𝑥))
56	53, 17, 55	sylancl 597	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → (𝑥 ≤ (1 / 4) ∨ (1 / 4) ≤ 𝑥))
57	56	orcanai 1018	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (1 / 4) ≤ 𝑥)
58		simplr 780	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ≤ (1 / 2))
59		halfre 12456	. . . . . . . . . . . . 13 ⊢ (1 / 2) ∈ ℝ
60	17, 59	elicc2i 13438	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) ↔ (𝑥 ∈ ℝ ∧ (1 / 4) ≤ 𝑥 ∧ 𝑥 ≤ (1 / 2)))
61	54, 57, 58, 60	syl3anbrc 1360	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ((1 / 4)[,](1 / 2)))
62	60	simp1bi 1161	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → 𝑥 ∈ ℝ)
63		readdcl 11182	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ ∧ (1 / 4) ∈ ℝ) → (𝑥 + (1 / 4)) ∈ ℝ)
64	62, 17, 63	sylancl 597	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ∈ ℝ)
65	17	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 4) ∈ ℝ)
66	60	simp2bi 1162	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 4) ≤ 𝑥)
67	65, 62, 65, 66	leadd1dd 11827	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → ((1 / 4) + (1 / 4)) ≤ (𝑥 + (1 / 4)))
68	34, 67	eqbrtrrid 5151	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 2) ≤ (𝑥 + (1 / 4)))
69	59	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 2) ∈ ℝ)
70	60	simp3bi 1163	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → 𝑥 ≤ (1 / 2))
71		2lt4 12417	. . . . . . . . . . . . . . . . 17 ⊢ 2 < 4
72		2re 12314	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ
73		4re 12324	. . . . . . . . . . . . . . . . . 18 ⊢ 4 ∈ ℝ
74		2pos 12344	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 2
75		4pos 12350	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 4
76	72, 73, 74, 75	ltrecii 12130	. . . . . . . . . . . . . . . . 17 ⊢ (2 < 4 ↔ (1 / 4) < (1 / 2))
77	71, 76	mpbi 233	. . . . . . . . . . . . . . . 16 ⊢ (1 / 4) < (1 / 2)
78	17, 59, 77	ltleii 11332	. . . . . . . . . . . . . . 15 ⊢ (1 / 4) ≤ (1 / 2)
79	78	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 4) ≤ (1 / 2))
80	62, 65, 69, 69, 70, 79	le2addd 11832	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ≤ ((1 / 2) + (1 / 2)))
81		ax-1cn 11157	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
82		2halves 12461	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℂ → ((1 / 2) + (1 / 2)) = 1)
83	81, 82	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((1 / 2) + (1 / 2)) = 1
84	80, 83	breqtrdi 5156	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ≤ 1)
85		1re 11207	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ
86	59, 85	elicc2i 13438	. . . . . . . . . . . 12 ⊢ ((𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1) ↔ ((𝑥 + (1 / 4)) ∈ ℝ ∧ (1 / 2) ≤ (𝑥 + (1 / 4)) ∧ (𝑥 + (1 / 4)) ≤ 1))
87	64, 68, 84, 86	syl3anbrc 1360	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1))
88	61, 87	syl 18	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1))
89		pcoass.5	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹‘1) = (𝐺‘0))
90	41, 42	pco0 25141	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐺(*_𝑝‘𝐽)𝐻)‘0) = (𝐺‘0))
91	89, 90	eqtr4d 2807	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹‘1) = ((𝐺(*_𝑝‘𝐽)𝐻)‘0))
92	40, 44, 91	pcoval2 25143	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))) = ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)))
93	52, 88, 92	syl2anc 595	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))) = ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)))
94	83	oveq2i 7422	. . . . . . . . . . . 12 ⊢ ((2 · (𝑥 + (1 / 4))) − ((1 / 2) + (1 / 2))) = ((2 · (𝑥 + (1 / 4))) − 1)
95		2cnd 12318	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 2 ∈ ℂ)
96	54	recnd 11236	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℂ)
97	22	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (1 / 4) ∈ ℂ)
98	95, 96, 97	adddid 11232	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · (𝑥 + (1 / 4))) = ((2 · 𝑥) + (2 · (1 / 4))))
99	35	oveq2i 7422	. . . . . . . . . . . . . 14 ⊢ ((2 · 𝑥) + (2 · (1 / 4))) = ((2 · 𝑥) + (1 / 2))
100	98, 99	eqtrdi 2820	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · (𝑥 + (1 / 4))) = ((2 · 𝑥) + (1 / 2)))
101	100	oveq1d 7426	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − ((1 / 2) + (1 / 2))) = (((2 · 𝑥) + (1 / 2)) − ((1 / 2) + (1 / 2))))
102	94, 101	eqtr3id 2818	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − 1) = (((2 · 𝑥) + (1 / 2)) − ((1 / 2) + (1 / 2))))
103		remulcl 11184	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (2 · 𝑥) ∈ ℝ)
104	72, 54, 103	sylancr 598	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈ ℝ)
105	104	recnd 11236	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈ ℂ)
106	31	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (1 / 2) ∈ ℂ)
107	105, 106, 106	pnpcan2d 11606	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (((2 · 𝑥) + (1 / 2)) − ((1 / 2) + (1 / 2))) = ((2 · 𝑥) − (1 / 2)))
108	102, 107	eqtrd 2804	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − 1) = ((2 · 𝑥) − (1 / 2)))
109	108	fveq2d 6886	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(_𝑝‘𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)) = ((𝐺(_𝑝‘𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))))
110	4, 96, 9	sylancr 598	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) = (𝑥 · 2))
111	81, 4, 24	divcan1i 11958	. . . . . . . . . . . . . . 15 ⊢ ((1 / 2) · 2) = 1
112	17, 59, 20, 36, 111	iccdili 13517	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 · 2) ∈ ((1 / 2)[,]1))
113	61, 112	syl 18	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (𝑥 · 2) ∈ ((1 / 2)[,]1))
114	110, 113	eqeltrd 2869	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈ ((1 / 2)[,]1))
115	31	subidi 11528	. . . . . . . . . . . . 13 ⊢ ((1 / 2) − (1 / 2)) = 0
116		1mhlfehlf 12462	. . . . . . . . . . . . 13 ⊢ (1 − (1 / 2)) = (1 / 2)
117	59, 85, 59, 115, 116	iccshftli 13515	. . . . . . . . . . . 12 ⊢ ((2 · 𝑥) ∈ ((1 / 2)[,]1) → ((2 · 𝑥) − (1 / 2)) ∈ (0[,](1 / 2)))
118	114, 117	syl 18	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · 𝑥) − (1 / 2)) ∈ (0[,](1 / 2)))
119	41, 42	pcoval1 25140	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((2 · 𝑥) − (1 / 2)) ∈ (0[,](1 / 2))) → ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))))
120	52, 118, 119	syl2anc 595	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))))
121	95, 105, 106	subdid 11669	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · ((2 · 𝑥) − (1 / 2))) = ((2 · (2 · 𝑥)) − (2 · (1 / 2))))
122	4, 24	recidi 11945	. . . . . . . . . . . . 13 ⊢ (2 · (1 / 2)) = 1
123	122	oveq2i 7422	. . . . . . . . . . . 12 ⊢ ((2 · (2 · 𝑥)) − (2 · (1 / 2))) = ((2 · (2 · 𝑥)) − 1)
124	121, 123	eqtrdi 2820	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · ((2 · 𝑥) − (1 / 2))) = ((2 · (2 · 𝑥)) − 1))
125	124	fveq2d 6886	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
126	120, 125	eqtrd 2804	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
127	93, 109, 126	3eqtrd 2808	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
128		iffalse 4501	. . . . . . . . . 10 ⊢ (¬ 𝑥 ≤ (1 / 4) → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (𝑥 + (1 / 4)))
129	128	fveq2d 6886	. . . . . . . . 9 ⊢ (¬ 𝑥 ≤ (1 / 4) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))))
130	129	adantl 486	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))))
131	40, 41, 89	pcoval2 25143	. . . . . . . . 9 ⊢ ((𝜑 ∧ (2 · 𝑥) ∈ ((1 / 2)[,]1)) → ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
132	52, 114, 131	syl2anc 595	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
133	127, 130, 132	3eqtr4d 2814	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
134	51, 133	pm2.61dan 824	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
135		iftrue 4498	. . . . . . . 8 ⊢ (𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))))
136	135	fveq2d 6886	. . . . . . 7 ⊢ (𝑥 ≤ (1 / 2) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))))
137	136	adantl 486	. . . . . 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 4498	. . . . . . 7 ⊢ (𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), ((𝐹(_𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = ((𝐹(_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
139	138	adantl 486	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → if(𝑥 ≤ (1 / 2), ((𝐹(_𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = ((𝐹(_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
140	134, 137, 139	3eqtr4d 2814	. . . . 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 25063	. . . . . . . 8 ⊢ ((𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 ≤ (1 / 2)) → 𝑥 ∈ ((1 / 2)[,]1))
142		halfge0 12459	. . . . . . . . . . . . . 14 ⊢ 0 ≤ (1 / 2)
143		halflt1 12460	. . . . . . . . . . . . . . 15 ⊢ (1 / 2) < 1
144	59, 85, 143	ltleii 11332	. . . . . . . . . . . . . 14 ⊢ (1 / 2) ≤ 1
145		elicc01 13492	. . . . . . . . . . . . . 14 ⊢ ((1 / 2) ∈ (0[,]1) ↔ ((1 / 2) ∈ ℝ ∧ 0 ≤ (1 / 2) ∧ (1 / 2) ≤ 1))
146	59, 142, 144, 145	mpbir3an 1358	. . . . . . . . . . . . 13 ⊢ (1 / 2) ∈ (0[,]1)
147		1elunit 13496	. . . . . . . . . . . . 13 ⊢ 1 ∈ (0[,]1)
148		iccss2 13443	. . . . . . . . . . . . 13 ⊢ (((1 / 2) ∈ (0[,]1) ∧ 1 ∈ (0[,]1)) → ((1 / 2)[,]1) ⊆ (0[,]1))
149	146, 147, 148	mp2an 704	. . . . . . . . . . . 12 ⊢ ((1 / 2)[,]1) ⊆ (0[,]1)
150	149	sseli 3941	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 𝑥 ∈ (0[,]1))
151	4, 24	div0i 11948	. . . . . . . . . . . 12 ⊢ (0 / 2) = 0
152		eqid 2769	. . . . . . . . . . . 12 ⊢ (1 / 2) = (1 / 2)
153	14, 85, 20, 151, 152	icccntri 13519	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (0[,]1) → (𝑥 / 2) ∈ (0[,](1 / 2)))
154	31	addlidi 11397	. . . . . . . . . . . 12 ⊢ (0 + (1 / 2)) = (1 / 2)
155	14, 59, 59, 154, 83	iccshftri 13513	. . . . . . . . . . 11 ⊢ ((𝑥 / 2) ∈ (0[,](1 / 2)) → ((𝑥 / 2) + (1 / 2)) ∈ ((1 / 2)[,]1))
156	150, 153, 155	3syl 19	. . . . . . . . . 10 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → ((𝑥 / 2) + (1 / 2)) ∈ ((1 / 2)[,]1))
157	40, 44, 91	pcoval2 25143	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 / 2) + (1 / 2)) ∈ ((1 / 2)[,]1)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)))
158	156, 157	sylan2 604	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)))
159	59, 85	elicc2i 13438	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 2)[,]1) ↔ (𝑥 ∈ ℝ ∧ (1 / 2) ≤ 𝑥 ∧ 𝑥 ≤ 1))
160	159	simp1bi 1161	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 𝑥 ∈ ℝ)
161	160	recnd 11236	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 𝑥 ∈ ℂ)
162		1cnd 11201	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 1 ∈ ℂ)
163		2cnd 12318	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 2 ∈ ℂ)
164	24	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 2 ≠ 0)
165	161, 162, 163, 164	divdird 12028	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → ((𝑥 + 1) / 2) = ((𝑥 / 2) + (1 / 2)))
166	165	oveq2d 7427	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → (2 · ((𝑥 + 1) / 2)) = (2 · ((𝑥 / 2) + (1 / 2))))
167		peano2cn 11381	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ → (𝑥 + 1) ∈ ℂ)
168	161, 167	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → (𝑥 + 1) ∈ ℂ)
169	168, 163, 164	divcan2d 11992	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → (2 · ((𝑥 + 1) / 2)) = (𝑥 + 1))
170	166, 169	eqtr3d 2806	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → (2 · ((𝑥 / 2) + (1 / 2))) = (𝑥 + 1))
171	161, 162, 170	mvrraddd 11625	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → ((2 · ((𝑥 / 2) + (1 / 2))) − 1) = 𝑥)
172	171	fveq2d 6886	. . . . . . . . . 10 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → ((𝐺(_𝑝‘𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)) = ((𝐺(_𝑝‘𝐽)𝐻)‘𝑥))
173	172	adantl 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝐺(_𝑝‘𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)) = ((𝐺(_𝑝‘𝐽)𝐻)‘𝑥))
174	41, 42, 43	pcoval2 25143	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝐺(*_𝑝‘𝐽)𝐻)‘𝑥) = (𝐻‘((2 · 𝑥) − 1)))
175	158, 173, 174	3eqtrd 2808	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1)))
176	141, 175	sylan2 604	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 ≤ (1 / 2))) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1)))
177	176	anassrs 472	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1)))
178		iffalse 4501	. . . . . . . 8 ⊢ (¬ 𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = ((𝑥 / 2) + (1 / 2)))
179	178	fveq2d 6886	. . . . . . 7 ⊢ (¬ 𝑥 ≤ (1 / 2) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))))
180	179	adantl 486	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))))
181		iffalse 4501	. . . . . . 7 ⊢ (¬ 𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = (𝐻‘((2 · 𝑥) − 1)))
182	181	adantl 486	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → if(𝑥 ≤ (1 / 2), ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = (𝐻‘((2 · 𝑥) − 1)))
183	177, 180, 182	3eqtr4d 2814	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = if(𝑥 ≤ (1 / 2), ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))))
184	140, 183	pm2.61dan 824	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = if(𝑥 ≤ (1 / 2), ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))))
185	184	mpteq2dva 5208	. . 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 25006	. . . . . . . . 9 ⊢ II ∈ (TopOn‘(0[,]1))
188	187	a1i 11	. . . . . . . 8 ⊢ (𝜑 → II ∈ (TopOn‘(0[,]1)))
189	188	cnmptid 23786	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ 𝑥) ∈ (II Cn II))
190		0elunit 13495	. . . . . . . . . 10 ⊢ 0 ∈ (0[,]1)
191	190	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0[,]1))
192	188, 188, 191	cnmptc 23787	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ 0) ∈ (II Cn II))
193		eqid 2769	. . . . . . . . 9 ⊢ (topGen‘ran (,)) = (topGen‘ran (,))
194		eqid 2769	. . . . . . . . 9 ⊢ ((topGen‘ran (,)) ↾_t (0[,](1 / 2))) = ((topGen‘ran (,)) ↾_t (0[,](1 / 2)))
195		eqid 2769	. . . . . . . . 9 ⊢ ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) = ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1))
196		dfii2 25009	. . . . . . . . 9 ⊢ II = ((topGen‘ran (,)) ↾_t (0[,]1))
197		0red 11210	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ ℝ)
198		1red 11208	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℝ)
199	146	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (1 / 2) ∈ (0[,]1))
200		simprl 782	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → 𝑦 = (1 / 2))
201	200	oveq1d 7426	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 2) + (1 / 4)))
202	31, 22	addcomi 11400	. . . . . . . . . . 11 ⊢ ((1 / 2) + (1 / 4)) = ((1 / 4) + (1 / 2))
203	201, 202	eqtrdi 2820	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 4) + (1 / 2)))
204	17, 59	ltnlei 11330	. . . . . . . . . . . . 13 ⊢ ((1 / 4) < (1 / 2) ↔ ¬ (1 / 2) ≤ (1 / 4))
205	77, 204	mpbi 233	. . . . . . . . . . . 12 ⊢ ¬ (1 / 2) ≤ (1 / 4)
206	200	breq1d 5123	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 ≤ (1 / 4) ↔ (1 / 2) ≤ (1 / 4)))
207	205, 206	mtbiri 330	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → ¬ 𝑦 ≤ (1 / 4))
208	207	iffalsed 4503	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))) = (𝑦 + (1 / 4)))
209	200	oveq1d 7426	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 / 2) = ((1 / 2) / 2))
210	209, 29	eqtrdi 2820	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 / 2) = (1 / 4))
211	210	oveq1d 7426	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → ((𝑦 / 2) + (1 / 2)) = ((1 / 4) + (1 / 2)))
212	203, 208, 211	3eqtr4d 2814	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))) = ((𝑦 / 2) + (1 / 2)))
213		eqid 2769	. . . . . . . . . 10 ⊢ ((topGen‘ran (,)) ↾_t (0[,](1 / 4))) = ((topGen‘ran (,)) ↾_t (0[,](1 / 4)))
214		eqid 2769	. . . . . . . . . 10 ⊢ ((topGen‘ran (,)) ↾_t ((1 / 4)[,](1 / 2))) = ((topGen‘ran (,)) ↾_t ((1 / 4)[,](1 / 2)))
215	59	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (1 / 2) ∈ ℝ)
216	73, 75	recgt0ii 12120	. . . . . . . . . . . . 13 ⊢ 0 < (1 / 4)
217	14, 17, 216	ltleii 11332	. . . . . . . . . . . 12 ⊢ 0 ≤ (1 / 4)
218	14, 59	elicc2i 13438	. . . . . . . . . . . 12 ⊢ ((1 / 4) ∈ (0[,](1 / 2)) ↔ ((1 / 4) ∈ ℝ ∧ 0 ≤ (1 / 4) ∧ (1 / 4) ≤ (1 / 2)))
219	17, 217, 78, 218	mpbir3an 1358	. . . . . . . . . . 11 ⊢ (1 / 4) ∈ (0[,](1 / 2))
220	219	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (1 / 4) ∈ (0[,](1 / 2)))
221		simprl 782	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → 𝑦 = (1 / 4))
222	221	oveq2d 7427	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = (2 · (1 / 4)))
223	221	oveq1d 7426	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 4) + (1 / 4)))
224	23, 222, 223	3eqtr4a 2830	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = (𝑦 + (1 / 4)))
225		retopon 24888	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ)
226		0xr 11255	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ^*
227	59	rexri 11266	. . . . . . . . . . . . . . . 16 ⊢ (1 / 2) ∈ ℝ^*
228		lbicc2 13490	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℝ^* ∧ (1 / 2) ∈ ℝ^* ∧ 0 ≤ (1 / 2)) → 0 ∈ (0[,](1 / 2)))
229	226, 227, 142, 228	mp3an 1487	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ (0[,](1 / 2))
230		iccss2 13443	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ (0[,](1 / 2)) ∧ (1 / 4) ∈ (0[,](1 / 2))) → (0[,](1 / 4)) ⊆ (0[,](1 / 2)))
231	229, 219, 230	mp2an 704	. . . . . . . . . . . . . 14 ⊢ (0[,](1 / 4)) ⊆ (0[,](1 / 2))
232		iccssre 13455	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (0[,](1 / 2)) ⊆ ℝ)
233	14, 59, 232	mp2an 704	. . . . . . . . . . . . . 14 ⊢ (0[,](1 / 2)) ⊆ ℝ
234	231, 233	sstri 3954	. . . . . . . . . . . . 13 ⊢ (0[,](1 / 4)) ⊆ ℝ
235		resttopon 23286	. . . . . . . . . . . . 13 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 / 4)) ⊆ ℝ) → ((topGen‘ran (,)) ↾_t (0[,](1 / 4))) ∈ (TopOn‘(0[,](1 / 4))))
236	225, 234, 235	mp2an 704	. . . . . . . . . . . 12 ⊢ ((topGen‘ran (,)) ↾_t (0[,](1 / 4))) ∈ (TopOn‘(0[,](1 / 4)))
237	236	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ((topGen‘ran (,)) ↾_t (0[,](1 / 4))) ∈ (TopOn‘(0[,](1 / 4))))
238	237, 188	cnmpt1st 23793	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 4)), 𝑧 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,)) ↾_t (0[,](1 / 4))) ×_t II) Cn ((topGen‘ran (,)) ↾_t (0[,](1 / 4)))))
239		retop 24886	. . . . . . . . . . . . . 14 ⊢ (topGen‘ran (,)) ∈ Top
240		ovex 7444	. . . . . . . . . . . . . 14 ⊢ (0[,](1 / 2)) ∈ V
241		restabs 23290	. . . . . . . . . . . . . 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))))
242	239, 231, 240, 241	mp3an 1487	. . . . . . . . . . . . 13 ⊢ (((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ↾_t (0[,](1 / 4))) = ((topGen‘ran (,)) ↾_t (0[,](1 / 4)))
243	242	eqcomi 2778	. . . . . . . . . . . 12 ⊢ ((topGen‘ran (,)) ↾_t (0[,](1 / 4))) = (((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ↾_t (0[,](1 / 4)))
244		resttopon 23286	. . . . . . . . . . . . . 14 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 / 2)) ⊆ ℝ) → ((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 / 2))))
245	225, 233, 244	mp2an 704	. . . . . . . . . . . . 13 ⊢ ((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 / 2)))
246	245	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 / 2))))
247	231	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (0[,](1 / 4)) ⊆ (0[,](1 / 2)))
248	194	iihalf1cn 25059	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (0[,](1 / 2)) ↦ (2 · 𝑥)) ∈ (((topGen‘ran (,)) ↾_t (0[,](1 / 2))) Cn II)
249	248	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ (0[,](1 / 2)) ↦ (2 · 𝑥)) ∈ (((topGen‘ran (,)) ↾_t (0[,](1 / 2))) Cn II))
250	243, 246, 247, 249	cnmpt1res 23801	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (0[,](1 / 4)) ↦ (2 · 𝑥)) ∈ (((topGen‘ran (,)) ↾_t (0[,](1 / 4))) Cn II))
251		oveq2 7419	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
252	237, 188, 238, 237, 250, 251	cnmpt21 23796	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 4)), 𝑧 ∈ (0[,]1) ↦ (2 · 𝑦)) ∈ ((((topGen‘ran (,)) ↾_t (0[,](1 / 4))) ×_t II) Cn II))
253		iccssre 13455	. . . . . . . . . . . . . 14 ⊢ (((1 / 4) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → ((1 / 4)[,](1 / 2)) ⊆ ℝ)
254	17, 59, 253	mp2an 704	. . . . . . . . . . . . 13 ⊢ ((1 / 4)[,](1 / 2)) ⊆ ℝ
255		resttopon 23286	. . . . . . . . . . . . 13 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 / 4)[,](1 / 2)) ⊆ ℝ) → ((topGen‘ran (,)) ↾_t ((1 / 4)[,](1 / 2))) ∈ (TopOn‘((1 / 4)[,](1 / 2))))
256	225, 254, 255	mp2an 704	. . . . . . . . . . . 12 ⊢ ((topGen‘ran (,)) ↾_t ((1 / 4)[,](1 / 2))) ∈ (TopOn‘((1 / 4)[,](1 / 2)))
257	256	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ((topGen‘ran (,)) ↾_t ((1 / 4)[,](1 / 2))) ∈ (TopOn‘((1 / 4)[,](1 / 2))))
258	257, 188	cnmpt1st 23793	. . . . . . . . . . 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 2769	. . . . . . . . . . . 12 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
260	254	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1 / 4)[,](1 / 2)) ⊆ ℝ)
261		unitssre 13525	. . . . . . . . . . . . 13 ⊢ (0[,]1) ⊆ ℝ
262	261	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (0[,]1) ⊆ ℝ)
263	149, 87	sselid 3943	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ∈ (0[,]1))
264	263	adantl 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 4)[,](1 / 2))) → (𝑥 + (1 / 4)) ∈ (0[,]1))
265	259	cnfldtopon 24907	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
266	265	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ))
267	266	cnmptid 23786	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ 𝑥) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
268	17	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 / 4) ∈ ℝ)
269	268	recnd 11236	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 / 4) ∈ ℂ)
270	266, 266, 269	cnmptc 23787	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (1 / 4)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
271	259	addcn 24991	. . . . . . . . . . . . . 14 ⊢ + ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld))
272	271	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → + ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld)))
273	266, 267, 270, 272	cnmpt12f 23791	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (𝑥 + (1 / 4))) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
274	259, 214, 196, 260, 262, 264, 273	cnmptre 25054	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ ((1 / 4)[,](1 / 2)) ↦ (𝑥 + (1 / 4))) ∈ (((topGen‘ran (,)) ↾_t ((1 / 4)[,](1 / 2))) Cn II))
275		oveq1 7418	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 + (1 / 4)) = (𝑦 + (1 / 4)))
276	257, 188, 258, 257, 274, 275	cnmpt21 23796	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ ((1 / 4)[,](1 / 2)), 𝑧 ∈ (0[,]1) ↦ (𝑦 + (1 / 4))) ∈ ((((topGen‘ran (,)) ↾_t ((1 / 4)[,](1 / 2))) ×_t II) Cn II))
277	193, 213, 214, 194, 197, 215, 220, 188, 224, 252, 276	cnmpopc 25055	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 2)), 𝑧 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4)))) ∈ ((((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ×_t II) Cn II))
278		iccssre 13455	. . . . . . . . . . . . 13 ⊢ (((1 / 2) ∈ ℝ ∧ 1 ∈ ℝ) → ((1 / 2)[,]1) ⊆ ℝ)
279	59, 85, 278	mp2an 704	. . . . . . . . . . . 12 ⊢ ((1 / 2)[,]1) ⊆ ℝ
280		resttopon 23286	. . . . . . . . . . . 12 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 / 2)[,]1) ⊆ ℝ) → ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1)))
281	225, 279, 280	mp2an 704	. . . . . . . . . . 11 ⊢ ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1))
282	281	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1)))
283	282, 188	cnmpt1st 23793	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ ((1 / 2)[,]1), 𝑧 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) ×_t II) Cn ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1))))
284	279	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ((1 / 2)[,]1) ⊆ ℝ)
285	149, 156	sselid 3943	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → ((𝑥 / 2) + (1 / 2)) ∈ (0[,]1))
286	285	adantl 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝑥 / 2) + (1 / 2)) ∈ (0[,]1))
287	259	divccn 25000	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℂ ∧ 2 ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
288	4, 24, 287	mp2an 704	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld))
289	288	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
290	31	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 / 2) ∈ ℂ)
291	266, 266, 290	cnmptc 23787	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (1 / 2)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
292	266, 289, 291, 272	cnmpt12f 23791	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((𝑥 / 2) + (1 / 2))) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
293	259, 195, 196, 284, 262, 286, 292	cnmptre 25054	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ ((1 / 2)[,]1) ↦ ((𝑥 / 2) + (1 / 2))) ∈ (((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) Cn II))
294		oveq1 7418	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 / 2) = (𝑦 / 2))
295	294	oveq1d 7426	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 / 2) + (1 / 2)) = ((𝑦 / 2) + (1 / 2)))
296	282, 188, 283, 282, 293, 295	cnmpt21 23796	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ ((1 / 2)[,]1), 𝑧 ∈ (0[,]1) ↦ ((𝑦 / 2) + (1 / 2))) ∈ ((((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) ×_t II) Cn II))
297	193, 194, 195, 196, 197, 198, 199, 188, 212, 277, 296	cnmpopc 25055	. . . . . . . 8 ⊢ (𝜑 → (𝑦 ∈ (0[,]1), 𝑧 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 2), if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))), ((𝑦 / 2) + (1 / 2)))) ∈ ((II ×_t II) Cn II))
298		breq1 5116	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑥 ≤ (1 / 2) ↔ 𝑦 ≤ (1 / 2)))
299		breq1 5116	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝑥 ≤ (1 / 4) ↔ 𝑦 ≤ (1 / 4)))
300	299, 251, 275	ifbieq12d 4521	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))))
301	298, 300, 295	ifbieq12d 4521	. . . . . . . . . . 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))))
302	301	equcoms 2047	. . . . . . . . . 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))))
303	302	adantr 485	. . . . . . . . 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))))
304	303	eqcomd 2775	. . . . . . . 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))))
305	188, 189, 192, 188, 188, 297, 304	cnmpt12 23792	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) ∈ (II Cn II))
306	186, 305	eqeltrid 2873	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ (II Cn II))
307		iiuni 25008	. . . . . . 7 ⊢ (0[,]1) = ∪ II
308	307, 307	cnf 23371	. . . . . 6 ⊢ (𝑃 ∈ (II Cn II) → 𝑃:(0[,]1)⟶(0[,]1))
309	306, 308	syl 18	. . . . 5 ⊢ (𝜑 → 𝑃:(0[,]1)⟶(0[,]1))
310	186	fmpt 7106	. . . . 5 ⊢ (∀𝑥 ∈ (0[,]1)if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) ∈ (0[,]1) ↔ 𝑃:(0[,]1)⟶(0[,]1))
311	309, 310	sylibr 237	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ (0[,]1)if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) ∈ (0[,]1))
312	186	a1i 11	. . . 4 ⊢ (𝜑 → 𝑃 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))))
313	40, 44, 91	pcocn 25144	. . . . . 6 ⊢ (𝜑 → (𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) ∈ (II Cn 𝐽))
314		eqid 2769	. . . . . . 7 ⊢ ∪ 𝐽 = ∪ 𝐽
315	307, 314	cnf 23371	. . . . . 6 ⊢ ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) ∈ (II Cn 𝐽) → (𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)):(0[,]1)⟶∪ 𝐽)
316	313, 315	syl 18	. . . . 5 ⊢ (𝜑 → (𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)):(0[,]1)⟶∪ 𝐽)
317	316	feqmptd 6950	. . . 4 ⊢ (𝜑 → (𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) = (𝑦 ∈ (0[,]1) ↦ ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘𝑦)))
318		fveq2 6882	. . . 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)))))
319	311, 312, 317, 318	fmptcof 7127	. . 3 ⊢ (𝜑 → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) ∘ 𝑃) = (𝑥 ∈ (0[,]1) ↦ ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))))))
320	40, 41, 89	pcocn 25144	. . . 4 ⊢ (𝜑 → (𝐹(*_𝑝‘𝐽)𝐺) ∈ (II Cn 𝐽))
321	320, 42	pcoval 25138	. . 3 ⊢ (𝜑 → ((𝐹(_𝑝‘𝐽)𝐺)(_𝑝‘𝐽)𝐻) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1)))))
322	185, 319, 321	3eqtr4rd 2815	. 2 ⊢ (𝜑 → ((𝐹(_𝑝‘𝐽)𝐺)(_𝑝‘𝐽)𝐻) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) ∘ 𝑃))
323		id 23	. . . . . . . 8 ⊢ (𝑥 = 0 → 𝑥 = 0)
324	323, 142	eqbrtrdi 5154	. . . . . . 7 ⊢ (𝑥 = 0 → 𝑥 ≤ (1 / 2))
325	324	iftrued 4500	. . . . . 6 ⊢ (𝑥 = 0 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))))
326	323, 217	eqbrtrdi 5154	. . . . . . 7 ⊢ (𝑥 = 0 → 𝑥 ≤ (1 / 4))
327	326	iftrued 4500	. . . . . 6 ⊢ (𝑥 = 0 → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (2 · 𝑥))
328		oveq2 7419	. . . . . . 7 ⊢ (𝑥 = 0 → (2 · 𝑥) = (2 · 0))
329		2t0e0 12410	. . . . . . 7 ⊢ (2 · 0) = 0
330	328, 329	eqtrdi 2820	. . . . . 6 ⊢ (𝑥 = 0 → (2 · 𝑥) = 0)
331	325, 327, 330	3eqtrd 2808	. . . . 5 ⊢ (𝑥 = 0 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = 0)
332		c0ex 11199	. . . . 5 ⊢ 0 ∈ V
333	331, 186, 332	fvmpt 6990	. . . 4 ⊢ (0 ∈ (0[,]1) → (𝑃‘0) = 0)
334	191, 333	syl 18	. . 3 ⊢ (𝜑 → (𝑃‘0) = 0)
335	147	a1i 11	. . . 4 ⊢ (𝜑 → 1 ∈ (0[,]1))
336	59, 85	ltnlei 11330	. . . . . . . . 9 ⊢ ((1 / 2) < 1 ↔ ¬ 1 ≤ (1 / 2))
337	143, 336	mpbi 233	. . . . . . . 8 ⊢ ¬ 1 ≤ (1 / 2)
338		breq1 5116	. . . . . . . 8 ⊢ (𝑥 = 1 → (𝑥 ≤ (1 / 2) ↔ 1 ≤ (1 / 2)))
339	337, 338	mtbiri 330	. . . . . . 7 ⊢ (𝑥 = 1 → ¬ 𝑥 ≤ (1 / 2))
340	339	iffalsed 4503	. . . . . 6 ⊢ (𝑥 = 1 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = ((𝑥 / 2) + (1 / 2)))
341		oveq1 7418	. . . . . . . 8 ⊢ (𝑥 = 1 → (𝑥 / 2) = (1 / 2))
342	341	oveq1d 7426	. . . . . . 7 ⊢ (𝑥 = 1 → ((𝑥 / 2) + (1 / 2)) = ((1 / 2) + (1 / 2)))
343	342, 83	eqtrdi 2820	. . . . . 6 ⊢ (𝑥 = 1 → ((𝑥 / 2) + (1 / 2)) = 1)
344	340, 343	eqtrd 2804	. . . . 5 ⊢ (𝑥 = 1 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = 1)
345		1ex 11202	. . . . 5 ⊢ 1 ∈ V
346	344, 186, 345	fvmpt 6990	. . . 4 ⊢ (1 ∈ (0[,]1) → (𝑃‘1) = 1)
347	335, 346	syl 18	. . 3 ⊢ (𝜑 → (𝑃‘1) = 1)
348	313, 306, 334, 347	reparpht 25125	. 2 ⊢ (𝜑 → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) ∘ 𝑃)( ≃_ph‘𝐽)(𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)))
349	322, 348	eqbrtrd 5137	1 ⊢ (𝜑 → ((𝐹(_𝑝‘𝐽)𝐺)(_𝑝‘𝐽)𝐻)( ≃_ph‘𝐽)(𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 400 ∨ wo 860 = wceq 1567 ∈ wcel 2149 ≠ wne 2964 ∀wral 3085 Vcvv 3463 ⊆ wss 3913 ifcif 4492 ∪ cuni 4876 class class class wbr 5113 ↦ cmpt 5196 ran crn 5663 ∘ ccom 5666 ⟶wf 6533 ‘cfv 6537 (class class class)co 7411 ℂcc 11097 ℝcr 11098 0cc0 11099 1c1 11100 + caddc 11102 · cmul 11104 ℝ^*cxr 11241 < clt 11242 ≤ cle 11243 − cmin 11440 / cdiv 11870 ℕcn 12232 2c2 12294 4c4 12296 (,)cioo 13371 [,]cicc 13374 ↾_t crest 17472 TopOpenctopn 17473 topGenctg 17489 ℂ_fldccnfld 21490 Topctop 23018 TopOnctopon 23035 Cn ccn 23349 ×_t ctx 23685 IIcii 25002 ≃_phcphtpc 25096 *_𝑝cpco 25127

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176 ax-pre-sup 11177 ax-addf 11178

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-tp 4599 df-op 4601 df-uni 4877 df-int 4917 df-iun 4962 df-iin 4963 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-se 5616 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-of 7675 df-om 7862 df-1st 7985 df-2nd 7986 df-supp 8156 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-2o 8453 df-er 8693 df-map 8825 df-ixp 8895 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-fsupp 9321 df-fi 9370 df-sup 9401 df-inf 9402 df-oi 9471 df-card 9924 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-div 11871 df-nn 12233 df-2 12302 df-3 12303 df-4 12304 df-5 12305 df-6 12306 df-7 12307 df-8 12308 df-9 12309 df-n0 12504 df-z 12591 df-dec 12711 df-uz 12862 df-q 12972 df-rp 13016 df-xneg 13136 df-xadd 13137 df-xmul 13138 df-ioo 13375 df-icc 13378 df-fz 13535 df-fzo 13682 df-seq 14037 df-exp 14097 df-hash 14366 df-cj 15149 df-re 15150 df-im 15151 df-sqrt 15285 df-abs 15286 df-struct 17206 df-sets 17223 df-slot 17241 df-ndx 17253 df-base 17269 df-ress 17290 df-plusg 17322 df-mulr 17323 df-starv 17324 df-sca 17325 df-vsca 17326 df-ip 17327 df-tset 17328 df-ple 17329 df-ds 17331 df-unif 17332 df-hom 17333 df-cco 17334 df-rest 17474 df-topn 17475 df-0g 17493 df-gsum 17494 df-topgen 17495 df-pt 17496 df-prds 17499 df-xrs 17555 df-qtop 17560 df-imas 17561 df-xps 17563 df-mre 17637 df-mrc 17638 df-acs 17640 df-mgm 18697 df-sgrp 18776 df-mnd 18792 df-submnd 18841 df-mulg 19133 df-cntz 19386 df-cmn 19851 df-psmet 21482 df-xmet 21483 df-met 21484 df-bl 21485 df-mopn 21486 df-cnfld 21491 df-top 23019 df-topon 23036 df-topsp 23058 df-bases 23071 df-cld 23144 df-cn 23352 df-cnp 23353 df-tx 23687 df-hmeo 23880 df-xms 24445 df-ms 24446 df-tms 24447 df-ii 25004 df-htpy 25097 df-phtpy 25098 df-phtpc 25119 df-pco 25132

This theorem is referenced by: pcophtb 25156 pi1grplem 25176 pi1xfr 25182 pi1xfrcnvlem 25183

W3C validator