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 23630

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 4475	. . . . . . . . . . 11 ⊢ (𝑥 ≤ (1 / 4) → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (2 · 𝑥))
2	1	fveq2d 6676	. . . . . . . . . 10 ⊢ (𝑥 ≤ (1 / 4) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(2 · 𝑥)))
3	2	adantl 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(2 · 𝑥)))
4		2cn 11715	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℂ
5		elicc01 12857	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (0[,]1) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1))
6	5	simp1bi 1141	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0[,]1) → 𝑥 ∈ ℝ)
7	6	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℝ)
8	7	recnd 10671	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℂ)
9		mulcom 10625	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) = (𝑥 · 2))
10	4, 8, 9	sylancr 589	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) = (𝑥 · 2))
11	5	simp2bi 1142	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0[,]1) → 0 ≤ 𝑥)
12	11	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 0 ≤ 𝑥)
13		simpr 487	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ≤ (1 / 4))
14		0re 10645	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℝ
15		4nn 11723	. . . . . . . . . . . . . . . 16 ⊢ 4 ∈ ℕ
16		nnrecre 11682	. . . . . . . . . . . . . . . 16 ⊢ (4 ∈ ℕ → (1 / 4) ∈ ℝ)
17	15, 16	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (1 / 4) ∈ ℝ
18	14, 17	elicc2i 12805	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (0[,](1 / 4)) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ (1 / 4)))
19	7, 12, 13, 18	syl3anbrc 1339	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ (0[,](1 / 4)))
20		2rp 12397	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℝ⁺
21	4	mul02i 10831	. . . . . . . . . . . . . 14 ⊢ (0 · 2) = 0
22	17	recni 10657	. . . . . . . . . . . . . . 15 ⊢ (1 / 4) ∈ ℂ
23	22	2timesi 11778	. . . . . . . . . . . . . . . 16 ⊢ (2 · (1 / 4)) = ((1 / 4) + (1 / 4))
24		2ne0 11744	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ≠ 0
25		recdiv2 11355	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((1 / 2) / 2) = (1 / (2 · 2)))
26	4, 24, 4, 24, 25	mp4an 691	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 / 2) / 2) = (1 / (2 · 2))
27		2t2e4 11804	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2 · 2) = 4
28	27	oveq2i 7169	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 / (2 · 2)) = (1 / 4)
29	26, 28	eqtri 2846	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 / 2) / 2) = (1 / 4)
30	29, 29	oveq12i 7170	. . . . . . . . . . . . . . . . 17 ⊢ (((1 / 2) / 2) + ((1 / 2) / 2)) = ((1 / 4) + (1 / 4))
31		halfcn 11855	. . . . . . . . . . . . . . . . . 18 ⊢ (1 / 2) ∈ ℂ
32		2halves 11868	. . . . . . . . . . . . . . . . . 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 2848	. . . . . . . . . . . . . . . 16 ⊢ ((1 / 4) + (1 / 4)) = (1 / 2)
35	23, 34	eqtri 2846	. . . . . . . . . . . . . . 15 ⊢ (2 · (1 / 4)) = (1 / 2)
36	4, 22, 35	mulcomli 10652	. . . . . . . . . . . . . 14 ⊢ ((1 / 4) · 2) = (1 / 2)
37	14, 17, 20, 21, 36	iccdili 12880	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (0[,](1 / 4)) → (𝑥 · 2) ∈ (0[,](1 / 2)))
38	19, 37	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → (𝑥 · 2) ∈ (0[,](1 / 2)))
39	10, 38	eqeltrd 2915	. . . . . . . . . . 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 23623	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺(*_𝑝‘𝐽)𝐻) ∈ (II Cn 𝐽))
45	40, 44	pcoval1 23619	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(2 · 𝑥)) = (𝐹‘(2 · (2 · 𝑥))))
46	40, 41	pcoval1 23619	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) → ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)) = (𝐹‘(2 · (2 · 𝑥))))
47	45, 46	eqtr4d 2861	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
48	39, 47	sylan2 594	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4))) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
49	48	anassrs 470	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
50	3, 49	eqtrd 2858	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
51	50	adantlr 713	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
52		simplll 773	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝜑)
53	6	ad2antlr 725	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → 𝑥 ∈ ℝ)
54	53	adantr 483	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℝ)
55		letric 10742	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ ∧ (1 / 4) ∈ ℝ) → (𝑥 ≤ (1 / 4) ∨ (1 / 4) ≤ 𝑥))
56	53, 17, 55	sylancl 588	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → (𝑥 ≤ (1 / 4) ∨ (1 / 4) ≤ 𝑥))
57	56	orcanai 999	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (1 / 4) ≤ 𝑥)
58		simplr 767	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ≤ (1 / 2))
59		halfre 11854	. . . . . . . . . . . . 13 ⊢ (1 / 2) ∈ ℝ
60	17, 59	elicc2i 12805	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) ↔ (𝑥 ∈ ℝ ∧ (1 / 4) ≤ 𝑥 ∧ 𝑥 ≤ (1 / 2)))
61	54, 57, 58, 60	syl3anbrc 1339	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ((1 / 4)[,](1 / 2)))
62	60	simp1bi 1141	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → 𝑥 ∈ ℝ)
63		readdcl 10622	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ ∧ (1 / 4) ∈ ℝ) → (𝑥 + (1 / 4)) ∈ ℝ)
64	62, 17, 63	sylancl 588	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ∈ ℝ)
65	17	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 4) ∈ ℝ)
66	60	simp2bi 1142	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 4) ≤ 𝑥)
67	65, 62, 65, 66	leadd1dd 11256	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → ((1 / 4) + (1 / 4)) ≤ (𝑥 + (1 / 4)))
68	34, 67	eqbrtrrid 5104	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 2) ≤ (𝑥 + (1 / 4)))
69	59	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 2) ∈ ℝ)
70	60	simp3bi 1143	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → 𝑥 ≤ (1 / 2))
71		2lt4 11815	. . . . . . . . . . . . . . . . 17 ⊢ 2 < 4
72		2re 11714	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ
73		4re 11724	. . . . . . . . . . . . . . . . . 18 ⊢ 4 ∈ ℝ
74		2pos 11743	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 2
75		4pos 11747	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 4
76	72, 73, 74, 75	ltrecii 11558	. . . . . . . . . . . . . . . . 17 ⊢ (2 < 4 ↔ (1 / 4) < (1 / 2))
77	71, 76	mpbi 232	. . . . . . . . . . . . . . . 16 ⊢ (1 / 4) < (1 / 2)
78	17, 59, 77	ltleii 10765	. . . . . . . . . . . . . . 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 11261	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ≤ ((1 / 2) + (1 / 2)))
81		ax-1cn 10597	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
82		2halves 11868	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℂ → ((1 / 2) + (1 / 2)) = 1)
83	81, 82	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((1 / 2) + (1 / 2)) = 1
84	80, 83	breqtrdi 5109	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ≤ 1)
85		1re 10643	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ
86	59, 85	elicc2i 12805	. . . . . . . . . . . 12 ⊢ ((𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1) ↔ ((𝑥 + (1 / 4)) ∈ ℝ ∧ (1 / 2) ≤ (𝑥 + (1 / 4)) ∧ (𝑥 + (1 / 4)) ≤ 1))
87	64, 68, 84, 86	syl3anbrc 1339	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1))
88	61, 87	syl 17	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1))
89		pcoass.5	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹‘1) = (𝐺‘0))
90	41, 42	pco0 23620	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐺(*_𝑝‘𝐽)𝐻)‘0) = (𝐺‘0))
91	89, 90	eqtr4d 2861	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹‘1) = ((𝐺(*_𝑝‘𝐽)𝐻)‘0))
92	40, 44, 91	pcoval2 23622	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))) = ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)))
93	52, 88, 92	syl2anc 586	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))) = ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)))
94	83	oveq2i 7169	. . . . . . . . . . . 12 ⊢ ((2 · (𝑥 + (1 / 4))) − ((1 / 2) + (1 / 2))) = ((2 · (𝑥 + (1 / 4))) − 1)
95		2cnd 11718	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 2 ∈ ℂ)
96	54	recnd 10671	. . . . . . . . . . . . . . 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 10667	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · (𝑥 + (1 / 4))) = ((2 · 𝑥) + (2 · (1 / 4))))
99	35	oveq2i 7169	. . . . . . . . . . . . . 14 ⊢ ((2 · 𝑥) + (2 · (1 / 4))) = ((2 · 𝑥) + (1 / 2))
100	98, 99	syl6eq 2874	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · (𝑥 + (1 / 4))) = ((2 · 𝑥) + (1 / 2)))
101	100	oveq1d 7173	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − ((1 / 2) + (1 / 2))) = (((2 · 𝑥) + (1 / 2)) − ((1 / 2) + (1 / 2))))
102	94, 101	syl5eqr 2872	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − 1) = (((2 · 𝑥) + (1 / 2)) − ((1 / 2) + (1 / 2))))
103		remulcl 10624	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (2 · 𝑥) ∈ ℝ)
104	72, 54, 103	sylancr 589	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈ ℝ)
105	104	recnd 10671	. . . . . . . . . . . 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 11037	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (((2 · 𝑥) + (1 / 2)) − ((1 / 2) + (1 / 2))) = ((2 · 𝑥) − (1 / 2)))
108	102, 107	eqtrd 2858	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − 1) = ((2 · 𝑥) − (1 / 2)))
109	108	fveq2d 6676	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(_𝑝‘𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)) = ((𝐺(_𝑝‘𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))))
110	4, 96, 9	sylancr 589	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) = (𝑥 · 2))
111	81, 4, 24	divcan1i 11386	. . . . . . . . . . . . . . 15 ⊢ ((1 / 2) · 2) = 1
112	17, 59, 20, 36, 111	iccdili 12880	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 · 2) ∈ ((1 / 2)[,]1))
113	61, 112	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (𝑥 · 2) ∈ ((1 / 2)[,]1))
114	110, 113	eqeltrd 2915	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈ ((1 / 2)[,]1))
115	31	subidi 10959	. . . . . . . . . . . . 13 ⊢ ((1 / 2) − (1 / 2)) = 0
116		1mhlfehlf 11859	. . . . . . . . . . . . 13 ⊢ (1 − (1 / 2)) = (1 / 2)
117	59, 85, 59, 115, 116	iccshftli 12878	. . . . . . . . . . . 12 ⊢ ((2 · 𝑥) ∈ ((1 / 2)[,]1) → ((2 · 𝑥) − (1 / 2)) ∈ (0[,](1 / 2)))
118	114, 117	syl 17	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · 𝑥) − (1 / 2)) ∈ (0[,](1 / 2)))
119	41, 42	pcoval1 23619	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((2 · 𝑥) − (1 / 2)) ∈ (0[,](1 / 2))) → ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))))
120	52, 118, 119	syl2anc 586	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))))
121	95, 105, 106	subdid 11098	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · ((2 · 𝑥) − (1 / 2))) = ((2 · (2 · 𝑥)) − (2 · (1 / 2))))
122	4, 24	recidi 11373	. . . . . . . . . . . . 13 ⊢ (2 · (1 / 2)) = 1
123	122	oveq2i 7169	. . . . . . . . . . . 12 ⊢ ((2 · (2 · 𝑥)) − (2 · (1 / 2))) = ((2 · (2 · 𝑥)) − 1)
124	121, 123	syl6eq 2874	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · ((2 · 𝑥) − (1 / 2))) = ((2 · (2 · 𝑥)) − 1))
125	124	fveq2d 6676	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
126	120, 125	eqtrd 2858	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
127	93, 109, 126	3eqtrd 2862	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
128		iffalse 4478	. . . . . . . . . 10 ⊢ (¬ 𝑥 ≤ (1 / 4) → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (𝑥 + (1 / 4)))
129	128	fveq2d 6676	. . . . . . . . 9 ⊢ (¬ 𝑥 ≤ (1 / 4) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))))
130	129	adantl 484	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))))
131	40, 41, 89	pcoval2 23622	. . . . . . . . 9 ⊢ ((𝜑 ∧ (2 · 𝑥) ∈ ((1 / 2)[,]1)) → ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
132	52, 114, 131	syl2anc 586	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
133	127, 130, 132	3eqtr4d 2868	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
134	51, 133	pm2.61dan 811	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
135		iftrue 4475	. . . . . . . 8 ⊢ (𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))))
136	135	fveq2d 6676	. . . . . . 7 ⊢ (𝑥 ≤ (1 / 2) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))))
137	136	adantl 484	. . . . . 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 4475	. . . . . . 7 ⊢ (𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), ((𝐹(_𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = ((𝐹(_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
139	138	adantl 484	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → if(𝑥 ≤ (1 / 2), ((𝐹(_𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = ((𝐹(_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
140	134, 137, 139	3eqtr4d 2868	. . . . 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 23542	. . . . . . . 8 ⊢ ((𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 ≤ (1 / 2)) → 𝑥 ∈ ((1 / 2)[,]1))
142		halfge0 11857	. . . . . . . . . . . . . 14 ⊢ 0 ≤ (1 / 2)
143		halflt1 11858	. . . . . . . . . . . . . . 15 ⊢ (1 / 2) < 1
144	59, 85, 143	ltleii 10765	. . . . . . . . . . . . . 14 ⊢ (1 / 2) ≤ 1
145		elicc01 12857	. . . . . . . . . . . . . 14 ⊢ ((1 / 2) ∈ (0[,]1) ↔ ((1 / 2) ∈ ℝ ∧ 0 ≤ (1 / 2) ∧ (1 / 2) ≤ 1))
146	59, 142, 144, 145	mpbir3an 1337	. . . . . . . . . . . . 13 ⊢ (1 / 2) ∈ (0[,]1)
147		1elunit 12859	. . . . . . . . . . . . 13 ⊢ 1 ∈ (0[,]1)
148		iccss2 12810	. . . . . . . . . . . . 13 ⊢ (((1 / 2) ∈ (0[,]1) ∧ 1 ∈ (0[,]1)) → ((1 / 2)[,]1) ⊆ (0[,]1))
149	146, 147, 148	mp2an 690	. . . . . . . . . . . 12 ⊢ ((1 / 2)[,]1) ⊆ (0[,]1)
150	149	sseli 3965	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 𝑥 ∈ (0[,]1))
151	4, 24	div0i 11376	. . . . . . . . . . . 12 ⊢ (0 / 2) = 0
152		eqid 2823	. . . . . . . . . . . 12 ⊢ (1 / 2) = (1 / 2)
153	14, 85, 20, 151, 152	icccntri 12882	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (0[,]1) → (𝑥 / 2) ∈ (0[,](1 / 2)))
154	31	addid2i 10830	. . . . . . . . . . . 12 ⊢ (0 + (1 / 2)) = (1 / 2)
155	14, 59, 59, 154, 83	iccshftri 12876	. . . . . . . . . . 11 ⊢ ((𝑥 / 2) ∈ (0[,](1 / 2)) → ((𝑥 / 2) + (1 / 2)) ∈ ((1 / 2)[,]1))
156	150, 153, 155	3syl 18	. . . . . . . . . 10 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → ((𝑥 / 2) + (1 / 2)) ∈ ((1 / 2)[,]1))
157	40, 44, 91	pcoval2 23622	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 / 2) + (1 / 2)) ∈ ((1 / 2)[,]1)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)))
158	156, 157	sylan2 594	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)))
159	59, 85	elicc2i 12805	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 2)[,]1) ↔ (𝑥 ∈ ℝ ∧ (1 / 2) ≤ 𝑥 ∧ 𝑥 ≤ 1))
160	159	simp1bi 1141	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 𝑥 ∈ ℝ)
161	160	recnd 10671	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 𝑥 ∈ ℂ)
162		1cnd 10638	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 1 ∈ ℂ)
163		2cnd 11718	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 2 ∈ ℂ)
164	24	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 2 ≠ 0)
165	161, 162, 163, 164	divdird 11456	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → ((𝑥 + 1) / 2) = ((𝑥 / 2) + (1 / 2)))
166	165	oveq2d 7174	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → (2 · ((𝑥 + 1) / 2)) = (2 · ((𝑥 / 2) + (1 / 2))))
167		peano2cn 10814	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ → (𝑥 + 1) ∈ ℂ)
168	161, 167	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → (𝑥 + 1) ∈ ℂ)
169	168, 163, 164	divcan2d 11420	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → (2 · ((𝑥 + 1) / 2)) = (𝑥 + 1))
170	166, 169	eqtr3d 2860	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → (2 · ((𝑥 / 2) + (1 / 2))) = (𝑥 + 1))
171	161, 162, 170	mvrraddd 11054	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → ((2 · ((𝑥 / 2) + (1 / 2))) − 1) = 𝑥)
172	171	fveq2d 6676	. . . . . . . . . 10 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → ((𝐺(_𝑝‘𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)) = ((𝐺(_𝑝‘𝐽)𝐻)‘𝑥))
173	172	adantl 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝐺(_𝑝‘𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)) = ((𝐺(_𝑝‘𝐽)𝐻)‘𝑥))
174	41, 42, 43	pcoval2 23622	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝐺(*_𝑝‘𝐽)𝐻)‘𝑥) = (𝐻‘((2 · 𝑥) − 1)))
175	158, 173, 174	3eqtrd 2862	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1)))
176	141, 175	sylan2 594	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 ≤ (1 / 2))) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1)))
177	176	anassrs 470	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1)))
178		iffalse 4478	. . . . . . . 8 ⊢ (¬ 𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = ((𝑥 / 2) + (1 / 2)))
179	178	fveq2d 6676	. . . . . . 7 ⊢ (¬ 𝑥 ≤ (1 / 2) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))))
180	179	adantl 484	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))))
181		iffalse 4478	. . . . . . 7 ⊢ (¬ 𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = (𝐻‘((2 · 𝑥) − 1)))
182	181	adantl 484	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → if(𝑥 ≤ (1 / 2), ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = (𝐻‘((2 · 𝑥) − 1)))
183	177, 180, 182	3eqtr4d 2868	. . . . 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 811	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = if(𝑥 ≤ (1 / 2), ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))))
185	184	mpteq2dva 5163	. . 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 23489	. . . . . . . . 9 ⊢ II ∈ (TopOn‘(0[,]1))
188	187	a1i 11	. . . . . . . 8 ⊢ (𝜑 → II ∈ (TopOn‘(0[,]1)))
189	188	cnmptid 22271	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ 𝑥) ∈ (II Cn II))
190		0elunit 12858	. . . . . . . . . 10 ⊢ 0 ∈ (0[,]1)
191	190	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0[,]1))
192	188, 188, 191	cnmptc 22272	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ 0) ∈ (II Cn II))
193		eqid 2823	. . . . . . . . 9 ⊢ (topGen‘ran (,)) = (topGen‘ran (,))
194		eqid 2823	. . . . . . . . 9 ⊢ ((topGen‘ran (,)) ↾_t (0[,](1 / 2))) = ((topGen‘ran (,)) ↾_t (0[,](1 / 2)))
195		eqid 2823	. . . . . . . . 9 ⊢ ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) = ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1))
196		dfii2 23492	. . . . . . . . 9 ⊢ II = ((topGen‘ran (,)) ↾_t (0[,]1))
197		0red 10646	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ ℝ)
198		1red 10644	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℝ)
199	146	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (1 / 2) ∈ (0[,]1))
200		simprl 769	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → 𝑦 = (1 / 2))
201	200	oveq1d 7173	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 2) + (1 / 4)))
202	31, 22	addcomi 10833	. . . . . . . . . . 11 ⊢ ((1 / 2) + (1 / 4)) = ((1 / 4) + (1 / 2))
203	201, 202	syl6eq 2874	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 4) + (1 / 2)))
204	17, 59	ltnlei 10763	. . . . . . . . . . . . 13 ⊢ ((1 / 4) < (1 / 2) ↔ ¬ (1 / 2) ≤ (1 / 4))
205	77, 204	mpbi 232	. . . . . . . . . . . 12 ⊢ ¬ (1 / 2) ≤ (1 / 4)
206	200	breq1d 5078	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 ≤ (1 / 4) ↔ (1 / 2) ≤ (1 / 4)))
207	205, 206	mtbiri 329	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → ¬ 𝑦 ≤ (1 / 4))
208	207	iffalsed 4480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))) = (𝑦 + (1 / 4)))
209	200	oveq1d 7173	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 / 2) = ((1 / 2) / 2))
210	209, 29	syl6eq 2874	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 / 2) = (1 / 4))
211	210	oveq1d 7173	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → ((𝑦 / 2) + (1 / 2)) = ((1 / 4) + (1 / 2)))
212	203, 208, 211	3eqtr4d 2868	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))) = ((𝑦 / 2) + (1 / 2)))
213		eqid 2823	. . . . . . . . . 10 ⊢ ((topGen‘ran (,)) ↾_t (0[,](1 / 4))) = ((topGen‘ran (,)) ↾_t (0[,](1 / 4)))
214		eqid 2823	. . . . . . . . . 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 11548	. . . . . . . . . . . . 13 ⊢ 0 < (1 / 4)
217	14, 17, 216	ltleii 10765	. . . . . . . . . . . 12 ⊢ 0 ≤ (1 / 4)
218	14, 59	elicc2i 12805	. . . . . . . . . . . 12 ⊢ ((1 / 4) ∈ (0[,](1 / 2)) ↔ ((1 / 4) ∈ ℝ ∧ 0 ≤ (1 / 4) ∧ (1 / 4) ≤ (1 / 2)))
219	17, 217, 78, 218	mpbir3an 1337	. . . . . . . . . . 11 ⊢ (1 / 4) ∈ (0[,](1 / 2))
220	219	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (1 / 4) ∈ (0[,](1 / 2)))
221		simprl 769	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → 𝑦 = (1 / 4))
222	221	oveq2d 7174	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = (2 · (1 / 4)))
223	221	oveq1d 7173	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 4) + (1 / 4)))
224	23, 222, 223	3eqtr4a 2884	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = (𝑦 + (1 / 4)))
225		retopon 23374	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ)
226		0xr 10690	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ^*
227	59	rexri 10701	. . . . . . . . . . . . . . . 16 ⊢ (1 / 2) ∈ ℝ^*
228		lbicc2 12855	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℝ^* ∧ (1 / 2) ∈ ℝ^* ∧ 0 ≤ (1 / 2)) → 0 ∈ (0[,](1 / 2)))
229	226, 227, 142, 228	mp3an 1457	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ (0[,](1 / 2))
230		iccss2 12810	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ (0[,](1 / 2)) ∧ (1 / 4) ∈ (0[,](1 / 2))) → (0[,](1 / 4)) ⊆ (0[,](1 / 2)))
231	229, 219, 230	mp2an 690	. . . . . . . . . . . . . 14 ⊢ (0[,](1 / 4)) ⊆ (0[,](1 / 2))
232		iccssre 12821	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (0[,](1 / 2)) ⊆ ℝ)
233	14, 59, 232	mp2an 690	. . . . . . . . . . . . . 14 ⊢ (0[,](1 / 2)) ⊆ ℝ
234	231, 233	sstri 3978	. . . . . . . . . . . . 13 ⊢ (0[,](1 / 4)) ⊆ ℝ
235		resttopon 21771	. . . . . . . . . . . . 13 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 / 4)) ⊆ ℝ) → ((topGen‘ran (,)) ↾_t (0[,](1 / 4))) ∈ (TopOn‘(0[,](1 / 4))))
236	225, 234, 235	mp2an 690	. . . . . . . . . . . 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 22278	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 4)), 𝑧 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,)) ↾_t (0[,](1 / 4))) ×_t II) Cn ((topGen‘ran (,)) ↾_t (0[,](1 / 4)))))
239		retop 23372	. . . . . . . . . . . . . 14 ⊢ (topGen‘ran (,)) ∈ Top
240		ovex 7191	. . . . . . . . . . . . . 14 ⊢ (0[,](1 / 2)) ∈ V
241		restabs 21775	. . . . . . . . . . . . . 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 1457	. . . . . . . . . . . . 13 ⊢ (((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ↾_t (0[,](1 / 4))) = ((topGen‘ran (,)) ↾_t (0[,](1 / 4)))
243	242	eqcomi 2832	. . . . . . . . . . . 12 ⊢ ((topGen‘ran (,)) ↾_t (0[,](1 / 4))) = (((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ↾_t (0[,](1 / 4)))
244		resttopon 21771	. . . . . . . . . . . . . 14 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 / 2)) ⊆ ℝ) → ((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 / 2))))
245	225, 233, 244	mp2an 690	. . . . . . . . . . . . 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 23538	. . . . . . . . . . . . 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 22286	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (0[,](1 / 4)) ↦ (2 · 𝑥)) ∈ (((topGen‘ran (,)) ↾_t (0[,](1 / 4))) Cn II))
251		oveq2 7166	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
252	237, 188, 238, 237, 250, 251	cnmpt21 22281	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 4)), 𝑧 ∈ (0[,]1) ↦ (2 · 𝑦)) ∈ ((((topGen‘ran (,)) ↾_t (0[,](1 / 4))) ×_t II) Cn II))
253		iccssre 12821	. . . . . . . . . . . . . 14 ⊢ (((1 / 4) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → ((1 / 4)[,](1 / 2)) ⊆ ℝ)
254	17, 59, 253	mp2an 690	. . . . . . . . . . . . 13 ⊢ ((1 / 4)[,](1 / 2)) ⊆ ℝ
255		resttopon 21771	. . . . . . . . . . . . 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 690	. . . . . . . . . . . 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 22278	. . . . . . . . . . 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 2823	. . . . . . . . . . . 12 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
260	254	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1 / 4)[,](1 / 2)) ⊆ ℝ)
261		unitssre 12888	. . . . . . . . . . . . 13 ⊢ (0[,]1) ⊆ ℝ
262	261	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (0[,]1) ⊆ ℝ)
263	149, 87	sseldi 3967	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ∈ (0[,]1))
264	263	adantl 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 4)[,](1 / 2))) → (𝑥 + (1 / 4)) ∈ (0[,]1))
265	259	cnfldtopon 23393	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
266	265	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ))
267	266	cnmptid 22271	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ 𝑥) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
268	17	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 / 4) ∈ ℝ)
269	268	recnd 10671	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 / 4) ∈ ℂ)
270	266, 266, 269	cnmptc 22272	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (1 / 4)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
271	259	addcn 23475	. . . . . . . . . . . . . 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 22276	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (𝑥 + (1 / 4))) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
274	259, 214, 196, 260, 262, 264, 273	cnmptre 23533	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ ((1 / 4)[,](1 / 2)) ↦ (𝑥 + (1 / 4))) ∈ (((topGen‘ran (,)) ↾_t ((1 / 4)[,](1 / 2))) Cn II))
275		oveq1 7165	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 + (1 / 4)) = (𝑦 + (1 / 4)))
276	257, 188, 258, 257, 274, 275	cnmpt21 22281	. . . . . . . . . 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 23534	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 2)), 𝑧 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4)))) ∈ ((((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ×_t II) Cn II))
278		iccssre 12821	. . . . . . . . . . . . 13 ⊢ (((1 / 2) ∈ ℝ ∧ 1 ∈ ℝ) → ((1 / 2)[,]1) ⊆ ℝ)
279	59, 85, 278	mp2an 690	. . . . . . . . . . . 12 ⊢ ((1 / 2)[,]1) ⊆ ℝ
280		resttopon 21771	. . . . . . . . . . . 12 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 / 2)[,]1) ⊆ ℝ) → ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1)))
281	225, 279, 280	mp2an 690	. . . . . . . . . . 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 22278	. . . . . . . . . 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	sseldi 3967	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → ((𝑥 / 2) + (1 / 2)) ∈ (0[,]1))
286	285	adantl 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝑥 / 2) + (1 / 2)) ∈ (0[,]1))
287	259	divccn 23483	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℂ ∧ 2 ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
288	4, 24, 287	mp2an 690	. . . . . . . . . . . . 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 22272	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (1 / 2)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
292	266, 289, 291, 272	cnmpt12f 22276	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((𝑥 / 2) + (1 / 2))) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
293	259, 195, 196, 284, 262, 286, 292	cnmptre 23533	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ ((1 / 2)[,]1) ↦ ((𝑥 / 2) + (1 / 2))) ∈ (((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) Cn II))
294		oveq1 7165	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 / 2) = (𝑦 / 2))
295	294	oveq1d 7173	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 / 2) + (1 / 2)) = ((𝑦 / 2) + (1 / 2)))
296	282, 188, 283, 282, 293, 295	cnmpt21 22281	. . . . . . . . 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 23534	. . . . . . . 8 ⊢ (𝜑 → (𝑦 ∈ (0[,]1), 𝑧 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 2), if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))), ((𝑦 / 2) + (1 / 2)))) ∈ ((II ×_t II) Cn II))
298		breq1 5071	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑥 ≤ (1 / 2) ↔ 𝑦 ≤ (1 / 2)))
299		breq1 5071	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝑥 ≤ (1 / 4) ↔ 𝑦 ≤ (1 / 4)))
300	299, 251, 275	ifbieq12d 4496	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))))
301	298, 300, 295	ifbieq12d 4496	. . . . . . . . . . 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 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))))
303	302	adantr 483	. . . . . . . . 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 2829	. . . . . . . 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 22277	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) ∈ (II Cn II))
306	186, 305	eqeltrid 2919	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ (II Cn II))
307		iiuni 23491	. . . . . . 7 ⊢ (0[,]1) = ∪ II
308	307, 307	cnf 21856	. . . . . 6 ⊢ (𝑃 ∈ (II Cn II) → 𝑃:(0[,]1)⟶(0[,]1))
309	306, 308	syl 17	. . . . 5 ⊢ (𝜑 → 𝑃:(0[,]1)⟶(0[,]1))
310	186	fmpt 6876	. . . . 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 236	. . . 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 23623	. . . . . 6 ⊢ (𝜑 → (𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) ∈ (II Cn 𝐽))
314		eqid 2823	. . . . . . 7 ⊢ ∪ 𝐽 = ∪ 𝐽
315	307, 314	cnf 21856	. . . . . 6 ⊢ ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) ∈ (II Cn 𝐽) → (𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)):(0[,]1)⟶∪ 𝐽)
316	313, 315	syl 17	. . . . 5 ⊢ (𝜑 → (𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)):(0[,]1)⟶∪ 𝐽)
317	316	feqmptd 6735	. . . 4 ⊢ (𝜑 → (𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) = (𝑦 ∈ (0[,]1) ↦ ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘𝑦)))
318		fveq2 6672	. . . 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 6894	. . 3 ⊢ (𝜑 → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) ∘ 𝑃) = (𝑥 ∈ (0[,]1) ↦ ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))))))
320	40, 41, 89	pcocn 23623	. . . 4 ⊢ (𝜑 → (𝐹(*_𝑝‘𝐽)𝐺) ∈ (II Cn 𝐽))
321	320, 42	pcoval 23617	. . 3 ⊢ (𝜑 → ((𝐹(_𝑝‘𝐽)𝐺)(_𝑝‘𝐽)𝐻) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1)))))
322	185, 319, 321	3eqtr4rd 2869	. 2 ⊢ (𝜑 → ((𝐹(_𝑝‘𝐽)𝐺)(_𝑝‘𝐽)𝐻) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) ∘ 𝑃))
323		id 22	. . . . . . . 8 ⊢ (𝑥 = 0 → 𝑥 = 0)
324	323, 142	eqbrtrdi 5107	. . . . . . 7 ⊢ (𝑥 = 0 → 𝑥 ≤ (1 / 2))
325	324	iftrued 4477	. . . . . 6 ⊢ (𝑥 = 0 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))))
326	323, 217	eqbrtrdi 5107	. . . . . . 7 ⊢ (𝑥 = 0 → 𝑥 ≤ (1 / 4))
327	326	iftrued 4477	. . . . . 6 ⊢ (𝑥 = 0 → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (2 · 𝑥))
328		oveq2 7166	. . . . . . 7 ⊢ (𝑥 = 0 → (2 · 𝑥) = (2 · 0))
329		2t0e0 11809	. . . . . . 7 ⊢ (2 · 0) = 0
330	328, 329	syl6eq 2874	. . . . . 6 ⊢ (𝑥 = 0 → (2 · 𝑥) = 0)
331	325, 327, 330	3eqtrd 2862	. . . . 5 ⊢ (𝑥 = 0 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = 0)
332		c0ex 10637	. . . . 5 ⊢ 0 ∈ V
333	331, 186, 332	fvmpt 6770	. . . 4 ⊢ (0 ∈ (0[,]1) → (𝑃‘0) = 0)
334	191, 333	syl 17	. . 3 ⊢ (𝜑 → (𝑃‘0) = 0)
335	147	a1i 11	. . . 4 ⊢ (𝜑 → 1 ∈ (0[,]1))
336	59, 85	ltnlei 10763	. . . . . . . . 9 ⊢ ((1 / 2) < 1 ↔ ¬ 1 ≤ (1 / 2))
337	143, 336	mpbi 232	. . . . . . . 8 ⊢ ¬ 1 ≤ (1 / 2)
338		breq1 5071	. . . . . . . 8 ⊢ (𝑥 = 1 → (𝑥 ≤ (1 / 2) ↔ 1 ≤ (1 / 2)))
339	337, 338	mtbiri 329	. . . . . . 7 ⊢ (𝑥 = 1 → ¬ 𝑥 ≤ (1 / 2))
340	339	iffalsed 4480	. . . . . 6 ⊢ (𝑥 = 1 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = ((𝑥 / 2) + (1 / 2)))
341		oveq1 7165	. . . . . . . 8 ⊢ (𝑥 = 1 → (𝑥 / 2) = (1 / 2))
342	341	oveq1d 7173	. . . . . . 7 ⊢ (𝑥 = 1 → ((𝑥 / 2) + (1 / 2)) = ((1 / 2) + (1 / 2)))
343	342, 83	syl6eq 2874	. . . . . 6 ⊢ (𝑥 = 1 → ((𝑥 / 2) + (1 / 2)) = 1)
344	340, 343	eqtrd 2858	. . . . 5 ⊢ (𝑥 = 1 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = 1)
345		1ex 10639	. . . . 5 ⊢ 1 ∈ V
346	344, 186, 345	fvmpt 6770	. . . 4 ⊢ (1 ∈ (0[,]1) → (𝑃‘1) = 1)
347	335, 346	syl 17	. . 3 ⊢ (𝜑 → (𝑃‘1) = 1)
348	313, 306, 334, 347	reparpht 23604	. 2 ⊢ (𝜑 → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) ∘ 𝑃)( ≃_ph‘𝐽)(𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)))
349	322, 348	eqbrtrd 5090	1 ⊢ (𝜑 → ((𝐹(_𝑝‘𝐽)𝐺)(_𝑝‘𝐽)𝐻)( ≃_ph‘𝐽)(𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 398 ∨ wo 843 = wceq 1537 ∈ wcel 2114 ≠ wne 3018 ∀wral 3140 Vcvv 3496 ⊆ wss 3938 ifcif 4469 ∪ cuni 4840 class class class wbr 5068 ↦ cmpt 5148 ran crn 5558 ∘ ccom 5561 ⟶wf 6353 ‘cfv 6357 (class class class)co 7158 ℂcc 10537 ℝcr 10538 0cc0 10539 1c1 10540 + caddc 10542 · cmul 10544 ℝ^*cxr 10676 < clt 10677 ≤ cle 10678 − cmin 10872 / cdiv 11299 ℕcn 11640 2c2 11695 4c4 11697 (,)cioo 12741 [,]cicc 12744 ↾_t crest 16696 TopOpenctopn 16697 topGenctg 16713 ℂ_fldccnfld 20547 Topctop 21503 TopOnctopon 21520 Cn ccn 21834 ×_t ctx 22170 IIcii 23485 ≃_phcphtpc 23575 *_𝑝cpco 23606

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-rep 5192 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463 ax-cnex 10595 ax-resscn 10596 ax-1cn 10597 ax-icn 10598 ax-addcl 10599 ax-addrcl 10600 ax-mulcl 10601 ax-mulrcl 10602 ax-mulcom 10603 ax-addass 10604 ax-mulass 10605 ax-distr 10606 ax-i2m1 10607 ax-1ne0 10608 ax-1rid 10609 ax-rnegex 10610 ax-rrecex 10611 ax-cnre 10612 ax-pre-lttri 10613 ax-pre-lttrn 10614 ax-pre-ltadd 10615 ax-pre-mulgt0 10616 ax-pre-sup 10617 ax-addf 10618 ax-mulf 10619

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-nel 3126 df-ral 3145 df-rex 3146 df-reu 3147 df-rmo 3148 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-pss 3956 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-tp 4574 df-op 4576 df-uni 4841 df-int 4879 df-iun 4923 df-iin 4924 df-br 5069 df-opab 5131 df-mpt 5149 df-tr 5175 df-id 5462 df-eprel 5467 df-po 5476 df-so 5477 df-fr 5516 df-se 5517 df-we 5518 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-pred 6150 df-ord 6196 df-on 6197 df-lim 6198 df-suc 6199 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-fv 6365 df-isom 6366 df-riota 7116 df-ov 7161 df-oprab 7162 df-mpo 7163 df-of 7411 df-om 7583 df-1st 7691 df-2nd 7692 df-supp 7833 df-wrecs 7949 df-recs 8010 df-rdg 8048 df-1o 8104 df-2o 8105 df-oadd 8108 df-er 8291 df-map 8410 df-ixp 8464 df-en 8512 df-dom 8513 df-sdom 8514 df-fin 8515 df-fsupp 8836 df-fi 8877 df-sup 8908 df-inf 8909 df-oi 8976 df-card 9370 df-pnf 10679 df-mnf 10680 df-xr 10681 df-ltxr 10682 df-le 10683 df-sub 10874 df-neg 10875 df-div 11300 df-nn 11641 df-2 11703 df-3 11704 df-4 11705 df-5 11706 df-6 11707 df-7 11708 df-8 11709 df-9 11710 df-n0 11901 df-z 11985 df-dec 12102 df-uz 12247 df-q 12352 df-rp 12393 df-xneg 12510 df-xadd 12511 df-xmul 12512 df-ioo 12745 df-icc 12748 df-fz 12896 df-fzo 13037 df-seq 13373 df-exp 13433 df-hash 13694 df-cj 14460 df-re 14461 df-im 14462 df-sqrt 14596 df-abs 14597 df-struct 16487 df-ndx 16488 df-slot 16489 df-base 16491 df-sets 16492 df-ress 16493 df-plusg 16580 df-mulr 16581 df-starv 16582 df-sca 16583 df-vsca 16584 df-ip 16585 df-tset 16586 df-ple 16587 df-ds 16589 df-unif 16590 df-hom 16591 df-cco 16592 df-rest 16698 df-topn 16699 df-0g 16717 df-gsum 16718 df-topgen 16719 df-pt 16720 df-prds 16723 df-xrs 16777 df-qtop 16782 df-imas 16783 df-xps 16785 df-mre 16859 df-mrc 16860 df-acs 16862 df-mgm 17854 df-sgrp 17903 df-mnd 17914 df-submnd 17959 df-mulg 18227 df-cntz 18449 df-cmn 18910 df-psmet 20539 df-xmet 20540 df-met 20541 df-bl 20542 df-mopn 20543 df-cnfld 20548 df-top 21504 df-topon 21521 df-topsp 21543 df-bases 21556 df-cld 21629 df-cn 21837 df-cnp 21838 df-tx 22172 df-hmeo 22365 df-xms 22932 df-ms 22933 df-tms 22934 df-ii 23487 df-htpy 23576 df-phtpy 23577 df-phtpc 23598 df-pco 23611

This theorem is referenced by: pcophtb 23635 pi1grplem 23655 pi1xfr 23661 pi1xfrcnvlem 23662

W3C validator