| Step | Hyp | Ref
| Expression |
| 1 | | pcohtpy.5 |
. . . . 5
⊢ (𝜑 → 𝐹( ≃ph‘𝐽)𝐻) |
| 2 | | isphtpc 25026 |
. . . . 5
⊢ (𝐹(
≃ph‘𝐽)𝐻 ↔ (𝐹 ∈ (II Cn 𝐽) ∧ 𝐻 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐻) ≠ ∅)) |
| 3 | 1, 2 | sylib 218 |
. . . 4
⊢ (𝜑 → (𝐹 ∈ (II Cn 𝐽) ∧ 𝐻 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐻) ≠ ∅)) |
| 4 | 3 | simp1d 1143 |
. . 3
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) |
| 5 | | pcohtpy.6 |
. . . . 5
⊢ (𝜑 → 𝐺( ≃ph‘𝐽)𝐾) |
| 6 | | isphtpc 25026 |
. . . . 5
⊢ (𝐺(
≃ph‘𝐽)𝐾 ↔ (𝐺 ∈ (II Cn 𝐽) ∧ 𝐾 ∈ (II Cn 𝐽) ∧ (𝐺(PHtpy‘𝐽)𝐾) ≠ ∅)) |
| 7 | 5, 6 | sylib 218 |
. . . 4
⊢ (𝜑 → (𝐺 ∈ (II Cn 𝐽) ∧ 𝐾 ∈ (II Cn 𝐽) ∧ (𝐺(PHtpy‘𝐽)𝐾) ≠ ∅)) |
| 8 | 7 | simp1d 1143 |
. . 3
⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) |
| 9 | | pcohtpy.4 |
. . 3
⊢ (𝜑 → (𝐹‘1) = (𝐺‘0)) |
| 10 | 4, 8, 9 | pcocn 25050 |
. 2
⊢ (𝜑 → (𝐹(*𝑝‘𝐽)𝐺) ∈ (II Cn 𝐽)) |
| 11 | 3 | simp2d 1144 |
. . 3
⊢ (𝜑 → 𝐻 ∈ (II Cn 𝐽)) |
| 12 | 7 | simp2d 1144 |
. . 3
⊢ (𝜑 → 𝐾 ∈ (II Cn 𝐽)) |
| 13 | | pcohtpylem.8 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ (𝐹(PHtpy‘𝐽)𝐻)) |
| 14 | 4, 11, 13 | phtpy01 25017 |
. . . . 5
⊢ (𝜑 → ((𝐹‘0) = (𝐻‘0) ∧ (𝐹‘1) = (𝐻‘1))) |
| 15 | 14 | simprd 495 |
. . . 4
⊢ (𝜑 → (𝐹‘1) = (𝐻‘1)) |
| 16 | | pcohtpylem.9 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ (𝐺(PHtpy‘𝐽)𝐾)) |
| 17 | 8, 12, 16 | phtpy01 25017 |
. . . . 5
⊢ (𝜑 → ((𝐺‘0) = (𝐾‘0) ∧ (𝐺‘1) = (𝐾‘1))) |
| 18 | 17 | simpld 494 |
. . . 4
⊢ (𝜑 → (𝐺‘0) = (𝐾‘0)) |
| 19 | 9, 15, 18 | 3eqtr3d 2785 |
. . 3
⊢ (𝜑 → (𝐻‘1) = (𝐾‘0)) |
| 20 | 11, 12, 19 | pcocn 25050 |
. 2
⊢ (𝜑 → (𝐻(*𝑝‘𝐽)𝐾) ∈ (II Cn 𝐽)) |
| 21 | | pcohtpylem.7 |
. . 3
⊢ 𝑃 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), ((2 · 𝑥)𝑀𝑦), (((2 · 𝑥) − 1)𝑁𝑦))) |
| 22 | | eqid 2737 |
. . . 4
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
| 23 | | eqid 2737 |
. . . 4
⊢
((topGen‘ran (,)) ↾t (0[,](1 / 2))) =
((topGen‘ran (,)) ↾t (0[,](1 / 2))) |
| 24 | | eqid 2737 |
. . . 4
⊢
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) =
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) |
| 25 | | dfii2 24908 |
. . . 4
⊢ II =
((topGen‘ran (,)) ↾t (0[,]1)) |
| 26 | | 0red 11264 |
. . . 4
⊢ (𝜑 → 0 ∈
ℝ) |
| 27 | | 1red 11262 |
. . . 4
⊢ (𝜑 → 1 ∈
ℝ) |
| 28 | | halfre 12480 |
. . . . . 6
⊢ (1 / 2)
∈ ℝ |
| 29 | | halfge0 12483 |
. . . . . 6
⊢ 0 ≤ (1
/ 2) |
| 30 | | 1re 11261 |
. . . . . . 7
⊢ 1 ∈
ℝ |
| 31 | | halflt1 12484 |
. . . . . . 7
⊢ (1 / 2)
< 1 |
| 32 | 28, 30, 31 | ltleii 11384 |
. . . . . 6
⊢ (1 / 2)
≤ 1 |
| 33 | | elicc01 13506 |
. . . . . 6
⊢ ((1 / 2)
∈ (0[,]1) ↔ ((1 / 2) ∈ ℝ ∧ 0 ≤ (1 / 2) ∧ (1 /
2) ≤ 1)) |
| 34 | 28, 29, 32, 33 | mpbir3an 1342 |
. . . . 5
⊢ (1 / 2)
∈ (0[,]1) |
| 35 | 34 | a1i 11 |
. . . 4
⊢ (𝜑 → (1 / 2) ∈
(0[,]1)) |
| 36 | | iitopon 24905 |
. . . . 5
⊢ II ∈
(TopOn‘(0[,]1)) |
| 37 | 36 | a1i 11 |
. . . 4
⊢ (𝜑 → II ∈
(TopOn‘(0[,]1))) |
| 38 | 9 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → (𝐹‘1) = (𝐺‘0)) |
| 39 | 4, 11, 13 | phtpyi 25016 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (0[,]1)) → ((0𝑀𝑦) = (𝐹‘0) ∧ (1𝑀𝑦) = (𝐹‘1))) |
| 40 | 39 | simprd 495 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (0[,]1)) → (1𝑀𝑦) = (𝐹‘1)) |
| 41 | 40 | adantrl 716 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → (1𝑀𝑦) = (𝐹‘1)) |
| 42 | 8, 12, 16 | phtpyi 25016 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (0[,]1)) → ((0𝑁𝑦) = (𝐺‘0) ∧ (1𝑁𝑦) = (𝐺‘1))) |
| 43 | 42 | simpld 494 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (0[,]1)) → (0𝑁𝑦) = (𝐺‘0)) |
| 44 | 43 | adantrl 716 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → (0𝑁𝑦) = (𝐺‘0)) |
| 45 | 38, 41, 44 | 3eqtr4d 2787 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → (1𝑀𝑦) = (0𝑁𝑦)) |
| 46 | | simprl 771 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → 𝑥 = (1 / 2)) |
| 47 | 46 | oveq2d 7447 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → (2 · 𝑥) = (2 · (1 /
2))) |
| 48 | | 2cn 12341 |
. . . . . . . 8
⊢ 2 ∈
ℂ |
| 49 | | 2ne0 12370 |
. . . . . . . 8
⊢ 2 ≠
0 |
| 50 | 48, 49 | recidi 11998 |
. . . . . . 7
⊢ (2
· (1 / 2)) = 1 |
| 51 | 47, 50 | eqtrdi 2793 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → (2 · 𝑥) = 1) |
| 52 | 51 | oveq1d 7446 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → ((2 · 𝑥)𝑀𝑦) = (1𝑀𝑦)) |
| 53 | 51 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → ((2 · 𝑥) − 1) = (1 −
1)) |
| 54 | | 1m1e0 12338 |
. . . . . . 7
⊢ (1
− 1) = 0 |
| 55 | 53, 54 | eqtrdi 2793 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → ((2 · 𝑥) − 1) =
0) |
| 56 | 55 | oveq1d 7446 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → (((2 · 𝑥) − 1)𝑁𝑦) = (0𝑁𝑦)) |
| 57 | 45, 52, 56 | 3eqtr4d 2787 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → ((2 · 𝑥)𝑀𝑦) = (((2 · 𝑥) − 1)𝑁𝑦)) |
| 58 | | retopon 24784 |
. . . . . . 7
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
| 59 | | 0re 11263 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
| 60 | | iccssre 13469 |
. . . . . . . 8
⊢ ((0
∈ ℝ ∧ (1 / 2) ∈ ℝ) → (0[,](1 / 2)) ⊆
ℝ) |
| 61 | 59, 28, 60 | mp2an 692 |
. . . . . . 7
⊢ (0[,](1 /
2)) ⊆ ℝ |
| 62 | | resttopon 23169 |
. . . . . . 7
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 /
2)) ⊆ ℝ) → ((topGen‘ran (,)) ↾t (0[,](1
/ 2))) ∈ (TopOn‘(0[,](1 / 2)))) |
| 63 | 58, 61, 62 | mp2an 692 |
. . . . . 6
⊢
((topGen‘ran (,)) ↾t (0[,](1 / 2))) ∈
(TopOn‘(0[,](1 / 2))) |
| 64 | 63 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((topGen‘ran (,))
↾t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 /
2)))) |
| 65 | 64, 37 | cnmpt1st 23676 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (0[,](1 / 2)), 𝑦 ∈ (0[,]1) ↦ 𝑥) ∈ ((((topGen‘ran (,))
↾t (0[,](1 / 2))) ×t II) Cn
((topGen‘ran (,)) ↾t (0[,](1 / 2))))) |
| 66 | 23 | iihalf1cn 24959 |
. . . . . . 7
⊢ (𝑧 ∈ (0[,](1 / 2)) ↦ (2
· 𝑧)) ∈
(((topGen‘ran (,)) ↾t (0[,](1 / 2))) Cn
II) |
| 67 | 66 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑧 ∈ (0[,](1 / 2)) ↦ (2 ·
𝑧)) ∈
(((topGen‘ran (,)) ↾t (0[,](1 / 2))) Cn
II)) |
| 68 | | oveq2 7439 |
. . . . . 6
⊢ (𝑧 = 𝑥 → (2 · 𝑧) = (2 · 𝑥)) |
| 69 | 64, 37, 65, 64, 67, 68 | cnmpt21 23679 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (0[,](1 / 2)), 𝑦 ∈ (0[,]1) ↦ (2 · 𝑥)) ∈ ((((topGen‘ran
(,)) ↾t (0[,](1 / 2))) ×t II) Cn
II)) |
| 70 | 64, 37 | cnmpt2nd 23677 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (0[,](1 / 2)), 𝑦 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,))
↾t (0[,](1 / 2))) ×t II) Cn
II)) |
| 71 | 4, 11 | phtpycn 25015 |
. . . . . 6
⊢ (𝜑 → (𝐹(PHtpy‘𝐽)𝐻) ⊆ ((II ×t II) Cn
𝐽)) |
| 72 | 71, 13 | sseldd 3984 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ((II ×t II) Cn
𝐽)) |
| 73 | 64, 37, 69, 70, 72 | cnmpt22f 23683 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (0[,](1 / 2)), 𝑦 ∈ (0[,]1) ↦ ((2 · 𝑥)𝑀𝑦)) ∈ ((((topGen‘ran (,))
↾t (0[,](1 / 2))) ×t II) Cn 𝐽)) |
| 74 | | iccssre 13469 |
. . . . . . . 8
⊢ (((1 / 2)
∈ ℝ ∧ 1 ∈ ℝ) → ((1 / 2)[,]1) ⊆
ℝ) |
| 75 | 28, 30, 74 | mp2an 692 |
. . . . . . 7
⊢ ((1 /
2)[,]1) ⊆ ℝ |
| 76 | | resttopon 23169 |
. . . . . . 7
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 /
2)[,]1) ⊆ ℝ) → ((topGen‘ran (,)) ↾t ((1
/ 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1))) |
| 77 | 58, 75, 76 | mp2an 692 |
. . . . . 6
⊢
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ∈
(TopOn‘((1 / 2)[,]1)) |
| 78 | 77 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ∈ (TopOn‘((1 /
2)[,]1))) |
| 79 | 78, 37 | cnmpt1st 23676 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ((1 / 2)[,]1), 𝑦 ∈ (0[,]1) ↦ 𝑥) ∈ ((((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ×t II) Cn
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)))) |
| 80 | 24 | iihalf2cn 24962 |
. . . . . . 7
⊢ (𝑧 ∈ ((1 / 2)[,]1) ↦
((2 · 𝑧) − 1))
∈ (((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) Cn
II) |
| 81 | 80 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑧 ∈ ((1 / 2)[,]1) ↦ ((2 ·
𝑧) − 1)) ∈
(((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) Cn
II)) |
| 82 | 68 | oveq1d 7446 |
. . . . . 6
⊢ (𝑧 = 𝑥 → ((2 · 𝑧) − 1) = ((2 · 𝑥) − 1)) |
| 83 | 78, 37, 79, 78, 81, 82 | cnmpt21 23679 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ((1 / 2)[,]1), 𝑦 ∈ (0[,]1) ↦ ((2 · 𝑥) − 1)) ∈
((((topGen‘ran (,)) ↾t ((1 / 2)[,]1))
×t II) Cn II)) |
| 84 | 78, 37 | cnmpt2nd 23677 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ((1 / 2)[,]1), 𝑦 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ×t II) Cn
II)) |
| 85 | 8, 12 | phtpycn 25015 |
. . . . . 6
⊢ (𝜑 → (𝐺(PHtpy‘𝐽)𝐾) ⊆ ((II ×t II) Cn
𝐽)) |
| 86 | 85, 16 | sseldd 3984 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ((II ×t II) Cn
𝐽)) |
| 87 | 78, 37, 83, 84, 86 | cnmpt22f 23683 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ((1 / 2)[,]1), 𝑦 ∈ (0[,]1) ↦ (((2 · 𝑥) − 1)𝑁𝑦)) ∈ ((((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ×t II) Cn 𝐽)) |
| 88 | 22, 23, 24, 25, 26, 27, 35, 37, 57, 73, 87 | cnmpopc 24955 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), ((2 · 𝑥)𝑀𝑦), (((2 · 𝑥) − 1)𝑁𝑦))) ∈ ((II ×t II) Cn
𝐽)) |
| 89 | 21, 88 | eqeltrid 2845 |
. 2
⊢ (𝜑 → 𝑃 ∈ ((II ×t II) Cn
𝐽)) |
| 90 | | simpll 767 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≤ (1 / 2)) → 𝜑) |
| 91 | | elii1 24964 |
. . . . . . . 8
⊢ (𝑠 ∈ (0[,](1 / 2)) ↔
(𝑠 ∈ (0[,]1) ∧
𝑠 ≤ (1 /
2))) |
| 92 | | iihalf1 24958 |
. . . . . . . 8
⊢ (𝑠 ∈ (0[,](1 / 2)) → (2
· 𝑠) ∈
(0[,]1)) |
| 93 | 91, 92 | sylbir 235 |
. . . . . . 7
⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≤ (1 / 2)) → (2
· 𝑠) ∈
(0[,]1)) |
| 94 | 93 | adantll 714 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≤ (1 / 2)) → (2 · 𝑠) ∈
(0[,]1)) |
| 95 | 4, 11 | phtpyhtpy 25014 |
. . . . . . . 8
⊢ (𝜑 → (𝐹(PHtpy‘𝐽)𝐻) ⊆ (𝐹(II Htpy 𝐽)𝐻)) |
| 96 | 95, 13 | sseldd 3984 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ (𝐹(II Htpy 𝐽)𝐻)) |
| 97 | 37, 4, 11, 96 | htpyi 25006 |
. . . . . 6
⊢ ((𝜑 ∧ (2 · 𝑠) ∈ (0[,]1)) → (((2
· 𝑠)𝑀0) = (𝐹‘(2 · 𝑠)) ∧ ((2 · 𝑠)𝑀1) = (𝐻‘(2 · 𝑠)))) |
| 98 | 90, 94, 97 | syl2anc 584 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≤ (1 / 2)) → (((2 · 𝑠)𝑀0) = (𝐹‘(2 · 𝑠)) ∧ ((2 · 𝑠)𝑀1) = (𝐻‘(2 · 𝑠)))) |
| 99 | 98 | simpld 494 |
. . . 4
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≤ (1 / 2)) → ((2 · 𝑠)𝑀0) = (𝐹‘(2 · 𝑠))) |
| 100 | | simpll 767 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → 𝜑) |
| 101 | | elii2 24965 |
. . . . . . . 8
⊢ ((𝑠 ∈ (0[,]1) ∧ ¬
𝑠 ≤ (1 / 2)) →
𝑠 ∈ ((1 /
2)[,]1)) |
| 102 | 101 | adantll 714 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → 𝑠 ∈ ((1 /
2)[,]1)) |
| 103 | | iihalf2 24961 |
. . . . . . 7
⊢ (𝑠 ∈ ((1 / 2)[,]1) → ((2
· 𝑠) − 1)
∈ (0[,]1)) |
| 104 | 102, 103 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → ((2
· 𝑠) − 1)
∈ (0[,]1)) |
| 105 | 8, 12 | phtpyhtpy 25014 |
. . . . . . . 8
⊢ (𝜑 → (𝐺(PHtpy‘𝐽)𝐾) ⊆ (𝐺(II Htpy 𝐽)𝐾)) |
| 106 | 105, 16 | sseldd 3984 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ (𝐺(II Htpy 𝐽)𝐾)) |
| 107 | 37, 8, 12, 106 | htpyi 25006 |
. . . . . 6
⊢ ((𝜑 ∧ ((2 · 𝑠) − 1) ∈ (0[,]1))
→ ((((2 · 𝑠)
− 1)𝑁0) = (𝐺‘((2 · 𝑠) − 1)) ∧ (((2
· 𝑠) − 1)𝑁1) = (𝐾‘((2 · 𝑠) − 1)))) |
| 108 | 100, 104,
107 | syl2anc 584 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → ((((2
· 𝑠) − 1)𝑁0) = (𝐺‘((2 · 𝑠) − 1)) ∧ (((2 · 𝑠) − 1)𝑁1) = (𝐾‘((2 · 𝑠) − 1)))) |
| 109 | 108 | simpld 494 |
. . . 4
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → (((2
· 𝑠) − 1)𝑁0) = (𝐺‘((2 · 𝑠) − 1))) |
| 110 | 99, 109 | ifeq12da 4559 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀0), (((2 · 𝑠) − 1)𝑁0)) = if(𝑠 ≤ (1 / 2), (𝐹‘(2 · 𝑠)), (𝐺‘((2 · 𝑠) − 1)))) |
| 111 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → 𝑠 ∈ (0[,]1)) |
| 112 | | 0elunit 13509 |
. . . 4
⊢ 0 ∈
(0[,]1) |
| 113 | | simpl 482 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → 𝑥 = 𝑠) |
| 114 | 113 | breq1d 5153 |
. . . . . 6
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → (𝑥 ≤ (1 / 2) ↔ 𝑠 ≤ (1 / 2))) |
| 115 | 113 | oveq2d 7447 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → (2 · 𝑥) = (2 · 𝑠)) |
| 116 | | simpr 484 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → 𝑦 = 0) |
| 117 | 115, 116 | oveq12d 7449 |
. . . . . 6
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → ((2 · 𝑥)𝑀𝑦) = ((2 · 𝑠)𝑀0)) |
| 118 | 115 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → ((2 · 𝑥) − 1) = ((2 · 𝑠) − 1)) |
| 119 | 118, 116 | oveq12d 7449 |
. . . . . 6
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → (((2 · 𝑥) − 1)𝑁𝑦) = (((2 · 𝑠) − 1)𝑁0)) |
| 120 | 114, 117,
119 | ifbieq12d 4554 |
. . . . 5
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → if(𝑥 ≤ (1 / 2), ((2 · 𝑥)𝑀𝑦), (((2 · 𝑥) − 1)𝑁𝑦)) = if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀0), (((2 · 𝑠) − 1)𝑁0))) |
| 121 | | ovex 7464 |
. . . . . 6
⊢ ((2
· 𝑠)𝑀0) ∈ V |
| 122 | | ovex 7464 |
. . . . . 6
⊢ (((2
· 𝑠) − 1)𝑁0) ∈ V |
| 123 | 121, 122 | ifex 4576 |
. . . . 5
⊢ if(𝑠 ≤ (1 / 2), ((2 ·
𝑠)𝑀0), (((2 · 𝑠) − 1)𝑁0)) ∈ V |
| 124 | 120, 21, 123 | ovmpoa 7588 |
. . . 4
⊢ ((𝑠 ∈ (0[,]1) ∧ 0 ∈
(0[,]1)) → (𝑠𝑃0) = if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀0), (((2 · 𝑠) − 1)𝑁0))) |
| 125 | 111, 112,
124 | sylancl 586 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝑠𝑃0) = if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀0), (((2 · 𝑠) − 1)𝑁0))) |
| 126 | 4, 8 | pcovalg 25045 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((𝐹(*𝑝‘𝐽)𝐺)‘𝑠) = if(𝑠 ≤ (1 / 2), (𝐹‘(2 · 𝑠)), (𝐺‘((2 · 𝑠) − 1)))) |
| 127 | 110, 125,
126 | 3eqtr4d 2787 |
. 2
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝑠𝑃0) = ((𝐹(*𝑝‘𝐽)𝐺)‘𝑠)) |
| 128 | 98 | simprd 495 |
. . . 4
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≤ (1 / 2)) → ((2 · 𝑠)𝑀1) = (𝐻‘(2 · 𝑠))) |
| 129 | 108 | simprd 495 |
. . . 4
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → (((2
· 𝑠) − 1)𝑁1) = (𝐾‘((2 · 𝑠) − 1))) |
| 130 | 128, 129 | ifeq12da 4559 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀1), (((2 · 𝑠) − 1)𝑁1)) = if(𝑠 ≤ (1 / 2), (𝐻‘(2 · 𝑠)), (𝐾‘((2 · 𝑠) − 1)))) |
| 131 | | 1elunit 13510 |
. . . 4
⊢ 1 ∈
(0[,]1) |
| 132 | | simpl 482 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → 𝑥 = 𝑠) |
| 133 | 132 | breq1d 5153 |
. . . . . 6
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → (𝑥 ≤ (1 / 2) ↔ 𝑠 ≤ (1 / 2))) |
| 134 | 132 | oveq2d 7447 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → (2 · 𝑥) = (2 · 𝑠)) |
| 135 | | simpr 484 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → 𝑦 = 1) |
| 136 | 134, 135 | oveq12d 7449 |
. . . . . 6
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → ((2 · 𝑥)𝑀𝑦) = ((2 · 𝑠)𝑀1)) |
| 137 | 134 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → ((2 · 𝑥) − 1) = ((2 · 𝑠) − 1)) |
| 138 | 137, 135 | oveq12d 7449 |
. . . . . 6
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → (((2 · 𝑥) − 1)𝑁𝑦) = (((2 · 𝑠) − 1)𝑁1)) |
| 139 | 133, 136,
138 | ifbieq12d 4554 |
. . . . 5
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → if(𝑥 ≤ (1 / 2), ((2 · 𝑥)𝑀𝑦), (((2 · 𝑥) − 1)𝑁𝑦)) = if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀1), (((2 · 𝑠) − 1)𝑁1))) |
| 140 | | ovex 7464 |
. . . . . 6
⊢ ((2
· 𝑠)𝑀1) ∈ V |
| 141 | | ovex 7464 |
. . . . . 6
⊢ (((2
· 𝑠) − 1)𝑁1) ∈ V |
| 142 | 140, 141 | ifex 4576 |
. . . . 5
⊢ if(𝑠 ≤ (1 / 2), ((2 ·
𝑠)𝑀1), (((2 · 𝑠) − 1)𝑁1)) ∈ V |
| 143 | 139, 21, 142 | ovmpoa 7588 |
. . . 4
⊢ ((𝑠 ∈ (0[,]1) ∧ 1 ∈
(0[,]1)) → (𝑠𝑃1) = if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀1), (((2 · 𝑠) − 1)𝑁1))) |
| 144 | 111, 131,
143 | sylancl 586 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝑠𝑃1) = if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀1), (((2 · 𝑠) − 1)𝑁1))) |
| 145 | 11, 12 | pcovalg 25045 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((𝐻(*𝑝‘𝐽)𝐾)‘𝑠) = if(𝑠 ≤ (1 / 2), (𝐻‘(2 · 𝑠)), (𝐾‘((2 · 𝑠) − 1)))) |
| 146 | 130, 144,
145 | 3eqtr4d 2787 |
. 2
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝑠𝑃1) = ((𝐻(*𝑝‘𝐽)𝐾)‘𝑠)) |
| 147 | 4, 11, 13 | phtpyi 25016 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((0𝑀𝑠) = (𝐹‘0) ∧ (1𝑀𝑠) = (𝐹‘1))) |
| 148 | 147 | simpld 494 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (0𝑀𝑠) = (𝐹‘0)) |
| 149 | | simpl 482 |
. . . . . . . 8
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → 𝑥 = 0) |
| 150 | 149, 29 | eqbrtrdi 5182 |
. . . . . . 7
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → 𝑥 ≤ (1 / 2)) |
| 151 | 150 | iftrued 4533 |
. . . . . 6
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → if(𝑥 ≤ (1 / 2), ((2 · 𝑥)𝑀𝑦), (((2 · 𝑥) − 1)𝑁𝑦)) = ((2 · 𝑥)𝑀𝑦)) |
| 152 | 149 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → (2 · 𝑥) = (2 · 0)) |
| 153 | | 2t0e0 12435 |
. . . . . . . 8
⊢ (2
· 0) = 0 |
| 154 | 152, 153 | eqtrdi 2793 |
. . . . . . 7
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → (2 · 𝑥) = 0) |
| 155 | | simpr 484 |
. . . . . . 7
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → 𝑦 = 𝑠) |
| 156 | 154, 155 | oveq12d 7449 |
. . . . . 6
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → ((2 · 𝑥)𝑀𝑦) = (0𝑀𝑠)) |
| 157 | 151, 156 | eqtrd 2777 |
. . . . 5
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → if(𝑥 ≤ (1 / 2), ((2 · 𝑥)𝑀𝑦), (((2 · 𝑥) − 1)𝑁𝑦)) = (0𝑀𝑠)) |
| 158 | | ovex 7464 |
. . . . 5
⊢ (0𝑀𝑠) ∈ V |
| 159 | 157, 21, 158 | ovmpoa 7588 |
. . . 4
⊢ ((0
∈ (0[,]1) ∧ 𝑠
∈ (0[,]1)) → (0𝑃𝑠) = (0𝑀𝑠)) |
| 160 | 112, 111,
159 | sylancr 587 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (0𝑃𝑠) = (0𝑀𝑠)) |
| 161 | 4, 8 | pco0 25047 |
. . . 4
⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐺)‘0) = (𝐹‘0)) |
| 162 | 161 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((𝐹(*𝑝‘𝐽)𝐺)‘0) = (𝐹‘0)) |
| 163 | 148, 160,
162 | 3eqtr4d 2787 |
. 2
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (0𝑃𝑠) = ((𝐹(*𝑝‘𝐽)𝐺)‘0)) |
| 164 | 8, 12, 16 | phtpyi 25016 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((0𝑁𝑠) = (𝐺‘0) ∧ (1𝑁𝑠) = (𝐺‘1))) |
| 165 | 164 | simprd 495 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (1𝑁𝑠) = (𝐺‘1)) |
| 166 | 28, 30 | ltnlei 11382 |
. . . . . . . . 9
⊢ ((1 / 2)
< 1 ↔ ¬ 1 ≤ (1 / 2)) |
| 167 | 31, 166 | mpbi 230 |
. . . . . . . 8
⊢ ¬ 1
≤ (1 / 2) |
| 168 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → 𝑥 = 1) |
| 169 | 168 | breq1d 5153 |
. . . . . . . 8
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → (𝑥 ≤ (1 / 2) ↔ 1 ≤ (1 /
2))) |
| 170 | 167, 169 | mtbiri 327 |
. . . . . . 7
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → ¬ 𝑥 ≤ (1 / 2)) |
| 171 | 170 | iffalsed 4536 |
. . . . . 6
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → if(𝑥 ≤ (1 / 2), ((2 · 𝑥)𝑀𝑦), (((2 · 𝑥) − 1)𝑁𝑦)) = (((2 · 𝑥) − 1)𝑁𝑦)) |
| 172 | 168 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → (2 · 𝑥) = (2 · 1)) |
| 173 | | 2t1e2 12429 |
. . . . . . . . . 10
⊢ (2
· 1) = 2 |
| 174 | 172, 173 | eqtrdi 2793 |
. . . . . . . . 9
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → (2 · 𝑥) = 2) |
| 175 | 174 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → ((2 · 𝑥) − 1) = (2 −
1)) |
| 176 | | 2m1e1 12392 |
. . . . . . . 8
⊢ (2
− 1) = 1 |
| 177 | 175, 176 | eqtrdi 2793 |
. . . . . . 7
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → ((2 · 𝑥) − 1) = 1) |
| 178 | | simpr 484 |
. . . . . . 7
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → 𝑦 = 𝑠) |
| 179 | 177, 178 | oveq12d 7449 |
. . . . . 6
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → (((2 · 𝑥) − 1)𝑁𝑦) = (1𝑁𝑠)) |
| 180 | 171, 179 | eqtrd 2777 |
. . . . 5
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → if(𝑥 ≤ (1 / 2), ((2 · 𝑥)𝑀𝑦), (((2 · 𝑥) − 1)𝑁𝑦)) = (1𝑁𝑠)) |
| 181 | | ovex 7464 |
. . . . 5
⊢ (1𝑁𝑠) ∈ V |
| 182 | 180, 21, 181 | ovmpoa 7588 |
. . . 4
⊢ ((1
∈ (0[,]1) ∧ 𝑠
∈ (0[,]1)) → (1𝑃𝑠) = (1𝑁𝑠)) |
| 183 | 131, 111,
182 | sylancr 587 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (1𝑃𝑠) = (1𝑁𝑠)) |
| 184 | 4, 8 | pco1 25048 |
. . . 4
⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐺)‘1) = (𝐺‘1)) |
| 185 | 184 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((𝐹(*𝑝‘𝐽)𝐺)‘1) = (𝐺‘1)) |
| 186 | 165, 183,
185 | 3eqtr4d 2787 |
. 2
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (1𝑃𝑠) = ((𝐹(*𝑝‘𝐽)𝐺)‘1)) |
| 187 | 10, 20, 89, 127, 146, 163, 186 | isphtpy2d 25019 |
1
⊢ (𝜑 → 𝑃 ∈ ((𝐹(*𝑝‘𝐽)𝐺)(PHtpy‘𝐽)(𝐻(*𝑝‘𝐽)𝐾))) |