Step | Hyp | Ref
| Expression |
1 | | pcorev.1 |
. . . . 5
⊢ 𝐺 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥))) |
2 | | iitopon 23090 |
. . . . . . 7
⊢ II ∈
(TopOn‘(0[,]1)) |
3 | 2 | a1i 11 |
. . . . . 6
⊢ (𝐹 ∈ (II Cn 𝐽) → II ∈
(TopOn‘(0[,]1))) |
4 | | iirevcn 23137 |
. . . . . . 7
⊢ (𝑥 ∈ (0[,]1) ↦ (1
− 𝑥)) ∈ (II Cn
II) |
5 | 4 | a1i 11 |
. . . . . 6
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑥 ∈ (0[,]1) ↦ (1 − 𝑥)) ∈ (II Cn
II)) |
6 | | id 22 |
. . . . . 6
⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐹 ∈ (II Cn 𝐽)) |
7 | 3, 5, 6 | cnmpt11f 21876 |
. . . . 5
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥))) ∈ (II Cn 𝐽)) |
8 | 1, 7 | syl5eqel 2862 |
. . . 4
⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐺 ∈ (II Cn 𝐽)) |
9 | | 1elunit 12606 |
. . . . 5
⊢ 1 ∈
(0[,]1) |
10 | | oveq2 6930 |
. . . . . . . 8
⊢ (𝑥 = 1 → (1 − 𝑥) = (1 −
1)) |
11 | | 1m1e0 11447 |
. . . . . . . 8
⊢ (1
− 1) = 0 |
12 | 10, 11 | syl6eq 2829 |
. . . . . . 7
⊢ (𝑥 = 1 → (1 − 𝑥) = 0) |
13 | 12 | fveq2d 6450 |
. . . . . 6
⊢ (𝑥 = 1 → (𝐹‘(1 − 𝑥)) = (𝐹‘0)) |
14 | | fvex 6459 |
. . . . . 6
⊢ (𝐹‘0) ∈
V |
15 | 13, 1, 14 | fvmpt 6542 |
. . . . 5
⊢ (1 ∈
(0[,]1) → (𝐺‘1)
= (𝐹‘0)) |
16 | 9, 15 | mp1i 13 |
. . . 4
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐺‘1) = (𝐹‘0)) |
17 | 8, 6, 16 | pcocn 23224 |
. . 3
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐺(*𝑝‘𝐽)𝐹) ∈ (II Cn 𝐽)) |
18 | | cntop2 21453 |
. . . . . 6
⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐽 ∈ Top) |
19 | | eqid 2777 |
. . . . . . 7
⊢ ∪ 𝐽 =
∪ 𝐽 |
20 | 19 | toptopon 21129 |
. . . . . 6
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
21 | 18, 20 | sylib 210 |
. . . . 5
⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐽 ∈ (TopOn‘∪ 𝐽)) |
22 | | iiuni 23092 |
. . . . . . 7
⊢ (0[,]1) =
∪ II |
23 | 22, 19 | cnf 21458 |
. . . . . 6
⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐹:(0[,]1)⟶∪
𝐽) |
24 | | ffvelrn 6621 |
. . . . . 6
⊢ ((𝐹:(0[,]1)⟶∪ 𝐽
∧ 1 ∈ (0[,]1)) → (𝐹‘1) ∈ ∪ 𝐽) |
25 | 23, 9, 24 | sylancl 580 |
. . . . 5
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐹‘1) ∈ ∪ 𝐽) |
26 | | pcorev.2 |
. . . . . 6
⊢ 𝑃 = ((0[,]1) × {(𝐹‘1)}) |
27 | 26 | pcoptcl 23228 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽)
∧ (𝐹‘1) ∈
∪ 𝐽) → (𝑃 ∈ (II Cn 𝐽) ∧ (𝑃‘0) = (𝐹‘1) ∧ (𝑃‘1) = (𝐹‘1))) |
28 | 21, 25, 27 | syl2anc 579 |
. . . 4
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑃 ∈ (II Cn 𝐽) ∧ (𝑃‘0) = (𝐹‘1) ∧ (𝑃‘1) = (𝐹‘1))) |
29 | 28 | simp1d 1133 |
. . 3
⊢ (𝐹 ∈ (II Cn 𝐽) → 𝑃 ∈ (II Cn 𝐽)) |
30 | | pcorevlem.3 |
. . . 4
⊢ 𝐻 = (𝑠 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ (𝐹‘if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 −
𝑡) · (1 − ((2
· 𝑠) −
1))))))) |
31 | | eqid 2777 |
. . . . . 6
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
32 | | eqid 2777 |
. . . . . 6
⊢
((topGen‘ran (,)) ↾t (0[,](1 / 2))) =
((topGen‘ran (,)) ↾t (0[,](1 / 2))) |
33 | | eqid 2777 |
. . . . . 6
⊢
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) =
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) |
34 | | dfii2 23093 |
. . . . . 6
⊢ II =
((topGen‘ran (,)) ↾t (0[,]1)) |
35 | | 0red 10380 |
. . . . . 6
⊢ (𝐹 ∈ (II Cn 𝐽) → 0 ∈ ℝ) |
36 | | 1red 10377 |
. . . . . 6
⊢ (𝐹 ∈ (II Cn 𝐽) → 1 ∈ ℝ) |
37 | | halfre 11596 |
. . . . . . . 8
⊢ (1 / 2)
∈ ℝ |
38 | | 0re 10378 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
39 | | halfgt0 11598 |
. . . . . . . . 9
⊢ 0 < (1
/ 2) |
40 | 38, 37, 39 | ltleii 10499 |
. . . . . . . 8
⊢ 0 ≤ (1
/ 2) |
41 | | 1re 10376 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
42 | | halflt1 11600 |
. . . . . . . . 9
⊢ (1 / 2)
< 1 |
43 | 37, 41, 42 | ltleii 10499 |
. . . . . . . 8
⊢ (1 / 2)
≤ 1 |
44 | | elicc01 12604 |
. . . . . . . 8
⊢ ((1 / 2)
∈ (0[,]1) ↔ ((1 / 2) ∈ ℝ ∧ 0 ≤ (1 / 2) ∧ (1 /
2) ≤ 1)) |
45 | 37, 40, 43, 44 | mpbir3an 1398 |
. . . . . . 7
⊢ (1 / 2)
∈ (0[,]1) |
46 | 45 | a1i 11 |
. . . . . 6
⊢ (𝐹 ∈ (II Cn 𝐽) → (1 / 2) ∈
(0[,]1)) |
47 | | simprl 761 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → 𝑠 = (1 / 2)) |
48 | 47 | oveq2d 6938 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → (2 · 𝑠) = (2 · (1 /
2))) |
49 | | 2cn 11450 |
. . . . . . . . . . 11
⊢ 2 ∈
ℂ |
50 | | 2ne0 11486 |
. . . . . . . . . . 11
⊢ 2 ≠
0 |
51 | 49, 50 | recidi 11106 |
. . . . . . . . . 10
⊢ (2
· (1 / 2)) = 1 |
52 | 48, 51 | syl6eq 2829 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → (2 · 𝑠) = 1) |
53 | 52 | oveq1d 6937 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → ((2 · 𝑠) − 1) = (1 −
1)) |
54 | 53, 11 | syl6eq 2829 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → ((2 · 𝑠) − 1) =
0) |
55 | 54 | oveq2d 6938 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → (1 − ((2
· 𝑠) − 1)) =
(1 − 0)) |
56 | | 1m0e1 11503 |
. . . . . . . . . 10
⊢ (1
− 0) = 1 |
57 | 55, 56 | syl6eq 2829 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → (1 − ((2
· 𝑠) − 1)) =
1) |
58 | 52, 57 | eqtr4d 2816 |
. . . . . . . 8
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → (2 · 𝑠) = (1 − ((2 ·
𝑠) −
1))) |
59 | 58 | oveq2d 6938 |
. . . . . . 7
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → ((1 − 𝑡) · (2 · 𝑠)) = ((1 − 𝑡) · (1 − ((2
· 𝑠) −
1)))) |
60 | 59 | oveq2d 6938 |
. . . . . 6
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → (1 − ((1
− 𝑡) · (2
· 𝑠))) = (1 −
((1 − 𝑡) · (1
− ((2 · 𝑠)
− 1))))) |
61 | | retopon 22975 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
62 | | iccssre 12567 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ (1 / 2) ∈ ℝ) → (0[,](1 / 2)) ⊆
ℝ) |
63 | 38, 37, 62 | mp2an 682 |
. . . . . . . . 9
⊢ (0[,](1 /
2)) ⊆ ℝ |
64 | | resttopon 21373 |
. . . . . . . . 9
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 /
2)) ⊆ ℝ) → ((topGen‘ran (,)) ↾t (0[,](1
/ 2))) ∈ (TopOn‘(0[,](1 / 2)))) |
65 | 61, 63, 64 | mp2an 682 |
. . . . . . . 8
⊢
((topGen‘ran (,)) ↾t (0[,](1 / 2))) ∈
(TopOn‘(0[,](1 / 2))) |
66 | 65 | a1i 11 |
. . . . . . 7
⊢ (𝐹 ∈ (II Cn 𝐽) → ((topGen‘ran (,))
↾t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 /
2)))) |
67 | 66, 3 | cnmpt2nd 21881 |
. . . . . . . . 9
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ (0[,](1 / 2)), 𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((((topGen‘ran (,))
↾t (0[,](1 / 2))) ×t II) Cn
II)) |
68 | | oveq2 6930 |
. . . . . . . . 9
⊢ (𝑥 = 𝑡 → (1 − 𝑥) = (1 − 𝑡)) |
69 | 66, 3, 67, 3, 5, 68 | cnmpt21 21883 |
. . . . . . . 8
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ (0[,](1 / 2)), 𝑡 ∈ (0[,]1) ↦ (1 − 𝑡)) ∈ ((((topGen‘ran
(,)) ↾t (0[,](1 / 2))) ×t II) Cn
II)) |
70 | 66, 3 | cnmpt1st 21880 |
. . . . . . . . 9
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ (0[,](1 / 2)), 𝑡 ∈ (0[,]1) ↦ 𝑠) ∈ ((((topGen‘ran (,))
↾t (0[,](1 / 2))) ×t II) Cn
((topGen‘ran (,)) ↾t (0[,](1 / 2))))) |
71 | 32 | iihalf1cn 23139 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0[,](1 / 2)) ↦ (2
· 𝑥)) ∈
(((topGen‘ran (,)) ↾t (0[,](1 / 2))) Cn
II) |
72 | 71 | a1i 11 |
. . . . . . . . 9
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑥 ∈ (0[,](1 / 2)) ↦ (2 ·
𝑥)) ∈
(((topGen‘ran (,)) ↾t (0[,](1 / 2))) Cn
II)) |
73 | | oveq2 6930 |
. . . . . . . . 9
⊢ (𝑥 = 𝑠 → (2 · 𝑥) = (2 · 𝑠)) |
74 | 66, 3, 70, 66, 72, 73 | cnmpt21 21883 |
. . . . . . . 8
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ (0[,](1 / 2)), 𝑡 ∈ (0[,]1) ↦ (2 · 𝑠)) ∈ ((((topGen‘ran
(,)) ↾t (0[,](1 / 2))) ×t II) Cn
II)) |
75 | | iimulcn 23145 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝑥 · 𝑦)) ∈ ((II ×t II) Cn
II) |
76 | 75 | a1i 11 |
. . . . . . . 8
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝑥 · 𝑦)) ∈ ((II ×t II) Cn
II)) |
77 | | oveq12 6931 |
. . . . . . . 8
⊢ ((𝑥 = (1 − 𝑡) ∧ 𝑦 = (2 · 𝑠)) → (𝑥 · 𝑦) = ((1 − 𝑡) · (2 · 𝑠))) |
78 | 66, 3, 69, 74, 3, 3, 76, 77 | cnmpt22 21886 |
. . . . . . 7
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ (0[,](1 / 2)), 𝑡 ∈ (0[,]1) ↦ ((1 − 𝑡) · (2 · 𝑠))) ∈ ((((topGen‘ran
(,)) ↾t (0[,](1 / 2))) ×t II) Cn
II)) |
79 | | oveq2 6930 |
. . . . . . 7
⊢ (𝑥 = ((1 − 𝑡) · (2 · 𝑠)) → (1 − 𝑥) = (1 − ((1 − 𝑡) · (2 · 𝑠)))) |
80 | 66, 3, 78, 3, 5, 79 | cnmpt21 21883 |
. . . . . 6
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ (0[,](1 / 2)), 𝑡 ∈ (0[,]1) ↦ (1 − ((1
− 𝑡) · (2
· 𝑠)))) ∈
((((topGen‘ran (,)) ↾t (0[,](1 / 2)))
×t II) Cn II)) |
81 | | iccssre 12567 |
. . . . . . . . . 10
⊢ (((1 / 2)
∈ ℝ ∧ 1 ∈ ℝ) → ((1 / 2)[,]1) ⊆
ℝ) |
82 | 37, 41, 81 | mp2an 682 |
. . . . . . . . 9
⊢ ((1 /
2)[,]1) ⊆ ℝ |
83 | | resttopon 21373 |
. . . . . . . . 9
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 /
2)[,]1) ⊆ ℝ) → ((topGen‘ran (,)) ↾t ((1
/ 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1))) |
84 | 61, 82, 83 | mp2an 682 |
. . . . . . . 8
⊢
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ∈
(TopOn‘((1 / 2)[,]1)) |
85 | 84 | a1i 11 |
. . . . . . 7
⊢ (𝐹 ∈ (II Cn 𝐽) → ((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ∈ (TopOn‘((1 /
2)[,]1))) |
86 | 85, 3 | cnmpt2nd 21881 |
. . . . . . . . 9
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ ((1 / 2)[,]1), 𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ×t II) Cn
II)) |
87 | 85, 3, 86, 3, 5, 68 | cnmpt21 21883 |
. . . . . . . 8
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ ((1 / 2)[,]1), 𝑡 ∈ (0[,]1) ↦ (1 − 𝑡)) ∈ ((((topGen‘ran
(,)) ↾t ((1 / 2)[,]1)) ×t II) Cn
II)) |
88 | 85, 3 | cnmpt1st 21880 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ ((1 / 2)[,]1), 𝑡 ∈ (0[,]1) ↦ 𝑠) ∈ ((((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ×t II) Cn
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)))) |
89 | 33 | iihalf2cn 23141 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ((1 / 2)[,]1) ↦
((2 · 𝑥) − 1))
∈ (((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) Cn
II) |
90 | 89 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑥 ∈ ((1 / 2)[,]1) ↦ ((2 ·
𝑥) − 1)) ∈
(((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) Cn
II)) |
91 | 73 | oveq1d 6937 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑠 → ((2 · 𝑥) − 1) = ((2 · 𝑠) − 1)) |
92 | 85, 3, 88, 85, 90, 91 | cnmpt21 21883 |
. . . . . . . . 9
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ ((1 / 2)[,]1), 𝑡 ∈ (0[,]1) ↦ ((2 · 𝑠) − 1)) ∈
((((topGen‘ran (,)) ↾t ((1 / 2)[,]1))
×t II) Cn II)) |
93 | | oveq2 6930 |
. . . . . . . . 9
⊢ (𝑥 = ((2 · 𝑠) − 1) → (1 −
𝑥) = (1 − ((2
· 𝑠) −
1))) |
94 | 85, 3, 92, 3, 5, 93 | cnmpt21 21883 |
. . . . . . . 8
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ ((1 / 2)[,]1), 𝑡 ∈ (0[,]1) ↦ (1 − ((2
· 𝑠) − 1)))
∈ ((((topGen‘ran (,)) ↾t ((1 / 2)[,]1))
×t II) Cn II)) |
95 | | oveq12 6931 |
. . . . . . . 8
⊢ ((𝑥 = (1 − 𝑡) ∧ 𝑦 = (1 − ((2 · 𝑠) − 1))) → (𝑥 · 𝑦) = ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1)))) |
96 | 85, 3, 87, 94, 3, 3, 76, 95 | cnmpt22 21886 |
. . . . . . 7
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ ((1 / 2)[,]1), 𝑡 ∈ (0[,]1) ↦ ((1 − 𝑡) · (1 − ((2
· 𝑠) − 1))))
∈ ((((topGen‘ran (,)) ↾t ((1 / 2)[,]1))
×t II) Cn II)) |
97 | | oveq2 6930 |
. . . . . . 7
⊢ (𝑥 = ((1 − 𝑡) · (1 − ((2
· 𝑠) − 1)))
→ (1 − 𝑥) = (1
− ((1 − 𝑡)
· (1 − ((2 · 𝑠) − 1))))) |
98 | 85, 3, 96, 3, 5, 97 | cnmpt21 21883 |
. . . . . 6
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ ((1 / 2)[,]1), 𝑡 ∈ (0[,]1) ↦ (1 − ((1
− 𝑡) · (1
− ((2 · 𝑠)
− 1))))) ∈ ((((topGen‘ran (,)) ↾t ((1 /
2)[,]1)) ×t II) Cn II)) |
99 | 31, 32, 33, 34, 35, 36, 46, 3, 60, 80, 98 | cnmpt2pc 23135 |
. . . . 5
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 −
𝑡) · (1 − ((2
· 𝑠) − 1))))))
∈ ((II ×t II) Cn II)) |
100 | 3, 3, 99, 6 | cnmpt21f 21884 |
. . . 4
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ (𝐹‘if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 −
𝑡) · (1 − ((2
· 𝑠) −
1))))))) ∈ ((II ×t II) Cn 𝐽)) |
101 | 30, 100 | syl5eqel 2862 |
. . 3
⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐻 ∈ ((II ×t II) Cn
𝐽)) |
102 | | simpr 479 |
. . . . 5
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → 𝑦 ∈ (0[,]1)) |
103 | | 0elunit 12605 |
. . . . 5
⊢ 0 ∈
(0[,]1) |
104 | | simpl 476 |
. . . . . . . . 9
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → 𝑠 = 𝑦) |
105 | 104 | breq1d 4896 |
. . . . . . . 8
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → (𝑠 ≤ (1 / 2) ↔ 𝑦 ≤ (1 / 2))) |
106 | | simpr 479 |
. . . . . . . . . . . 12
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → 𝑡 = 0) |
107 | 106 | oveq2d 6938 |
. . . . . . . . . . 11
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → (1 − 𝑡) = (1 − 0)) |
108 | 107, 56 | syl6eq 2829 |
. . . . . . . . . 10
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → (1 − 𝑡) = 1) |
109 | 104 | oveq2d 6938 |
. . . . . . . . . 10
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → (2 · 𝑠) = (2 · 𝑦)) |
110 | 108, 109 | oveq12d 6940 |
. . . . . . . . 9
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → ((1 − 𝑡) · (2 · 𝑠)) = (1 · (2 · 𝑦))) |
111 | 110 | oveq2d 6938 |
. . . . . . . 8
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → (1 − ((1 − 𝑡) · (2 · 𝑠))) = (1 − (1 · (2
· 𝑦)))) |
112 | 109 | oveq1d 6937 |
. . . . . . . . . . 11
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → ((2 · 𝑠) − 1) = ((2 · 𝑦) − 1)) |
113 | 112 | oveq2d 6938 |
. . . . . . . . . 10
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → (1 − ((2 · 𝑠) − 1)) = (1 − ((2
· 𝑦) −
1))) |
114 | 108, 113 | oveq12d 6940 |
. . . . . . . . 9
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1))) = (1 · (1
− ((2 · 𝑦)
− 1)))) |
115 | 114 | oveq2d 6938 |
. . . . . . . 8
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → (1 − ((1 − 𝑡) · (1 − ((2
· 𝑠) − 1)))) =
(1 − (1 · (1 − ((2 · 𝑦) − 1))))) |
116 | 105, 111,
115 | ifbieq12d 4333 |
. . . . . . 7
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 −
𝑡) · (1 − ((2
· 𝑠) − 1)))))
= if(𝑦 ≤ (1 / 2), (1
− (1 · (2 · 𝑦))), (1 − (1 · (1 − ((2
· 𝑦) −
1)))))) |
117 | 116 | fveq2d 6450 |
. . . . . 6
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → (𝐹‘if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 −
𝑡) · (1 − ((2
· 𝑠) − 1))))))
= (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (1
· (2 · 𝑦))),
(1 − (1 · (1 − ((2 · 𝑦) − 1))))))) |
118 | | fvex 6459 |
. . . . . 6
⊢ (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (1 · (2
· 𝑦))), (1 −
(1 · (1 − ((2 · 𝑦) − 1)))))) ∈ V |
119 | 117, 30, 118 | ovmpt2a 7068 |
. . . . 5
⊢ ((𝑦 ∈ (0[,]1) ∧ 0 ∈
(0[,]1)) → (𝑦𝐻0) = (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (1 · (2
· 𝑦))), (1 −
(1 · (1 − ((2 · 𝑦) − 1))))))) |
120 | 102, 103,
119 | sylancl 580 |
. . . 4
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (𝑦𝐻0) = (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (1 · (2
· 𝑦))), (1 −
(1 · (1 − ((2 · 𝑦) − 1))))))) |
121 | | iftrue 4312 |
. . . . . . . 8
⊢ (𝑦 ≤ (1 / 2) → if(𝑦 ≤ (1 / 2), (1 − (1
· (2 · 𝑦))),
(1 − (1 · (1 − ((2 · 𝑦) − 1))))) = (1 − (1 · (2
· 𝑦)))) |
122 | 121 | adantl 475 |
. . . . . . 7
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) ∧ 𝑦 ≤ (1 / 2)) → if(𝑦 ≤ (1 / 2), (1 − (1 · (2
· 𝑦))), (1 −
(1 · (1 − ((2 · 𝑦) − 1))))) = (1 − (1 · (2
· 𝑦)))) |
123 | 122 | fveq2d 6450 |
. . . . . 6
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) ∧ 𝑦 ≤ (1 / 2)) → (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (1 · (2
· 𝑦))), (1 −
(1 · (1 − ((2 · 𝑦) − 1)))))) = (𝐹‘(1 − (1 · (2 ·
𝑦))))) |
124 | | elii1 23142 |
. . . . . . . 8
⊢ (𝑦 ∈ (0[,](1 / 2)) ↔
(𝑦 ∈ (0[,]1) ∧
𝑦 ≤ (1 /
2))) |
125 | 8, 6 | pcoval1 23220 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,](1 / 2))) → ((𝐺(*𝑝‘𝐽)𝐹)‘𝑦) = (𝐺‘(2 · 𝑦))) |
126 | | iihalf1 23138 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (0[,](1 / 2)) → (2
· 𝑦) ∈
(0[,]1)) |
127 | 126 | adantl 475 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,](1 / 2))) → (2 ·
𝑦) ∈
(0[,]1)) |
128 | | oveq2 6930 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (2 · 𝑦) → (1 − 𝑥) = (1 − (2 · 𝑦))) |
129 | 128 | fveq2d 6450 |
. . . . . . . . . . . 12
⊢ (𝑥 = (2 · 𝑦) → (𝐹‘(1 − 𝑥)) = (𝐹‘(1 − (2 · 𝑦)))) |
130 | | fvex 6459 |
. . . . . . . . . . . 12
⊢ (𝐹‘(1 − (2 ·
𝑦))) ∈
V |
131 | 129, 1, 130 | fvmpt 6542 |
. . . . . . . . . . 11
⊢ ((2
· 𝑦) ∈ (0[,]1)
→ (𝐺‘(2 ·
𝑦)) = (𝐹‘(1 − (2 · 𝑦)))) |
132 | | unitssre 12636 |
. . . . . . . . . . . . . . . 16
⊢ (0[,]1)
⊆ ℝ |
133 | 132 | sseli 3816 |
. . . . . . . . . . . . . . 15
⊢ ((2
· 𝑦) ∈ (0[,]1)
→ (2 · 𝑦)
∈ ℝ) |
134 | 133 | recnd 10405 |
. . . . . . . . . . . . . 14
⊢ ((2
· 𝑦) ∈ (0[,]1)
→ (2 · 𝑦)
∈ ℂ) |
135 | 134 | mulid2d 10395 |
. . . . . . . . . . . . 13
⊢ ((2
· 𝑦) ∈ (0[,]1)
→ (1 · (2 · 𝑦)) = (2 · 𝑦)) |
136 | 135 | oveq2d 6938 |
. . . . . . . . . . . 12
⊢ ((2
· 𝑦) ∈ (0[,]1)
→ (1 − (1 · (2 · 𝑦))) = (1 − (2 · 𝑦))) |
137 | 136 | fveq2d 6450 |
. . . . . . . . . . 11
⊢ ((2
· 𝑦) ∈ (0[,]1)
→ (𝐹‘(1 −
(1 · (2 · 𝑦)))) = (𝐹‘(1 − (2 · 𝑦)))) |
138 | 131, 137 | eqtr4d 2816 |
. . . . . . . . . 10
⊢ ((2
· 𝑦) ∈ (0[,]1)
→ (𝐺‘(2 ·
𝑦)) = (𝐹‘(1 − (1 · (2 ·
𝑦))))) |
139 | 127, 138 | syl 17 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,](1 / 2))) → (𝐺‘(2 · 𝑦)) = (𝐹‘(1 − (1 · (2 ·
𝑦))))) |
140 | 125, 139 | eqtrd 2813 |
. . . . . . . 8
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,](1 / 2))) → ((𝐺(*𝑝‘𝐽)𝐹)‘𝑦) = (𝐹‘(1 − (1 · (2 ·
𝑦))))) |
141 | 124, 140 | sylan2br 588 |
. . . . . . 7
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑦 ∈ (0[,]1) ∧ 𝑦 ≤ (1 / 2))) → ((𝐺(*𝑝‘𝐽)𝐹)‘𝑦) = (𝐹‘(1 − (1 · (2 ·
𝑦))))) |
142 | 141 | anassrs 461 |
. . . . . 6
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) ∧ 𝑦 ≤ (1 / 2)) → ((𝐺(*𝑝‘𝐽)𝐹)‘𝑦) = (𝐹‘(1 − (1 · (2 ·
𝑦))))) |
143 | 123, 142 | eqtr4d 2816 |
. . . . 5
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) ∧ 𝑦 ≤ (1 / 2)) → (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (1 · (2
· 𝑦))), (1 −
(1 · (1 − ((2 · 𝑦) − 1)))))) = ((𝐺(*𝑝‘𝐽)𝐹)‘𝑦)) |
144 | | iffalse 4315 |
. . . . . . . 8
⊢ (¬
𝑦 ≤ (1 / 2) →
if(𝑦 ≤ (1 / 2), (1
− (1 · (2 · 𝑦))), (1 − (1 · (1 − ((2
· 𝑦) − 1)))))
= (1 − (1 · (1 − ((2 · 𝑦) − 1))))) |
145 | 144 | adantl 475 |
. . . . . . 7
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) ∧ ¬ 𝑦 ≤ (1 / 2)) → if(𝑦 ≤ (1 / 2), (1 − (1
· (2 · 𝑦))),
(1 − (1 · (1 − ((2 · 𝑦) − 1))))) = (1 − (1 · (1
− ((2 · 𝑦)
− 1))))) |
146 | 145 | fveq2d 6450 |
. . . . . 6
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) ∧ ¬ 𝑦 ≤ (1 / 2)) → (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (1 · (2
· 𝑦))), (1 −
(1 · (1 − ((2 · 𝑦) − 1)))))) = (𝐹‘(1 − (1 · (1 − ((2
· 𝑦) −
1)))))) |
147 | | elii2 23143 |
. . . . . . . 8
⊢ ((𝑦 ∈ (0[,]1) ∧ ¬
𝑦 ≤ (1 / 2)) →
𝑦 ∈ ((1 /
2)[,]1)) |
148 | 8, 6, 16 | pcoval2 23223 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ ((1 / 2)[,]1)) → ((𝐺(*𝑝‘𝐽)𝐹)‘𝑦) = (𝐹‘((2 · 𝑦) − 1))) |
149 | | iihalf2 23140 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ((1 / 2)[,]1) → ((2
· 𝑦) − 1)
∈ (0[,]1)) |
150 | 149 | adantl 475 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ ((1 / 2)[,]1)) → ((2 ·
𝑦) − 1) ∈
(0[,]1)) |
151 | | ax-1cn 10330 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ |
152 | 132 | sseli 3816 |
. . . . . . . . . . . . . . . 16
⊢ (((2
· 𝑦) − 1)
∈ (0[,]1) → ((2 · 𝑦) − 1) ∈ ℝ) |
153 | 152 | recnd 10405 |
. . . . . . . . . . . . . . 15
⊢ (((2
· 𝑦) − 1)
∈ (0[,]1) → ((2 · 𝑦) − 1) ∈ ℂ) |
154 | | subcl 10621 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℂ ∧ ((2 · 𝑦) − 1) ∈ ℂ) → (1
− ((2 · 𝑦)
− 1)) ∈ ℂ) |
155 | 151, 153,
154 | sylancr 581 |
. . . . . . . . . . . . . 14
⊢ (((2
· 𝑦) − 1)
∈ (0[,]1) → (1 − ((2 · 𝑦) − 1)) ∈
ℂ) |
156 | 155 | mulid2d 10395 |
. . . . . . . . . . . . 13
⊢ (((2
· 𝑦) − 1)
∈ (0[,]1) → (1 · (1 − ((2 · 𝑦) − 1))) = (1 − ((2 ·
𝑦) −
1))) |
157 | 156 | oveq2d 6938 |
. . . . . . . . . . . 12
⊢ (((2
· 𝑦) − 1)
∈ (0[,]1) → (1 − (1 · (1 − ((2 · 𝑦) − 1)))) = (1 − (1
− ((2 · 𝑦)
− 1)))) |
158 | | nncan 10652 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℂ ∧ ((2 · 𝑦) − 1) ∈ ℂ) → (1
− (1 − ((2 · 𝑦) − 1))) = ((2 · 𝑦) − 1)) |
159 | 151, 153,
158 | sylancr 581 |
. . . . . . . . . . . 12
⊢ (((2
· 𝑦) − 1)
∈ (0[,]1) → (1 − (1 − ((2 · 𝑦) − 1))) = ((2 · 𝑦) − 1)) |
160 | 157, 159 | eqtr2d 2814 |
. . . . . . . . . . 11
⊢ (((2
· 𝑦) − 1)
∈ (0[,]1) → ((2 · 𝑦) − 1) = (1 − (1 · (1
− ((2 · 𝑦)
− 1))))) |
161 | 150, 160 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ ((1 / 2)[,]1)) → ((2 ·
𝑦) − 1) = (1 −
(1 · (1 − ((2 · 𝑦) − 1))))) |
162 | 161 | fveq2d 6450 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ ((1 / 2)[,]1)) → (𝐹‘((2 · 𝑦) − 1)) = (𝐹‘(1 − (1 · (1
− ((2 · 𝑦)
− 1)))))) |
163 | 148, 162 | eqtrd 2813 |
. . . . . . . 8
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ ((1 / 2)[,]1)) → ((𝐺(*𝑝‘𝐽)𝐹)‘𝑦) = (𝐹‘(1 − (1 · (1 − ((2
· 𝑦) −
1)))))) |
164 | 147, 163 | sylan2 586 |
. . . . . . 7
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑦 ∈ (0[,]1) ∧ ¬ 𝑦 ≤ (1 / 2))) → ((𝐺(*𝑝‘𝐽)𝐹)‘𝑦) = (𝐹‘(1 − (1 · (1 − ((2
· 𝑦) −
1)))))) |
165 | 164 | anassrs 461 |
. . . . . 6
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) ∧ ¬ 𝑦 ≤ (1 / 2)) → ((𝐺(*𝑝‘𝐽)𝐹)‘𝑦) = (𝐹‘(1 − (1 · (1 − ((2
· 𝑦) −
1)))))) |
166 | 146, 165 | eqtr4d 2816 |
. . . . 5
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) ∧ ¬ 𝑦 ≤ (1 / 2)) → (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (1 · (2
· 𝑦))), (1 −
(1 · (1 − ((2 · 𝑦) − 1)))))) = ((𝐺(*𝑝‘𝐽)𝐹)‘𝑦)) |
167 | 143, 166 | pm2.61dan 803 |
. . . 4
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (1 · (2
· 𝑦))), (1 −
(1 · (1 − ((2 · 𝑦) − 1)))))) = ((𝐺(*𝑝‘𝐽)𝐹)‘𝑦)) |
168 | 120, 167 | eqtrd 2813 |
. . 3
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (𝑦𝐻0) = ((𝐺(*𝑝‘𝐽)𝐹)‘𝑦)) |
169 | 132 | sseli 3816 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (0[,]1) → 𝑦 ∈
ℝ) |
170 | 169 | recnd 10405 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (0[,]1) → 𝑦 ∈
ℂ) |
171 | | mulcl 10356 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℂ ∧ 𝑦
∈ ℂ) → (2 · 𝑦) ∈ ℂ) |
172 | 49, 170, 171 | sylancr 581 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (0[,]1) → (2
· 𝑦) ∈
ℂ) |
173 | 172 | adantl 475 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (2 · 𝑦) ∈
ℂ) |
174 | 173 | mul02d 10574 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (0 · (2
· 𝑦)) =
0) |
175 | 174 | oveq2d 6938 |
. . . . . . . 8
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (1 − (0
· (2 · 𝑦))) =
(1 − 0)) |
176 | 175, 56 | syl6eq 2829 |
. . . . . . 7
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (1 − (0
· (2 · 𝑦))) =
1) |
177 | | subcl 10621 |
. . . . . . . . . . . 12
⊢ (((2
· 𝑦) ∈ ℂ
∧ 1 ∈ ℂ) → ((2 · 𝑦) − 1) ∈ ℂ) |
178 | 173, 151,
177 | sylancl 580 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → ((2 · 𝑦) − 1) ∈
ℂ) |
179 | 151, 178,
154 | sylancr 581 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (1 − ((2
· 𝑦) − 1))
∈ ℂ) |
180 | 179 | mul02d 10574 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (0 · (1
− ((2 · 𝑦)
− 1))) = 0) |
181 | 180 | oveq2d 6938 |
. . . . . . . 8
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (1 − (0
· (1 − ((2 · 𝑦) − 1)))) = (1 −
0)) |
182 | 181, 56 | syl6eq 2829 |
. . . . . . 7
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (1 − (0
· (1 − ((2 · 𝑦) − 1)))) = 1) |
183 | 176, 182 | ifeq12d 4326 |
. . . . . 6
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → if(𝑦 ≤ (1 / 2), (1 − (0 · (2
· 𝑦))), (1 −
(0 · (1 − ((2 · 𝑦) − 1))))) = if(𝑦 ≤ (1 / 2), 1, 1)) |
184 | | ifid 4345 |
. . . . . 6
⊢ if(𝑦 ≤ (1 / 2), 1, 1) =
1 |
185 | 183, 184 | syl6eq 2829 |
. . . . 5
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → if(𝑦 ≤ (1 / 2), (1 − (0 · (2
· 𝑦))), (1 −
(0 · (1 − ((2 · 𝑦) − 1))))) = 1) |
186 | 185 | fveq2d 6450 |
. . . 4
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (0 · (2
· 𝑦))), (1 −
(0 · (1 − ((2 · 𝑦) − 1)))))) = (𝐹‘1)) |
187 | | simpl 476 |
. . . . . . . . 9
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → 𝑠 = 𝑦) |
188 | 187 | breq1d 4896 |
. . . . . . . 8
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → (𝑠 ≤ (1 / 2) ↔ 𝑦 ≤ (1 / 2))) |
189 | | simpr 479 |
. . . . . . . . . . . 12
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → 𝑡 = 1) |
190 | 189 | oveq2d 6938 |
. . . . . . . . . . 11
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → (1 − 𝑡) = (1 − 1)) |
191 | 190, 11 | syl6eq 2829 |
. . . . . . . . . 10
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → (1 − 𝑡) = 0) |
192 | 187 | oveq2d 6938 |
. . . . . . . . . 10
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → (2 · 𝑠) = (2 · 𝑦)) |
193 | 191, 192 | oveq12d 6940 |
. . . . . . . . 9
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → ((1 − 𝑡) · (2 · 𝑠)) = (0 · (2 · 𝑦))) |
194 | 193 | oveq2d 6938 |
. . . . . . . 8
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → (1 − ((1 − 𝑡) · (2 · 𝑠))) = (1 − (0 · (2
· 𝑦)))) |
195 | 192 | oveq1d 6937 |
. . . . . . . . . . 11
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → ((2 · 𝑠) − 1) = ((2 · 𝑦) − 1)) |
196 | 195 | oveq2d 6938 |
. . . . . . . . . 10
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → (1 − ((2 · 𝑠) − 1)) = (1 − ((2
· 𝑦) −
1))) |
197 | 191, 196 | oveq12d 6940 |
. . . . . . . . 9
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1))) = (0 · (1
− ((2 · 𝑦)
− 1)))) |
198 | 197 | oveq2d 6938 |
. . . . . . . 8
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → (1 − ((1 − 𝑡) · (1 − ((2
· 𝑠) − 1)))) =
(1 − (0 · (1 − ((2 · 𝑦) − 1))))) |
199 | 188, 194,
198 | ifbieq12d 4333 |
. . . . . . 7
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 −
𝑡) · (1 − ((2
· 𝑠) − 1)))))
= if(𝑦 ≤ (1 / 2), (1
− (0 · (2 · 𝑦))), (1 − (0 · (1 − ((2
· 𝑦) −
1)))))) |
200 | 199 | fveq2d 6450 |
. . . . . 6
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → (𝐹‘if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 −
𝑡) · (1 − ((2
· 𝑠) − 1))))))
= (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (0
· (2 · 𝑦))),
(1 − (0 · (1 − ((2 · 𝑦) − 1))))))) |
201 | | fvex 6459 |
. . . . . 6
⊢ (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (0 · (2
· 𝑦))), (1 −
(0 · (1 − ((2 · 𝑦) − 1)))))) ∈ V |
202 | 200, 30, 201 | ovmpt2a 7068 |
. . . . 5
⊢ ((𝑦 ∈ (0[,]1) ∧ 1 ∈
(0[,]1)) → (𝑦𝐻1) = (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (0 · (2
· 𝑦))), (1 −
(0 · (1 − ((2 · 𝑦) − 1))))))) |
203 | 102, 9, 202 | sylancl 580 |
. . . 4
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (𝑦𝐻1) = (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (0 · (2
· 𝑦))), (1 −
(0 · (1 − ((2 · 𝑦) − 1))))))) |
204 | 26 | fveq1i 6447 |
. . . . 5
⊢ (𝑃‘𝑦) = (((0[,]1) × {(𝐹‘1)})‘𝑦) |
205 | | fvex 6459 |
. . . . . . 7
⊢ (𝐹‘1) ∈
V |
206 | 205 | fvconst2 6741 |
. . . . . 6
⊢ (𝑦 ∈ (0[,]1) → (((0[,]1)
× {(𝐹‘1)})‘𝑦) = (𝐹‘1)) |
207 | 206 | adantl 475 |
. . . . 5
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (((0[,]1) ×
{(𝐹‘1)})‘𝑦) = (𝐹‘1)) |
208 | 204, 207 | syl5eq 2825 |
. . . 4
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (𝑃‘𝑦) = (𝐹‘1)) |
209 | 186, 203,
208 | 3eqtr4d 2823 |
. . 3
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (𝑦𝐻1) = (𝑃‘𝑦)) |
210 | | simpl 476 |
. . . . . . . . . . 11
⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → 𝑠 = 0) |
211 | 210, 40 | syl6eqbr 4925 |
. . . . . . . . . 10
⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → 𝑠 ≤ (1 / 2)) |
212 | 211 | iftrued 4314 |
. . . . . . . . 9
⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 −
𝑡) · (1 − ((2
· 𝑠) − 1)))))
= (1 − ((1 − 𝑡)
· (2 · 𝑠)))) |
213 | | simpr 479 |
. . . . . . . . . . . 12
⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → 𝑡 = 𝑦) |
214 | 213 | oveq2d 6938 |
. . . . . . . . . . 11
⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → (1 − 𝑡) = (1 − 𝑦)) |
215 | 210 | oveq2d 6938 |
. . . . . . . . . . . 12
⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → (2 · 𝑠) = (2 · 0)) |
216 | | 2t0e0 11551 |
. . . . . . . . . . . 12
⊢ (2
· 0) = 0 |
217 | 215, 216 | syl6eq 2829 |
. . . . . . . . . . 11
⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → (2 · 𝑠) = 0) |
218 | 214, 217 | oveq12d 6940 |
. . . . . . . . . 10
⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → ((1 − 𝑡) · (2 · 𝑠)) = ((1 − 𝑦) · 0)) |
219 | 218 | oveq2d 6938 |
. . . . . . . . 9
⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → (1 − ((1 − 𝑡) · (2 · 𝑠))) = (1 − ((1 −
𝑦) ·
0))) |
220 | 212, 219 | eqtrd 2813 |
. . . . . . . 8
⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 −
𝑡) · (1 − ((2
· 𝑠) − 1)))))
= (1 − ((1 − 𝑦)
· 0))) |
221 | 220 | fveq2d 6450 |
. . . . . . 7
⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → (𝐹‘if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 −
𝑡) · (1 − ((2
· 𝑠) − 1))))))
= (𝐹‘(1 − ((1
− 𝑦) ·
0)))) |
222 | | fvex 6459 |
. . . . . . 7
⊢ (𝐹‘(1 − ((1 −
𝑦) · 0))) ∈
V |
223 | 221, 30, 222 | ovmpt2a 7068 |
. . . . . 6
⊢ ((0
∈ (0[,]1) ∧ 𝑦
∈ (0[,]1)) → (0𝐻𝑦) = (𝐹‘(1 − ((1 − 𝑦) ·
0)))) |
224 | 103, 223 | mpan 680 |
. . . . 5
⊢ (𝑦 ∈ (0[,]1) → (0𝐻𝑦) = (𝐹‘(1 − ((1 − 𝑦) ·
0)))) |
225 | | subcl 10621 |
. . . . . . . . . 10
⊢ ((1
∈ ℂ ∧ 𝑦
∈ ℂ) → (1 − 𝑦) ∈ ℂ) |
226 | 151, 170,
225 | sylancr 581 |
. . . . . . . . 9
⊢ (𝑦 ∈ (0[,]1) → (1
− 𝑦) ∈
ℂ) |
227 | 226 | mul01d 10575 |
. . . . . . . 8
⊢ (𝑦 ∈ (0[,]1) → ((1
− 𝑦) · 0) =
0) |
228 | 227 | oveq2d 6938 |
. . . . . . 7
⊢ (𝑦 ∈ (0[,]1) → (1
− ((1 − 𝑦)
· 0)) = (1 − 0)) |
229 | 228, 56 | syl6eq 2829 |
. . . . . 6
⊢ (𝑦 ∈ (0[,]1) → (1
− ((1 − 𝑦)
· 0)) = 1) |
230 | 229 | fveq2d 6450 |
. . . . 5
⊢ (𝑦 ∈ (0[,]1) → (𝐹‘(1 − ((1 −
𝑦) · 0))) = (𝐹‘1)) |
231 | 224, 230 | eqtrd 2813 |
. . . 4
⊢ (𝑦 ∈ (0[,]1) → (0𝐻𝑦) = (𝐹‘1)) |
232 | 8, 6 | pco0 23221 |
. . . . 5
⊢ (𝐹 ∈ (II Cn 𝐽) → ((𝐺(*𝑝‘𝐽)𝐹)‘0) = (𝐺‘0)) |
233 | | oveq2 6930 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (1 − 𝑥) = (1 −
0)) |
234 | 233, 56 | syl6eq 2829 |
. . . . . . . 8
⊢ (𝑥 = 0 → (1 − 𝑥) = 1) |
235 | 234 | fveq2d 6450 |
. . . . . . 7
⊢ (𝑥 = 0 → (𝐹‘(1 − 𝑥)) = (𝐹‘1)) |
236 | 235, 1, 205 | fvmpt 6542 |
. . . . . 6
⊢ (0 ∈
(0[,]1) → (𝐺‘0)
= (𝐹‘1)) |
237 | 103, 236 | ax-mp 5 |
. . . . 5
⊢ (𝐺‘0) = (𝐹‘1) |
238 | 232, 237 | syl6req 2830 |
. . . 4
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐹‘1) = ((𝐺(*𝑝‘𝐽)𝐹)‘0)) |
239 | 231, 238 | sylan9eqr 2835 |
. . 3
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (0𝐻𝑦) = ((𝐺(*𝑝‘𝐽)𝐹)‘0)) |
240 | 37, 41 | ltnlei 10497 |
. . . . . . . . . . . 12
⊢ ((1 / 2)
< 1 ↔ ¬ 1 ≤ (1 / 2)) |
241 | 42, 240 | mpbi 222 |
. . . . . . . . . . 11
⊢ ¬ 1
≤ (1 / 2) |
242 | | simpl 476 |
. . . . . . . . . . . 12
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → 𝑠 = 1) |
243 | 242 | breq1d 4896 |
. . . . . . . . . . 11
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → (𝑠 ≤ (1 / 2) ↔ 1 ≤ (1 /
2))) |
244 | 241, 243 | mtbiri 319 |
. . . . . . . . . 10
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → ¬ 𝑠 ≤ (1 / 2)) |
245 | 244 | iffalsed 4317 |
. . . . . . . . 9
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 −
𝑡) · (1 − ((2
· 𝑠) − 1)))))
= (1 − ((1 − 𝑡)
· (1 − ((2 · 𝑠) − 1))))) |
246 | | simpr 479 |
. . . . . . . . . . . 12
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → 𝑡 = 𝑦) |
247 | 246 | oveq2d 6938 |
. . . . . . . . . . 11
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → (1 − 𝑡) = (1 − 𝑦)) |
248 | 242 | oveq2d 6938 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → (2 · 𝑠) = (2 · 1)) |
249 | | 2t1e2 11545 |
. . . . . . . . . . . . . . . 16
⊢ (2
· 1) = 2 |
250 | 248, 249 | syl6eq 2829 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → (2 · 𝑠) = 2) |
251 | 250 | oveq1d 6937 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → ((2 · 𝑠) − 1) = (2 −
1)) |
252 | | 2m1e1 11508 |
. . . . . . . . . . . . . 14
⊢ (2
− 1) = 1 |
253 | 251, 252 | syl6eq 2829 |
. . . . . . . . . . . . 13
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → ((2 · 𝑠) − 1) = 1) |
254 | 253 | oveq2d 6938 |
. . . . . . . . . . . 12
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → (1 − ((2 · 𝑠) − 1)) = (1 −
1)) |
255 | 254, 11 | syl6eq 2829 |
. . . . . . . . . . 11
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → (1 − ((2 · 𝑠) − 1)) =
0) |
256 | 247, 255 | oveq12d 6940 |
. . . . . . . . . 10
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1))) = ((1 −
𝑦) ·
0)) |
257 | 256 | oveq2d 6938 |
. . . . . . . . 9
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → (1 − ((1 − 𝑡) · (1 − ((2
· 𝑠) − 1)))) =
(1 − ((1 − 𝑦)
· 0))) |
258 | 245, 257 | eqtrd 2813 |
. . . . . . . 8
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 −
𝑡) · (1 − ((2
· 𝑠) − 1)))))
= (1 − ((1 − 𝑦)
· 0))) |
259 | 258 | fveq2d 6450 |
. . . . . . 7
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → (𝐹‘if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 −
𝑡) · (1 − ((2
· 𝑠) − 1))))))
= (𝐹‘(1 − ((1
− 𝑦) ·
0)))) |
260 | 259, 30, 222 | ovmpt2a 7068 |
. . . . . 6
⊢ ((1
∈ (0[,]1) ∧ 𝑦
∈ (0[,]1)) → (1𝐻𝑦) = (𝐹‘(1 − ((1 − 𝑦) ·
0)))) |
261 | 9, 260 | mpan 680 |
. . . . 5
⊢ (𝑦 ∈ (0[,]1) → (1𝐻𝑦) = (𝐹‘(1 − ((1 − 𝑦) ·
0)))) |
262 | 261, 230 | eqtrd 2813 |
. . . 4
⊢ (𝑦 ∈ (0[,]1) → (1𝐻𝑦) = (𝐹‘1)) |
263 | 8, 6 | pco1 23222 |
. . . . 5
⊢ (𝐹 ∈ (II Cn 𝐽) → ((𝐺(*𝑝‘𝐽)𝐹)‘1) = (𝐹‘1)) |
264 | 263 | eqcomd 2783 |
. . . 4
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐹‘1) = ((𝐺(*𝑝‘𝐽)𝐹)‘1)) |
265 | 262, 264 | sylan9eqr 2835 |
. . 3
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (1𝐻𝑦) = ((𝐺(*𝑝‘𝐽)𝐹)‘1)) |
266 | 17, 29, 101, 168, 209, 239, 265 | isphtpy2d 23194 |
. 2
⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐻 ∈ ((𝐺(*𝑝‘𝐽)𝐹)(PHtpy‘𝐽)𝑃)) |
267 | 266 | ne0d 4149 |
. . 3
⊢ (𝐹 ∈ (II Cn 𝐽) → ((𝐺(*𝑝‘𝐽)𝐹)(PHtpy‘𝐽)𝑃) ≠ ∅) |
268 | | isphtpc 23201 |
. . 3
⊢ ((𝐺(*𝑝‘𝐽)𝐹)( ≃ph‘𝐽)𝑃 ↔ ((𝐺(*𝑝‘𝐽)𝐹) ∈ (II Cn 𝐽) ∧ 𝑃 ∈ (II Cn 𝐽) ∧ ((𝐺(*𝑝‘𝐽)𝐹)(PHtpy‘𝐽)𝑃) ≠ ∅)) |
269 | 17, 29, 267, 268 | syl3anbrc 1400 |
. 2
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐺(*𝑝‘𝐽)𝐹)( ≃ph‘𝐽)𝑃) |
270 | 266, 269 | jca 507 |
1
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐻 ∈ ((𝐺(*𝑝‘𝐽)𝐹)(PHtpy‘𝐽)𝑃) ∧ (𝐺(*𝑝‘𝐽)𝐹)( ≃ph‘𝐽)𝑃)) |