Step | Hyp | Ref
| Expression |
1 | | pcopt.1 |
. . . . . . . . . 10
⊢ 𝑃 = ((0[,]1) × {𝑌}) |
2 | 1 | fveq1i 6718 |
. . . . . . . . 9
⊢ (𝑃‘(2 · 𝑥)) = (((0[,]1) × {𝑌})‘(2 · 𝑥)) |
3 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝐹‘0) = 𝑌) |
4 | | iiuni 23778 |
. . . . . . . . . . . . . 14
⊢ (0[,]1) =
∪ II |
5 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝐽 =
∪ 𝐽 |
6 | 4, 5 | cnf 22143 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐹:(0[,]1)⟶∪
𝐽) |
7 | 6 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → 𝐹:(0[,]1)⟶∪
𝐽) |
8 | | 0elunit 13057 |
. . . . . . . . . . . 12
⊢ 0 ∈
(0[,]1) |
9 | | ffvelrn 6902 |
. . . . . . . . . . . 12
⊢ ((𝐹:(0[,]1)⟶∪ 𝐽
∧ 0 ∈ (0[,]1)) → (𝐹‘0) ∈ ∪ 𝐽) |
10 | 7, 8, 9 | sylancl 589 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝐹‘0) ∈ ∪ 𝐽) |
11 | 3, 10 | eqeltrrd 2839 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → 𝑌 ∈ ∪ 𝐽) |
12 | | elii1 23832 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0[,](1 / 2)) ↔
(𝑥 ∈ (0[,]1) ∧
𝑥 ≤ (1 /
2))) |
13 | | iihalf1 23828 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0[,](1 / 2)) → (2
· 𝑥) ∈
(0[,]1)) |
14 | 12, 13 | sylbir 238 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 2)) → (2
· 𝑥) ∈
(0[,]1)) |
15 | | fvconst2g 7017 |
. . . . . . . . . 10
⊢ ((𝑌 ∈ ∪ 𝐽
∧ (2 · 𝑥) ∈
(0[,]1)) → (((0[,]1) × {𝑌})‘(2 · 𝑥)) = 𝑌) |
16 | 11, 14, 15 | syl2an 599 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 2))) → (((0[,]1) ×
{𝑌})‘(2 ·
𝑥)) = 𝑌) |
17 | 2, 16 | syl5eq 2790 |
. . . . . . . 8
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 2))) → (𝑃‘(2 · 𝑥)) = 𝑌) |
18 | | simplr 769 |
. . . . . . . 8
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 2))) → (𝐹‘0) = 𝑌) |
19 | 17, 18 | eqtr4d 2780 |
. . . . . . 7
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 2))) → (𝑃‘(2 · 𝑥)) = (𝐹‘0)) |
20 | 19 | ifeq1d 4458 |
. . . . . 6
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) ∧ (𝑥 ∈ (0[,]1) ∧ 𝑥 ≤ (1 / 2))) → if(𝑥 ≤ (1 / 2), (𝑃‘(2 · 𝑥)), (𝐹‘((2 · 𝑥) − 1))) = if(𝑥 ≤ (1 / 2), (𝐹‘0), (𝐹‘((2 · 𝑥) − 1)))) |
21 | 20 | expr 460 |
. . . . 5
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) ∧ 𝑥 ∈ (0[,]1)) → (𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), (𝑃‘(2 · 𝑥)), (𝐹‘((2 · 𝑥) − 1))) = if(𝑥 ≤ (1 / 2), (𝐹‘0), (𝐹‘((2 · 𝑥) − 1))))) |
22 | | iffalse 4448 |
. . . . . 6
⊢ (¬
𝑥 ≤ (1 / 2) →
if(𝑥 ≤ (1 / 2), (𝑃‘(2 · 𝑥)), (𝐹‘((2 · 𝑥) − 1))) = (𝐹‘((2 · 𝑥) − 1))) |
23 | | iffalse 4448 |
. . . . . 6
⊢ (¬
𝑥 ≤ (1 / 2) →
if(𝑥 ≤ (1 / 2), (𝐹‘0), (𝐹‘((2 · 𝑥) − 1))) = (𝐹‘((2 · 𝑥) − 1))) |
24 | 22, 23 | eqtr4d 2780 |
. . . . 5
⊢ (¬
𝑥 ≤ (1 / 2) →
if(𝑥 ≤ (1 / 2), (𝑃‘(2 · 𝑥)), (𝐹‘((2 · 𝑥) − 1))) = if(𝑥 ≤ (1 / 2), (𝐹‘0), (𝐹‘((2 · 𝑥) − 1)))) |
25 | 21, 24 | pm2.61d1 183 |
. . . 4
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) ∧ 𝑥 ∈ (0[,]1)) → if(𝑥 ≤ (1 / 2), (𝑃‘(2 · 𝑥)), (𝐹‘((2 · 𝑥) − 1))) = if(𝑥 ≤ (1 / 2), (𝐹‘0), (𝐹‘((2 · 𝑥) − 1)))) |
26 | 25 | mpteq2dva 5150 |
. . 3
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑃‘(2 · 𝑥)), (𝐹‘((2 · 𝑥) − 1)))) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝐹‘0), (𝐹‘((2 · 𝑥) − 1))))) |
27 | | cntop2 22138 |
. . . . . . . 8
⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐽 ∈ Top) |
28 | 27 | adantr 484 |
. . . . . . 7
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → 𝐽 ∈ Top) |
29 | | toptopon2 21815 |
. . . . . . 7
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
30 | 28, 29 | sylib 221 |
. . . . . 6
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → 𝐽 ∈ (TopOn‘∪ 𝐽)) |
31 | 1 | pcoptcl 23918 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽)
∧ 𝑌 ∈ ∪ 𝐽)
→ (𝑃 ∈ (II Cn
𝐽) ∧ (𝑃‘0) = 𝑌 ∧ (𝑃‘1) = 𝑌)) |
32 | 30, 11, 31 | syl2anc 587 |
. . . . 5
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑃 ∈ (II Cn 𝐽) ∧ (𝑃‘0) = 𝑌 ∧ (𝑃‘1) = 𝑌)) |
33 | 32 | simp1d 1144 |
. . . 4
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → 𝑃 ∈ (II Cn 𝐽)) |
34 | | simpl 486 |
. . . 4
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → 𝐹 ∈ (II Cn 𝐽)) |
35 | 33, 34 | pcoval 23908 |
. . 3
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑃(*𝑝‘𝐽)𝐹) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑃‘(2 · 𝑥)), (𝐹‘((2 · 𝑥) − 1))))) |
36 | | iffalse 4448 |
. . . . . . . . 9
⊢ (¬
𝑥 ≤ (1 / 2) →
if(𝑥 ≤ (1 / 2), 0, ((2
· 𝑥) − 1)) =
((2 · 𝑥) −
1)) |
37 | 36 | adantl 485 |
. . . . . . . 8
⊢ ((𝑥 ∈ (0[,]1) ∧ ¬
𝑥 ≤ (1 / 2)) →
if(𝑥 ≤ (1 / 2), 0, ((2
· 𝑥) − 1)) =
((2 · 𝑥) −
1)) |
38 | | elii2 23833 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (0[,]1) ∧ ¬
𝑥 ≤ (1 / 2)) →
𝑥 ∈ ((1 /
2)[,]1)) |
39 | | iihalf2 23830 |
. . . . . . . . 9
⊢ (𝑥 ∈ ((1 / 2)[,]1) → ((2
· 𝑥) − 1)
∈ (0[,]1)) |
40 | 38, 39 | syl 17 |
. . . . . . . 8
⊢ ((𝑥 ∈ (0[,]1) ∧ ¬
𝑥 ≤ (1 / 2)) → ((2
· 𝑥) − 1)
∈ (0[,]1)) |
41 | 37, 40 | eqeltrd 2838 |
. . . . . . 7
⊢ ((𝑥 ∈ (0[,]1) ∧ ¬
𝑥 ≤ (1 / 2)) →
if(𝑥 ≤ (1 / 2), 0, ((2
· 𝑥) − 1))
∈ (0[,]1)) |
42 | 41 | ex 416 |
. . . . . 6
⊢ (𝑥 ∈ (0[,]1) → (¬
𝑥 ≤ (1 / 2) →
if(𝑥 ≤ (1 / 2), 0, ((2
· 𝑥) − 1))
∈ (0[,]1))) |
43 | | iftrue 4445 |
. . . . . . 7
⊢ (𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), 0, ((2 ·
𝑥) − 1)) =
0) |
44 | 43, 8 | eqeltrdi 2846 |
. . . . . 6
⊢ (𝑥 ≤ (1 / 2) → if(𝑥 ≤ (1 / 2), 0, ((2 ·
𝑥) − 1)) ∈
(0[,]1)) |
45 | 42, 44 | pm2.61d2 184 |
. . . . 5
⊢ (𝑥 ∈ (0[,]1) → if(𝑥 ≤ (1 / 2), 0, ((2 ·
𝑥) − 1)) ∈
(0[,]1)) |
46 | 45 | adantl 485 |
. . . 4
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) ∧ 𝑥 ∈ (0[,]1)) → if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)) ∈
(0[,]1)) |
47 | | eqid 2737 |
. . . . 5
⊢ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), 0, ((2 ·
𝑥) − 1))) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), 0, ((2 ·
𝑥) −
1))) |
48 | 47 | a1i 11 |
. . . 4
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1))) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), 0, ((2 ·
𝑥) −
1)))) |
49 | 7 | feqmptd 6780 |
. . . 4
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → 𝐹 = (𝑦 ∈ (0[,]1) ↦ (𝐹‘𝑦))) |
50 | | fveq2 6717 |
. . . . 5
⊢ (𝑦 = if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)) → (𝐹‘𝑦) = (𝐹‘if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)))) |
51 | | fvif 6733 |
. . . . 5
⊢ (𝐹‘if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1))) = if(𝑥 ≤ (1 / 2), (𝐹‘0), (𝐹‘((2 · 𝑥) − 1))) |
52 | 50, 51 | eqtrdi 2794 |
. . . 4
⊢ (𝑦 = if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)) → (𝐹‘𝑦) = if(𝑥 ≤ (1 / 2), (𝐹‘0), (𝐹‘((2 · 𝑥) − 1)))) |
53 | 46, 48, 49, 52 | fmptco 6944 |
. . 3
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝐹 ∘ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)))) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝐹‘0), (𝐹‘((2 · 𝑥) − 1))))) |
54 | 26, 35, 53 | 3eqtr4d 2787 |
. 2
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑃(*𝑝‘𝐽)𝐹) = (𝐹 ∘ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) −
1))))) |
55 | | iitopon 23776 |
. . . . 5
⊢ II ∈
(TopOn‘(0[,]1)) |
56 | 55 | a1i 11 |
. . . 4
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → II ∈
(TopOn‘(0[,]1))) |
57 | 56 | cnmptid 22558 |
. . . 4
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑥 ∈ (0[,]1) ↦ 𝑥) ∈ (II Cn II)) |
58 | 8 | a1i 11 |
. . . . 5
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → 0 ∈ (0[,]1)) |
59 | 56, 56, 58 | cnmptc 22559 |
. . . 4
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑥 ∈ (0[,]1) ↦ 0) ∈ (II Cn
II)) |
60 | | eqid 2737 |
. . . . 5
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
61 | | eqid 2737 |
. . . . 5
⊢
((topGen‘ran (,)) ↾t (0[,](1 / 2))) =
((topGen‘ran (,)) ↾t (0[,](1 / 2))) |
62 | | eqid 2737 |
. . . . 5
⊢
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) =
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) |
63 | | dfii2 23779 |
. . . . 5
⊢ II =
((topGen‘ran (,)) ↾t (0[,]1)) |
64 | | 0re 10835 |
. . . . . 6
⊢ 0 ∈
ℝ |
65 | 64 | a1i 11 |
. . . . 5
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → 0 ∈ ℝ) |
66 | | 1re 10833 |
. . . . . 6
⊢ 1 ∈
ℝ |
67 | 66 | a1i 11 |
. . . . 5
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → 1 ∈ ℝ) |
68 | | halfre 12044 |
. . . . . . 7
⊢ (1 / 2)
∈ ℝ |
69 | | halfge0 12047 |
. . . . . . 7
⊢ 0 ≤ (1
/ 2) |
70 | | halflt1 12048 |
. . . . . . . 8
⊢ (1 / 2)
< 1 |
71 | 68, 66, 70 | ltleii 10955 |
. . . . . . 7
⊢ (1 / 2)
≤ 1 |
72 | | elicc01 13054 |
. . . . . . 7
⊢ ((1 / 2)
∈ (0[,]1) ↔ ((1 / 2) ∈ ℝ ∧ 0 ≤ (1 / 2) ∧ (1 /
2) ≤ 1)) |
73 | 68, 69, 71, 72 | mpbir3an 1343 |
. . . . . 6
⊢ (1 / 2)
∈ (0[,]1) |
74 | 73 | a1i 11 |
. . . . 5
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (1 / 2) ∈
(0[,]1)) |
75 | | simprl 771 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → 𝑦 = (1 / 2)) |
76 | 75 | oveq2d 7229 |
. . . . . . . 8
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = (2 · (1 /
2))) |
77 | | 2cn 11905 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
78 | | 2ne0 11934 |
. . . . . . . . 9
⊢ 2 ≠
0 |
79 | 77, 78 | recidi 11563 |
. . . . . . . 8
⊢ (2
· (1 / 2)) = 1 |
80 | 76, 79 | eqtrdi 2794 |
. . . . . . 7
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → (2 · 𝑦) = 1) |
81 | 80 | oveq1d 7228 |
. . . . . 6
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → ((2 · 𝑦) − 1) = (1 −
1)) |
82 | | 1m1e0 11902 |
. . . . . 6
⊢ (1
− 1) = 0 |
83 | 81, 82 | eqtr2di 2795 |
. . . . 5
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) ∧ (𝑦 = (1 / 2) ∧ 𝑧 ∈ (0[,]1))) → 0 = ((2 ·
𝑦) −
1)) |
84 | | retopon 23661 |
. . . . . . . 8
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
85 | | iccssre 13017 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ (1 / 2) ∈ ℝ) → (0[,](1 / 2)) ⊆
ℝ) |
86 | 64, 68, 85 | mp2an 692 |
. . . . . . . 8
⊢ (0[,](1 /
2)) ⊆ ℝ |
87 | | resttopon 22058 |
. . . . . . . 8
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 /
2)) ⊆ ℝ) → ((topGen‘ran (,)) ↾t (0[,](1
/ 2))) ∈ (TopOn‘(0[,](1 / 2)))) |
88 | 84, 86, 87 | mp2an 692 |
. . . . . . 7
⊢
((topGen‘ran (,)) ↾t (0[,](1 / 2))) ∈
(TopOn‘(0[,](1 / 2))) |
89 | 88 | a1i 11 |
. . . . . 6
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → ((topGen‘ran (,))
↾t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 /
2)))) |
90 | 89, 56, 56, 58 | cnmpt2c 22567 |
. . . . 5
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑦 ∈ (0[,](1 / 2)), 𝑧 ∈ (0[,]1) ↦ 0) ∈
((((topGen‘ran (,)) ↾t (0[,](1 / 2)))
×t II) Cn II)) |
91 | | iccssre 13017 |
. . . . . . . . 9
⊢ (((1 / 2)
∈ ℝ ∧ 1 ∈ ℝ) → ((1 / 2)[,]1) ⊆
ℝ) |
92 | 68, 66, 91 | mp2an 692 |
. . . . . . . 8
⊢ ((1 /
2)[,]1) ⊆ ℝ |
93 | | resttopon 22058 |
. . . . . . . 8
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 /
2)[,]1) ⊆ ℝ) → ((topGen‘ran (,)) ↾t ((1
/ 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1))) |
94 | 84, 92, 93 | mp2an 692 |
. . . . . . 7
⊢
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ∈
(TopOn‘((1 / 2)[,]1)) |
95 | 94 | a1i 11 |
. . . . . 6
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → ((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ∈ (TopOn‘((1 /
2)[,]1))) |
96 | 95, 56 | cnmpt1st 22565 |
. . . . . 6
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑦 ∈ ((1 / 2)[,]1), 𝑧 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ×t II) Cn
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)))) |
97 | 62 | iihalf2cn 23831 |
. . . . . . 7
⊢ (𝑥 ∈ ((1 / 2)[,]1) ↦
((2 · 𝑥) − 1))
∈ (((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) Cn
II) |
98 | 97 | a1i 11 |
. . . . . 6
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑥 ∈ ((1 / 2)[,]1) ↦ ((2 ·
𝑥) − 1)) ∈
(((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) Cn
II)) |
99 | | oveq2 7221 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦)) |
100 | 99 | oveq1d 7228 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((2 · 𝑥) − 1) = ((2 · 𝑦) − 1)) |
101 | 95, 56, 96, 95, 98, 100 | cnmpt21 22568 |
. . . . 5
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑦 ∈ ((1 / 2)[,]1), 𝑧 ∈ (0[,]1) ↦ ((2 · 𝑦) − 1)) ∈
((((topGen‘ran (,)) ↾t ((1 / 2)[,]1))
×t II) Cn II)) |
102 | 60, 61, 62, 63, 65, 67, 74, 56, 83, 90, 101 | cnmpopc 23825 |
. . . 4
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑦 ∈ (0[,]1), 𝑧 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 2), 0, ((2 · 𝑦) − 1))) ∈ ((II
×t II) Cn II)) |
103 | | breq1 5056 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (𝑦 ≤ (1 / 2) ↔ 𝑥 ≤ (1 / 2))) |
104 | | oveq2 7221 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (2 · 𝑦) = (2 · 𝑥)) |
105 | 104 | oveq1d 7228 |
. . . . . 6
⊢ (𝑦 = 𝑥 → ((2 · 𝑦) − 1) = ((2 · 𝑥) − 1)) |
106 | 103, 105 | ifbieq2d 4465 |
. . . . 5
⊢ (𝑦 = 𝑥 → if(𝑦 ≤ (1 / 2), 0, ((2 · 𝑦) − 1)) = if(𝑥 ≤ (1 / 2), 0, ((2 ·
𝑥) −
1))) |
107 | 106 | adantr 484 |
. . . 4
⊢ ((𝑦 = 𝑥 ∧ 𝑧 = 0) → if(𝑦 ≤ (1 / 2), 0, ((2 · 𝑦) − 1)) = if(𝑥 ≤ (1 / 2), 0, ((2 ·
𝑥) −
1))) |
108 | 56, 57, 59, 56, 56, 102, 107 | cnmpt12 22564 |
. . 3
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1))) ∈ (II Cn
II)) |
109 | | id 22 |
. . . . . . 7
⊢ (𝑥 = 0 → 𝑥 = 0) |
110 | 109, 69 | eqbrtrdi 5092 |
. . . . . 6
⊢ (𝑥 = 0 → 𝑥 ≤ (1 / 2)) |
111 | 110, 43 | syl 17 |
. . . . 5
⊢ (𝑥 = 0 → if(𝑥 ≤ (1 / 2), 0, ((2 ·
𝑥) − 1)) =
0) |
112 | | c0ex 10827 |
. . . . 5
⊢ 0 ∈
V |
113 | 111, 47, 112 | fvmpt 6818 |
. . . 4
⊢ (0 ∈
(0[,]1) → ((𝑥 ∈
(0[,]1) ↦ if(𝑥 ≤
(1 / 2), 0, ((2 · 𝑥)
− 1)))‘0) = 0) |
114 | 8, 113 | mp1i 13 |
. . 3
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → ((𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)))‘0) =
0) |
115 | | 1elunit 13058 |
. . . 4
⊢ 1 ∈
(0[,]1) |
116 | 68, 66 | ltnlei 10953 |
. . . . . . . . 9
⊢ ((1 / 2)
< 1 ↔ ¬ 1 ≤ (1 / 2)) |
117 | 70, 116 | mpbi 233 |
. . . . . . . 8
⊢ ¬ 1
≤ (1 / 2) |
118 | | breq1 5056 |
. . . . . . . 8
⊢ (𝑥 = 1 → (𝑥 ≤ (1 / 2) ↔ 1 ≤ (1 /
2))) |
119 | 117, 118 | mtbiri 330 |
. . . . . . 7
⊢ (𝑥 = 1 → ¬ 𝑥 ≤ (1 / 2)) |
120 | 119, 36 | syl 17 |
. . . . . 6
⊢ (𝑥 = 1 → if(𝑥 ≤ (1 / 2), 0, ((2 ·
𝑥) − 1)) = ((2
· 𝑥) −
1)) |
121 | | oveq2 7221 |
. . . . . . . . 9
⊢ (𝑥 = 1 → (2 · 𝑥) = (2 ·
1)) |
122 | | 2t1e2 11993 |
. . . . . . . . 9
⊢ (2
· 1) = 2 |
123 | 121, 122 | eqtrdi 2794 |
. . . . . . . 8
⊢ (𝑥 = 1 → (2 · 𝑥) = 2) |
124 | 123 | oveq1d 7228 |
. . . . . . 7
⊢ (𝑥 = 1 → ((2 · 𝑥) − 1) = (2 −
1)) |
125 | | 2m1e1 11956 |
. . . . . . 7
⊢ (2
− 1) = 1 |
126 | 124, 125 | eqtrdi 2794 |
. . . . . 6
⊢ (𝑥 = 1 → ((2 · 𝑥) − 1) =
1) |
127 | 120, 126 | eqtrd 2777 |
. . . . 5
⊢ (𝑥 = 1 → if(𝑥 ≤ (1 / 2), 0, ((2 ·
𝑥) − 1)) =
1) |
128 | | 1ex 10829 |
. . . . 5
⊢ 1 ∈
V |
129 | 127, 47, 128 | fvmpt 6818 |
. . . 4
⊢ (1 ∈
(0[,]1) → ((𝑥 ∈
(0[,]1) ↦ if(𝑥 ≤
(1 / 2), 0, ((2 · 𝑥)
− 1)))‘1) = 1) |
130 | 115, 129 | mp1i 13 |
. . 3
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → ((𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1)))‘1) =
1) |
131 | 34, 108, 114, 130 | reparpht 23895 |
. 2
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝐹 ∘ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), 0, ((2 · 𝑥) − 1))))(
≃ph‘𝐽)𝐹) |
132 | 54, 131 | eqbrtrd 5075 |
1
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑃(*𝑝‘𝐽)𝐹)( ≃ph‘𝐽)𝐹) |