| Step | Hyp | Ref
| Expression |
| 1 | | pcoval.2 |
. . 3
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) |
| 2 | | pcoval.3 |
. . 3
⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) |
| 3 | 1, 2 | pcoval 25044 |
. 2
⊢ (𝜑 → (𝐹(*𝑝‘𝐽)𝐺) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝐹‘(2 · 𝑥)), (𝐺‘((2 · 𝑥) − 1))))) |
| 4 | | iitopon 24905 |
. . . 4
⊢ II ∈
(TopOn‘(0[,]1)) |
| 5 | 4 | a1i 11 |
. . 3
⊢ (𝜑 → II ∈
(TopOn‘(0[,]1))) |
| 6 | 5 | cnmptid 23669 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ 𝑥) ∈ (II Cn II)) |
| 7 | | 0elunit 13509 |
. . . . 5
⊢ 0 ∈
(0[,]1) |
| 8 | 7 | a1i 11 |
. . . 4
⊢ (𝜑 → 0 ∈
(0[,]1)) |
| 9 | 5, 5, 8 | cnmptc 23670 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ 0) ∈ (II Cn
II)) |
| 10 | | eqid 2737 |
. . . 4
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
| 11 | | eqid 2737 |
. . . 4
⊢
((topGen‘ran (,)) ↾t (0[,](1 / 2))) =
((topGen‘ran (,)) ↾t (0[,](1 / 2))) |
| 12 | | eqid 2737 |
. . . 4
⊢
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) =
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) |
| 13 | | dfii2 24908 |
. . . 4
⊢ II =
((topGen‘ran (,)) ↾t (0[,]1)) |
| 14 | | 0re 11263 |
. . . . 5
⊢ 0 ∈
ℝ |
| 15 | 14 | a1i 11 |
. . . 4
⊢ (𝜑 → 0 ∈
ℝ) |
| 16 | | 1re 11261 |
. . . . 5
⊢ 1 ∈
ℝ |
| 17 | 16 | a1i 11 |
. . . 4
⊢ (𝜑 → 1 ∈
ℝ) |
| 18 | | halfre 12480 |
. . . . . 6
⊢ (1 / 2)
∈ ℝ |
| 19 | | halfge0 12483 |
. . . . . 6
⊢ 0 ≤ (1
/ 2) |
| 20 | | halflt1 12484 |
. . . . . . 7
⊢ (1 / 2)
< 1 |
| 21 | 18, 16, 20 | ltleii 11384 |
. . . . . 6
⊢ (1 / 2)
≤ 1 |
| 22 | | elicc01 13506 |
. . . . . 6
⊢ ((1 / 2)
∈ (0[,]1) ↔ ((1 / 2) ∈ ℝ ∧ 0 ≤ (1 / 2) ∧ (1 /
2) ≤ 1)) |
| 23 | 18, 19, 21, 22 | mpbir3an 1342 |
. . . . 5
⊢ (1 / 2)
∈ (0[,]1) |
| 24 | 23 | a1i 11 |
. . . 4
⊢ (𝜑 → (1 / 2) ∈
(0[,]1)) |
| 25 | | pcoval2.4 |
. . . . . 6
⊢ (𝜑 → (𝐹‘1) = (𝐺‘0)) |
| 26 | 25 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝐹‘1) = (𝐺‘0)) |
| 27 | | simprl 771 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → 𝑦 = (1 / 2)) |
| 28 | 27 | oveq2d 7447 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = (2 · (1 /
2))) |
| 29 | | 2cn 12341 |
. . . . . . . 8
⊢ 2 ∈
ℂ |
| 30 | | 2ne0 12370 |
. . . . . . . 8
⊢ 2 ≠
0 |
| 31 | 29, 30 | recidi 11998 |
. . . . . . 7
⊢ (2
· (1 / 2)) = 1 |
| 32 | 28, 31 | eqtrdi 2793 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = 1) |
| 33 | 32 | fveq2d 6910 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝐹‘(2 · 𝑦)) = (𝐹‘1)) |
| 34 | 32 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → ((2 · 𝑦) − 1) = (1 −
1)) |
| 35 | | 1m1e0 12338 |
. . . . . . 7
⊢ (1
− 1) = 0 |
| 36 | 34, 35 | eqtrdi 2793 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → ((2 · 𝑦) − 1) =
0) |
| 37 | 36 | fveq2d 6910 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝐺‘((2 · 𝑦) − 1)) = (𝐺‘0)) |
| 38 | 26, 33, 37 | 3eqtr4d 2787 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (𝐹‘(2 · 𝑦)) = (𝐺‘((2 · 𝑦) − 1))) |
| 39 | | retopon 24784 |
. . . . . . 7
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
| 40 | | iccssre 13469 |
. . . . . . . 8
⊢ ((0
∈ ℝ ∧ (1 / 2) ∈ ℝ) → (0[,](1 / 2)) ⊆
ℝ) |
| 41 | 14, 18, 40 | mp2an 692 |
. . . . . . 7
⊢ (0[,](1 /
2)) ⊆ ℝ |
| 42 | | resttopon 23169 |
. . . . . . 7
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 /
2)) ⊆ ℝ) → ((topGen‘ran (,)) ↾t (0[,](1
/ 2))) ∈ (TopOn‘(0[,](1 / 2)))) |
| 43 | 39, 41, 42 | mp2an 692 |
. . . . . 6
⊢
((topGen‘ran (,)) ↾t (0[,](1 / 2))) ∈
(TopOn‘(0[,](1 / 2))) |
| 44 | 43 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((topGen‘ran (,))
↾t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 /
2)))) |
| 45 | 44, 5 | cnmpt1st 23676 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 2)), 𝑧 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,))
↾t (0[,](1 / 2))) ×t II) Cn
((topGen‘ran (,)) ↾t (0[,](1 / 2))))) |
| 46 | 11 | iihalf1cn 24959 |
. . . . . . 7
⊢ (𝑥 ∈ (0[,](1 / 2)) ↦ (2
· 𝑥)) ∈
(((topGen‘ran (,)) ↾t (0[,](1 / 2))) Cn
II) |
| 47 | 46 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (0[,](1 / 2)) ↦ (2 ·
𝑥)) ∈
(((topGen‘ran (,)) ↾t (0[,](1 / 2))) Cn
II)) |
| 48 | | oveq2 7439 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦)) |
| 49 | 44, 5, 45, 44, 47, 48 | cnmpt21 23679 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 2)), 𝑧 ∈ (0[,]1) ↦ (2 · 𝑦)) ∈ ((((topGen‘ran
(,)) ↾t (0[,](1 / 2))) ×t II) Cn
II)) |
| 50 | 44, 5, 49, 1 | cnmpt21f 23680 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (0[,](1 / 2)), 𝑧 ∈ (0[,]1) ↦ (𝐹‘(2 · 𝑦))) ∈ ((((topGen‘ran (,))
↾t (0[,](1 / 2))) ×t II) Cn 𝐽)) |
| 51 | | iccssre 13469 |
. . . . . . . 8
⊢ (((1 / 2)
∈ ℝ ∧ 1 ∈ ℝ) → ((1 / 2)[,]1) ⊆
ℝ) |
| 52 | 18, 16, 51 | mp2an 692 |
. . . . . . 7
⊢ ((1 /
2)[,]1) ⊆ ℝ |
| 53 | | resttopon 23169 |
. . . . . . 7
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 /
2)[,]1) ⊆ ℝ) → ((topGen‘ran (,)) ↾t ((1
/ 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1))) |
| 54 | 39, 52, 53 | mp2an 692 |
. . . . . 6
⊢
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ∈
(TopOn‘((1 / 2)[,]1)) |
| 55 | 54 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ∈ (TopOn‘((1 /
2)[,]1))) |
| 56 | 55, 5 | cnmpt1st 23676 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ ((1 / 2)[,]1), 𝑧 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ×t II) Cn
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)))) |
| 57 | 12 | iihalf2cn 24962 |
. . . . . . 7
⊢ (𝑥 ∈ ((1 / 2)[,]1) ↦
((2 · 𝑥) − 1))
∈ (((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) Cn
II) |
| 58 | 57 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ((1 / 2)[,]1) ↦ ((2 ·
𝑥) − 1)) ∈
(((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) Cn
II)) |
| 59 | 48 | oveq1d 7446 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) |
| 60 | 55, 5, 56, 55, 58, 59 | cnmpt21 23679 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ ((1 / 2)[,]1), 𝑧 ∈ (0[,]1) ↦ ((2 · 𝑦) − 1)) ∈
((((topGen‘ran (,)) ↾t ((1 / 2)[,]1))
×t II) Cn II)) |
| 61 | 55, 5, 60, 2 | cnmpt21f 23680 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ ((1 / 2)[,]1), 𝑧 ∈ (0[,]1) ↦ (𝐺‘((2 · 𝑦) − 1))) ∈ ((((topGen‘ran
(,)) ↾t ((1 / 2)[,]1)) ×t II) Cn 𝐽)) |
| 62 | 10, 11, 12, 13, 15, 17, 24, 5, 38, 50, 61 | cnmpopc 24955 |
. . 3
⊢ (𝜑 → (𝑦 ∈ (0[,]1), 𝑧 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 2), (𝐹‘(2 · 𝑦)), (𝐺‘((2 · 𝑦) − 1)))) ∈ ((II
×t II) Cn 𝐽)) |
| 63 | | breq1 5146 |
. . . . 5
⊢ (𝑦 = 𝑥 → (𝑦 ≤ (1 / 2) ↔ 𝑥 ≤ (1 / 2))) |
| 64 | | oveq2 7439 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (2 · 𝑦) = (2 · 𝑥)) |
| 65 | 64 | fveq2d 6910 |
. . . . 5
⊢ (𝑦 = 𝑥 → (𝐹‘(2 · 𝑦)) = (𝐹‘(2 · 𝑥))) |
| 66 | 64 | oveq1d 7446 |
. . . . . 6
⊢ (𝑦 = 𝑥 → ((2 · 𝑦) − 1) = ((2 · 𝑥) − 1)) |
| 67 | 66 | fveq2d 6910 |
. . . . 5
⊢ (𝑦 = 𝑥 → (𝐺‘((2 · 𝑦) − 1)) = (𝐺‘((2 · 𝑥) − 1))) |
| 68 | 63, 65, 67 | ifbieq12d 4554 |
. . . 4
⊢ (𝑦 = 𝑥 → if(𝑦 ≤ (1 / 2), (𝐹‘(2 · 𝑦)), (𝐺‘((2 · 𝑦) − 1))) = if(𝑥 ≤ (1 / 2), (𝐹‘(2 · 𝑥)), (𝐺‘((2 · 𝑥) − 1)))) |
| 69 | 68 | adantr 480 |
. . 3
⊢ ((𝑦 = 𝑥 ∧ 𝑧 = 0) → if(𝑦 ≤ (1 / 2), (𝐹‘(2 · 𝑦)), (𝐺‘((2 · 𝑦) − 1))) = if(𝑥 ≤ (1 / 2), (𝐹‘(2 · 𝑥)), (𝐺‘((2 · 𝑥) − 1)))) |
| 70 | 5, 6, 9, 5, 5, 62,
69 | cnmpt12 23675 |
. 2
⊢ (𝜑 → (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝐹‘(2 · 𝑥)), (𝐺‘((2 · 𝑥) − 1)))) ∈ (II Cn 𝐽)) |
| 71 | 3, 70 | eqeltrd 2841 |
1
⊢ (𝜑 → (𝐹(*𝑝‘𝐽)𝐺) ∈ (II Cn 𝐽)) |