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 23875

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 4431	. . . . . . . . . . 11 ⊢ (𝑥 ≤ (1 / 4) → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (2 · 𝑥))
2	1	fveq2d 6699	. . . . . . . . . 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 11870	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℂ
5		elicc01 13019	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (0[,]1) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1))
6	5	simp1bi 1147	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0[,]1) → 𝑥 ∈ ℝ)
7	6	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℝ)
8	7	recnd 10826	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℂ)
9		mulcom 10780	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) = (𝑥 · 2))
10	4, 8, 9	sylancr 590	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) = (𝑥 · 2))
11	5	simp2bi 1148	. . . . . . . . . . . . . . 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 10800	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℝ
15		4nn 11878	. . . . . . . . . . . . . . . 16 ⊢ 4 ∈ ℕ
16		nnrecre 11837	. . . . . . . . . . . . . . . 16 ⊢ (4 ∈ ℕ → (1 / 4) ∈ ℝ)
17	15, 16	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (1 / 4) ∈ ℝ
18	14, 17	elicc2i 12966	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (0[,](1 / 4)) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ (1 / 4)))
19	7, 12, 13, 18	syl3anbrc 1345	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ (0[,](1 / 4)))
20		2rp 12556	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℝ⁺
21	4	mul02i 10986	. . . . . . . . . . . . . 14 ⊢ (0 · 2) = 0
22	17	recni 10812	. . . . . . . . . . . . . . 15 ⊢ (1 / 4) ∈ ℂ
23	22	2timesi 11933	. . . . . . . . . . . . . . . 16 ⊢ (2 · (1 / 4)) = ((1 / 4) + (1 / 4))
24		2ne0 11899	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ≠ 0
25		recdiv2 11510	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((1 / 2) / 2) = (1 / (2 · 2)))
26	4, 24, 4, 24, 25	mp4an 693	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 / 2) / 2) = (1 / (2 · 2))
27		2t2e4 11959	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2 · 2) = 4
28	27	oveq2i 7202	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 / (2 · 2)) = (1 / 4)
29	26, 28	eqtri 2759	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 / 2) / 2) = (1 / 4)
30	29, 29	oveq12i 7203	. . . . . . . . . . . . . . . . 17 ⊢ (((1 / 2) / 2) + ((1 / 2) / 2)) = ((1 / 4) + (1 / 4))
31		halfcn 12010	. . . . . . . . . . . . . . . . . 18 ⊢ (1 / 2) ∈ ℂ
32		2halves 12023	. . . . . . . . . . . . . . . . . 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 2761	. . . . . . . . . . . . . . . 16 ⊢ ((1 / 4) + (1 / 4)) = (1 / 2)
35	23, 34	eqtri 2759	. . . . . . . . . . . . . . 15 ⊢ (2 · (1 / 4)) = (1 / 2)
36	4, 22, 35	mulcomli 10807	. . . . . . . . . . . . . 14 ⊢ ((1 / 4) · 2) = (1 / 2)
37	14, 17, 20, 21, 36	iccdili 13044	. . . . . . . . . . . . 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 2831	. . . . . . . . . . 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 23868	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺(*_𝑝‘𝐽)𝐻) ∈ (II Cn 𝐽))
45	40, 44	pcoval1 23864	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(2 · 𝑥)) = (𝐹‘(2 · (2 · 𝑥))))
46	40, 41	pcoval1 23864	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) → ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)) = (𝐹‘(2 · (2 · 𝑥))))
47	45, 46	eqtr4d 2774	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (2 · 𝑥) ∈ (0[,](1 / 2))) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
48	39, 47	sylan2 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 4))) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
49	48	anassrs 471	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(2 · 𝑥)) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
50	3, 49	eqtrd 2771	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4)))) = ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)))
51	50	adantlr 715	. . . . . . 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 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → 𝑥 ∈ ℝ)
54	53	adantr 484	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ∈ ℝ)
55		letric 10897	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ ∧ (1 / 4) ∈ ℝ) → (𝑥 ≤ (1 / 4) ∨ (1 / 4) ≤ 𝑥))
56	53, 17, 55	sylancl 589	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) → (𝑥 ≤ (1 / 4) ∨ (1 / 4) ≤ 𝑥))
57	56	orcanai 1003	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (1 / 4) ≤ 𝑥)
58		simplr 769	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 𝑥 ≤ (1 / 2))
59		halfre 12009	. . . . . . . . . . . . 13 ⊢ (1 / 2) ∈ ℝ
60	17, 59	elicc2i 12966	. . . . . . . . . . . 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 1147	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → 𝑥 ∈ ℝ)
63		readdcl 10777	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ ∧ (1 / 4) ∈ ℝ) → (𝑥 + (1 / 4)) ∈ ℝ)
64	62, 17, 63	sylancl 589	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ∈ ℝ)
65	17	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 4) ∈ ℝ)
66	60	simp2bi 1148	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 4) ≤ 𝑥)
67	65, 62, 65, 66	leadd1dd 11411	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → ((1 / 4) + (1 / 4)) ≤ (𝑥 + (1 / 4)))
68	34, 67	eqbrtrrid 5075	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 2) ≤ (𝑥 + (1 / 4)))
69	59	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (1 / 2) ∈ ℝ)
70	60	simp3bi 1149	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → 𝑥 ≤ (1 / 2))
71		2lt4 11970	. . . . . . . . . . . . . . . . 17 ⊢ 2 < 4
72		2re 11869	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ
73		4re 11879	. . . . . . . . . . . . . . . . . 18 ⊢ 4 ∈ ℝ
74		2pos 11898	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 2
75		4pos 11902	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 4
76	72, 73, 74, 75	ltrecii 11713	. . . . . . . . . . . . . . . . 17 ⊢ (2 < 4 ↔ (1 / 4) < (1 / 2))
77	71, 76	mpbi 233	. . . . . . . . . . . . . . . 16 ⊢ (1 / 4) < (1 / 2)
78	17, 59, 77	ltleii 10920	. . . . . . . . . . . . . . 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 11416	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ≤ ((1 / 2) + (1 / 2)))
81		ax-1cn 10752	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
82		2halves 12023	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℂ → ((1 / 2) + (1 / 2)) = 1)
83	81, 82	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((1 / 2) + (1 / 2)) = 1
84	80, 83	breqtrdi 5080	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 4)[,](1 / 2)) → (𝑥 + (1 / 4)) ≤ 1)
85		1re 10798	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ
86	59, 85	elicc2i 12966	. . . . . . . . . . . 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 23865	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐺(*_𝑝‘𝐽)𝐻)‘0) = (𝐺‘0))
91	89, 90	eqtr4d 2774	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹‘1) = ((𝐺(*_𝑝‘𝐽)𝐻)‘0))
92	40, 44, 91	pcoval2 23867	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 + (1 / 4)) ∈ ((1 / 2)[,]1)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))) = ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)))
93	52, 88, 92	syl2anc 587	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))) = ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)))
94	83	oveq2i 7202	. . . . . . . . . . . 12 ⊢ ((2 · (𝑥 + (1 / 4))) − ((1 / 2) + (1 / 2))) = ((2 · (𝑥 + (1 / 4))) − 1)
95		2cnd 11873	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → 2 ∈ ℂ)
96	54	recnd 10826	. . . . . . . . . . . . . . 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 10822	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · (𝑥 + (1 / 4))) = ((2 · 𝑥) + (2 · (1 / 4))))
99	35	oveq2i 7202	. . . . . . . . . . . . . 14 ⊢ ((2 · 𝑥) + (2 · (1 / 4))) = ((2 · 𝑥) + (1 / 2))
100	98, 99	eqtrdi 2787	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · (𝑥 + (1 / 4))) = ((2 · 𝑥) + (1 / 2)))
101	100	oveq1d 7206	. . . . . . . . . . . 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 2785	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − 1) = (((2 · 𝑥) + (1 / 2)) − ((1 / 2) + (1 / 2))))
103		remulcl 10779	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (2 · 𝑥) ∈ ℝ)
104	72, 54, 103	sylancr 590	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈ ℝ)
105	104	recnd 10826	. . . . . . . . . . . 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 11192	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (((2 · 𝑥) + (1 / 2)) − ((1 / 2) + (1 / 2))) = ((2 · 𝑥) − (1 / 2)))
108	102, 107	eqtrd 2771	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((2 · (𝑥 + (1 / 4))) − 1) = ((2 · 𝑥) − (1 / 2)))
109	108	fveq2d 6699	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(_𝑝‘𝐽)𝐻)‘((2 · (𝑥 + (1 / 4))) − 1)) = ((𝐺(_𝑝‘𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))))
110	4, 96, 9	sylancr 590	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) = (𝑥 · 2))
111	81, 4, 24	divcan1i 11541	. . . . . . . . . . . . . . 15 ⊢ ((1 / 2) · 2) = 1
112	17, 59, 20, 36, 111	iccdili 13044	. . . . . . . . . . . . . 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 2831	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · 𝑥) ∈ ((1 / 2)[,]1))
115	31	subidi 11114	. . . . . . . . . . . . 13 ⊢ ((1 / 2) − (1 / 2)) = 0
116		1mhlfehlf 12014	. . . . . . . . . . . . 13 ⊢ (1 − (1 / 2)) = (1 / 2)
117	59, 85, 59, 115, 116	iccshftli 13042	. . . . . . . . . . . 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 23864	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((2 · 𝑥) − (1 / 2)) ∈ (0[,](1 / 2))) → ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))))
120	52, 118, 119	syl2anc 587	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))))
121	95, 105, 106	subdid 11253	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · ((2 · 𝑥) − (1 / 2))) = ((2 · (2 · 𝑥)) − (2 · (1 / 2))))
122	4, 24	recidi 11528	. . . . . . . . . . . . 13 ⊢ (2 · (1 / 2)) = 1
123	122	oveq2i 7202	. . . . . . . . . . . 12 ⊢ ((2 · (2 · 𝑥)) − (2 · (1 / 2))) = ((2 · (2 · 𝑥)) − 1)
124	121, 123	eqtrdi 2787	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (2 · ((2 · 𝑥) − (1 / 2))) = ((2 · (2 · 𝑥)) − 1))
125	124	fveq2d 6699	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → (𝐺‘(2 · ((2 · 𝑥) − (1 / 2)))) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
126	120, 125	eqtrd 2771	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · 𝑥) − (1 / 2))) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
127	93, 109, 126	3eqtrd 2775	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘(𝑥 + (1 / 4))) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
128		iffalse 4434	. . . . . . . . . 10 ⊢ (¬ 𝑥 ≤ (1 / 4) → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (𝑥 + (1 / 4)))
129	128	fveq2d 6699	. . . . . . . . 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 23867	. . . . . . . . 9 ⊢ ((𝜑 ∧ (2 · 𝑥) ∈ ((1 / 2)[,]1)) → ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
132	52, 114, 131	syl2anc 587	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ 𝑥 ≤ (1 / 2)) ∧ ¬ 𝑥 ≤ (1 / 4)) → ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)) = (𝐺‘((2 · (2 · 𝑥)) − 1)))
133	127, 130, 132	3eqtr4d 2781	. . . . . . 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 4431	. . . . . . . 8 ⊢ (𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))))
136	135	fveq2d 6699	. . . . . . 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 4431	. . . . . . 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 2781	. . . . 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 23787	. . . . . . . 8 ⊢ ((𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 ≤ (1 / 2)) → 𝑥 ∈ ((1 / 2)[,]1))
142		halfge0 12012	. . . . . . . . . . . . . 14 ⊢ 0 ≤ (1 / 2)
143		halflt1 12013	. . . . . . . . . . . . . . 15 ⊢ (1 / 2) < 1
144	59, 85, 143	ltleii 10920	. . . . . . . . . . . . . 14 ⊢ (1 / 2) ≤ 1
145		elicc01 13019	. . . . . . . . . . . . . 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 13023	. . . . . . . . . . . . 13 ⊢ 1 ∈ (0[,]1)
148		iccss2 12971	. . . . . . . . . . . . 13 ⊢ (((1 / 2) ∈ (0[,]1) ∧ 1 ∈ (0[,]1)) → ((1 / 2)[,]1) ⊆ (0[,]1))
149	146, 147, 148	mp2an 692	. . . . . . . . . . . 12 ⊢ ((1 / 2)[,]1) ⊆ (0[,]1)
150	149	sseli 3883	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 𝑥 ∈ (0[,]1))
151	4, 24	div0i 11531	. . . . . . . . . . . 12 ⊢ (0 / 2) = 0
152		eqid 2736	. . . . . . . . . . . 12 ⊢ (1 / 2) = (1 / 2)
153	14, 85, 20, 151, 152	icccntri 13046	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (0[,]1) → (𝑥 / 2) ∈ (0[,](1 / 2)))
154	31	addid2i 10985	. . . . . . . . . . . 12 ⊢ (0 + (1 / 2)) = (1 / 2)
155	14, 59, 59, 154, 83	iccshftri 13040	. . . . . . . . . . 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 23867	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 / 2) + (1 / 2)) ∈ ((1 / 2)[,]1)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)))
158	156, 157	sylan2 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = ((𝐺(*_𝑝‘𝐽)𝐻)‘((2 · ((𝑥 / 2) + (1 / 2))) − 1)))
159	59, 85	elicc2i 12966	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 2)[,]1) ↔ (𝑥 ∈ ℝ ∧ (1 / 2) ≤ 𝑥 ∧ 𝑥 ≤ 1))
160	159	simp1bi 1147	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 𝑥 ∈ ℝ)
161	160	recnd 10826	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 𝑥 ∈ ℂ)
162		1cnd 10793	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 1 ∈ ℂ)
163		2cnd 11873	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 2 ∈ ℂ)
164	24	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → 2 ≠ 0)
165	161, 162, 163, 164	divdird 11611	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → ((𝑥 + 1) / 2) = ((𝑥 / 2) + (1 / 2)))
166	165	oveq2d 7207	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → (2 · ((𝑥 + 1) / 2)) = (2 · ((𝑥 / 2) + (1 / 2))))
167		peano2cn 10969	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ → (𝑥 + 1) ∈ ℂ)
168	161, 167	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → (𝑥 + 1) ∈ ℂ)
169	168, 163, 164	divcan2d 11575	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → (2 · ((𝑥 + 1) / 2)) = (𝑥 + 1))
170	166, 169	eqtr3d 2773	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → (2 · ((𝑥 / 2) + (1 / 2))) = (𝑥 + 1))
171	161, 162, 170	mvrraddd 11209	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ((1 / 2)[,]1) → ((2 · ((𝑥 / 2) + (1 / 2))) − 1) = 𝑥)
172	171	fveq2d 6699	. . . . . . . . . 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 23867	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝐺(*_𝑝‘𝐽)𝐻)‘𝑥) = (𝐻‘((2 · 𝑥) − 1)))
175	158, 173, 174	3eqtrd 2775	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((1 / 2)[,]1)) → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘((𝑥 / 2) + (1 / 2))) = (𝐻‘((2 · 𝑥) − 1)))
176	141, 175	sylan2 596	. . . . . . 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 4434	. . . . . . . 8 ⊢ (¬ 𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = ((𝑥 / 2) + (1 / 2)))
179	178	fveq2d 6699	. . . . . . 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 4434	. . . . . . 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 2781	. . . . 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 5135	. . 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 23730	. . . . . . . . 9 ⊢ II ∈ (TopOn‘(0[,]1))
188	187	a1i 11	. . . . . . . 8 ⊢ (𝜑 → II ∈ (TopOn‘(0[,]1)))
189	188	cnmptid 22512	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ 𝑥) ∈ (II Cn II))
190		0elunit 13022	. . . . . . . . . 10 ⊢ 0 ∈ (0[,]1)
191	190	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0[,]1))
192	188, 188, 191	cnmptc 22513	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ 0) ∈ (II Cn II))
193		eqid 2736	. . . . . . . . 9 ⊢ (topGen‘ran (,)) = (topGen‘ran (,))
194		eqid 2736	. . . . . . . . 9 ⊢ ((topGen‘ran (,)) ↾_t (0[,](1 / 2))) = ((topGen‘ran (,)) ↾_t (0[,](1 / 2)))
195		eqid 2736	. . . . . . . . 9 ⊢ ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) = ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1))
196		dfii2 23733	. . . . . . . . 9 ⊢ II = ((topGen‘ran (,)) ↾_t (0[,]1))
197		0red 10801	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ ℝ)
198		1red 10799	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℝ)
199	146	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (1 / 2) ∈ (0[,]1))
200		simprl 771	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → 𝑦 = (1 / 2))
201	200	oveq1d 7206	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 2) + (1 / 4)))
202	31, 22	addcomi 10988	. . . . . . . . . . 11 ⊢ ((1 / 2) + (1 / 4)) = ((1 / 4) + (1 / 2))
203	201, 202	eqtrdi 2787	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 4) + (1 / 2)))
204	17, 59	ltnlei 10918	. . . . . . . . . . . . 13 ⊢ ((1 / 4) < (1 / 2) ↔ ¬ (1 / 2) ≤ (1 / 4))
205	77, 204	mpbi 233	. . . . . . . . . . . 12 ⊢ ¬ (1 / 2) ≤ (1 / 4)
206	200	breq1d 5049	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 ≤ (1 / 4) ↔ (1 / 2) ≤ (1 / 4)))
207	205, 206	mtbiri 330	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → ¬ 𝑦 ≤ (1 / 4))
208	207	iffalsed 4436	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))) = (𝑦 + (1 / 4)))
209	200	oveq1d 7206	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 / 2) = ((1 / 2) / 2))
210	209, 29	eqtrdi 2787	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 / 2) = (1 / 4))
211	210	oveq1d 7206	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → ((𝑦 / 2) + (1 / 2)) = ((1 / 4) + (1 / 2)))
212	203, 208, 211	3eqtr4d 2781	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))) = ((𝑦 / 2) + (1 / 2)))
213		eqid 2736	. . . . . . . . . 10 ⊢ ((topGen‘ran (,)) ↾_t (0[,](1 / 4))) = ((topGen‘ran (,)) ↾_t (0[,](1 / 4)))
214		eqid 2736	. . . . . . . . . 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 11703	. . . . . . . . . . . . 13 ⊢ 0 < (1 / 4)
217	14, 17, 216	ltleii 10920	. . . . . . . . . . . 12 ⊢ 0 ≤ (1 / 4)
218	14, 59	elicc2i 12966	. . . . . . . . . . . 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 7207	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = (2 · (1 / 4)))
223	221	oveq1d 7206	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (𝑦 + (1 / 4)) = ((1 / 4) + (1 / 4)))
224	23, 222, 223	3eqtr4a 2797	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 = (1 / 4) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = (𝑦 + (1 / 4)))
225		retopon 23615	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ)
226		0xr 10845	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ^*
227	59	rexri 10856	. . . . . . . . . . . . . . . 16 ⊢ (1 / 2) ∈ ℝ^*
228		lbicc2 13017	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℝ^* ∧ (1 / 2) ∈ ℝ^* ∧ 0 ≤ (1 / 2)) → 0 ∈ (0[,](1 / 2)))
229	226, 227, 142, 228	mp3an 1463	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ (0[,](1 / 2))
230		iccss2 12971	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ (0[,](1 / 2)) ∧ (1 / 4) ∈ (0[,](1 / 2))) → (0[,](1 / 4)) ⊆ (0[,](1 / 2)))
231	229, 219, 230	mp2an 692	. . . . . . . . . . . . . 14 ⊢ (0[,](1 / 4)) ⊆ (0[,](1 / 2))
232		iccssre 12982	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (0[,](1 / 2)) ⊆ ℝ)
233	14, 59, 232	mp2an 692	. . . . . . . . . . . . . 14 ⊢ (0[,](1 / 2)) ⊆ ℝ
234	231, 233	sstri 3896	. . . . . . . . . . . . 13 ⊢ (0[,](1 / 4)) ⊆ ℝ
235		resttopon 22012	. . . . . . . . . . . . 13 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 / 4)) ⊆ ℝ) → ((topGen‘ran (,)) ↾_t (0[,](1 / 4))) ∈ (TopOn‘(0[,](1 / 4))))
236	225, 234, 235	mp2an 692	. . . . . . . . . . . 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 22519	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 4)), 𝑧 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,)) ↾_t (0[,](1 / 4))) ×_t II) Cn ((topGen‘ran (,)) ↾_t (0[,](1 / 4)))))
239		retop 23613	. . . . . . . . . . . . . 14 ⊢ (topGen‘ran (,)) ∈ Top
240		ovex 7224	. . . . . . . . . . . . . 14 ⊢ (0[,](1 / 2)) ∈ V
241		restabs 22016	. . . . . . . . . . . . . 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 1463	. . . . . . . . . . . . 13 ⊢ (((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ↾_t (0[,](1 / 4))) = ((topGen‘ran (,)) ↾_t (0[,](1 / 4)))
243	242	eqcomi 2745	. . . . . . . . . . . 12 ⊢ ((topGen‘ran (,)) ↾_t (0[,](1 / 4))) = (((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ↾_t (0[,](1 / 4)))
244		resttopon 22012	. . . . . . . . . . . . . 14 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 / 2)) ⊆ ℝ) → ((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 / 2))))
245	225, 233, 244	mp2an 692	. . . . . . . . . . . . 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 23783	. . . . . . . . . . . . 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 22527	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (0[,](1 / 4)) ↦ (2 · 𝑥)) ∈ (((topGen‘ran (,)) ↾_t (0[,](1 / 4))) Cn II))
251		oveq2 7199	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
252	237, 188, 238, 237, 250, 251	cnmpt21 22522	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 4)), 𝑧 ∈ (0[,]1) ↦ (2 · 𝑦)) ∈ ((((topGen‘ran (,)) ↾_t (0[,](1 / 4))) ×_t II) Cn II))
253		iccssre 12982	. . . . . . . . . . . . . 14 ⊢ (((1 / 4) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → ((1 / 4)[,](1 / 2)) ⊆ ℝ)
254	17, 59, 253	mp2an 692	. . . . . . . . . . . . 13 ⊢ ((1 / 4)[,](1 / 2)) ⊆ ℝ
255		resttopon 22012	. . . . . . . . . . . . 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 692	. . . . . . . . . . . 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 22519	. . . . . . . . . . 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 2736	. . . . . . . . . . . 12 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
260	254	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1 / 4)[,](1 / 2)) ⊆ ℝ)
261		unitssre 13052	. . . . . . . . . . . . 13 ⊢ (0[,]1) ⊆ ℝ
262	261	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (0[,]1) ⊆ ℝ)
263	149, 87	sseldi 3885	. . . . . . . . . . . . 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 23634	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
266	265	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ))
267	266	cnmptid 22512	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ 𝑥) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
268	17	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 / 4) ∈ ℝ)
269	268	recnd 10826	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 / 4) ∈ ℂ)
270	266, 266, 269	cnmptc 22513	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (1 / 4)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
271	259	addcn 23716	. . . . . . . . . . . . . 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 22517	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (𝑥 + (1 / 4))) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
274	259, 214, 196, 260, 262, 264, 273	cnmptre 23778	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ ((1 / 4)[,](1 / 2)) ↦ (𝑥 + (1 / 4))) ∈ (((topGen‘ran (,)) ↾_t ((1 / 4)[,](1 / 2))) Cn II))
275		oveq1 7198	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 + (1 / 4)) = (𝑦 + (1 / 4)))
276	257, 188, 258, 257, 274, 275	cnmpt21 22522	. . . . . . . . . 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 23779	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 2)), 𝑧 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4)))) ∈ ((((topGen‘ran (,)) ↾_t (0[,](1 / 2))) ×_t II) Cn II))
278		iccssre 12982	. . . . . . . . . . . . 13 ⊢ (((1 / 2) ∈ ℝ ∧ 1 ∈ ℝ) → ((1 / 2)[,]1) ⊆ ℝ)
279	59, 85, 278	mp2an 692	. . . . . . . . . . . 12 ⊢ ((1 / 2)[,]1) ⊆ ℝ
280		resttopon 22012	. . . . . . . . . . . 12 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 / 2)[,]1) ⊆ ℝ) → ((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1)))
281	225, 279, 280	mp2an 692	. . . . . . . . . . 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 22519	. . . . . . . . . 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 3885	. . . . . . . . . . . 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 23724	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℂ ∧ 2 ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
288	4, 24, 287	mp2an 692	. . . . . . . . . . . . 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 22513	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ (1 / 2)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
292	266, 289, 291, 272	cnmpt12f 22517	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((𝑥 / 2) + (1 / 2))) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
293	259, 195, 196, 284, 262, 286, 292	cnmptre 23778	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ ((1 / 2)[,]1) ↦ ((𝑥 / 2) + (1 / 2))) ∈ (((topGen‘ran (,)) ↾_t ((1 / 2)[,]1)) Cn II))
294		oveq1 7198	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 / 2) = (𝑦 / 2))
295	294	oveq1d 7206	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 / 2) + (1 / 2)) = ((𝑦 / 2) + (1 / 2)))
296	282, 188, 283, 282, 293, 295	cnmpt21 22522	. . . . . . . . 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 23779	. . . . . . . 8 ⊢ (𝜑 → (𝑦 ∈ (0[,]1), 𝑧 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 2), if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))), ((𝑦 / 2) + (1 / 2)))) ∈ ((II ×_t II) Cn II))
298		breq1 5042	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑥 ≤ (1 / 2) ↔ 𝑦 ≤ (1 / 2)))
299		breq1 5042	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝑥 ≤ (1 / 4) ↔ 𝑦 ≤ (1 / 4)))
300	299, 251, 275	ifbieq12d 4453	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = if(𝑦 ≤ (1 / 4), (2 · 𝑦), (𝑦 + (1 / 4))))
301	298, 300, 295	ifbieq12d 4453	. . . . . . . . . . 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 2030	. . . . . . . . . 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 2742	. . . . . . . 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 22518	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) ∈ (II Cn II))
306	186, 305	eqeltrid 2835	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ (II Cn II))
307		iiuni 23732	. . . . . . 7 ⊢ (0[,]1) = ∪ II
308	307, 307	cnf 22097	. . . . . 6 ⊢ (𝑃 ∈ (II Cn II) → 𝑃:(0[,]1)⟶(0[,]1))
309	306, 308	syl 17	. . . . 5 ⊢ (𝜑 → 𝑃:(0[,]1)⟶(0[,]1))
310	186	fmpt 6905	. . . . 5 ⊢ (∀𝑥 ∈ (0[,]1)if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) ∈ (0[,]1) ↔ 𝑃:(0[,]1)⟶(0[,]1))
311	309, 310	sylibr 237	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ (0[,]1)if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) ∈ (0[,]1))
312	186	a1i 11	. . . 4 ⊢ (𝜑 → 𝑃 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))))
313	40, 44, 91	pcocn 23868	. . . . . 6 ⊢ (𝜑 → (𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) ∈ (II Cn 𝐽))
314		eqid 2736	. . . . . . 7 ⊢ ∪ 𝐽 = ∪ 𝐽
315	307, 314	cnf 22097	. . . . . 6 ⊢ ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) ∈ (II Cn 𝐽) → (𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)):(0[,]1)⟶∪ 𝐽)
316	313, 315	syl 17	. . . . 5 ⊢ (𝜑 → (𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)):(0[,]1)⟶∪ 𝐽)
317	316	feqmptd 6758	. . . 4 ⊢ (𝜑 → (𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) = (𝑦 ∈ (0[,]1) ↦ ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘𝑦)))
318		fveq2 6695	. . . 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 6923	. . 3 ⊢ (𝜑 → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) ∘ 𝑃) = (𝑥 ∈ (0[,]1) ↦ ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻))‘if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))))))
320	40, 41, 89	pcocn 23868	. . . 4 ⊢ (𝜑 → (𝐹(*_𝑝‘𝐽)𝐺) ∈ (II Cn 𝐽))
321	320, 42	pcoval 23862	. . 3 ⊢ (𝜑 → ((𝐹(_𝑝‘𝐽)𝐺)(_𝑝‘𝐽)𝐻) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), ((𝐹(*_𝑝‘𝐽)𝐺)‘(2 · 𝑥)), (𝐻‘((2 · 𝑥) − 1)))))
322	185, 319, 321	3eqtr4rd 2782	. 2 ⊢ (𝜑 → ((𝐹(_𝑝‘𝐽)𝐺)(_𝑝‘𝐽)𝐻) = ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) ∘ 𝑃))
323		id 22	. . . . . . . 8 ⊢ (𝑥 = 0 → 𝑥 = 0)
324	323, 142	eqbrtrdi 5078	. . . . . . 7 ⊢ (𝑥 = 0 → 𝑥 ≤ (1 / 2))
325	324	iftrued 4433	. . . . . 6 ⊢ (𝑥 = 0 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))))
326	323, 217	eqbrtrdi 5078	. . . . . . 7 ⊢ (𝑥 = 0 → 𝑥 ≤ (1 / 4))
327	326	iftrued 4433	. . . . . 6 ⊢ (𝑥 = 0 → if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))) = (2 · 𝑥))
328		oveq2 7199	. . . . . . 7 ⊢ (𝑥 = 0 → (2 · 𝑥) = (2 · 0))
329		2t0e0 11964	. . . . . . 7 ⊢ (2 · 0) = 0
330	328, 329	eqtrdi 2787	. . . . . 6 ⊢ (𝑥 = 0 → (2 · 𝑥) = 0)
331	325, 327, 330	3eqtrd 2775	. . . . 5 ⊢ (𝑥 = 0 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = 0)
332		c0ex 10792	. . . . 5 ⊢ 0 ∈ V
333	331, 186, 332	fvmpt 6796	. . . 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 10918	. . . . . . . . 9 ⊢ ((1 / 2) < 1 ↔ ¬ 1 ≤ (1 / 2))
337	143, 336	mpbi 233	. . . . . . . 8 ⊢ ¬ 1 ≤ (1 / 2)
338		breq1 5042	. . . . . . . 8 ⊢ (𝑥 = 1 → (𝑥 ≤ (1 / 2) ↔ 1 ≤ (1 / 2)))
339	337, 338	mtbiri 330	. . . . . . 7 ⊢ (𝑥 = 1 → ¬ 𝑥 ≤ (1 / 2))
340	339	iffalsed 4436	. . . . . 6 ⊢ (𝑥 = 1 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = ((𝑥 / 2) + (1 / 2)))
341		oveq1 7198	. . . . . . . 8 ⊢ (𝑥 = 1 → (𝑥 / 2) = (1 / 2))
342	341	oveq1d 7206	. . . . . . 7 ⊢ (𝑥 = 1 → ((𝑥 / 2) + (1 / 2)) = ((1 / 2) + (1 / 2)))
343	342, 83	eqtrdi 2787	. . . . . 6 ⊢ (𝑥 = 1 → ((𝑥 / 2) + (1 / 2)) = 1)
344	340, 343	eqtrd 2771	. . . . 5 ⊢ (𝑥 = 1 → if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2))) = 1)
345		1ex 10794	. . . . 5 ⊢ 1 ∈ V
346	344, 186, 345	fvmpt 6796	. . . 4 ⊢ (1 ∈ (0[,]1) → (𝑃‘1) = 1)
347	335, 346	syl 17	. . 3 ⊢ (𝜑 → (𝑃‘1) = 1)
348	313, 306, 334, 347	reparpht 23849	. 2 ⊢ (𝜑 → ((𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)) ∘ 𝑃)( ≃_ph‘𝐽)(𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)))
349	322, 348	eqbrtrd 5061	1 ⊢ (𝜑 → ((𝐹(_𝑝‘𝐽)𝐺)(_𝑝‘𝐽)𝐻)( ≃_ph‘𝐽)(𝐹(_𝑝‘𝐽)(𝐺(_𝑝‘𝐽)𝐻)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 399 ∨ wo 847 = wceq 1543 ∈ wcel 2112 ≠ wne 2932 ∀wral 3051 Vcvv 3398 ⊆ wss 3853 ifcif 4425 ∪ cuni 4805 class class class wbr 5039 ↦ cmpt 5120 ran crn 5537 ∘ ccom 5540 ⟶wf 6354 ‘cfv 6358 (class class class)co 7191 ℂcc 10692 ℝcr 10693 0cc0 10694 1c1 10695 + caddc 10697 · cmul 10699 ℝ^*cxr 10831 < clt 10832 ≤ cle 10833 − cmin 11027 / cdiv 11454 ℕcn 11795 2c2 11850 4c4 11852 (,)cioo 12900 [,]cicc 12903 ↾_t crest 16879 TopOpenctopn 16880 topGenctg 16896 ℂ_fldccnfld 20317 Topctop 21744 TopOnctopon 21761 Cn ccn 22075 ×_t ctx 22411 IIcii 23726 ≃_phcphtpc 23820 *_𝑝cpco 23851

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2708 ax-rep 5164 ax-sep 5177 ax-nul 5184 ax-pow 5243 ax-pr 5307 ax-un 7501 ax-cnex 10750 ax-resscn 10751 ax-1cn 10752 ax-icn 10753 ax-addcl 10754 ax-addrcl 10755 ax-mulcl 10756 ax-mulrcl 10757 ax-mulcom 10758 ax-addass 10759 ax-mulass 10760 ax-distr 10761 ax-i2m1 10762 ax-1ne0 10763 ax-1rid 10764 ax-rnegex 10765 ax-rrecex 10766 ax-cnre 10767 ax-pre-lttri 10768 ax-pre-lttrn 10769 ax-pre-ltadd 10770 ax-pre-mulgt0 10771 ax-pre-sup 10772 ax-addf 10773 ax-mulf 10774

This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2728 df-clel 2809 df-nfc 2879 df-ne 2933 df-nel 3037 df-ral 3056 df-rex 3057 df-reu 3058 df-rmo 3059 df-rab 3060 df-v 3400 df-sbc 3684 df-csb 3799 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-pss 3872 df-nul 4224 df-if 4426 df-pw 4501 df-sn 4528 df-pr 4530 df-tp 4532 df-op 4534 df-uni 4806 df-int 4846 df-iun 4892 df-iin 4893 df-br 5040 df-opab 5102 df-mpt 5121 df-tr 5147 df-id 5440 df-eprel 5445 df-po 5453 df-so 5454 df-fr 5494 df-se 5495 df-we 5496 df-xp 5542 df-rel 5543 df-cnv 5544 df-co 5545 df-dm 5546 df-rn 5547 df-res 5548 df-ima 5549 df-pred 6140 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6316 df-fun 6360 df-fn 6361 df-f 6362 df-f1 6363 df-fo 6364 df-f1o 6365 df-fv 6366 df-isom 6367 df-riota 7148 df-ov 7194 df-oprab 7195 df-mpo 7196 df-of 7447 df-om 7623 df-1st 7739 df-2nd 7740 df-supp 7882 df-wrecs 8025 df-recs 8086 df-rdg 8124 df-1o 8180 df-2o 8181 df-er 8369 df-map 8488 df-ixp 8557 df-en 8605 df-dom 8606 df-sdom 8607 df-fin 8608 df-fsupp 8964 df-fi 9005 df-sup 9036 df-inf 9037 df-oi 9104 df-card 9520 df-pnf 10834 df-mnf 10835 df-xr 10836 df-ltxr 10837 df-le 10838 df-sub 11029 df-neg 11030 df-div 11455 df-nn 11796 df-2 11858 df-3 11859 df-4 11860 df-5 11861 df-6 11862 df-7 11863 df-8 11864 df-9 11865 df-n0 12056 df-z 12142 df-dec 12259 df-uz 12404 df-q 12510 df-rp 12552 df-xneg 12669 df-xadd 12670 df-xmul 12671 df-ioo 12904 df-icc 12907 df-fz 13061 df-fzo 13204 df-seq 13540 df-exp 13601 df-hash 13862 df-cj 14627 df-re 14628 df-im 14629 df-sqrt 14763 df-abs 14764 df-struct 16668 df-ndx 16669 df-slot 16670 df-base 16672 df-sets 16673 df-ress 16674 df-plusg 16762 df-mulr 16763 df-starv 16764 df-sca 16765 df-vsca 16766 df-ip 16767 df-tset 16768 df-ple 16769 df-ds 16771 df-unif 16772 df-hom 16773 df-cco 16774 df-rest 16881 df-topn 16882 df-0g 16900 df-gsum 16901 df-topgen 16902 df-pt 16903 df-prds 16906 df-xrs 16961 df-qtop 16966 df-imas 16967 df-xps 16969 df-mre 17043 df-mrc 17044 df-acs 17046 df-mgm 18068 df-sgrp 18117 df-mnd 18128 df-submnd 18173 df-mulg 18443 df-cntz 18665 df-cmn 19126 df-psmet 20309 df-xmet 20310 df-met 20311 df-bl 20312 df-mopn 20313 df-cnfld 20318 df-top 21745 df-topon 21762 df-topsp 21784 df-bases 21797 df-cld 21870 df-cn 22078 df-cnp 22079 df-tx 22413 df-hmeo 22606 df-xms 23172 df-ms 23173 df-tms 23174 df-ii 23728 df-htpy 23821 df-phtpy 23822 df-phtpc 23843 df-pco 23856

This theorem is referenced by: pcophtb 23880 pi1grplem 23900 pi1xfr 23906 pi1xfrcnvlem 23907

W3C validator