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 25086

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 4486	. . . . . . . . . . 11 ⊢ (𝑥 ≤ (1 / 4) → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (2 · 𝑥))
2	1	fveq2d 6871	. . . . . . . . . 10 ⊢ (𝑥 ≤ (1 / 4) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(2 · 𝑥)))
3	2	adantl 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(2 · 𝑥)))
4		2cn 12293	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℂ
5		elicc01 13470	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (0[,]1) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1))
6	5	simp1bi 1158	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0[,]1) → 𝑥 ∈ ℝ)
7	6	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℝ)
8	7	recnd 11210	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℂ)
9		mulcom 11159	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) = (𝑥 · 2))
10	4, 8, 9	sylancr 596	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) = (𝑥 · 2))
11	5	simp2bi 1159	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0[,]1) → 0 ≤ 𝑥)
12	11	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 0 ≤ 𝑥)
13		simpr 488	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ≤ (1 / 4))
14		0re 11183	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℝ
15		4nn 12301	. . . . . . . . . . . . . . . 16 ⊢ 4 ∈ ℕ
16		nnrecre 12255	. . . . . . . . . . . . . . . 16 ⊢ (4 ∈ ℕ → (1 / 4) ∈ ℝ)
17	15, 16	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (1 / 4) ∈ ℝ
18	14, 17	elicc2i 13416	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (0[,](1 / 4)) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ (1 / 4)))
19	7, 12, 13, 18	syl3anbrc 1357	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ (0[,](1 / 4)))
20		2rp 12998	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℝ⁺
21	4	mul02i 11372	. . . . . . . . . . . . . 14 ⊢ (0 · 2) = 0
22	17	recni 11196	. . . . . . . . . . . . . . 15 ⊢ (1 / 4) ∈ ℂ
23	22	2timesi 12355	. . . . . . . . . . . . . . . 16 ⊢ (2 · (1 / 4)) = ((1 / 4) + (1 / 4))
24		2ne0 12324	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ≠ 0
25		recdiv2 11904	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((1 / 2) / 2) = (1 / (2 · 2)))
26	4, 24, 4, 24, 25	mp4an 703	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 / 2) / 2) = (1 / (2 · 2))
27		2t2e4 12381	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2 · 2) = 4
28	27	oveq2i 7407	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 / (2 · 2)) = (1 / 4)
29	26, 28	eqtri 2785	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 / 2) / 2) = (1 / 4)
30	29, 29	oveq12i 7408	. . . . . . . . . . . . . . . . 17 ⊢ (((1 / 2) / 2) + ((1 / 2) / 2)) = ((1 / 4) + (1 / 4))
31		halfcn 12435	. . . . . . . . . . . . . . . . . 18 ⊢ (1 / 2) ∈ ℂ
32		2halves 12439	. . . . . . . . . . . . . . . . . 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 2787	. . . . . . . . . . . . . . . 16 ⊢ ((1 / 4) + (1 / 4)) = (1 / 2)
35	23, 34	eqtri 2785	. . . . . . . . . . . . . . 15 ⊢ (2 · (1 / 4)) = (1 / 2)
36	4, 22, 35	mulcomli 11191	. . . . . . . . . . . . . 14 ⊢ ((1 / 4) · 2) = (1 / 2)
37	14, 17, 20, 21, 36	iccdili 13495	. . . . . . . . . . . . 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 2862	. . . . . . . . . . 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 25079	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺(*_𝑝‘𝐽)𝐻) ∈ (II Cn 𝐽))
45	40, 44	pcoval1 25075	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(2 · 𝑥)) = (𝐹‘(2 · (2 · 𝑥))))
46	40, 41	pcoval1 25075	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) → ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)) = (𝐹‘(2 · (2 · 𝑥))))
47	45, 46	eqtr4d 2800	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
48	39, 47	sylan2 602	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4))) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
49	48	anassrs 471	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
50	3, 49	eqtrd 2797	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
51	50	adantlr 725	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
52		simplll 784	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝜑)
53	6	ad2antlr 737	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → 𝑥 ∈ ℝ)
54	53	adantr 484	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℝ)
55		letric 11283	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ ∧ (1 / 4) ∈ ℝ) → (𝑥 ≤ (1 / 4) ∨ (1 / 4) ≤ 𝑥))
56	53, 17, 55	sylancl 595	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → (𝑥 ≤ (1 / 4) ∨ (1 / 4) ≤ 𝑥))
57	56	orcanai 1016	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (1 / 4) ≤ 𝑥)
58		simplr 778	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ≤ (1 / 2))
59		halfre 12434	. . . . . . . . . . . . 13 ⊢ (1 / 2) ∈ ℝ
60	17, 59	elicc2i 13416	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) ↔ (𝑥 ∈ ℝ ∧ (1 / 4) ≤ 𝑥 ∧ 𝑥 ≤ (1 / 2)))
61	54, 57, 58, 60	syl3anbrc 1357	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ((1 / 4)[,](1 / 2)))
62	60	simp1bi 1158	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → 𝑥 ∈ ℝ)
63		readdcl 11156	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ ∧ (1 / 4) ∈ ℝ) → (𝑥 + (1 / 4)) ∈ ℝ)
64	62, 17, 63	sylancl 595	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ∈ ℝ)
65	17	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 4) ∈ ℝ)
66	60	simp2bi 1159	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 4) ≤ 𝑥)
67	65, 62, 65, 66	leadd1dd 11801	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → ((1 / 4) + (1 / 4)) ≤ (𝑥 + (1 / 4)))
68	34, 67	eqbrtrrid 5136	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 2) ≤ (𝑥 + (1 / 4)))
69	59	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 2) ∈ ℝ)
70	60	simp3bi 1160	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → 𝑥 ≤ (1 / 2))
71		2lt4 12395	. . . . . . . . . . . . . . . . 17 ⊢ 2 < 4
72		2re 12292	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ
73		4re 12302	. . . . . . . . . . . . . . . . . 18 ⊢ 4 ∈ ℝ
74		2pos 12322	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 2
75		4pos 12328	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 4
76	72, 73, 74, 75	ltrecii 12108	. . . . . . . . . . . . . . . . 17 ⊢ (2 < 4 ↔ (1 / 4) < (1 / 2))
77	71, 76	mpbi 232	. . . . . . . . . . . . . . . 16 ⊢ (1 / 4) < (1 / 2)
78	17, 59, 77	ltleii 11306	. . . . . . . . . . . . . . 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 11806	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ≤ ((1 / 2) + (1 / 2)))
81		ax-1cn 11131	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
82		2halves 12439	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℂ → ((1 / 2) + (1 / 2)) = 1)
83	81, 82	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((1 / 2) + (1 / 2)) = 1
84	80, 83	breqtrdi 5141	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ≤ 1)
85		1re 11181	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ
86	59, 85	elicc2i 13416	. . . . . . . . . . . 12 ⊢ ((𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1) ↔ ((𝑥 + (1 / 4)) ∈ ℝ ∧ (1 / 2) ≤ (𝑥 + (1 / 4)) ∧ (𝑥 + (1 / 4)) ≤ 1))
87	64, 68, 84, 86	syl3anbrc 1357	. . . . . . . . . . 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 25076	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐺(*_𝑝‘𝐽)𝐻)‘0) = (𝐺‘0))
91	89, 90	eqtr4d 2800	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹‘1) = ((𝐺(*_𝑝‘𝐽)𝐻)‘0))
92	40, 44, 91	pcoval2 25078	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))) = ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)))
93	52, 88, 92	syl2anc 593	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))) = ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)))
94	83	oveq2i 7407	. . . . . . . . . . . 12 ⊢ ((2 · (𝑥 + (1 / 4))) − ((1 / 2) + (1 / 2))) = ((2 · (𝑥 + (1 / 4))) − 1)
95		2cnd 12296	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 2 ∈ ℂ)
96	54	recnd 11210	. . . . . . . . . . . . . . 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 11206	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · (𝑥 + (1 / 4))) = ((2 · 𝑥) + (2 · (1 / 4))))
99	35	oveq2i 7407	. . . . . . . . . . . . . 14 ⊢ ((2 · 𝑥) + (2 · (1 / 4))) = ((2 · 𝑥) + (1 / 2))
100	98, 99	eqtrdi 2813	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · (𝑥 + (1 / 4))) = ((2 · 𝑥) + (1 / 2)))
101	100	oveq1d 7411	. . . . . . . . . . . 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 2811	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − 1) = (((2 · 𝑥) + (1 / 2)) − ((1 / 2) + (1 / 2))))
103		remulcl 11158	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (2 · 𝑥) ∈ ℝ)
104	72, 54, 103	sylancr 596	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈ ℝ)
105	104	recnd 11210	. . . . . . . . . . . 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 11580	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (((2 · 𝑥) + (1 / 2)) − ((1 / 2) + (1 / 2))) = ((2 · 𝑥) − (1 / 2)))
108	102, 107	eqtrd 2797	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − 1) = ((2 · 𝑥) − (1 / 2)))
109	108	fveq2d 6871	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(_𝑝‘𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)) = ((𝐺(_𝑝‘𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))))
110	4, 96, 9	sylancr 596	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) = (𝑥 · 2))
111	81, 4, 24	divcan1i 11935	. . . . . . . . . . . . . . 15 ⊢ ((1 / 2) · 2) = 1
112	17, 59, 20, 36, 111	iccdili 13495	. . . . . . . . . . . . . 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 2862	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈ ((1 / 2)[,]1))
115	31	subidi 11502	. . . . . . . . . . . . 13 ⊢ ((1 / 2) − (1 / 2)) = 0
116		1mhlfehlf 12440	. . . . . . . . . . . . 13 ⊢ (1 − (1 / 2)) = (1 / 2)
117	59, 85, 59, 115, 116	iccshftli 13493	. . . . . . . . . . . 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 25075	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((2 · 𝑥) − (1 / 2)) ∈ (0[,](1 / 2))) → ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))))
120	52, 118, 119	syl2anc 593	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))))
121	95, 105, 106	subdid 11643	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · ((2 · 𝑥) − (1 / 2))) = ((2 · (2 · 𝑥)) − (2 · (1 / 2))))
122	4, 24	recidi 11922	. . . . . . . . . . . . 13 ⊢ (2 · (1 / 2)) = 1
123	122	oveq2i 7407	. . . . . . . . . . . 12 ⊢ ((2 · (2 · 𝑥)) − (2 · (1 / 2))) = ((2 · (2 · 𝑥)) − 1)
124	121, 123	eqtrdi 2813	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · ((2 · 𝑥) − (1 / 2))) = ((2 · (2 · 𝑥)) − 1))
125	124	fveq2d 6871	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
126	120, 125	eqtrd 2797	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
127	93, 109, 126	3eqtrd 2801	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
128		iffalse 4489	. . . . . . . . . 10 ⊢ (¬ 𝑥 ≤ (1 / 4) → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (𝑥 + (1 / 4)))
129	128	fveq2d 6871	. . . . . . . . 9 ⊢ (¬ 𝑥 ≤ (1 / 4) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))))
130	129	adantl 485	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))))
131	40, 41, 89	pcoval2 25078	. . . . . . . . 9 ⊢ ((𝜑 ∧ (2 · 𝑥) ∈ ((1 / 2)[,]1)) → ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
132	52, 114, 131	syl2anc 593	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
133	127, 130, 132	3eqtr4d 2807	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
134	51, 133	pm2.61dan 822	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
135		iftrue 4486	. . . . . . . 8 ⊢ (𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))))
136	135	fveq2d 6871	. . . . . . 7 ⊢ (𝑥 ≤ (1 / 2) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))))
137	136	adantl 485	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))))
138		iftrue 4486	. . . . . . 7 ⊢ (𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), ((𝐹(_𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = ((𝐹(_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
139	138	adantl 485	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → if(𝑥 ≤ (1 / 2), ((𝐹(_𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = ((𝐹(_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
140	134, 137, 139	3eqtr4d 2807	. . . . 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 24998	. . . . . . . 8 ⊢ ((𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 ≤ (1 / 2)) → 𝑥 ∈ ((1 / 2)[,]1))
142		halfge0 12437	. . . . . . . . . . . . . 14 ⊢ 0 ≤ (1 / 2)
143		halflt1 12438	. . . . . . . . . . . . . . 15 ⊢ (1 / 2) < 1
144	59, 85, 143	ltleii 11306	. . . . . . . . . . . . . 14 ⊢ (1 / 2) ≤ 1
145		elicc01 13470	. . . . . . . . . . . . . 14 ⊢ ((1 / 2) ∈ (0[,]1) ↔ ((1 / 2) ∈ ℝ ∧ 0 ≤ (1 / 2) ∧ (1 / 2) ≤ 1))
146	59, 142, 144, 145	mpbir3an 1355	. . . . . . . . . . . . 13 ⊢ (1 / 2) ∈ (0[,]1)
147		1elunit 13474	. . . . . . . . . . . . 13 ⊢ 1 ∈ (0[,]1)
148		iccss2 13421	. . . . . . . . . . . . 13 ⊢ (((1 / 2) ∈ (0[,]1) ∧ 1 ∈ (0[,]1)) → ((1 / 2)[,]1) ⊆ (0[,]1))
149	146, 147, 148	mp2an 702	. . . . . . . . . . . 12 ⊢ ((1 / 2)[,]1) ⊆ (0[,]1)
150	149	sseli 3932	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 𝑥 ∈ (0[,]1))
151	4, 24	div0i 11925	. . . . . . . . . . . 12 ⊢ (0 / 2) = 0
152		eqid 2762	. . . . . . . . . . . 12 ⊢ (1 / 2) = (1 / 2)
153	14, 85, 20, 151, 152	icccntri 13497	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (0[,]1) → (𝑥 / 2) ∈ (0[,](1 / 2)))
154	31	addlidi 11371	. . . . . . . . . . . 12 ⊢ (0 + (1 / 2)) = (1 / 2)
155	14, 59, 59, 154, 83	iccshftri 13491	. . . . . . . . . . 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 25078	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 / 2) + (1 / 2)) ∈ ((1 / 2)[,]1)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)))
158	156, 157	sylan2 602	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)))
159	59, 85	elicc2i 13416	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 2)[,]1) ↔ (𝑥 ∈ ℝ ∧ (1 / 2) ≤ 𝑥 ∧ 𝑥 ≤ 1))
160	159	simp1bi 1158	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 𝑥 ∈ ℝ)
161	160	recnd 11210	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 𝑥 ∈ ℂ)
162		1cnd 11175	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 1 ∈ ℂ)
163		2cnd 12296	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 2 ∈ ℂ)
164	24	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 2 ≠ 0)
165	161, 162, 163, 164	divdird 12005	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → ((𝑥 + 1) / 2) = ((𝑥 / 2) + (1 / 2)))
166	165	oveq2d 7412	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → (2 · ((𝑥 + 1) / 2)) = (2 · ((𝑥 / 2) + (1 / 2))))
167		peano2cn 11355	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ → (𝑥 + 1) ∈ ℂ)
168	161, 167	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → (𝑥 + 1) ∈ ℂ)
169	168, 163, 164	divcan2d 11969	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → (2 · ((𝑥 + 1) / 2)) = (𝑥 + 1))
170	166, 169	eqtr3d 2799	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → (2 · ((𝑥 / 2) + (1 / 2))) = (𝑥 + 1))
171	161, 162, 170	mvrraddd 11599	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → ((2 · ((𝑥 / 2) + (1 / 2))) − 1) = 𝑥)
172	171	fveq2d 6871	. . . . . . . . . 10 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → ((𝐺(_𝑝‘𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)) = ((𝐺(_𝑝‘𝐽)𝐻)‘𝑥))
173	172	adantl 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝐺(_𝑝‘𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)) = ((𝐺(_𝑝‘𝐽)𝐻)‘𝑥))
174	41, 42, 43	pcoval2 25078	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝐺(*_𝑝‘𝐽)𝐻)‘𝑥) = (𝐻‘((2 · 𝑥) − 1)))
175	158, 173, 174	3eqtrd 2801	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1)))
176	141, 175	sylan2 602	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 ≤ (1 / 2))) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1)))
177	176	anassrs 471	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1)))
178		iffalse 4489	. . . . . . . 8 ⊢ (¬ 𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = ((𝑥 / 2) + (1 / 2)))
179	178	fveq2d 6871	. . . . . . 7 ⊢ (¬ 𝑥 ≤ (1 / 2) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))))
180	179	adantl 485	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))))
181		iffalse 4489	. . . . . . 7 ⊢ (¬ 𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = (𝐻‘((2 · 𝑥) − 1)))
182	181	adantl 485	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → if(𝑥 ≤ (1 / 2), ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = (𝐻‘((2 · 𝑥) − 1)))
183	177, 180, 182	3eqtr4d 2807	. . . . 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 822	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = if(𝑥 ≤ (1 / 2), ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))))
185	184	mpteq2dva 5193	. . 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 24941	. . . . . . . . 9 ⊢ II ∈ (TopOn‘(0[,]1))
188	187	a1i 11	. . . . . . . 8 ⊢ (𝜑 → II ∈ (TopOn‘(0[,]1)))
189	188	cnmptid 23721	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ 𝑥) ∈ (II Cn II))
190		0elunit 13473	. . . . . . . . . 10 ⊢ 0 ∈ (0[,]1)
191	190	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0[,]1))
192	188, 188, 191	cnmptc 23722	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ 0) ∈ (II Cn II))
193		eqid 2762	. . . . . . . . 9 ⊢ (topGen‘ran (,)) = (topGen‘ran (,))
194		eqid 2762	. . . . . . . . 9 ⊢ ((topGen‘ran (,)) ↾_t (0[,](1 / 2))) = ((topGen‘ran (,)) ↾_t (0[,](1 / 2)))
195		eqid 2762	. . . . . . . . 9 ⊢ ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) = ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1))
196		dfii2 24944	. . . . . . . . 9 ⊢ II = ((topGen‘ran (,)) ↾_t (0[,]1))
197		0red 11184	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ ℝ)
198		1red 11182	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℝ)
199	146	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (1 / 2) ∈ (0[,]1))
200		simprl 780	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → 𝑦 = (1 / 2))
201	200	oveq1d 7411	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 2) + (1 / 4)))
202	31, 22	addcomi 11374	. . . . . . . . . . 11 ⊢ ((1 / 2) + (1 / 4)) = ((1 / 4) + (1 / 2))
203	201, 202	eqtrdi 2813	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 4) + (1 / 2)))
204	17, 59	ltnlei 11304	. . . . . . . . . . . . 13 ⊢ ((1 / 4) < (1 / 2) ↔ ¬ (1 / 2) ≤ (1 / 4))
205	77, 204	mpbi 232	. . . . . . . . . . . 12 ⊢ ¬ (1 / 2) ≤ (1 / 4)
206	200	breq1d 5110	. . . . . . . . . . . 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 4491	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))) = (𝑦 + (1 / 4)))
209	200	oveq1d 7411	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 / 2) = ((1 / 2) / 2))
210	209, 29	eqtrdi 2813	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 / 2) = (1 / 4))
211	210	oveq1d 7411	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → ((𝑦 / 2) + (1 / 2)) = ((1 / 4) + (1 / 2)))
212	203, 208, 211	3eqtr4d 2807	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))) = ((𝑦 / 2) + (1 / 2)))
213		eqid 2762	. . . . . . . . . 10 ⊢ ((topGen‘ran (,)) ↾_t (0[,](1 / 4))) = ((topGen‘ran (,)) ↾_t (0[,](1 / 4)))
214		eqid 2762	. . . . . . . . . 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 12098	. . . . . . . . . . . . 13 ⊢ 0 < (1 / 4)
217	14, 17, 216	ltleii 11306	. . . . . . . . . . . 12 ⊢ 0 ≤ (1 / 4)
218	14, 59	elicc2i 13416	. . . . . . . . . . . 12 ⊢ ((1 / 4) ∈ (0[,](1 / 2)) ↔ ((1 / 4) ∈ ℝ ∧ 0 ≤ (1 / 4) ∧ (1 / 4) ≤ (1 / 2)))
219	17, 217, 78, 218	mpbir3an 1355	. . . . . . . . . . 11 ⊢ (1 / 4) ∈ (0[,](1 / 2))
220	219	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (1 / 4) ∈ (0[,](1 / 2)))
221		simprl 780	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → 𝑦 = (1 / 4))
222	221	oveq2d 7412	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = (2 · (1 / 4)))
223	221	oveq1d 7411	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 4) + (1 / 4)))
224	23, 222, 223	3eqtr4a 2823	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = (𝑦 + (1 / 4)))
225		retopon 24823	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ)
226		0xr 11229	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ^*
227	59	rexri 11240	. . . . . . . . . . . . . . . 16 ⊢ (1 / 2) ∈ ℝ^*
228		lbicc2 13468	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℝ^* ∧ (1 / 2) ∈ ℝ^* ∧ 0 ≤ (1 / 2)) → 0 ∈ (0[,](1 / 2)))
229	226, 227, 142, 228	mp3an 1482	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ (0[,](1 / 2))
230		iccss2 13421	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ (0[,](1 / 2)) ∧ (1 / 4) ∈ (0[,](1 / 2))) → (0[,](1 / 4)) ⊆ (0[,](1 / 2)))
231	229, 219, 230	mp2an 702	. . . . . . . . . . . . . 14 ⊢ (0[,](1 / 4)) ⊆ (0[,](1 / 2))
232		iccssre 13433	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (0[,](1 / 2)) ⊆ ℝ)
233	14, 59, 232	mp2an 702	. . . . . . . . . . . . . 14 ⊢ (0[,](1 / 2)) ⊆ ℝ
234	231, 233	sstri 3945	. . . . . . . . . . . . 13 ⊢ (0[,](1 / 4)) ⊆ ℝ
235		resttopon 23221	. . . . . . . . . . . . 13 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 / 4)) ⊆ ℝ) → ((topGen‘ran (,)) ↾_t (0[,](1 / 4))) ∈ (TopOn‘(0[,](1 / 4))))
236	225, 234, 235	mp2an 702	. . . . . . . . . . . 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 23728	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 4)), 𝑧 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,)) ↾_t (0[,](1 / 4))) ×_t II) Cn ((topGen‘ran (,)) ↾_t (0[,](1 / 4)))))
239		retop 24821	. . . . . . . . . . . . . 14 ⊢ (topGen‘ran (,)) ∈ Top
240		ovex 7429	. . . . . . . . . . . . . 14 ⊢ (0[,](1 / 2)) ∈ V
241		restabs 23225	. . . . . . . . . . . . . 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 1482	. . . . . . . . . . . . 13 ⊢ (((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ↾_t (0[,](1 / 4))) = ((topGen‘ran (,)) ↾_t (0[,](1 / 4)))
243	242	eqcomi 2771	. . . . . . . . . . . 12 ⊢ ((topGen‘ran (,)) ↾_t (0[,](1 / 4))) = (((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ↾_t (0[,](1 / 4)))
244		resttopon 23221	. . . . . . . . . . . . . 14 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 / 2)) ⊆ ℝ) → ((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 / 2))))
245	225, 233, 244	mp2an 702	. . . . . . . . . . . . 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 24994	. . . . . . . . . . . . 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 23736	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (0[,](1 / 4)) ↦ (2 · 𝑥)) ∈ (((topGen‘ran (,)) ↾_t (0[,](1 / 4))) Cn II))
251		oveq2 7404	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
252	237, 188, 238, 237, 250, 251	cnmpt21 23731	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 4)), 𝑧 ∈ (0[,]1) ↦ (2 · 𝑦)) ∈ ((((topGen‘ran (,)) ↾_t (0[,](1 / 4))) ×_t II) Cn II))
253		iccssre 13433	. . . . . . . . . . . . . 14 ⊢ (((1 / 4) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → ((1 / 4)[,](1 / 2)) ⊆ ℝ)
254	17, 59, 253	mp2an 702	. . . . . . . . . . . . 13 ⊢ ((1 / 4)[,](1 / 2)) ⊆ ℝ
255		resttopon 23221	. . . . . . . . . . . . 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 702	. . . . . . . . . . . 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 23728	. . . . . . . . . . 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 2762	. . . . . . . . . . . 12 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
260	254	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1 / 4)[,](1 / 2)) ⊆ ℝ)
261		unitssre 13503	. . . . . . . . . . . . 13 ⊢ (0[,]1) ⊆ ℝ
262	261	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (0[,]1) ⊆ ℝ)
263	149, 87	sselid 3934	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ∈ (0[,]1))
264	263	adantl 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 4)[,](1 / 2))) → (𝑥 + (1 / 4)) ∈ (0[,]1))
265	259	cnfldtopon 24842	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
266	265	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ))
267	266	cnmptid 23721	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ 𝑥) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
268	17	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 / 4) ∈ ℝ)
269	268	recnd 11210	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 / 4) ∈ ℂ)
270	266, 266, 269	cnmptc 23722	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (1 / 4)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
271	259	addcn 24926	. . . . . . . . . . . . . 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 23726	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (𝑥 + (1 / 4))) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
274	259, 214, 196, 260, 262, 264, 273	cnmptre 24989	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ ((1 / 4)[,](1 / 2)) ↦ (𝑥 + (1 / 4))) ∈ (((topGen‘ran (,)) ↾_t ((1 / 4)[,](1 / 2))) Cn II))
275		oveq1 7403	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 + (1 / 4)) = (𝑦 + (1 / 4)))
276	257, 188, 258, 257, 274, 275	cnmpt21 23731	. . . . . . . . . 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 24990	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 2)), 𝑧 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4)))) ∈ ((((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ×_t II) Cn II))
278		iccssre 13433	. . . . . . . . . . . . 13 ⊢ (((1 / 2) ∈ ℝ ∧ 1 ∈ ℝ) → ((1 / 2)[,]1) ⊆ ℝ)
279	59, 85, 278	mp2an 702	. . . . . . . . . . . 12 ⊢ ((1 / 2)[,]1) ⊆ ℝ
280		resttopon 23221	. . . . . . . . . . . 12 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 / 2)[,]1) ⊆ ℝ) → ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1)))
281	225, 279, 280	mp2an 702	. . . . . . . . . . 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 23728	. . . . . . . . . 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 3934	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → ((𝑥 / 2) + (1 / 2)) ∈ (0[,]1))
286	285	adantl 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝑥 / 2) + (1 / 2)) ∈ (0[,]1))
287	259	divccn 24935	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℂ ∧ 2 ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
288	4, 24, 287	mp2an 702	. . . . . . . . . . . . 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 23722	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (1 / 2)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
292	266, 289, 291, 272	cnmpt12f 23726	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((𝑥 / 2) + (1 / 2))) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
293	259, 195, 196, 284, 262, 286, 292	cnmptre 24989	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ ((1 / 2)[,]1) ↦ ((𝑥 / 2) + (1 / 2))) ∈ (((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) Cn II))
294		oveq1 7403	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 / 2) = (𝑦 / 2))
295	294	oveq1d 7411	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 / 2) + (1 / 2)) = ((𝑦 / 2) + (1 / 2)))
296	282, 188, 283, 282, 293, 295	cnmpt21 23731	. . . . . . . . 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 24990	. . . . . . . 8 ⊢ (𝜑 → (𝑦 ∈ (0[,]1), 𝑧 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 2), if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))), ((𝑦 / 2) + (1 / 2)))) ∈ ((II ×_t II) Cn II))
298		breq1 5103	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑥 ≤ (1 / 2) ↔ 𝑦 ≤ (1 / 2)))
299		breq1 5103	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝑥 ≤ (1 / 4) ↔ 𝑦 ≤ (1 / 4)))
300	299, 251, 275	ifbieq12d 4509	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))))
301	298, 300, 295	ifbieq12d 4509	. . . . . . . . . . 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 2040	. . . . . . . . . 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 484	. . . . . . . . 9 ⊢ ((𝑦 = 𝑥 ∧ 𝑧 = 0) → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑦 ≤ (1 / 2), if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))), ((𝑦 / 2) + (1 / 2))))
304	303	eqcomd 2768	. . . . . . . 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 23727	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) ∈ (II Cn II))
306	186, 305	eqeltrid 2866	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ (II Cn II))
307		iiuni 24943	. . . . . . 7 ⊢ (0[,]1) = ∪ II
308	307, 307	cnf 23306	. . . . . 6 ⊢ (𝑃 ∈ (II Cn II) → 𝑃:(0[,]1)⟶(0[,]1))
309	306, 308	syl 17	. . . . 5 ⊢ (𝜑 → 𝑃:(0[,]1)⟶(0[,]1))
310	186	fmpt 7091	. . . . 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 25079	. . . . . 6 ⊢ (𝜑 → (𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) ∈ (II Cn 𝐽))
314		eqid 2762	. . . . . . 7 ⊢ ∪ 𝐽 = ∪ 𝐽
315	307, 314	cnf 23306	. . . . . 6 ⊢ ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) ∈ (II Cn 𝐽) → (𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)):(0[,]1)⟶∪ 𝐽)
316	313, 315	syl 17	. . . . 5 ⊢ (𝜑 → (𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)):(0[,]1)⟶∪ 𝐽)
317	316	feqmptd 6935	. . . 4 ⊢ (𝜑 → (𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) = (𝑦 ∈ (0[,]1) ↦ ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘𝑦)))
318		fveq2 6867	. . . 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 7112	. . 3 ⊢ (𝜑 → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) ∘ 𝑃) = (𝑥 ∈ (0[,]1) ↦ ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))))))
320	40, 41, 89	pcocn 25079	. . . 4 ⊢ (𝜑 → (𝐹(*_𝑝‘𝐽)𝐺) ∈ (II Cn 𝐽))
321	320, 42	pcoval 25073	. . 3 ⊢ (𝜑 → ((𝐹(_𝑝‘𝐽)𝐺)(_𝑝‘𝐽)𝐻) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1)))))
322	185, 319, 321	3eqtr4rd 2808	. 2 ⊢ (𝜑 → ((𝐹(_𝑝‘𝐽)𝐺)(_𝑝‘𝐽)𝐻) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) ∘ 𝑃))
323		id 22	. . . . . . . 8 ⊢ (𝑥 = 0 → 𝑥 = 0)
324	323, 142	eqbrtrdi 5139	. . . . . . 7 ⊢ (𝑥 = 0 → 𝑥 ≤ (1 / 2))
325	324	iftrued 4488	. . . . . 6 ⊢ (𝑥 = 0 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))))
326	323, 217	eqbrtrdi 5139	. . . . . . 7 ⊢ (𝑥 = 0 → 𝑥 ≤ (1 / 4))
327	326	iftrued 4488	. . . . . 6 ⊢ (𝑥 = 0 → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (2 · 𝑥))
328		oveq2 7404	. . . . . . 7 ⊢ (𝑥 = 0 → (2 · 𝑥) = (2 · 0))
329		2t0e0 12388	. . . . . . 7 ⊢ (2 · 0) = 0
330	328, 329	eqtrdi 2813	. . . . . 6 ⊢ (𝑥 = 0 → (2 · 𝑥) = 0)
331	325, 327, 330	3eqtrd 2801	. . . . 5 ⊢ (𝑥 = 0 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = 0)
332		c0ex 11173	. . . . 5 ⊢ 0 ∈ V
333	331, 186, 332	fvmpt 6975	. . . 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 11304	. . . . . . . . 9 ⊢ ((1 / 2) < 1 ↔ ¬ 1 ≤ (1 / 2))
337	143, 336	mpbi 232	. . . . . . . 8 ⊢ ¬ 1 ≤ (1 / 2)
338		breq1 5103	. . . . . . . 8 ⊢ (𝑥 = 1 → (𝑥 ≤ (1 / 2) ↔ 1 ≤ (1 / 2)))
339	337, 338	mtbiri 329	. . . . . . 7 ⊢ (𝑥 = 1 → ¬ 𝑥 ≤ (1 / 2))
340	339	iffalsed 4491	. . . . . 6 ⊢ (𝑥 = 1 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = ((𝑥 / 2) + (1 / 2)))
341		oveq1 7403	. . . . . . . 8 ⊢ (𝑥 = 1 → (𝑥 / 2) = (1 / 2))
342	341	oveq1d 7411	. . . . . . 7 ⊢ (𝑥 = 1 → ((𝑥 / 2) + (1 / 2)) = ((1 / 2) + (1 / 2)))
343	342, 83	eqtrdi 2813	. . . . . 6 ⊢ (𝑥 = 1 → ((𝑥 / 2) + (1 / 2)) = 1)
344	340, 343	eqtrd 2797	. . . . 5 ⊢ (𝑥 = 1 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = 1)
345		1ex 11176	. . . . 5 ⊢ 1 ∈ V
346	344, 186, 345	fvmpt 6975	. . . 4 ⊢ (1 ∈ (0[,]1) → (𝑃‘1) = 1)
347	335, 346	syl 17	. . 3 ⊢ (𝜑 → (𝑃‘1) = 1)
348	313, 306, 334, 347	reparpht 25060	. 2 ⊢ (𝜑 → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) ∘ 𝑃)( ≃_ph‘𝐽)(𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)))
349	322, 348	eqbrtrd 5122	1 ⊢ (𝜑 → ((𝐹(_𝑝‘𝐽)𝐺)(_𝑝‘𝐽)𝐻)( ≃_ph‘𝐽)(𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 399 ∨ wo 858 = wceq 1560 ∈ wcel 2142 ≠ wne 2957 ∀wral 3076 Vcvv 3454 ⊆ wss 3904 ifcif 4480 ∪ cuni 4865 class class class wbr 5100 ↦ cmpt 5181 ran crn 5648 ∘ ccom 5651 ⟶wf 6517 ‘cfv 6521 (class class class)co 7396 ℂcc 11071 ℝcr 11072 0cc0 11073 1c1 11074 + caddc 11076 · cmul 11078 ℝ^*cxr 11215 < clt 11216 ≤ cle 11217 − cmin 11414 / cdiv 11844 ℕcn 12210 2c2 12272 4c4 12274 (,)cioo 13349 [,]cicc 13352 ↾_t crest 17449 TopOpenctopn 17450 topGenctg 17466 ℂ_fldccnfld 21424 Topctop 22953 TopOnctopon 22970 Cn ccn 23284 ×_t ctx 23620 IIcii 24937 ≃_phcphtpc 25031 *_𝑝cpco 25062

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5227 ax-sep 5246 ax-nul 5256 ax-pow 5322 ax-pr 5390 ax-un 7718 ax-cnex 11129 ax-resscn 11130 ax-1cn 11131 ax-icn 11132 ax-addcl 11133 ax-addrcl 11134 ax-mulcl 11135 ax-mulrcl 11136 ax-mulcom 11137 ax-addass 11138 ax-mulass 11139 ax-distr 11140 ax-i2m1 11141 ax-1ne0 11142 ax-1rid 11143 ax-rnegex 11144 ax-rrecex 11145 ax-cnre 11146 ax-pre-lttri 11147 ax-pre-lttrn 11148 ax-pre-ltadd 11149 ax-pre-mulgt0 11150 ax-pre-sup 11151 ax-addf 11152

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1099 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-nf 1804 df-sb 2091 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3456 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4481 df-pw 4557 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-int 4906 df-iun 4951 df-iin 4952 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-se 5601 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6288 df-ord 6349 df-on 6350 df-lim 6351 df-suc 6352 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 df-fv 6529 df-isom 6530 df-riota 7353 df-ov 7399 df-oprab 7400 df-mpo 7401 df-of 7660 df-om 7847 df-1st 7970 df-2nd 7971 df-supp 8141 df-frecs 8262 df-wrecs 8293 df-recs 8342 df-rdg 8381 df-1o 8437 df-2o 8438 df-er 8678 df-map 8810 df-ixp 8880 df-en 8928 df-dom 8929 df-sdom 8930 df-fin 8931 df-fsupp 9308 df-fi 9357 df-sup 9388 df-inf 9389 df-oi 9458 df-card 9897 df-pnf 11218 df-mnf 11219 df-xr 11220 df-ltxr 11221 df-le 11222 df-sub 11416 df-neg 11417 df-div 11845 df-nn 12211 df-2 12280 df-3 12281 df-4 12282 df-5 12283 df-6 12284 df-7 12285 df-8 12286 df-9 12287 df-n0 12482 df-z 12569 df-dec 12689 df-uz 12840 df-q 12950 df-rp 12994 df-xneg 13114 df-xadd 13115 df-xmul 13116 df-ioo 13353 df-icc 13356 df-fz 13513 df-fzo 13660 df-seq 14015 df-exp 14075 df-hash 14344 df-cj 15126 df-re 15127 df-im 15128 df-sqrt 15262 df-abs 15263 df-struct 17183 df-sets 17200 df-slot 17218 df-ndx 17230 df-base 17246 df-ress 17267 df-plusg 17299 df-mulr 17300 df-starv 17301 df-sca 17302 df-vsca 17303 df-ip 17304 df-tset 17305 df-ple 17306 df-ds 17308 df-unif 17309 df-hom 17310 df-cco 17311 df-rest 17451 df-topn 17452 df-0g 17470 df-gsum 17471 df-topgen 17472 df-pt 17473 df-prds 17476 df-xrs 17532 df-qtop 17537 df-imas 17538 df-xps 17540 df-mre 17614 df-mrc 17615 df-acs 17617 df-mgm 18674 df-sgrp 18753 df-mnd 18769 df-submnd 18818 df-mulg 19110 df-cntz 19357 df-cmn 19822 df-psmet 21416 df-xmet 21417 df-met 21418 df-bl 21419 df-mopn 21420 df-cnfld 21425 df-top 22954 df-topon 22971 df-topsp 22993 df-bases 23006 df-cld 23079 df-cn 23287 df-cnp 23288 df-tx 23622 df-hmeo 23815 df-xms 24380 df-ms 24381 df-tms 24382 df-ii 24939 df-htpy 25032 df-phtpy 25033 df-phtpc 25054 df-pco 25067

This theorem is referenced by: pcophtb 25091 pi1grplem 25111 pi1xfr 25117 pi1xfrcnvlem 25118

W3C validator