Step | Hyp | Ref
| Expression |
1 | | pcoval.2 |
. . 3
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) |
2 | | pcoval.3 |
. . 3
⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) |
3 | 1, 2 | pcoval 23180 |
. 2
⊢ (𝜑 → (𝐹(*𝑝‘𝐽)𝐺) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝐹‘(2 · 𝑥)), (𝐺‘((2 · 𝑥) − 1))))) |
4 | | iitopon 23052 |
. . . 4
⊢ II ∈
(TopOn‘(0[,]1)) |
5 | 4 | a1i 11 |
. . 3
⊢ (𝜑 → II ∈
(TopOn‘(0[,]1))) |
6 | 5 | cnmptid 21835 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ 𝑥) ∈ (II Cn II)) |
7 | | 0elunit 12581 |
. . . . 5
⊢ 0 ∈
(0[,]1) |
8 | 7 | a1i 11 |
. . . 4
⊢ (𝜑 → 0 ∈
(0[,]1)) |
9 | 5, 5, 8 | cnmptc 21836 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ 0) ∈ (II Cn
II)) |
10 | | eqid 2825 |
. . . 4
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
11 | | eqid 2825 |
. . . 4
⊢
((topGen‘ran (,)) ↾t (0[,](1 / 2))) =
((topGen‘ran (,)) ↾t (0[,](1 / 2))) |
12 | | eqid 2825 |
. . . 4
⊢
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) =
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) |
13 | | dfii2 23055 |
. . . 4
⊢ II =
((topGen‘ran (,)) ↾t (0[,]1)) |
14 | | 0re 10358 |
. . . . 5
⊢ 0 ∈
ℝ |
15 | 14 | a1i 11 |
. . . 4
⊢ (𝜑 → 0 ∈
ℝ) |
16 | | 1re 10356 |
. . . . 5
⊢ 1 ∈
ℝ |
17 | 16 | a1i 11 |
. . . 4
⊢ (𝜑 → 1 ∈
ℝ) |
18 | | halfre 11572 |
. . . . . 6
⊢ (1 / 2)
∈ ℝ |
19 | | halfgt0 11574 |
. . . . . . 7
⊢ 0 < (1
/ 2) |
20 | 14, 18, 19 | ltleii 10479 |
. . . . . 6
⊢ 0 ≤ (1
/ 2) |
21 | | halflt1 11576 |
. . . . . . 7
⊢ (1 / 2)
< 1 |
22 | 18, 16, 21 | ltleii 10479 |
. . . . . 6
⊢ (1 / 2)
≤ 1 |
23 | | elicc01 12580 |
. . . . . 6
⊢ ((1 / 2)
∈ (0[,]1) ↔ ((1 / 2) ∈ ℝ ∧ 0 ≤ (1 / 2) ∧ (1 /
2) ≤ 1)) |
24 | 18, 20, 22, 23 | mpbir3an 1445 |
. . . . 5
⊢ (1 / 2)
∈ (0[,]1) |
25 | 24 | a1i 11 |
. . . 4
⊢ (𝜑 → (1 / 2) ∈
(0[,]1)) |
26 | | pcoval2.4 |
. . . . . 6
⊢ (𝜑 → (𝐹‘1) = (𝐺‘0)) |
27 | 26 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝐹‘1) = (𝐺‘0)) |
28 | | simprl 787 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → 𝑦 = (1 / 2)) |
29 | 28 | oveq2d 6921 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = (2 · (1 /
2))) |
30 | | 2cn 11426 |
. . . . . . . 8
⊢ 2 ∈
ℂ |
31 | | 2ne0 11462 |
. . . . . . . 8
⊢ 2 ≠
0 |
32 | 30, 31 | recidi 11082 |
. . . . . . 7
⊢ (2
· (1 / 2)) = 1 |
33 | 29, 32 | syl6eq 2877 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = 1) |
34 | 33 | fveq2d 6437 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝐹‘(2 · 𝑦)) = (𝐹‘1)) |
35 | 33 | oveq1d 6920 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → ((2 · 𝑦) − 1) = (1 −
1)) |
36 | | 1m1e0 11423 |
. . . . . . 7
⊢ (1
− 1) = 0 |
37 | 35, 36 | syl6eq 2877 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → ((2 · 𝑦) − 1) =
0) |
38 | 37 | fveq2d 6437 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝐺‘((2 · 𝑦) − 1)) = (𝐺‘0)) |
39 | 27, 34, 38 | 3eqtr4d 2871 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝐹‘(2 · 𝑦)) = (𝐺‘((2 · 𝑦) − 1))) |
40 | | retopon 22937 |
. . . . . . 7
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
41 | | iccssre 12543 |
. . . . . . . 8
⊢ ((0
∈ ℝ ∧ (1 / 2) ∈ ℝ) → (0[,](1 / 2)) ⊆
ℝ) |
42 | 14, 18, 41 | mp2an 683 |
. . . . . . 7
⊢ (0[,](1 /
2)) ⊆ ℝ |
43 | | resttopon 21336 |
. . . . . . 7
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 /
2)) ⊆ ℝ) → ((topGen‘ran (,)) ↾t (0[,](1
/ 2))) ∈ (TopOn‘(0[,](1 / 2)))) |
44 | 40, 42, 43 | mp2an 683 |
. . . . . 6
⊢
((topGen‘ran (,)) ↾t (0[,](1 / 2))) ∈
(TopOn‘(0[,](1 / 2))) |
45 | 44 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((topGen‘ran (,))
↾t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 /
2)))) |
46 | 45, 5 | cnmpt1st 21842 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 2)), 𝑧 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,))
↾t (0[,](1 / 2))) ×t II) Cn
((topGen‘ran (,)) ↾t (0[,](1 / 2))))) |
47 | 11 | iihalf1cn 23101 |
. . . . . . 7
⊢ (𝑥 ∈ (0[,](1 / 2)) ↦ (2
· 𝑥)) ∈
(((topGen‘ran (,)) ↾t (0[,](1 / 2))) Cn
II) |
48 | 47 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (0[,](1 / 2)) ↦ (2 ·
𝑥)) ∈
(((topGen‘ran (,)) ↾t (0[,](1 / 2))) Cn
II)) |
49 | | oveq2 6913 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦)) |
50 | 45, 5, 46, 45, 48, 49 | cnmpt21 21845 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 2)), 𝑧 ∈ (0[,]1) ↦ (2 · 𝑦)) ∈ ((((topGen‘ran
(,)) ↾t (0[,](1 / 2))) ×t II) Cn
II)) |
51 | 45, 5, 50, 1 | cnmpt21f 21846 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 2)), 𝑧 ∈ (0[,]1) ↦ (𝐹‘(2 · 𝑦))) ∈ ((((topGen‘ran (,))
↾t (0[,](1 / 2))) ×t II) Cn 𝐽)) |
52 | | iccssre 12543 |
. . . . . . . 8
⊢ (((1 / 2)
∈ ℝ ∧ 1 ∈ ℝ) → ((1 / 2)[,]1) ⊆
ℝ) |
53 | 18, 16, 52 | mp2an 683 |
. . . . . . 7
⊢ ((1 /
2)[,]1) ⊆ ℝ |
54 | | resttopon 21336 |
. . . . . . 7
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 /
2)[,]1) ⊆ ℝ) → ((topGen‘ran (,)) ↾t ((1
/ 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1))) |
55 | 40, 53, 54 | mp2an 683 |
. . . . . 6
⊢
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ∈
(TopOn‘((1 / 2)[,]1)) |
56 | 55 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ∈ (TopOn‘((1 /
2)[,]1))) |
57 | 56, 5 | cnmpt1st 21842 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ ((1 / 2)[,]1), 𝑧 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ×t II) Cn
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)))) |
58 | 12 | iihalf2cn 23103 |
. . . . . . 7
⊢ (𝑥 ∈ ((1 / 2)[,]1) ↦
((2 · 𝑥) − 1))
∈ (((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) Cn
II) |
59 | 58 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ((1 / 2)[,]1) ↦ ((2 ·
𝑥) − 1)) ∈
(((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) Cn
II)) |
60 | 49 | oveq1d 6920 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) |
61 | 56, 5, 57, 56, 59, 60 | cnmpt21 21845 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ ((1 / 2)[,]1), 𝑧 ∈ (0[,]1) ↦ ((2 · 𝑦) − 1)) ∈
((((topGen‘ran (,)) ↾t ((1 / 2)[,]1))
×t II) Cn II)) |
62 | 56, 5, 61, 2 | cnmpt21f 21846 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ ((1 / 2)[,]1), 𝑧 ∈ (0[,]1) ↦ (𝐺‘((2 · 𝑦) − 1))) ∈ ((((topGen‘ran
(,)) ↾t ((1 / 2)[,]1)) ×t II) Cn 𝐽)) |
63 | 10, 11, 12, 13, 15, 17, 25, 5, 39, 51, 62 | cnmpt2pc 23097 |
. . 3
⊢ (𝜑 → (𝑦 ∈ (0[,]1), 𝑧 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 2), (𝐹‘(2 · 𝑦)), (𝐺‘((2 · 𝑦) − 1)))) ∈ ((II
×t II) Cn 𝐽)) |
64 | | breq1 4876 |
. . . . 5
⊢ (𝑦 = 𝑥 → (𝑦 ≤ (1 / 2) ↔ 𝑥 ≤ (1 / 2))) |
65 | | oveq2 6913 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (2 · 𝑦) = (2 · 𝑥)) |
66 | 65 | fveq2d 6437 |
. . . . 5
⊢ (𝑦 = 𝑥 → (𝐹‘(2 · 𝑦)) = (𝐹‘(2 · 𝑥))) |
67 | 65 | oveq1d 6920 |
. . . . . 6
⊢ (𝑦 = 𝑥 → ((2 · 𝑦) − 1) = ((2 · 𝑥) − 1)) |
68 | 67 | fveq2d 6437 |
. . . . 5
⊢ (𝑦 = 𝑥 → (𝐺‘((2 · 𝑦) − 1)) = (𝐺‘((2 · 𝑥) − 1))) |
69 | 64, 66, 68 | ifbieq12d 4333 |
. . . 4
⊢ (𝑦 = 𝑥 → if(𝑦 ≤ (1 / 2), (𝐹‘(2 · 𝑦)), (𝐺‘((2 · 𝑦) − 1))) = if(𝑥 ≤ (1 / 2), (𝐹‘(2 · 𝑥)), (𝐺‘((2 · 𝑥) − 1)))) |
70 | 69 | adantr 474 |
. . 3
⊢ ((𝑦 = 𝑥 ∧ 𝑧 = 0) → if(𝑦 ≤ (1 / 2), (𝐹‘(2 · 𝑦)), (𝐺‘((2 · 𝑦) − 1))) = if(𝑥 ≤ (1 / 2), (𝐹‘(2 · 𝑥)), (𝐺‘((2 · 𝑥) − 1)))) |
71 | 5, 6, 9, 5, 5, 63,
70 | cnmpt12 21841 |
. 2
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝐹‘(2 · 𝑥)), (𝐺‘((2 · 𝑥) − 1)))) ∈ (II Cn 𝐽)) |
72 | 3, 71 | eqeltrd 2906 |
1
⊢ (𝜑 → (𝐹(*𝑝‘𝐽)𝐺) ∈ (II Cn 𝐽)) |