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 25004

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 4473	. . . . . . . . . . 11 ⊢ (𝑥 ≤ (1 / 4) → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (2 · 𝑥))
2	1	fveq2d 6839	. . . . . . . . . 10 ⊢ (𝑥 ≤ (1 / 4) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(2 · 𝑥)))
3	2	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(2 · 𝑥)))
4		2cn 12250	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℂ
5		elicc01 13413	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (0[,]1) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1))
6	5	simp1bi 1146	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0[,]1) → 𝑥 ∈ ℝ)
7	6	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℝ)
8	7	recnd 11167	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℂ)
9		mulcom 11118	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) = (𝑥 · 2))
10	4, 8, 9	sylancr 588	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) = (𝑥 · 2))
11	5	simp2bi 1147	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0[,]1) → 0 ≤ 𝑥)
12	11	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 0 ≤ 𝑥)
13		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ≤ (1 / 4))
14		0re 11140	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℝ
15		4nn 12258	. . . . . . . . . . . . . . . 16 ⊢ 4 ∈ ℕ
16		nnrecre 12213	. . . . . . . . . . . . . . . 16 ⊢ (4 ∈ ℕ → (1 / 4) ∈ ℝ)
17	15, 16	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (1 / 4) ∈ ℝ
18	14, 17	elicc2i 13359	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (0[,](1 / 4)) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ (1 / 4)))
19	7, 12, 13, 18	syl3anbrc 1345	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ (0[,](1 / 4)))
20		2rp 12941	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℝ⁺
21	4	mul02i 11329	. . . . . . . . . . . . . 14 ⊢ (0 · 2) = 0
22	17	recni 11153	. . . . . . . . . . . . . . 15 ⊢ (1 / 4) ∈ ℂ
23	22	2timesi 12308	. . . . . . . . . . . . . . . 16 ⊢ (2 · (1 / 4)) = ((1 / 4) + (1 / 4))
24		2ne0 12279	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ≠ 0
25		recdiv2 11862	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((1 / 2) / 2) = (1 / (2 · 2)))
26	4, 24, 4, 24, 25	mp4an 694	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 / 2) / 2) = (1 / (2 · 2))
27		2t2e4 12334	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2 · 2) = 4
28	27	oveq2i 7372	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 / (2 · 2)) = (1 / 4)
29	26, 28	eqtri 2760	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 / 2) / 2) = (1 / 4)
30	29, 29	oveq12i 7373	. . . . . . . . . . . . . . . . 17 ⊢ (((1 / 2) / 2) + ((1 / 2) / 2)) = ((1 / 4) + (1 / 4))
31		halfcn 12385	. . . . . . . . . . . . . . . . . 18 ⊢ (1 / 2) ∈ ℂ
32		2halves 12389	. . . . . . . . . . . . . . . . . 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 2762	. . . . . . . . . . . . . . . 16 ⊢ ((1 / 4) + (1 / 4)) = (1 / 2)
35	23, 34	eqtri 2760	. . . . . . . . . . . . . . 15 ⊢ (2 · (1 / 4)) = (1 / 2)
36	4, 22, 35	mulcomli 11148	. . . . . . . . . . . . . 14 ⊢ ((1 / 4) · 2) = (1 / 2)
37	14, 17, 20, 21, 36	iccdili 13438	. . . . . . . . . . . . 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 2837	. . . . . . . . . . 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 24997	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺(*_𝑝‘𝐽)𝐻) ∈ (II Cn 𝐽))
45	40, 44	pcoval1 24993	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(2 · 𝑥)) = (𝐹‘(2 · (2 · 𝑥))))
46	40, 41	pcoval1 24993	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) → ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)) = (𝐹‘(2 · (2 · 𝑥))))
47	45, 46	eqtr4d 2775	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
48	39, 47	sylan2 594	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4))) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
49	48	anassrs 467	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
50	3, 49	eqtrd 2772	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
51	50	adantlr 716	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
52		simplll 775	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝜑)
53	6	ad2antlr 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → 𝑥 ∈ ℝ)
54	53	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℝ)
55		letric 11240	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ ∧ (1 / 4) ∈ ℝ) → (𝑥 ≤ (1 / 4) ∨ (1 / 4) ≤ 𝑥))
56	53, 17, 55	sylancl 587	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → (𝑥 ≤ (1 / 4) ∨ (1 / 4) ≤ 𝑥))
57	56	orcanai 1005	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (1 / 4) ≤ 𝑥)
58		simplr 769	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ≤ (1 / 2))
59		halfre 12384	. . . . . . . . . . . . 13 ⊢ (1 / 2) ∈ ℝ
60	17, 59	elicc2i 13359	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) ↔ (𝑥 ∈ ℝ ∧ (1 / 4) ≤ 𝑥 ∧ 𝑥 ≤ (1 / 2)))
61	54, 57, 58, 60	syl3anbrc 1345	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ((1 / 4)[,](1 / 2)))
62	60	simp1bi 1146	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → 𝑥 ∈ ℝ)
63		readdcl 11115	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ ∧ (1 / 4) ∈ ℝ) → (𝑥 + (1 / 4)) ∈ ℝ)
64	62, 17, 63	sylancl 587	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ∈ ℝ)
65	17	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 4) ∈ ℝ)
66	60	simp2bi 1147	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 4) ≤ 𝑥)
67	65, 62, 65, 66	leadd1dd 11758	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → ((1 / 4) + (1 / 4)) ≤ (𝑥 + (1 / 4)))
68	34, 67	eqbrtrrid 5122	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 2) ≤ (𝑥 + (1 / 4)))
69	59	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 2) ∈ ℝ)
70	60	simp3bi 1148	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → 𝑥 ≤ (1 / 2))
71		2lt4 12345	. . . . . . . . . . . . . . . . 17 ⊢ 2 < 4
72		2re 12249	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ
73		4re 12259	. . . . . . . . . . . . . . . . . 18 ⊢ 4 ∈ ℝ
74		2pos 12278	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 2
75		4pos 12282	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 4
76	72, 73, 74, 75	ltrecii 12066	. . . . . . . . . . . . . . . . 17 ⊢ (2 < 4 ↔ (1 / 4) < (1 / 2))
77	71, 76	mpbi 230	. . . . . . . . . . . . . . . 16 ⊢ (1 / 4) < (1 / 2)
78	17, 59, 77	ltleii 11263	. . . . . . . . . . . . . . 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 11763	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ≤ ((1 / 2) + (1 / 2)))
81		ax-1cn 11090	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
82		2halves 12389	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℂ → ((1 / 2) + (1 / 2)) = 1)
83	81, 82	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((1 / 2) + (1 / 2)) = 1
84	80, 83	breqtrdi 5127	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ≤ 1)
85		1re 11138	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ
86	59, 85	elicc2i 13359	. . . . . . . . . . . 12 ⊢ ((𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1) ↔ ((𝑥 + (1 / 4)) ∈ ℝ ∧ (1 / 2) ≤ (𝑥 + (1 / 4)) ∧ (𝑥 + (1 / 4)) ≤ 1))
87	64, 68, 84, 86	syl3anbrc 1345	. . . . . . . . . . 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 24994	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐺(*_𝑝‘𝐽)𝐻)‘0) = (𝐺‘0))
91	89, 90	eqtr4d 2775	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹‘1) = ((𝐺(*_𝑝‘𝐽)𝐻)‘0))
92	40, 44, 91	pcoval2 24996	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))) = ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)))
93	52, 88, 92	syl2anc 585	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))) = ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)))
94	83	oveq2i 7372	. . . . . . . . . . . 12 ⊢ ((2 · (𝑥 + (1 / 4))) − ((1 / 2) + (1 / 2))) = ((2 · (𝑥 + (1 / 4))) − 1)
95		2cnd 12253	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 2 ∈ ℂ)
96	54	recnd 11167	. . . . . . . . . . . . . . 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 11163	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · (𝑥 + (1 / 4))) = ((2 · 𝑥) + (2 · (1 / 4))))
99	35	oveq2i 7372	. . . . . . . . . . . . . 14 ⊢ ((2 · 𝑥) + (2 · (1 / 4))) = ((2 · 𝑥) + (1 / 2))
100	98, 99	eqtrdi 2788	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · (𝑥 + (1 / 4))) = ((2 · 𝑥) + (1 / 2)))
101	100	oveq1d 7376	. . . . . . . . . . . 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 2786	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − 1) = (((2 · 𝑥) + (1 / 2)) − ((1 / 2) + (1 / 2))))
103		remulcl 11117	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (2 · 𝑥) ∈ ℝ)
104	72, 54, 103	sylancr 588	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈ ℝ)
105	104	recnd 11167	. . . . . . . . . . . 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 11537	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (((2 · 𝑥) + (1 / 2)) − ((1 / 2) + (1 / 2))) = ((2 · 𝑥) − (1 / 2)))
108	102, 107	eqtrd 2772	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − 1) = ((2 · 𝑥) − (1 / 2)))
109	108	fveq2d 6839	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(_𝑝‘𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)) = ((𝐺(_𝑝‘𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))))
110	4, 96, 9	sylancr 588	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) = (𝑥 · 2))
111	81, 4, 24	divcan1i 11893	. . . . . . . . . . . . . . 15 ⊢ ((1 / 2) · 2) = 1
112	17, 59, 20, 36, 111	iccdili 13438	. . . . . . . . . . . . . 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 2837	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈ ((1 / 2)[,]1))
115	31	subidi 11459	. . . . . . . . . . . . 13 ⊢ ((1 / 2) − (1 / 2)) = 0
116		1mhlfehlf 12390	. . . . . . . . . . . . 13 ⊢ (1 − (1 / 2)) = (1 / 2)
117	59, 85, 59, 115, 116	iccshftli 13436	. . . . . . . . . . . 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 24993	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((2 · 𝑥) − (1 / 2)) ∈ (0[,](1 / 2))) → ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))))
120	52, 118, 119	syl2anc 585	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))))
121	95, 105, 106	subdid 11600	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · ((2 · 𝑥) − (1 / 2))) = ((2 · (2 · 𝑥)) − (2 · (1 / 2))))
122	4, 24	recidi 11880	. . . . . . . . . . . . 13 ⊢ (2 · (1 / 2)) = 1
123	122	oveq2i 7372	. . . . . . . . . . . 12 ⊢ ((2 · (2 · 𝑥)) − (2 · (1 / 2))) = ((2 · (2 · 𝑥)) − 1)
124	121, 123	eqtrdi 2788	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · ((2 · 𝑥) − (1 / 2))) = ((2 · (2 · 𝑥)) − 1))
125	124	fveq2d 6839	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
126	120, 125	eqtrd 2772	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
127	93, 109, 126	3eqtrd 2776	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
128		iffalse 4476	. . . . . . . . . 10 ⊢ (¬ 𝑥 ≤ (1 / 4) → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (𝑥 + (1 / 4)))
129	128	fveq2d 6839	. . . . . . . . 9 ⊢ (¬ 𝑥 ≤ (1 / 4) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))))
130	129	adantl 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))))
131	40, 41, 89	pcoval2 24996	. . . . . . . . 9 ⊢ ((𝜑 ∧ (2 · 𝑥) ∈ ((1 / 2)[,]1)) → ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
132	52, 114, 131	syl2anc 585	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
133	127, 130, 132	3eqtr4d 2782	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
134	51, 133	pm2.61dan 813	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
135		iftrue 4473	. . . . . . . 8 ⊢ (𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))))
136	135	fveq2d 6839	. . . . . . 7 ⊢ (𝑥 ≤ (1 / 2) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))))
137	136	adantl 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))))
138		iftrue 4473	. . . . . . 7 ⊢ (𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), ((𝐹(_𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = ((𝐹(_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
139	138	adantl 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → if(𝑥 ≤ (1 / 2), ((𝐹(_𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = ((𝐹(_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
140	134, 137, 139	3eqtr4d 2782	. . . . 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 24916	. . . . . . . 8 ⊢ ((𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 ≤ (1 / 2)) → 𝑥 ∈ ((1 / 2)[,]1))
142		halfge0 12387	. . . . . . . . . . . . . 14 ⊢ 0 ≤ (1 / 2)
143		halflt1 12388	. . . . . . . . . . . . . . 15 ⊢ (1 / 2) < 1
144	59, 85, 143	ltleii 11263	. . . . . . . . . . . . . 14 ⊢ (1 / 2) ≤ 1
145		elicc01 13413	. . . . . . . . . . . . . 14 ⊢ ((1 / 2) ∈ (0[,]1) ↔ ((1 / 2) ∈ ℝ ∧ 0 ≤ (1 / 2) ∧ (1 / 2) ≤ 1))
146	59, 142, 144, 145	mpbir3an 1343	. . . . . . . . . . . . 13 ⊢ (1 / 2) ∈ (0[,]1)
147		1elunit 13417	. . . . . . . . . . . . 13 ⊢ 1 ∈ (0[,]1)
148		iccss2 13364	. . . . . . . . . . . . 13 ⊢ (((1 / 2) ∈ (0[,]1) ∧ 1 ∈ (0[,]1)) → ((1 / 2)[,]1) ⊆ (0[,]1))
149	146, 147, 148	mp2an 693	. . . . . . . . . . . 12 ⊢ ((1 / 2)[,]1) ⊆ (0[,]1)
150	149	sseli 3918	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 𝑥 ∈ (0[,]1))
151	4, 24	div0i 11883	. . . . . . . . . . . 12 ⊢ (0 / 2) = 0
152		eqid 2737	. . . . . . . . . . . 12 ⊢ (1 / 2) = (1 / 2)
153	14, 85, 20, 151, 152	icccntri 13440	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (0[,]1) → (𝑥 / 2) ∈ (0[,](1 / 2)))
154	31	addlidi 11328	. . . . . . . . . . . 12 ⊢ (0 + (1 / 2)) = (1 / 2)
155	14, 59, 59, 154, 83	iccshftri 13434	. . . . . . . . . . 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 24996	. . . . . . . . . 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 13359	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 2)[,]1) ↔ (𝑥 ∈ ℝ ∧ (1 / 2) ≤ 𝑥 ∧ 𝑥 ≤ 1))
160	159	simp1bi 1146	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 𝑥 ∈ ℝ)
161	160	recnd 11167	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 𝑥 ∈ ℂ)
162		1cnd 11133	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 1 ∈ ℂ)
163		2cnd 12253	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 2 ∈ ℂ)
164	24	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 2 ≠ 0)
165	161, 162, 163, 164	divdird 11963	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → ((𝑥 + 1) / 2) = ((𝑥 / 2) + (1 / 2)))
166	165	oveq2d 7377	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → (2 · ((𝑥 + 1) / 2)) = (2 · ((𝑥 / 2) + (1 / 2))))
167		peano2cn 11312	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ → (𝑥 + 1) ∈ ℂ)
168	161, 167	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → (𝑥 + 1) ∈ ℂ)
169	168, 163, 164	divcan2d 11927	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → (2 · ((𝑥 + 1) / 2)) = (𝑥 + 1))
170	166, 169	eqtr3d 2774	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → (2 · ((𝑥 / 2) + (1 / 2))) = (𝑥 + 1))
171	161, 162, 170	mvrraddd 11556	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → ((2 · ((𝑥 / 2) + (1 / 2))) − 1) = 𝑥)
172	171	fveq2d 6839	. . . . . . . . . 10 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → ((𝐺(_𝑝‘𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)) = ((𝐺(_𝑝‘𝐽)𝐻)‘𝑥))
173	172	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝐺(_𝑝‘𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)) = ((𝐺(_𝑝‘𝐽)𝐻)‘𝑥))
174	41, 42, 43	pcoval2 24996	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝐺(*_𝑝‘𝐽)𝐻)‘𝑥) = (𝐻‘((2 · 𝑥) − 1)))
175	158, 173, 174	3eqtrd 2776	. . . . . . . 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 467	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1)))
178		iffalse 4476	. . . . . . . 8 ⊢ (¬ 𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = ((𝑥 / 2) + (1 / 2)))
179	178	fveq2d 6839	. . . . . . 7 ⊢ (¬ 𝑥 ≤ (1 / 2) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))))
180	179	adantl 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))))
181		iffalse 4476	. . . . . . 7 ⊢ (¬ 𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = (𝐻‘((2 · 𝑥) − 1)))
182	181	adantl 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ ¬ 𝑥 ≤ (1 / 2)) → if(𝑥 ≤ (1 / 2), ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))) = (𝐻‘((2 · 𝑥) − 1)))
183	177, 180, 182	3eqtr4d 2782	. . . . 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 813	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = if(𝑥 ≤ (1 / 2), ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1))))
185	184	mpteq2dva 5179	. . 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 24859	. . . . . . . . 9 ⊢ II ∈ (TopOn‘(0[,]1))
188	187	a1i 11	. . . . . . . 8 ⊢ (𝜑 → II ∈ (TopOn‘(0[,]1)))
189	188	cnmptid 23639	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ 𝑥) ∈ (II Cn II))
190		0elunit 13416	. . . . . . . . . 10 ⊢ 0 ∈ (0[,]1)
191	190	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0[,]1))
192	188, 188, 191	cnmptc 23640	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ 0) ∈ (II Cn II))
193		eqid 2737	. . . . . . . . 9 ⊢ (topGen‘ran (,)) = (topGen‘ran (,))
194		eqid 2737	. . . . . . . . 9 ⊢ ((topGen‘ran (,)) ↾_t (0[,](1 / 2))) = ((topGen‘ran (,)) ↾_t (0[,](1 / 2)))
195		eqid 2737	. . . . . . . . 9 ⊢ ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) = ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1))
196		dfii2 24862	. . . . . . . . 9 ⊢ II = ((topGen‘ran (,)) ↾_t (0[,]1))
197		0red 11141	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ ℝ)
198		1red 11139	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℝ)
199	146	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (1 / 2) ∈ (0[,]1))
200		simprl 771	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → 𝑦 = (1 / 2))
201	200	oveq1d 7376	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 2) + (1 / 4)))
202	31, 22	addcomi 11331	. . . . . . . . . . 11 ⊢ ((1 / 2) + (1 / 4)) = ((1 / 4) + (1 / 2))
203	201, 202	eqtrdi 2788	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 4) + (1 / 2)))
204	17, 59	ltnlei 11261	. . . . . . . . . . . . 13 ⊢ ((1 / 4) < (1 / 2) ↔ ¬ (1 / 2) ≤ (1 / 4))
205	77, 204	mpbi 230	. . . . . . . . . . . 12 ⊢ ¬ (1 / 2) ≤ (1 / 4)
206	200	breq1d 5096	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 ≤ (1 / 4) ↔ (1 / 2) ≤ (1 / 4)))
207	205, 206	mtbiri 327	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → ¬ 𝑦 ≤ (1 / 4))
208	207	iffalsed 4478	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))) = (𝑦 + (1 / 4)))
209	200	oveq1d 7376	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 / 2) = ((1 / 2) / 2))
210	209, 29	eqtrdi 2788	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 / 2) = (1 / 4))
211	210	oveq1d 7376	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → ((𝑦 / 2) + (1 / 2)) = ((1 / 4) + (1 / 2)))
212	203, 208, 211	3eqtr4d 2782	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))) = ((𝑦 / 2) + (1 / 2)))
213		eqid 2737	. . . . . . . . . 10 ⊢ ((topGen‘ran (,)) ↾_t (0[,](1 / 4))) = ((topGen‘ran (,)) ↾_t (0[,](1 / 4)))
214		eqid 2737	. . . . . . . . . 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 12056	. . . . . . . . . . . . 13 ⊢ 0 < (1 / 4)
217	14, 17, 216	ltleii 11263	. . . . . . . . . . . 12 ⊢ 0 ≤ (1 / 4)
218	14, 59	elicc2i 13359	. . . . . . . . . . . 12 ⊢ ((1 / 4) ∈ (0[,](1 / 2)) ↔ ((1 / 4) ∈ ℝ ∧ 0 ≤ (1 / 4) ∧ (1 / 4) ≤ (1 / 2)))
219	17, 217, 78, 218	mpbir3an 1343	. . . . . . . . . . 11 ⊢ (1 / 4) ∈ (0[,](1 / 2))
220	219	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (1 / 4) ∈ (0[,](1 / 2)))
221		simprl 771	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → 𝑦 = (1 / 4))
222	221	oveq2d 7377	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = (2 · (1 / 4)))
223	221	oveq1d 7376	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 4) + (1 / 4)))
224	23, 222, 223	3eqtr4a 2798	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = (𝑦 + (1 / 4)))
225		retopon 24741	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ)
226		0xr 11186	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ^*
227	59	rexri 11197	. . . . . . . . . . . . . . . 16 ⊢ (1 / 2) ∈ ℝ^*
228		lbicc2 13411	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℝ^* ∧ (1 / 2) ∈ ℝ^* ∧ 0 ≤ (1 / 2)) → 0 ∈ (0[,](1 / 2)))
229	226, 227, 142, 228	mp3an 1464	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ (0[,](1 / 2))
230		iccss2 13364	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ (0[,](1 / 2)) ∧ (1 / 4) ∈ (0[,](1 / 2))) → (0[,](1 / 4)) ⊆ (0[,](1 / 2)))
231	229, 219, 230	mp2an 693	. . . . . . . . . . . . . 14 ⊢ (0[,](1 / 4)) ⊆ (0[,](1 / 2))
232		iccssre 13376	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (0[,](1 / 2)) ⊆ ℝ)
233	14, 59, 232	mp2an 693	. . . . . . . . . . . . . 14 ⊢ (0[,](1 / 2)) ⊆ ℝ
234	231, 233	sstri 3932	. . . . . . . . . . . . 13 ⊢ (0[,](1 / 4)) ⊆ ℝ
235		resttopon 23139	. . . . . . . . . . . . 13 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 / 4)) ⊆ ℝ) → ((topGen‘ran (,)) ↾_t (0[,](1 / 4))) ∈ (TopOn‘(0[,](1 / 4))))
236	225, 234, 235	mp2an 693	. . . . . . . . . . . 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 23646	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 4)), 𝑧 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,)) ↾_t (0[,](1 / 4))) ×_t II) Cn ((topGen‘ran (,)) ↾_t (0[,](1 / 4)))))
239		retop 24739	. . . . . . . . . . . . . 14 ⊢ (topGen‘ran (,)) ∈ Top
240		ovex 7394	. . . . . . . . . . . . . 14 ⊢ (0[,](1 / 2)) ∈ V
241		restabs 23143	. . . . . . . . . . . . . 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 1464	. . . . . . . . . . . . 13 ⊢ (((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ↾_t (0[,](1 / 4))) = ((topGen‘ran (,)) ↾_t (0[,](1 / 4)))
243	242	eqcomi 2746	. . . . . . . . . . . 12 ⊢ ((topGen‘ran (,)) ↾_t (0[,](1 / 4))) = (((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ↾_t (0[,](1 / 4)))
244		resttopon 23139	. . . . . . . . . . . . . 14 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 / 2)) ⊆ ℝ) → ((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 / 2))))
245	225, 233, 244	mp2an 693	. . . . . . . . . . . . 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 24912	. . . . . . . . . . . . 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 23654	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (0[,](1 / 4)) ↦ (2 · 𝑥)) ∈ (((topGen‘ran (,)) ↾_t (0[,](1 / 4))) Cn II))
251		oveq2 7369	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
252	237, 188, 238, 237, 250, 251	cnmpt21 23649	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 4)), 𝑧 ∈ (0[,]1) ↦ (2 · 𝑦)) ∈ ((((topGen‘ran (,)) ↾_t (0[,](1 / 4))) ×_t II) Cn II))
253		iccssre 13376	. . . . . . . . . . . . . 14 ⊢ (((1 / 4) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → ((1 / 4)[,](1 / 2)) ⊆ ℝ)
254	17, 59, 253	mp2an 693	. . . . . . . . . . . . 13 ⊢ ((1 / 4)[,](1 / 2)) ⊆ ℝ
255		resttopon 23139	. . . . . . . . . . . . 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 693	. . . . . . . . . . . 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 23646	. . . . . . . . . . 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 2737	. . . . . . . . . . . 12 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
260	254	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1 / 4)[,](1 / 2)) ⊆ ℝ)
261		unitssre 13446	. . . . . . . . . . . . 13 ⊢ (0[,]1) ⊆ ℝ
262	261	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (0[,]1) ⊆ ℝ)
263	149, 87	sselid 3920	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ∈ (0[,]1))
264	263	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 4)[,](1 / 2))) → (𝑥 + (1 / 4)) ∈ (0[,]1))
265	259	cnfldtopon 24760	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
266	265	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ))
267	266	cnmptid 23639	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ 𝑥) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
268	17	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 / 4) ∈ ℝ)
269	268	recnd 11167	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 / 4) ∈ ℂ)
270	266, 266, 269	cnmptc 23640	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (1 / 4)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
271	259	addcn 24844	. . . . . . . . . . . . . 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 23644	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (𝑥 + (1 / 4))) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
274	259, 214, 196, 260, 262, 264, 273	cnmptre 24907	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ ((1 / 4)[,](1 / 2)) ↦ (𝑥 + (1 / 4))) ∈ (((topGen‘ran (,)) ↾_t ((1 / 4)[,](1 / 2))) Cn II))
275		oveq1 7368	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 + (1 / 4)) = (𝑦 + (1 / 4)))
276	257, 188, 258, 257, 274, 275	cnmpt21 23649	. . . . . . . . . 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 24908	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 2)), 𝑧 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4)))) ∈ ((((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ×_t II) Cn II))
278		iccssre 13376	. . . . . . . . . . . . 13 ⊢ (((1 / 2) ∈ ℝ ∧ 1 ∈ ℝ) → ((1 / 2)[,]1) ⊆ ℝ)
279	59, 85, 278	mp2an 693	. . . . . . . . . . . 12 ⊢ ((1 / 2)[,]1) ⊆ ℝ
280		resttopon 23139	. . . . . . . . . . . 12 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 / 2)[,]1) ⊆ ℝ) → ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1)))
281	225, 279, 280	mp2an 693	. . . . . . . . . . 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 23646	. . . . . . . . . 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 3920	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → ((𝑥 / 2) + (1 / 2)) ∈ (0[,]1))
286	285	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝑥 / 2) + (1 / 2)) ∈ (0[,]1))
287	259	divccn 24853	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℂ ∧ 2 ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
288	4, 24, 287	mp2an 693	. . . . . . . . . . . . 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 23640	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (1 / 2)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
292	266, 289, 291, 272	cnmpt12f 23644	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((𝑥 / 2) + (1 / 2))) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
293	259, 195, 196, 284, 262, 286, 292	cnmptre 24907	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ ((1 / 2)[,]1) ↦ ((𝑥 / 2) + (1 / 2))) ∈ (((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) Cn II))
294		oveq1 7368	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 / 2) = (𝑦 / 2))
295	294	oveq1d 7376	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 / 2) + (1 / 2)) = ((𝑦 / 2) + (1 / 2)))
296	282, 188, 283, 282, 293, 295	cnmpt21 23649	. . . . . . . . 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 24908	. . . . . . . 8 ⊢ (𝜑 → (𝑦 ∈ (0[,]1), 𝑧 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 2), if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))), ((𝑦 / 2) + (1 / 2)))) ∈ ((II ×_t II) Cn II))
298		breq1 5089	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑥 ≤ (1 / 2) ↔ 𝑦 ≤ (1 / 2)))
299		breq1 5089	. . . . . . . . . . . . 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 2022	. . . . . . . . . 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 480	. . . . . . . . 9 ⊢ ((𝑦 = 𝑥 ∧ 𝑧 = 0) → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑦 ≤ (1 / 2), if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))), ((𝑦 / 2) + (1 / 2))))
304	303	eqcomd 2743	. . . . . . . 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 23645	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) ∈ (II Cn II))
306	186, 305	eqeltrid 2841	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ (II Cn II))
307		iiuni 24861	. . . . . . 7 ⊢ (0[,]1) = ∪ II
308	307, 307	cnf 23224	. . . . . 6 ⊢ (𝑃 ∈ (II Cn II) → 𝑃:(0[,]1)⟶(0[,]1))
309	306, 308	syl 17	. . . . 5 ⊢ (𝜑 → 𝑃:(0[,]1)⟶(0[,]1))
310	186	fmpt 7057	. . . . 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 234	. . . 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 24997	. . . . . 6 ⊢ (𝜑 → (𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) ∈ (II Cn 𝐽))
314		eqid 2737	. . . . . . 7 ⊢ ∪ 𝐽 = ∪ 𝐽
315	307, 314	cnf 23224	. . . . . 6 ⊢ ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) ∈ (II Cn 𝐽) → (𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)):(0[,]1)⟶∪ 𝐽)
316	313, 315	syl 17	. . . . 5 ⊢ (𝜑 → (𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)):(0[,]1)⟶∪ 𝐽)
317	316	feqmptd 6903	. . . 4 ⊢ (𝜑 → (𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) = (𝑦 ∈ (0[,]1) ↦ ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘𝑦)))
318		fveq2 6835	. . . 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 7078	. . 3 ⊢ (𝜑 → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) ∘ 𝑃) = (𝑥 ∈ (0[,]1) ↦ ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))))))
320	40, 41, 89	pcocn 24997	. . . 4 ⊢ (𝜑 → (𝐹(*_𝑝‘𝐽)𝐺) ∈ (II Cn 𝐽))
321	320, 42	pcoval 24991	. . 3 ⊢ (𝜑 → ((𝐹(_𝑝‘𝐽)𝐺)(_𝑝‘𝐽)𝐻) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1)))))
322	185, 319, 321	3eqtr4rd 2783	. 2 ⊢ (𝜑 → ((𝐹(_𝑝‘𝐽)𝐺)(_𝑝‘𝐽)𝐻) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) ∘ 𝑃))
323		id 22	. . . . . . . 8 ⊢ (𝑥 = 0 → 𝑥 = 0)
324	323, 142	eqbrtrdi 5125	. . . . . . 7 ⊢ (𝑥 = 0 → 𝑥 ≤ (1 / 2))
325	324	iftrued 4475	. . . . . 6 ⊢ (𝑥 = 0 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))))
326	323, 217	eqbrtrdi 5125	. . . . . . 7 ⊢ (𝑥 = 0 → 𝑥 ≤ (1 / 4))
327	326	iftrued 4475	. . . . . 6 ⊢ (𝑥 = 0 → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (2 · 𝑥))
328		oveq2 7369	. . . . . . 7 ⊢ (𝑥 = 0 → (2 · 𝑥) = (2 · 0))
329		2t0e0 12339	. . . . . . 7 ⊢ (2 · 0) = 0
330	328, 329	eqtrdi 2788	. . . . . 6 ⊢ (𝑥 = 0 → (2 · 𝑥) = 0)
331	325, 327, 330	3eqtrd 2776	. . . . 5 ⊢ (𝑥 = 0 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = 0)
332		c0ex 11132	. . . . 5 ⊢ 0 ∈ V
333	331, 186, 332	fvmpt 6942	. . . 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 11261	. . . . . . . . 9 ⊢ ((1 / 2) < 1 ↔ ¬ 1 ≤ (1 / 2))
337	143, 336	mpbi 230	. . . . . . . 8 ⊢ ¬ 1 ≤ (1 / 2)
338		breq1 5089	. . . . . . . 8 ⊢ (𝑥 = 1 → (𝑥 ≤ (1 / 2) ↔ 1 ≤ (1 / 2)))
339	337, 338	mtbiri 327	. . . . . . 7 ⊢ (𝑥 = 1 → ¬ 𝑥 ≤ (1 / 2))
340	339	iffalsed 4478	. . . . . 6 ⊢ (𝑥 = 1 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = ((𝑥 / 2) + (1 / 2)))
341		oveq1 7368	. . . . . . . 8 ⊢ (𝑥 = 1 → (𝑥 / 2) = (1 / 2))
342	341	oveq1d 7376	. . . . . . 7 ⊢ (𝑥 = 1 → ((𝑥 / 2) + (1 / 2)) = ((1 / 2) + (1 / 2)))
343	342, 83	eqtrdi 2788	. . . . . 6 ⊢ (𝑥 = 1 → ((𝑥 / 2) + (1 / 2)) = 1)
344	340, 343	eqtrd 2772	. . . . 5 ⊢ (𝑥 = 1 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = 1)
345		1ex 11134	. . . . 5 ⊢ 1 ∈ V
346	344, 186, 345	fvmpt 6942	. . . 4 ⊢ (1 ∈ (0[,]1) → (𝑃‘1) = 1)
347	335, 346	syl 17	. . 3 ⊢ (𝜑 → (𝑃‘1) = 1)
348	313, 306, 334, 347	reparpht 24978	. 2 ⊢ (𝜑 → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) ∘ 𝑃)( ≃_ph‘𝐽)(𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)))
349	322, 348	eqbrtrd 5108	1 ⊢ (𝜑 → ((𝐹(_𝑝‘𝐽)𝐺)(_𝑝‘𝐽)𝐻)( ≃_ph‘𝐽)(𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∨ wo 848 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 Vcvv 3430 ⊆ wss 3890 ifcif 4467 ∪ cuni 4851 class class class wbr 5086 ↦ cmpt 5167 ran crn 5626 ∘ ccom 5629 ⟶wf 6489 ‘cfv 6493 (class class class)co 7361 ℂcc 11030 ℝcr 11031 0cc0 11032 1c1 11033 + caddc 11035 · cmul 11037 ℝ^*cxr 11172 < clt 11173 ≤ cle 11174 − cmin 11371 / cdiv 11801 ℕcn 12168 2c2 12230 4c4 12232 (,)cioo 13292 [,]cicc 13295 ↾_t crest 17377 TopOpenctopn 17378 topGenctg 17394 ℂ_fldccnfld 21347 Topctop 22871 TopOnctopon 22888 Cn ccn 23202 ×_t ctx 23538 IIcii 24855 ≃_phcphtpc 24949 *_𝑝cpco 24980

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5303 ax-pr 5371 ax-un 7683 ax-cnex 11088 ax-resscn 11089 ax-1cn 11090 ax-icn 11091 ax-addcl 11092 ax-addrcl 11093 ax-mulcl 11094 ax-mulrcl 11095 ax-mulcom 11096 ax-addass 11097 ax-mulass 11098 ax-distr 11099 ax-i2m1 11100 ax-1ne0 11101 ax-1rid 11102 ax-rnegex 11103 ax-rrecex 11104 ax-cnre 11105 ax-pre-lttri 11106 ax-pre-lttrn 11107 ax-pre-ltadd 11108 ax-pre-mulgt0 11109 ax-pre-sup 11110 ax-addf 11111

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-se 5579 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6260 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-isom 6502 df-riota 7318 df-ov 7364 df-oprab 7365 df-mpo 7366 df-of 7625 df-om 7812 df-1st 7936 df-2nd 7937 df-supp 8105 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-1o 8399 df-2o 8400 df-er 8637 df-map 8769 df-ixp 8840 df-en 8888 df-dom 8889 df-sdom 8890 df-fin 8891 df-fsupp 9269 df-fi 9318 df-sup 9349 df-inf 9350 df-oi 9419 df-card 9857 df-pnf 11175 df-mnf 11176 df-xr 11177 df-ltxr 11178 df-le 11179 df-sub 11373 df-neg 11374 df-div 11802 df-nn 12169 df-2 12238 df-3 12239 df-4 12240 df-5 12241 df-6 12242 df-7 12243 df-8 12244 df-9 12245 df-n0 12432 df-z 12519 df-dec 12639 df-uz 12783 df-q 12893 df-rp 12937 df-xneg 13057 df-xadd 13058 df-xmul 13059 df-ioo 13296 df-icc 13299 df-fz 13456 df-fzo 13603 df-seq 13958 df-exp 14018 df-hash 14287 df-cj 15055 df-re 15056 df-im 15057 df-sqrt 15191 df-abs 15192 df-struct 17111 df-sets 17128 df-slot 17146 df-ndx 17158 df-base 17174 df-ress 17195 df-plusg 17227 df-mulr 17228 df-starv 17229 df-sca 17230 df-vsca 17231 df-ip 17232 df-tset 17233 df-ple 17234 df-ds 17236 df-unif 17237 df-hom 17238 df-cco 17239 df-rest 17379 df-topn 17380 df-0g 17398 df-gsum 17399 df-topgen 17400 df-pt 17401 df-prds 17404 df-xrs 17460 df-qtop 17465 df-imas 17466 df-xps 17468 df-mre 17542 df-mrc 17543 df-acs 17545 df-mgm 18602 df-sgrp 18681 df-mnd 18697 df-submnd 18746 df-mulg 19038 df-cntz 19286 df-cmn 19751 df-psmet 21339 df-xmet 21340 df-met 21341 df-bl 21342 df-mopn 21343 df-cnfld 21348 df-top 22872 df-topon 22889 df-topsp 22911 df-bases 22924 df-cld 22997 df-cn 23205 df-cnp 23206 df-tx 23540 df-hmeo 23733 df-xms 24298 df-ms 24299 df-tms 24300 df-ii 24857 df-htpy 24950 df-phtpy 24951 df-phtpc 24972 df-pco 24985

This theorem is referenced by: pcophtb 25009 pi1grplem 25029 pi1xfr 25035 pi1xfrcnvlem 25036

W3C validator