| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | pcorev.1 | . . . . 5
⊢ 𝐺 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥))) | 
| 2 |  | iitopon 24905 | . . . . . . 7
⊢ II ∈
(TopOn‘(0[,]1)) | 
| 3 | 2 | a1i 11 | . . . . . 6
⊢ (𝐹 ∈ (II Cn 𝐽) → II ∈
(TopOn‘(0[,]1))) | 
| 4 |  | iirevcn 24957 | . . . . . . 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 23672 | . . . . 5
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥))) ∈ (II Cn 𝐽)) | 
| 8 | 1, 7 | eqeltrid 2845 | . . . 4
⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐺 ∈ (II Cn 𝐽)) | 
| 9 |  | 1elunit 13510 | . . . . 5
⊢ 1 ∈
(0[,]1) | 
| 10 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑥 = 1 → (1 − 𝑥) = (1 −
1)) | 
| 11 |  | 1m1e0 12338 | . . . . . . . 8
⊢ (1
− 1) = 0 | 
| 12 | 10, 11 | eqtrdi 2793 | . . . . . . 7
⊢ (𝑥 = 1 → (1 − 𝑥) = 0) | 
| 13 | 12 | fveq2d 6910 | . . . . . 6
⊢ (𝑥 = 1 → (𝐹‘(1 − 𝑥)) = (𝐹‘0)) | 
| 14 |  | fvex 6919 | . . . . . 6
⊢ (𝐹‘0) ∈
V | 
| 15 | 13, 1, 14 | fvmpt 7016 | . . . . 5
⊢ (1 ∈
(0[,]1) → (𝐺‘1)
= (𝐹‘0)) | 
| 16 | 9, 15 | mp1i 13 | . . . 4
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐺‘1) = (𝐹‘0)) | 
| 17 | 8, 6, 16 | pcocn 25050 | . . 3
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐺(*𝑝‘𝐽)𝐹) ∈ (II Cn 𝐽)) | 
| 18 |  | cntop2 23249 | . . . . . 6
⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐽 ∈ Top) | 
| 19 |  | toptopon2 22924 | . . . . . 6
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) | 
| 20 | 18, 19 | sylib 218 | . . . . 5
⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐽 ∈ (TopOn‘∪ 𝐽)) | 
| 21 |  | iiuni 24907 | . . . . . . 7
⊢ (0[,]1) =
∪ II | 
| 22 |  | eqid 2737 | . . . . . . 7
⊢ ∪ 𝐽 =
∪ 𝐽 | 
| 23 | 21, 22 | cnf 23254 | . . . . . 6
⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐹:(0[,]1)⟶∪
𝐽) | 
| 24 |  | ffvelcdm 7101 | . . . . . 6
⊢ ((𝐹:(0[,]1)⟶∪ 𝐽
∧ 1 ∈ (0[,]1)) → (𝐹‘1) ∈ ∪ 𝐽) | 
| 25 | 23, 9, 24 | sylancl 586 | . . . . 5
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐹‘1) ∈ ∪ 𝐽) | 
| 26 |  | pcorev.2 | . . . . . 6
⊢ 𝑃 = ((0[,]1) × {(𝐹‘1)}) | 
| 27 | 26 | pcoptcl 25054 | . . . . 5
⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽)
∧ (𝐹‘1) ∈
∪ 𝐽) → (𝑃 ∈ (II Cn 𝐽) ∧ (𝑃‘0) = (𝐹‘1) ∧ (𝑃‘1) = (𝐹‘1))) | 
| 28 | 20, 25, 27 | syl2anc 584 | . . . 4
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑃 ∈ (II Cn 𝐽) ∧ (𝑃‘0) = (𝐹‘1) ∧ (𝑃‘1) = (𝐹‘1))) | 
| 29 | 28 | simp1d 1143 | . . 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 2737 | . . . . . 6
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) | 
| 32 |  | eqid 2737 | . . . . . 6
⊢
((topGen‘ran (,)) ↾t (0[,](1 / 2))) =
((topGen‘ran (,)) ↾t (0[,](1 / 2))) | 
| 33 |  | eqid 2737 | . . . . . 6
⊢
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) =
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) | 
| 34 |  | dfii2 24908 | . . . . . 6
⊢ II =
((topGen‘ran (,)) ↾t (0[,]1)) | 
| 35 |  | 0red 11264 | . . . . . 6
⊢ (𝐹 ∈ (II Cn 𝐽) → 0 ∈ ℝ) | 
| 36 |  | 1red 11262 | . . . . . 6
⊢ (𝐹 ∈ (II Cn 𝐽) → 1 ∈ ℝ) | 
| 37 |  | halfre 12480 | . . . . . . . 8
⊢ (1 / 2)
∈ ℝ | 
| 38 |  | halfge0 12483 | . . . . . . . 8
⊢ 0 ≤ (1
/ 2) | 
| 39 |  | 1re 11261 | . . . . . . . . 9
⊢ 1 ∈
ℝ | 
| 40 |  | halflt1 12484 | . . . . . . . . 9
⊢ (1 / 2)
< 1 | 
| 41 | 37, 39, 40 | ltleii 11384 | . . . . . . . 8
⊢ (1 / 2)
≤ 1 | 
| 42 |  | elicc01 13506 | . . . . . . . 8
⊢ ((1 / 2)
∈ (0[,]1) ↔ ((1 / 2) ∈ ℝ ∧ 0 ≤ (1 / 2) ∧ (1 /
2) ≤ 1)) | 
| 43 | 37, 38, 41, 42 | mpbir3an 1342 | . . . . . . 7
⊢ (1 / 2)
∈ (0[,]1) | 
| 44 | 43 | a1i 11 | . . . . . 6
⊢ (𝐹 ∈ (II Cn 𝐽) → (1 / 2) ∈
(0[,]1)) | 
| 45 |  | simprl 771 | . . . . . . . . . . 11
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → 𝑠 = (1 / 2)) | 
| 46 | 45 | oveq2d 7447 | . . . . . . . . . 10
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → (2 · 𝑠) = (2 · (1 /
2))) | 
| 47 |  | 2cn 12341 | . . . . . . . . . . 11
⊢ 2 ∈
ℂ | 
| 48 |  | 2ne0 12370 | . . . . . . . . . . 11
⊢ 2 ≠
0 | 
| 49 | 47, 48 | recidi 11998 | . . . . . . . . . 10
⊢ (2
· (1 / 2)) = 1 | 
| 50 | 46, 49 | eqtrdi 2793 | . . . . . . . . 9
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → (2 · 𝑠) = 1) | 
| 51 | 50 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → ((2 · 𝑠) − 1) = (1 −
1)) | 
| 52 | 51, 11 | eqtrdi 2793 | . . . . . . . . . . 11
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → ((2 · 𝑠) − 1) =
0) | 
| 53 | 52 | oveq2d 7447 | . . . . . . . . . 10
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → (1 − ((2
· 𝑠) − 1)) =
(1 − 0)) | 
| 54 |  | 1m0e1 12387 | . . . . . . . . . 10
⊢ (1
− 0) = 1 | 
| 55 | 53, 54 | eqtrdi 2793 | . . . . . . . . 9
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → (1 − ((2
· 𝑠) − 1)) =
1) | 
| 56 | 50, 55 | eqtr4d 2780 | . . . . . . . 8
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → (2 · 𝑠) = (1 − ((2 ·
𝑠) −
1))) | 
| 57 | 56 | oveq2d 7447 | . . . . . . 7
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → ((1 − 𝑡) · (2 · 𝑠)) = ((1 − 𝑡) · (1 − ((2
· 𝑠) −
1)))) | 
| 58 | 57 | oveq2d 7447 | . . . . . 6
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑠 = (1 / 2) ∧ 𝑡 ∈ (0[,]1))) → (1 − ((1
− 𝑡) · (2
· 𝑠))) = (1 −
((1 − 𝑡) · (1
− ((2 · 𝑠)
− 1))))) | 
| 59 |  | retopon 24784 | . . . . . . . . 9
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) | 
| 60 |  | 0re 11263 | . . . . . . . . . 10
⊢ 0 ∈
ℝ | 
| 61 |  | iccssre 13469 | . . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ (1 / 2) ∈ ℝ) → (0[,](1 / 2)) ⊆
ℝ) | 
| 62 | 60, 37, 61 | mp2an 692 | . . . . . . . . 9
⊢ (0[,](1 /
2)) ⊆ ℝ | 
| 63 |  | resttopon 23169 | . . . . . . . . 9
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 /
2)) ⊆ ℝ) → ((topGen‘ran (,)) ↾t (0[,](1
/ 2))) ∈ (TopOn‘(0[,](1 / 2)))) | 
| 64 | 59, 62, 63 | mp2an 692 | . . . . . . . 8
⊢
((topGen‘ran (,)) ↾t (0[,](1 / 2))) ∈
(TopOn‘(0[,](1 / 2))) | 
| 65 | 64 | a1i 11 | . . . . . . 7
⊢ (𝐹 ∈ (II Cn 𝐽) → ((topGen‘ran (,))
↾t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 /
2)))) | 
| 66 | 65, 3 | cnmpt2nd 23677 | . . . . . . . . 9
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ (0[,](1 / 2)), 𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((((topGen‘ran (,))
↾t (0[,](1 / 2))) ×t II) Cn
II)) | 
| 67 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑥 = 𝑡 → (1 − 𝑥) = (1 − 𝑡)) | 
| 68 | 65, 3, 66, 3, 5, 67 | cnmpt21 23679 | . . . . . . . 8
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ (0[,](1 / 2)), 𝑡 ∈ (0[,]1) ↦ (1 − 𝑡)) ∈ ((((topGen‘ran
(,)) ↾t (0[,](1 / 2))) ×t II) Cn
II)) | 
| 69 | 65, 3 | cnmpt1st 23676 | . . . . . . . . 9
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ (0[,](1 / 2)), 𝑡 ∈ (0[,]1) ↦ 𝑠) ∈ ((((topGen‘ran (,))
↾t (0[,](1 / 2))) ×t II) Cn
((topGen‘ran (,)) ↾t (0[,](1 / 2))))) | 
| 70 | 32 | iihalf1cn 24959 | . . . . . . . . . 10
⊢ (𝑥 ∈ (0[,](1 / 2)) ↦ (2
· 𝑥)) ∈
(((topGen‘ran (,)) ↾t (0[,](1 / 2))) Cn
II) | 
| 71 | 70 | a1i 11 | . . . . . . . . 9
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑥 ∈ (0[,](1 / 2)) ↦ (2 ·
𝑥)) ∈
(((topGen‘ran (,)) ↾t (0[,](1 / 2))) Cn
II)) | 
| 72 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑥 = 𝑠 → (2 · 𝑥) = (2 · 𝑠)) | 
| 73 | 65, 3, 69, 65, 71, 72 | cnmpt21 23679 | . . . . . . . 8
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ (0[,](1 / 2)), 𝑡 ∈ (0[,]1) ↦ (2 · 𝑠)) ∈ ((((topGen‘ran
(,)) ↾t (0[,](1 / 2))) ×t II) Cn
II)) | 
| 74 |  | iimulcn 24967 | . . . . . . . . 9
⊢ (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝑥 · 𝑦)) ∈ ((II ×t II) Cn
II) | 
| 75 | 74 | a1i 11 | . . . . . . . 8
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝑥 · 𝑦)) ∈ ((II ×t II) Cn
II)) | 
| 76 |  | oveq12 7440 | . . . . . . . 8
⊢ ((𝑥 = (1 − 𝑡) ∧ 𝑦 = (2 · 𝑠)) → (𝑥 · 𝑦) = ((1 − 𝑡) · (2 · 𝑠))) | 
| 77 | 65, 3, 68, 73, 3, 3, 75, 76 | cnmpt22 23682 | . . . . . . 7
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ (0[,](1 / 2)), 𝑡 ∈ (0[,]1) ↦ ((1 − 𝑡) · (2 · 𝑠))) ∈ ((((topGen‘ran
(,)) ↾t (0[,](1 / 2))) ×t II) Cn
II)) | 
| 78 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑥 = ((1 − 𝑡) · (2 · 𝑠)) → (1 − 𝑥) = (1 − ((1 − 𝑡) · (2 · 𝑠)))) | 
| 79 | 65, 3, 77, 3, 5, 78 | cnmpt21 23679 | . . . . . 6
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ (0[,](1 / 2)), 𝑡 ∈ (0[,]1) ↦ (1 − ((1
− 𝑡) · (2
· 𝑠)))) ∈
((((topGen‘ran (,)) ↾t (0[,](1 / 2)))
×t II) Cn II)) | 
| 80 |  | iccssre 13469 | . . . . . . . . . 10
⊢ (((1 / 2)
∈ ℝ ∧ 1 ∈ ℝ) → ((1 / 2)[,]1) ⊆
ℝ) | 
| 81 | 37, 39, 80 | mp2an 692 | . . . . . . . . 9
⊢ ((1 /
2)[,]1) ⊆ ℝ | 
| 82 |  | resttopon 23169 | . . . . . . . . 9
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 /
2)[,]1) ⊆ ℝ) → ((topGen‘ran (,)) ↾t ((1
/ 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1))) | 
| 83 | 59, 81, 82 | mp2an 692 | . . . . . . . 8
⊢
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ∈
(TopOn‘((1 / 2)[,]1)) | 
| 84 | 83 | a1i 11 | . . . . . . 7
⊢ (𝐹 ∈ (II Cn 𝐽) → ((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ∈ (TopOn‘((1 /
2)[,]1))) | 
| 85 | 84, 3 | cnmpt2nd 23677 | . . . . . . . . 9
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ ((1 / 2)[,]1), 𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ×t II) Cn
II)) | 
| 86 | 84, 3, 85, 3, 5, 67 | cnmpt21 23679 | . . . . . . . 8
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ ((1 / 2)[,]1), 𝑡 ∈ (0[,]1) ↦ (1 − 𝑡)) ∈ ((((topGen‘ran
(,)) ↾t ((1 / 2)[,]1)) ×t II) Cn
II)) | 
| 87 | 84, 3 | cnmpt1st 23676 | . . . . . . . . . 10
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ ((1 / 2)[,]1), 𝑡 ∈ (0[,]1) ↦ 𝑠) ∈ ((((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ×t II) Cn
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)))) | 
| 88 | 33 | iihalf2cn 24962 | . . . . . . . . . . 11
⊢ (𝑥 ∈ ((1 / 2)[,]1) ↦
((2 · 𝑥) − 1))
∈ (((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) Cn
II) | 
| 89 | 88 | a1i 11 | . . . . . . . . . 10
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑥 ∈ ((1 / 2)[,]1) ↦ ((2 ·
𝑥) − 1)) ∈
(((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) Cn
II)) | 
| 90 | 72 | oveq1d 7446 | . . . . . . . . . 10
⊢ (𝑥 = 𝑠 → ((2 · 𝑥) − 1) = ((2 · 𝑠) − 1)) | 
| 91 | 84, 3, 87, 84, 89, 90 | cnmpt21 23679 | . . . . . . . . 9
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ ((1 / 2)[,]1), 𝑡 ∈ (0[,]1) ↦ ((2 · 𝑠) − 1)) ∈
((((topGen‘ran (,)) ↾t ((1 / 2)[,]1))
×t II) Cn II)) | 
| 92 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑥 = ((2 · 𝑠) − 1) → (1 −
𝑥) = (1 − ((2
· 𝑠) −
1))) | 
| 93 | 84, 3, 91, 3, 5, 92 | cnmpt21 23679 | . . . . . . . 8
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ ((1 / 2)[,]1), 𝑡 ∈ (0[,]1) ↦ (1 − ((2
· 𝑠) − 1)))
∈ ((((topGen‘ran (,)) ↾t ((1 / 2)[,]1))
×t II) Cn II)) | 
| 94 |  | oveq12 7440 | . . . . . . . 8
⊢ ((𝑥 = (1 − 𝑡) ∧ 𝑦 = (1 − ((2 · 𝑠) − 1))) → (𝑥 · 𝑦) = ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1)))) | 
| 95 | 84, 3, 86, 93, 3, 3, 75, 94 | cnmpt22 23682 | . . . . . . 7
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ ((1 / 2)[,]1), 𝑡 ∈ (0[,]1) ↦ ((1 − 𝑡) · (1 − ((2
· 𝑠) − 1))))
∈ ((((topGen‘ran (,)) ↾t ((1 / 2)[,]1))
×t II) Cn II)) | 
| 96 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑥 = ((1 − 𝑡) · (1 − ((2
· 𝑠) − 1)))
→ (1 − 𝑥) = (1
− ((1 − 𝑡)
· (1 − ((2 · 𝑠) − 1))))) | 
| 97 | 84, 3, 95, 3, 5, 96 | cnmpt21 23679 | . . . . . 6
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ ((1 / 2)[,]1), 𝑡 ∈ (0[,]1) ↦ (1 − ((1
− 𝑡) · (1
− ((2 · 𝑠)
− 1))))) ∈ ((((topGen‘ran (,)) ↾t ((1 /
2)[,]1)) ×t II) Cn II)) | 
| 98 | 31, 32, 33, 34, 35, 36, 44, 3, 58, 79, 97 | cnmpopc 24955 | . . . . 5
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 −
𝑡) · (1 − ((2
· 𝑠) − 1))))))
∈ ((II ×t II) Cn II)) | 
| 99 | 3, 3, 98, 6 | cnmpt21f 23680 | . . . 4
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝑠 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ (𝐹‘if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 −
𝑡) · (1 − ((2
· 𝑠) −
1))))))) ∈ ((II ×t II) Cn 𝐽)) | 
| 100 | 30, 99 | eqeltrid 2845 | . . 3
⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐻 ∈ ((II ×t II) Cn
𝐽)) | 
| 101 |  | simpr 484 | . . . . 5
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → 𝑦 ∈ (0[,]1)) | 
| 102 |  | 0elunit 13509 | . . . . 5
⊢ 0 ∈
(0[,]1) | 
| 103 |  | simpl 482 | . . . . . . . . 9
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → 𝑠 = 𝑦) | 
| 104 | 103 | breq1d 5153 | . . . . . . . 8
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → (𝑠 ≤ (1 / 2) ↔ 𝑦 ≤ (1 / 2))) | 
| 105 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → 𝑡 = 0) | 
| 106 | 105 | oveq2d 7447 | . . . . . . . . . . 11
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → (1 − 𝑡) = (1 − 0)) | 
| 107 | 106, 54 | eqtrdi 2793 | . . . . . . . . . 10
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → (1 − 𝑡) = 1) | 
| 108 | 103 | oveq2d 7447 | . . . . . . . . . 10
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → (2 · 𝑠) = (2 · 𝑦)) | 
| 109 | 107, 108 | oveq12d 7449 | . . . . . . . . 9
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → ((1 − 𝑡) · (2 · 𝑠)) = (1 · (2 · 𝑦))) | 
| 110 | 109 | oveq2d 7447 | . . . . . . . 8
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → (1 − ((1 − 𝑡) · (2 · 𝑠))) = (1 − (1 · (2
· 𝑦)))) | 
| 111 | 108 | oveq1d 7446 | . . . . . . . . . . 11
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → ((2 · 𝑠) − 1) = ((2 · 𝑦) − 1)) | 
| 112 | 111 | oveq2d 7447 | . . . . . . . . . 10
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → (1 − ((2 · 𝑠) − 1)) = (1 − ((2
· 𝑦) −
1))) | 
| 113 | 107, 112 | oveq12d 7449 | . . . . . . . . 9
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1))) = (1 · (1
− ((2 · 𝑦)
− 1)))) | 
| 114 | 113 | oveq2d 7447 | . . . . . . . 8
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → (1 − ((1 − 𝑡) · (1 − ((2
· 𝑠) − 1)))) =
(1 − (1 · (1 − ((2 · 𝑦) − 1))))) | 
| 115 | 104, 110,
114 | ifbieq12d 4554 | . . . . . . 7
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 −
𝑡) · (1 − ((2
· 𝑠) − 1)))))
= if(𝑦 ≤ (1 / 2), (1
− (1 · (2 · 𝑦))), (1 − (1 · (1 − ((2
· 𝑦) −
1)))))) | 
| 116 | 115 | fveq2d 6910 | . . . . . 6
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 0) → (𝐹‘if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 −
𝑡) · (1 − ((2
· 𝑠) − 1))))))
= (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (1
· (2 · 𝑦))),
(1 − (1 · (1 − ((2 · 𝑦) − 1))))))) | 
| 117 |  | fvex 6919 | . . . . . 6
⊢ (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (1 · (2
· 𝑦))), (1 −
(1 · (1 − ((2 · 𝑦) − 1)))))) ∈ V | 
| 118 | 116, 30, 117 | ovmpoa 7588 | . . . . 5
⊢ ((𝑦 ∈ (0[,]1) ∧ 0 ∈
(0[,]1)) → (𝑦𝐻0) = (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (1 · (2
· 𝑦))), (1 −
(1 · (1 − ((2 · 𝑦) − 1))))))) | 
| 119 | 101, 102,
118 | sylancl 586 | . . . 4
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (𝑦𝐻0) = (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (1 · (2
· 𝑦))), (1 −
(1 · (1 − ((2 · 𝑦) − 1))))))) | 
| 120 |  | iftrue 4531 | . . . . . . . 8
⊢ (𝑦 ≤ (1 / 2) → if(𝑦 ≤ (1 / 2), (1 − (1
· (2 · 𝑦))),
(1 − (1 · (1 − ((2 · 𝑦) − 1))))) = (1 − (1 · (2
· 𝑦)))) | 
| 121 | 120 | adantl 481 | . . . . . . 7
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) ∧ 𝑦 ≤ (1 / 2)) → if(𝑦 ≤ (1 / 2), (1 − (1 · (2
· 𝑦))), (1 −
(1 · (1 − ((2 · 𝑦) − 1))))) = (1 − (1 · (2
· 𝑦)))) | 
| 122 | 121 | fveq2d 6910 | . . . . . 6
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) ∧ 𝑦 ≤ (1 / 2)) → (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (1 · (2
· 𝑦))), (1 −
(1 · (1 − ((2 · 𝑦) − 1)))))) = (𝐹‘(1 − (1 · (2 ·
𝑦))))) | 
| 123 |  | elii1 24964 | . . . . . . . 8
⊢ (𝑦 ∈ (0[,](1 / 2)) ↔
(𝑦 ∈ (0[,]1) ∧
𝑦 ≤ (1 /
2))) | 
| 124 | 8, 6 | pcoval1 25046 | . . . . . . . . 9
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,](1 / 2))) → ((𝐺(*𝑝‘𝐽)𝐹)‘𝑦) = (𝐺‘(2 · 𝑦))) | 
| 125 |  | iihalf1 24958 | . . . . . . . . . . 11
⊢ (𝑦 ∈ (0[,](1 / 2)) → (2
· 𝑦) ∈
(0[,]1)) | 
| 126 | 125 | adantl 481 | . . . . . . . . . 10
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,](1 / 2))) → (2 ·
𝑦) ∈
(0[,]1)) | 
| 127 |  | oveq2 7439 | . . . . . . . . . . . . 13
⊢ (𝑥 = (2 · 𝑦) → (1 − 𝑥) = (1 − (2 · 𝑦))) | 
| 128 | 127 | fveq2d 6910 | . . . . . . . . . . . 12
⊢ (𝑥 = (2 · 𝑦) → (𝐹‘(1 − 𝑥)) = (𝐹‘(1 − (2 · 𝑦)))) | 
| 129 |  | fvex 6919 | . . . . . . . . . . . 12
⊢ (𝐹‘(1 − (2 ·
𝑦))) ∈
V | 
| 130 | 128, 1, 129 | fvmpt 7016 | . . . . . . . . . . 11
⊢ ((2
· 𝑦) ∈ (0[,]1)
→ (𝐺‘(2 ·
𝑦)) = (𝐹‘(1 − (2 · 𝑦)))) | 
| 131 |  | unitssre 13539 | . . . . . . . . . . . . . . . 16
⊢ (0[,]1)
⊆ ℝ | 
| 132 | 131 | sseli 3979 | . . . . . . . . . . . . . . 15
⊢ ((2
· 𝑦) ∈ (0[,]1)
→ (2 · 𝑦)
∈ ℝ) | 
| 133 | 132 | recnd 11289 | . . . . . . . . . . . . . 14
⊢ ((2
· 𝑦) ∈ (0[,]1)
→ (2 · 𝑦)
∈ ℂ) | 
| 134 | 133 | mullidd 11279 | . . . . . . . . . . . . 13
⊢ ((2
· 𝑦) ∈ (0[,]1)
→ (1 · (2 · 𝑦)) = (2 · 𝑦)) | 
| 135 | 134 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ ((2
· 𝑦) ∈ (0[,]1)
→ (1 − (1 · (2 · 𝑦))) = (1 − (2 · 𝑦))) | 
| 136 | 135 | fveq2d 6910 | . . . . . . . . . . 11
⊢ ((2
· 𝑦) ∈ (0[,]1)
→ (𝐹‘(1 −
(1 · (2 · 𝑦)))) = (𝐹‘(1 − (2 · 𝑦)))) | 
| 137 | 130, 136 | eqtr4d 2780 | . . . . . . . . . 10
⊢ ((2
· 𝑦) ∈ (0[,]1)
→ (𝐺‘(2 ·
𝑦)) = (𝐹‘(1 − (1 · (2 ·
𝑦))))) | 
| 138 | 126, 137 | syl 17 | . . . . . . . . 9
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,](1 / 2))) → (𝐺‘(2 · 𝑦)) = (𝐹‘(1 − (1 · (2 ·
𝑦))))) | 
| 139 | 124, 138 | eqtrd 2777 | . . . . . . . 8
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,](1 / 2))) → ((𝐺(*𝑝‘𝐽)𝐹)‘𝑦) = (𝐹‘(1 − (1 · (2 ·
𝑦))))) | 
| 140 | 123, 139 | sylan2br 595 | . . . . . . 7
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑦 ∈ (0[,]1) ∧ 𝑦 ≤ (1 / 2))) → ((𝐺(*𝑝‘𝐽)𝐹)‘𝑦) = (𝐹‘(1 − (1 · (2 ·
𝑦))))) | 
| 141 | 140 | anassrs 467 | . . . . . 6
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) ∧ 𝑦 ≤ (1 / 2)) → ((𝐺(*𝑝‘𝐽)𝐹)‘𝑦) = (𝐹‘(1 − (1 · (2 ·
𝑦))))) | 
| 142 | 122, 141 | eqtr4d 2780 | . . . . 5
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) ∧ 𝑦 ≤ (1 / 2)) → (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (1 · (2
· 𝑦))), (1 −
(1 · (1 − ((2 · 𝑦) − 1)))))) = ((𝐺(*𝑝‘𝐽)𝐹)‘𝑦)) | 
| 143 |  | iffalse 4534 | . . . . . . . 8
⊢ (¬
𝑦 ≤ (1 / 2) →
if(𝑦 ≤ (1 / 2), (1
− (1 · (2 · 𝑦))), (1 − (1 · (1 − ((2
· 𝑦) − 1)))))
= (1 − (1 · (1 − ((2 · 𝑦) − 1))))) | 
| 144 | 143 | adantl 481 | . . . . . . 7
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) ∧ ¬ 𝑦 ≤ (1 / 2)) → if(𝑦 ≤ (1 / 2), (1 − (1
· (2 · 𝑦))),
(1 − (1 · (1 − ((2 · 𝑦) − 1))))) = (1 − (1 · (1
− ((2 · 𝑦)
− 1))))) | 
| 145 | 144 | fveq2d 6910 | . . . . . 6
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) ∧ ¬ 𝑦 ≤ (1 / 2)) → (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (1 · (2
· 𝑦))), (1 −
(1 · (1 − ((2 · 𝑦) − 1)))))) = (𝐹‘(1 − (1 · (1 − ((2
· 𝑦) −
1)))))) | 
| 146 |  | elii2 24965 | . . . . . . . 8
⊢ ((𝑦 ∈ (0[,]1) ∧ ¬
𝑦 ≤ (1 / 2)) →
𝑦 ∈ ((1 /
2)[,]1)) | 
| 147 | 8, 6, 16 | pcoval2 25049 | . . . . . . . . 9
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ ((1 / 2)[,]1)) → ((𝐺(*𝑝‘𝐽)𝐹)‘𝑦) = (𝐹‘((2 · 𝑦) − 1))) | 
| 148 |  | iihalf2 24961 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ ((1 / 2)[,]1) → ((2
· 𝑦) − 1)
∈ (0[,]1)) | 
| 149 | 148 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ ((1 / 2)[,]1)) → ((2 ·
𝑦) − 1) ∈
(0[,]1)) | 
| 150 |  | ax-1cn 11213 | . . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ | 
| 151 | 131 | sseli 3979 | . . . . . . . . . . . . . . . 16
⊢ (((2
· 𝑦) − 1)
∈ (0[,]1) → ((2 · 𝑦) − 1) ∈ ℝ) | 
| 152 | 151 | recnd 11289 | . . . . . . . . . . . . . . 15
⊢ (((2
· 𝑦) − 1)
∈ (0[,]1) → ((2 · 𝑦) − 1) ∈ ℂ) | 
| 153 |  | subcl 11507 | . . . . . . . . . . . . . . 15
⊢ ((1
∈ ℂ ∧ ((2 · 𝑦) − 1) ∈ ℂ) → (1
− ((2 · 𝑦)
− 1)) ∈ ℂ) | 
| 154 | 150, 152,
153 | sylancr 587 | . . . . . . . . . . . . . 14
⊢ (((2
· 𝑦) − 1)
∈ (0[,]1) → (1 − ((2 · 𝑦) − 1)) ∈
ℂ) | 
| 155 | 154 | mullidd 11279 | . . . . . . . . . . . . 13
⊢ (((2
· 𝑦) − 1)
∈ (0[,]1) → (1 · (1 − ((2 · 𝑦) − 1))) = (1 − ((2 ·
𝑦) −
1))) | 
| 156 | 155 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ (((2
· 𝑦) − 1)
∈ (0[,]1) → (1 − (1 · (1 − ((2 · 𝑦) − 1)))) = (1 − (1
− ((2 · 𝑦)
− 1)))) | 
| 157 |  | nncan 11538 | . . . . . . . . . . . . 13
⊢ ((1
∈ ℂ ∧ ((2 · 𝑦) − 1) ∈ ℂ) → (1
− (1 − ((2 · 𝑦) − 1))) = ((2 · 𝑦) − 1)) | 
| 158 | 150, 152,
157 | sylancr 587 | . . . . . . . . . . . 12
⊢ (((2
· 𝑦) − 1)
∈ (0[,]1) → (1 − (1 − ((2 · 𝑦) − 1))) = ((2 · 𝑦) − 1)) | 
| 159 | 156, 158 | eqtr2d 2778 | . . . . . . . . . . 11
⊢ (((2
· 𝑦) − 1)
∈ (0[,]1) → ((2 · 𝑦) − 1) = (1 − (1 · (1
− ((2 · 𝑦)
− 1))))) | 
| 160 | 149, 159 | syl 17 | . . . . . . . . . 10
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ ((1 / 2)[,]1)) → ((2 ·
𝑦) − 1) = (1 −
(1 · (1 − ((2 · 𝑦) − 1))))) | 
| 161 | 160 | fveq2d 6910 | . . . . . . . . 9
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ ((1 / 2)[,]1)) → (𝐹‘((2 · 𝑦) − 1)) = (𝐹‘(1 − (1 · (1
− ((2 · 𝑦)
− 1)))))) | 
| 162 | 147, 161 | eqtrd 2777 | . . . . . . . 8
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ ((1 / 2)[,]1)) → ((𝐺(*𝑝‘𝐽)𝐹)‘𝑦) = (𝐹‘(1 − (1 · (1 − ((2
· 𝑦) −
1)))))) | 
| 163 | 146, 162 | sylan2 593 | . . . . . . 7
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝑦 ∈ (0[,]1) ∧ ¬ 𝑦 ≤ (1 / 2))) → ((𝐺(*𝑝‘𝐽)𝐹)‘𝑦) = (𝐹‘(1 − (1 · (1 − ((2
· 𝑦) −
1)))))) | 
| 164 | 163 | anassrs 467 | . . . . . 6
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) ∧ ¬ 𝑦 ≤ (1 / 2)) → ((𝐺(*𝑝‘𝐽)𝐹)‘𝑦) = (𝐹‘(1 − (1 · (1 − ((2
· 𝑦) −
1)))))) | 
| 165 | 145, 164 | eqtr4d 2780 | . . . . 5
⊢ (((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) ∧ ¬ 𝑦 ≤ (1 / 2)) → (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (1 · (2
· 𝑦))), (1 −
(1 · (1 − ((2 · 𝑦) − 1)))))) = ((𝐺(*𝑝‘𝐽)𝐹)‘𝑦)) | 
| 166 | 142, 165 | pm2.61dan 813 | . . . 4
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (1 · (2
· 𝑦))), (1 −
(1 · (1 − ((2 · 𝑦) − 1)))))) = ((𝐺(*𝑝‘𝐽)𝐹)‘𝑦)) | 
| 167 | 119, 166 | eqtrd 2777 | . . 3
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (𝑦𝐻0) = ((𝐺(*𝑝‘𝐽)𝐹)‘𝑦)) | 
| 168 | 131 | sseli 3979 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ (0[,]1) → 𝑦 ∈
ℝ) | 
| 169 | 168 | recnd 11289 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ (0[,]1) → 𝑦 ∈
ℂ) | 
| 170 |  | mulcl 11239 | . . . . . . . . . . . 12
⊢ ((2
∈ ℂ ∧ 𝑦
∈ ℂ) → (2 · 𝑦) ∈ ℂ) | 
| 171 | 47, 169, 170 | sylancr 587 | . . . . . . . . . . 11
⊢ (𝑦 ∈ (0[,]1) → (2
· 𝑦) ∈
ℂ) | 
| 172 | 171 | adantl 481 | . . . . . . . . . 10
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (2 · 𝑦) ∈
ℂ) | 
| 173 | 172 | mul02d 11459 | . . . . . . . . 9
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (0 · (2
· 𝑦)) =
0) | 
| 174 | 173 | oveq2d 7447 | . . . . . . . 8
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (1 − (0
· (2 · 𝑦))) =
(1 − 0)) | 
| 175 | 174, 54 | eqtrdi 2793 | . . . . . . 7
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (1 − (0
· (2 · 𝑦))) =
1) | 
| 176 |  | subcl 11507 | . . . . . . . . . . . 12
⊢ (((2
· 𝑦) ∈ ℂ
∧ 1 ∈ ℂ) → ((2 · 𝑦) − 1) ∈ ℂ) | 
| 177 | 172, 150,
176 | sylancl 586 | . . . . . . . . . . 11
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → ((2 · 𝑦) − 1) ∈
ℂ) | 
| 178 | 150, 177,
153 | sylancr 587 | . . . . . . . . . 10
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (1 − ((2
· 𝑦) − 1))
∈ ℂ) | 
| 179 | 178 | mul02d 11459 | . . . . . . . . 9
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (0 · (1
− ((2 · 𝑦)
− 1))) = 0) | 
| 180 | 179 | oveq2d 7447 | . . . . . . . 8
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (1 − (0
· (1 − ((2 · 𝑦) − 1)))) = (1 −
0)) | 
| 181 | 180, 54 | eqtrdi 2793 | . . . . . . 7
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (1 − (0
· (1 − ((2 · 𝑦) − 1)))) = 1) | 
| 182 | 175, 181 | ifeq12d 4547 | . . . . . 6
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → if(𝑦 ≤ (1 / 2), (1 − (0 · (2
· 𝑦))), (1 −
(0 · (1 − ((2 · 𝑦) − 1))))) = if(𝑦 ≤ (1 / 2), 1, 1)) | 
| 183 |  | ifid 4566 | . . . . . 6
⊢ if(𝑦 ≤ (1 / 2), 1, 1) =
1 | 
| 184 | 182, 183 | eqtrdi 2793 | . . . . 5
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → if(𝑦 ≤ (1 / 2), (1 − (0 · (2
· 𝑦))), (1 −
(0 · (1 − ((2 · 𝑦) − 1))))) = 1) | 
| 185 | 184 | fveq2d 6910 | . . . 4
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (0 · (2
· 𝑦))), (1 −
(0 · (1 − ((2 · 𝑦) − 1)))))) = (𝐹‘1)) | 
| 186 |  | simpl 482 | . . . . . . . . 9
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → 𝑠 = 𝑦) | 
| 187 | 186 | breq1d 5153 | . . . . . . . 8
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → (𝑠 ≤ (1 / 2) ↔ 𝑦 ≤ (1 / 2))) | 
| 188 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → 𝑡 = 1) | 
| 189 | 188 | oveq2d 7447 | . . . . . . . . . . 11
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → (1 − 𝑡) = (1 − 1)) | 
| 190 | 189, 11 | eqtrdi 2793 | . . . . . . . . . 10
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → (1 − 𝑡) = 0) | 
| 191 | 186 | oveq2d 7447 | . . . . . . . . . 10
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → (2 · 𝑠) = (2 · 𝑦)) | 
| 192 | 190, 191 | oveq12d 7449 | . . . . . . . . 9
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → ((1 − 𝑡) · (2 · 𝑠)) = (0 · (2 · 𝑦))) | 
| 193 | 192 | oveq2d 7447 | . . . . . . . 8
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → (1 − ((1 − 𝑡) · (2 · 𝑠))) = (1 − (0 · (2
· 𝑦)))) | 
| 194 | 191 | oveq1d 7446 | . . . . . . . . . . 11
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → ((2 · 𝑠) − 1) = ((2 · 𝑦) − 1)) | 
| 195 | 194 | oveq2d 7447 | . . . . . . . . . 10
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → (1 − ((2 · 𝑠) − 1)) = (1 − ((2
· 𝑦) −
1))) | 
| 196 | 190, 195 | oveq12d 7449 | . . . . . . . . 9
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1))) = (0 · (1
− ((2 · 𝑦)
− 1)))) | 
| 197 | 196 | oveq2d 7447 | . . . . . . . 8
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → (1 − ((1 − 𝑡) · (1 − ((2
· 𝑠) − 1)))) =
(1 − (0 · (1 − ((2 · 𝑦) − 1))))) | 
| 198 | 187, 193,
197 | ifbieq12d 4554 | . . . . . . 7
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 −
𝑡) · (1 − ((2
· 𝑠) − 1)))))
= if(𝑦 ≤ (1 / 2), (1
− (0 · (2 · 𝑦))), (1 − (0 · (1 − ((2
· 𝑦) −
1)))))) | 
| 199 | 198 | fveq2d 6910 | . . . . . 6
⊢ ((𝑠 = 𝑦 ∧ 𝑡 = 1) → (𝐹‘if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 −
𝑡) · (1 − ((2
· 𝑠) − 1))))))
= (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (0
· (2 · 𝑦))),
(1 − (0 · (1 − ((2 · 𝑦) − 1))))))) | 
| 200 |  | fvex 6919 | . . . . . 6
⊢ (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (0 · (2
· 𝑦))), (1 −
(0 · (1 − ((2 · 𝑦) − 1)))))) ∈ V | 
| 201 | 199, 30, 200 | ovmpoa 7588 | . . . . 5
⊢ ((𝑦 ∈ (0[,]1) ∧ 1 ∈
(0[,]1)) → (𝑦𝐻1) = (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (0 · (2
· 𝑦))), (1 −
(0 · (1 − ((2 · 𝑦) − 1))))))) | 
| 202 | 101, 9, 201 | sylancl 586 | . . . 4
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (𝑦𝐻1) = (𝐹‘if(𝑦 ≤ (1 / 2), (1 − (0 · (2
· 𝑦))), (1 −
(0 · (1 − ((2 · 𝑦) − 1))))))) | 
| 203 | 26 | fveq1i 6907 | . . . . 5
⊢ (𝑃‘𝑦) = (((0[,]1) × {(𝐹‘1)})‘𝑦) | 
| 204 |  | fvex 6919 | . . . . . . 7
⊢ (𝐹‘1) ∈
V | 
| 205 | 204 | fvconst2 7224 | . . . . . 6
⊢ (𝑦 ∈ (0[,]1) → (((0[,]1)
× {(𝐹‘1)})‘𝑦) = (𝐹‘1)) | 
| 206 | 205 | adantl 481 | . . . . 5
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (((0[,]1) ×
{(𝐹‘1)})‘𝑦) = (𝐹‘1)) | 
| 207 | 203, 206 | eqtrid 2789 | . . . 4
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (𝑃‘𝑦) = (𝐹‘1)) | 
| 208 | 185, 202,
207 | 3eqtr4d 2787 | . . 3
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (𝑦𝐻1) = (𝑃‘𝑦)) | 
| 209 |  | simpl 482 | . . . . . . . . . . 11
⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → 𝑠 = 0) | 
| 210 | 209, 38 | eqbrtrdi 5182 | . . . . . . . . . 10
⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → 𝑠 ≤ (1 / 2)) | 
| 211 | 210 | iftrued 4533 | . . . . . . . . 9
⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 −
𝑡) · (1 − ((2
· 𝑠) − 1)))))
= (1 − ((1 − 𝑡)
· (2 · 𝑠)))) | 
| 212 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → 𝑡 = 𝑦) | 
| 213 | 212 | oveq2d 7447 | . . . . . . . . . . 11
⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → (1 − 𝑡) = (1 − 𝑦)) | 
| 214 | 209 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → (2 · 𝑠) = (2 · 0)) | 
| 215 |  | 2t0e0 12435 | . . . . . . . . . . . 12
⊢ (2
· 0) = 0 | 
| 216 | 214, 215 | eqtrdi 2793 | . . . . . . . . . . 11
⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → (2 · 𝑠) = 0) | 
| 217 | 213, 216 | oveq12d 7449 | . . . . . . . . . 10
⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → ((1 − 𝑡) · (2 · 𝑠)) = ((1 − 𝑦) · 0)) | 
| 218 | 217 | oveq2d 7447 | . . . . . . . . 9
⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → (1 − ((1 − 𝑡) · (2 · 𝑠))) = (1 − ((1 −
𝑦) ·
0))) | 
| 219 | 211, 218 | eqtrd 2777 | . . . . . . . 8
⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 −
𝑡) · (1 − ((2
· 𝑠) − 1)))))
= (1 − ((1 − 𝑦)
· 0))) | 
| 220 | 219 | fveq2d 6910 | . . . . . . 7
⊢ ((𝑠 = 0 ∧ 𝑡 = 𝑦) → (𝐹‘if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 −
𝑡) · (1 − ((2
· 𝑠) − 1))))))
= (𝐹‘(1 − ((1
− 𝑦) ·
0)))) | 
| 221 |  | fvex 6919 | . . . . . . 7
⊢ (𝐹‘(1 − ((1 −
𝑦) · 0))) ∈
V | 
| 222 | 220, 30, 221 | ovmpoa 7588 | . . . . . 6
⊢ ((0
∈ (0[,]1) ∧ 𝑦
∈ (0[,]1)) → (0𝐻𝑦) = (𝐹‘(1 − ((1 − 𝑦) ·
0)))) | 
| 223 | 102, 222 | mpan 690 | . . . . 5
⊢ (𝑦 ∈ (0[,]1) → (0𝐻𝑦) = (𝐹‘(1 − ((1 − 𝑦) ·
0)))) | 
| 224 |  | subcl 11507 | . . . . . . . . . 10
⊢ ((1
∈ ℂ ∧ 𝑦
∈ ℂ) → (1 − 𝑦) ∈ ℂ) | 
| 225 | 150, 169,
224 | sylancr 587 | . . . . . . . . 9
⊢ (𝑦 ∈ (0[,]1) → (1
− 𝑦) ∈
ℂ) | 
| 226 | 225 | mul01d 11460 | . . . . . . . 8
⊢ (𝑦 ∈ (0[,]1) → ((1
− 𝑦) · 0) =
0) | 
| 227 | 226 | oveq2d 7447 | . . . . . . 7
⊢ (𝑦 ∈ (0[,]1) → (1
− ((1 − 𝑦)
· 0)) = (1 − 0)) | 
| 228 | 227, 54 | eqtrdi 2793 | . . . . . 6
⊢ (𝑦 ∈ (0[,]1) → (1
− ((1 − 𝑦)
· 0)) = 1) | 
| 229 | 228 | fveq2d 6910 | . . . . 5
⊢ (𝑦 ∈ (0[,]1) → (𝐹‘(1 − ((1 −
𝑦) · 0))) = (𝐹‘1)) | 
| 230 | 223, 229 | eqtrd 2777 | . . . 4
⊢ (𝑦 ∈ (0[,]1) → (0𝐻𝑦) = (𝐹‘1)) | 
| 231 | 8, 6 | pco0 25047 | . . . . 5
⊢ (𝐹 ∈ (II Cn 𝐽) → ((𝐺(*𝑝‘𝐽)𝐹)‘0) = (𝐺‘0)) | 
| 232 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑥 = 0 → (1 − 𝑥) = (1 −
0)) | 
| 233 | 232, 54 | eqtrdi 2793 | . . . . . . . 8
⊢ (𝑥 = 0 → (1 − 𝑥) = 1) | 
| 234 | 233 | fveq2d 6910 | . . . . . . 7
⊢ (𝑥 = 0 → (𝐹‘(1 − 𝑥)) = (𝐹‘1)) | 
| 235 | 234, 1, 204 | fvmpt 7016 | . . . . . 6
⊢ (0 ∈
(0[,]1) → (𝐺‘0)
= (𝐹‘1)) | 
| 236 | 102, 235 | ax-mp 5 | . . . . 5
⊢ (𝐺‘0) = (𝐹‘1) | 
| 237 | 231, 236 | eqtr2di 2794 | . . . 4
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐹‘1) = ((𝐺(*𝑝‘𝐽)𝐹)‘0)) | 
| 238 | 230, 237 | sylan9eqr 2799 | . . 3
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (0𝐻𝑦) = ((𝐺(*𝑝‘𝐽)𝐹)‘0)) | 
| 239 | 37, 39 | ltnlei 11382 | . . . . . . . . . . . 12
⊢ ((1 / 2)
< 1 ↔ ¬ 1 ≤ (1 / 2)) | 
| 240 | 40, 239 | mpbi 230 | . . . . . . . . . . 11
⊢  ¬ 1
≤ (1 / 2) | 
| 241 |  | simpl 482 | . . . . . . . . . . . 12
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → 𝑠 = 1) | 
| 242 | 241 | breq1d 5153 | . . . . . . . . . . 11
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → (𝑠 ≤ (1 / 2) ↔ 1 ≤ (1 /
2))) | 
| 243 | 240, 242 | mtbiri 327 | . . . . . . . . . 10
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → ¬ 𝑠 ≤ (1 / 2)) | 
| 244 | 243 | iffalsed 4536 | . . . . . . . . 9
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 −
𝑡) · (1 − ((2
· 𝑠) − 1)))))
= (1 − ((1 − 𝑡)
· (1 − ((2 · 𝑠) − 1))))) | 
| 245 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → 𝑡 = 𝑦) | 
| 246 | 245 | oveq2d 7447 | . . . . . . . . . . 11
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → (1 − 𝑡) = (1 − 𝑦)) | 
| 247 | 241 | oveq2d 7447 | . . . . . . . . . . . . . . . 16
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → (2 · 𝑠) = (2 · 1)) | 
| 248 |  | 2t1e2 12429 | . . . . . . . . . . . . . . . 16
⊢ (2
· 1) = 2 | 
| 249 | 247, 248 | eqtrdi 2793 | . . . . . . . . . . . . . . 15
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → (2 · 𝑠) = 2) | 
| 250 | 249 | oveq1d 7446 | . . . . . . . . . . . . . 14
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → ((2 · 𝑠) − 1) = (2 −
1)) | 
| 251 |  | 2m1e1 12392 | . . . . . . . . . . . . . 14
⊢ (2
− 1) = 1 | 
| 252 | 250, 251 | eqtrdi 2793 | . . . . . . . . . . . . 13
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → ((2 · 𝑠) − 1) = 1) | 
| 253 | 252 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → (1 − ((2 · 𝑠) − 1)) = (1 −
1)) | 
| 254 | 253, 11 | eqtrdi 2793 | . . . . . . . . . . 11
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → (1 − ((2 · 𝑠) − 1)) =
0) | 
| 255 | 246, 254 | oveq12d 7449 | . . . . . . . . . 10
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1))) = ((1 −
𝑦) ·
0)) | 
| 256 | 255 | oveq2d 7447 | . . . . . . . . 9
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → (1 − ((1 − 𝑡) · (1 − ((2
· 𝑠) − 1)))) =
(1 − ((1 − 𝑦)
· 0))) | 
| 257 | 244, 256 | eqtrd 2777 | . . . . . . . 8
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 −
𝑡) · (1 − ((2
· 𝑠) − 1)))))
= (1 − ((1 − 𝑦)
· 0))) | 
| 258 | 257 | fveq2d 6910 | . . . . . . 7
⊢ ((𝑠 = 1 ∧ 𝑡 = 𝑦) → (𝐹‘if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 −
𝑡) · (1 − ((2
· 𝑠) − 1))))))
= (𝐹‘(1 − ((1
− 𝑦) ·
0)))) | 
| 259 | 258, 30, 221 | ovmpoa 7588 | . . . . . 6
⊢ ((1
∈ (0[,]1) ∧ 𝑦
∈ (0[,]1)) → (1𝐻𝑦) = (𝐹‘(1 − ((1 − 𝑦) ·
0)))) | 
| 260 | 9, 259 | mpan 690 | . . . . 5
⊢ (𝑦 ∈ (0[,]1) → (1𝐻𝑦) = (𝐹‘(1 − ((1 − 𝑦) ·
0)))) | 
| 261 | 260, 229 | eqtrd 2777 | . . . 4
⊢ (𝑦 ∈ (0[,]1) → (1𝐻𝑦) = (𝐹‘1)) | 
| 262 | 8, 6 | pco1 25048 | . . . . 5
⊢ (𝐹 ∈ (II Cn 𝐽) → ((𝐺(*𝑝‘𝐽)𝐹)‘1) = (𝐹‘1)) | 
| 263 | 262 | eqcomd 2743 | . . . 4
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐹‘1) = ((𝐺(*𝑝‘𝐽)𝐹)‘1)) | 
| 264 | 261, 263 | sylan9eqr 2799 | . . 3
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (0[,]1)) → (1𝐻𝑦) = ((𝐺(*𝑝‘𝐽)𝐹)‘1)) | 
| 265 | 17, 29, 100, 167, 208, 238, 264 | isphtpy2d 25019 | . 2
⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐻 ∈ ((𝐺(*𝑝‘𝐽)𝐹)(PHtpy‘𝐽)𝑃)) | 
| 266 | 265 | ne0d 4342 | . . 3
⊢ (𝐹 ∈ (II Cn 𝐽) → ((𝐺(*𝑝‘𝐽)𝐹)(PHtpy‘𝐽)𝑃) ≠ ∅) | 
| 267 |  | isphtpc 25026 | . . 3
⊢ ((𝐺(*𝑝‘𝐽)𝐹)( ≃ph‘𝐽)𝑃 ↔ ((𝐺(*𝑝‘𝐽)𝐹) ∈ (II Cn 𝐽) ∧ 𝑃 ∈ (II Cn 𝐽) ∧ ((𝐺(*𝑝‘𝐽)𝐹)(PHtpy‘𝐽)𝑃) ≠ ∅)) | 
| 268 | 17, 29, 266, 267 | syl3anbrc 1344 | . 2
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐺(*𝑝‘𝐽)𝐹)( ≃ph‘𝐽)𝑃) | 
| 269 | 265, 268 | jca 511 | 1
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐻 ∈ ((𝐺(*𝑝‘𝐽)𝐹)(PHtpy‘𝐽)𝑃) ∧ (𝐺(*𝑝‘𝐽)𝐹)( ≃ph‘𝐽)𝑃)) |