Step | Hyp | Ref
| Expression |
1 | | pcohtpy.5 |
. . . . 5
⊢ (𝜑 → 𝐹( ≃ph‘𝐽)𝐻) |
2 | | isphtpc 22601 |
. . . . 5
⊢ (𝐹(
≃ph‘𝐽)𝐻 ↔ (𝐹 ∈ (II Cn 𝐽) ∧ 𝐻 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐻) ≠ ∅)) |
3 | 1, 2 | sylib 207 |
. . . 4
⊢ (𝜑 → (𝐹 ∈ (II Cn 𝐽) ∧ 𝐻 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐻) ≠ ∅)) |
4 | 3 | simp1d 1066 |
. . 3
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) |
5 | | pcohtpy.6 |
. . . . 5
⊢ (𝜑 → 𝐺( ≃ph‘𝐽)𝐾) |
6 | | isphtpc 22601 |
. . . . 5
⊢ (𝐺(
≃ph‘𝐽)𝐾 ↔ (𝐺 ∈ (II Cn 𝐽) ∧ 𝐾 ∈ (II Cn 𝐽) ∧ (𝐺(PHtpy‘𝐽)𝐾) ≠ ∅)) |
7 | 5, 6 | sylib 207 |
. . . 4
⊢ (𝜑 → (𝐺 ∈ (II Cn 𝐽) ∧ 𝐾 ∈ (II Cn 𝐽) ∧ (𝐺(PHtpy‘𝐽)𝐾) ≠ ∅)) |
8 | 7 | simp1d 1066 |
. . 3
⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) |
9 | | pcohtpy.4 |
. . 3
⊢ (𝜑 → (𝐹‘1) = (𝐺‘0)) |
10 | 4, 8, 9 | pcocn 22625 |
. 2
⊢ (𝜑 → (𝐹(*𝑝‘𝐽)𝐺) ∈ (II Cn 𝐽)) |
11 | 3 | simp2d 1067 |
. . 3
⊢ (𝜑 → 𝐻 ∈ (II Cn 𝐽)) |
12 | 7 | simp2d 1067 |
. . 3
⊢ (𝜑 → 𝐾 ∈ (II Cn 𝐽)) |
13 | | pcohtpylem.8 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ (𝐹(PHtpy‘𝐽)𝐻)) |
14 | 4, 11, 13 | phtpy01 22592 |
. . . . 5
⊢ (𝜑 → ((𝐹‘0) = (𝐻‘0) ∧ (𝐹‘1) = (𝐻‘1))) |
15 | 14 | simprd 478 |
. . . 4
⊢ (𝜑 → (𝐹‘1) = (𝐻‘1)) |
16 | | pcohtpylem.9 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ (𝐺(PHtpy‘𝐽)𝐾)) |
17 | 8, 12, 16 | phtpy01 22592 |
. . . . 5
⊢ (𝜑 → ((𝐺‘0) = (𝐾‘0) ∧ (𝐺‘1) = (𝐾‘1))) |
18 | 17 | simpld 474 |
. . . 4
⊢ (𝜑 → (𝐺‘0) = (𝐾‘0)) |
19 | 9, 15, 18 | 3eqtr3d 2652 |
. . 3
⊢ (𝜑 → (𝐻‘1) = (𝐾‘0)) |
20 | 11, 12, 19 | pcocn 22625 |
. 2
⊢ (𝜑 → (𝐻(*𝑝‘𝐽)𝐾) ∈ (II Cn 𝐽)) |
21 | | pcohtpylem.7 |
. . 3
⊢ 𝑃 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), ((2 · 𝑥)𝑀𝑦), (((2 · 𝑥) − 1)𝑁𝑦))) |
22 | | eqid 2610 |
. . . 4
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
23 | | eqid 2610 |
. . . 4
⊢
((topGen‘ran (,)) ↾t (0[,](1 / 2))) =
((topGen‘ran (,)) ↾t (0[,](1 / 2))) |
24 | | eqid 2610 |
. . . 4
⊢
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) =
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) |
25 | | dfii2 22493 |
. . . 4
⊢ II =
((topGen‘ran (,)) ↾t (0[,]1)) |
26 | | 0red 9920 |
. . . 4
⊢ (𝜑 → 0 ∈
ℝ) |
27 | | 1red 9934 |
. . . 4
⊢ (𝜑 → 1 ∈
ℝ) |
28 | | halfre 11123 |
. . . . . 6
⊢ (1 / 2)
∈ ℝ |
29 | | 0re 9919 |
. . . . . . 7
⊢ 0 ∈
ℝ |
30 | | halfgt0 11125 |
. . . . . . 7
⊢ 0 < (1
/ 2) |
31 | 29, 28, 30 | ltleii 10039 |
. . . . . 6
⊢ 0 ≤ (1
/ 2) |
32 | | 1re 9918 |
. . . . . . 7
⊢ 1 ∈
ℝ |
33 | | halflt1 11127 |
. . . . . . 7
⊢ (1 / 2)
< 1 |
34 | 28, 32, 33 | ltleii 10039 |
. . . . . 6
⊢ (1 / 2)
≤ 1 |
35 | 29, 32 | elicc2i 12110 |
. . . . . 6
⊢ ((1 / 2)
∈ (0[,]1) ↔ ((1 / 2) ∈ ℝ ∧ 0 ≤ (1 / 2) ∧ (1 /
2) ≤ 1)) |
36 | 28, 31, 34, 35 | mpbir3an 1237 |
. . . . 5
⊢ (1 / 2)
∈ (0[,]1) |
37 | 36 | a1i 11 |
. . . 4
⊢ (𝜑 → (1 / 2) ∈
(0[,]1)) |
38 | | iitopon 22490 |
. . . . 5
⊢ II ∈
(TopOn‘(0[,]1)) |
39 | 38 | a1i 11 |
. . . 4
⊢ (𝜑 → II ∈
(TopOn‘(0[,]1))) |
40 | 9 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → (𝐹‘1) = (𝐺‘0)) |
41 | 4, 11, 13 | phtpyi 22591 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (0[,]1)) → ((0𝑀𝑦) = (𝐹‘0) ∧ (1𝑀𝑦) = (𝐹‘1))) |
42 | 41 | simprd 478 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (0[,]1)) → (1𝑀𝑦) = (𝐹‘1)) |
43 | 42 | adantrl 748 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → (1𝑀𝑦) = (𝐹‘1)) |
44 | 8, 12, 16 | phtpyi 22591 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (0[,]1)) → ((0𝑁𝑦) = (𝐺‘0) ∧ (1𝑁𝑦) = (𝐺‘1))) |
45 | 44 | simpld 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (0[,]1)) → (0𝑁𝑦) = (𝐺‘0)) |
46 | 45 | adantrl 748 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → (0𝑁𝑦) = (𝐺‘0)) |
47 | 40, 43, 46 | 3eqtr4d 2654 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → (1𝑀𝑦) = (0𝑁𝑦)) |
48 | | simprl 790 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → 𝑥 = (1 / 2)) |
49 | 48 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → (2 · 𝑥) = (2 · (1 /
2))) |
50 | | 2cn 10968 |
. . . . . . . 8
⊢ 2 ∈
ℂ |
51 | | 2ne0 10990 |
. . . . . . . 8
⊢ 2 ≠
0 |
52 | 50, 51 | recidi 10635 |
. . . . . . 7
⊢ (2
· (1 / 2)) = 1 |
53 | 49, 52 | syl6eq 2660 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → (2 · 𝑥) = 1) |
54 | 53 | oveq1d 6564 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → ((2 · 𝑥)𝑀𝑦) = (1𝑀𝑦)) |
55 | 53 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → ((2 · 𝑥) − 1) = (1 −
1)) |
56 | | 1m1e0 10966 |
. . . . . . 7
⊢ (1
− 1) = 0 |
57 | 55, 56 | syl6eq 2660 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → ((2 · 𝑥) − 1) =
0) |
58 | 57 | oveq1d 6564 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → (((2 · 𝑥) − 1)𝑁𝑦) = (0𝑁𝑦)) |
59 | 47, 54, 58 | 3eqtr4d 2654 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → ((2 · 𝑥)𝑀𝑦) = (((2 · 𝑥) − 1)𝑁𝑦)) |
60 | | retopon 22377 |
. . . . . . 7
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
61 | | iccssre 12126 |
. . . . . . . 8
⊢ ((0
∈ ℝ ∧ (1 / 2) ∈ ℝ) → (0[,](1 / 2)) ⊆
ℝ) |
62 | 29, 28, 61 | mp2an 704 |
. . . . . . 7
⊢ (0[,](1 /
2)) ⊆ ℝ |
63 | | resttopon 20775 |
. . . . . . 7
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 /
2)) ⊆ ℝ) → ((topGen‘ran (,)) ↾t (0[,](1
/ 2))) ∈ (TopOn‘(0[,](1 / 2)))) |
64 | 60, 62, 63 | mp2an 704 |
. . . . . 6
⊢
((topGen‘ran (,)) ↾t (0[,](1 / 2))) ∈
(TopOn‘(0[,](1 / 2))) |
65 | 64 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((topGen‘ran (,))
↾t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 /
2)))) |
66 | 65, 39 | cnmpt1st 21281 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (0[,](1 / 2)), 𝑦 ∈ (0[,]1) ↦ 𝑥) ∈ ((((topGen‘ran (,))
↾t (0[,](1 / 2))) ×t II) Cn
((topGen‘ran (,)) ↾t (0[,](1 / 2))))) |
67 | 23 | iihalf1cn 22539 |
. . . . . . 7
⊢ (𝑧 ∈ (0[,](1 / 2)) ↦ (2
· 𝑧)) ∈
(((topGen‘ran (,)) ↾t (0[,](1 / 2))) Cn
II) |
68 | 67 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑧 ∈ (0[,](1 / 2)) ↦ (2 ·
𝑧)) ∈
(((topGen‘ran (,)) ↾t (0[,](1 / 2))) Cn
II)) |
69 | | oveq2 6557 |
. . . . . 6
⊢ (𝑧 = 𝑥 → (2 · 𝑧) = (2 · 𝑥)) |
70 | 65, 39, 66, 65, 68, 69 | cnmpt21 21284 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (0[,](1 / 2)), 𝑦 ∈ (0[,]1) ↦ (2 · 𝑥)) ∈ ((((topGen‘ran
(,)) ↾t (0[,](1 / 2))) ×t II) Cn
II)) |
71 | 65, 39 | cnmpt2nd 21282 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (0[,](1 / 2)), 𝑦 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,))
↾t (0[,](1 / 2))) ×t II) Cn
II)) |
72 | 4, 11 | phtpycn 22590 |
. . . . . 6
⊢ (𝜑 → (𝐹(PHtpy‘𝐽)𝐻) ⊆ ((II ×t II) Cn
𝐽)) |
73 | 72, 13 | sseldd 3569 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ((II ×t II) Cn
𝐽)) |
74 | 65, 39, 70, 71, 73 | cnmpt22f 21288 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (0[,](1 / 2)), 𝑦 ∈ (0[,]1) ↦ ((2 · 𝑥)𝑀𝑦)) ∈ ((((topGen‘ran (,))
↾t (0[,](1 / 2))) ×t II) Cn 𝐽)) |
75 | | iccssre 12126 |
. . . . . . . 8
⊢ (((1 / 2)
∈ ℝ ∧ 1 ∈ ℝ) → ((1 / 2)[,]1) ⊆
ℝ) |
76 | 28, 32, 75 | mp2an 704 |
. . . . . . 7
⊢ ((1 /
2)[,]1) ⊆ ℝ |
77 | | resttopon 20775 |
. . . . . . 7
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 /
2)[,]1) ⊆ ℝ) → ((topGen‘ran (,)) ↾t ((1
/ 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1))) |
78 | 60, 76, 77 | mp2an 704 |
. . . . . 6
⊢
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ∈
(TopOn‘((1 / 2)[,]1)) |
79 | 78 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ∈ (TopOn‘((1 /
2)[,]1))) |
80 | 79, 39 | cnmpt1st 21281 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ((1 / 2)[,]1), 𝑦 ∈ (0[,]1) ↦ 𝑥) ∈ ((((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ×t II) Cn
((topGen‘ran (,)) ↾t ((1 / 2)[,]1)))) |
81 | 24 | iihalf2cn 22541 |
. . . . . . 7
⊢ (𝑧 ∈ ((1 / 2)[,]1) ↦
((2 · 𝑧) − 1))
∈ (((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) Cn
II) |
82 | 81 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑧 ∈ ((1 / 2)[,]1) ↦ ((2 ·
𝑧) − 1)) ∈
(((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) Cn
II)) |
83 | 69 | oveq1d 6564 |
. . . . . 6
⊢ (𝑧 = 𝑥 → ((2 · 𝑧) − 1) = ((2 · 𝑥) − 1)) |
84 | 79, 39, 80, 79, 82, 83 | cnmpt21 21284 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ((1 / 2)[,]1), 𝑦 ∈ (0[,]1) ↦ ((2 · 𝑥) − 1)) ∈
((((topGen‘ran (,)) ↾t ((1 / 2)[,]1))
×t II) Cn II)) |
85 | 79, 39 | cnmpt2nd 21282 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ((1 / 2)[,]1), 𝑦 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ×t II) Cn
II)) |
86 | 8, 12 | phtpycn 22590 |
. . . . . 6
⊢ (𝜑 → (𝐺(PHtpy‘𝐽)𝐾) ⊆ ((II ×t II) Cn
𝐽)) |
87 | 86, 16 | sseldd 3569 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ((II ×t II) Cn
𝐽)) |
88 | 79, 39, 84, 85, 87 | cnmpt22f 21288 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ((1 / 2)[,]1), 𝑦 ∈ (0[,]1) ↦ (((2 · 𝑥) − 1)𝑁𝑦)) ∈ ((((topGen‘ran (,))
↾t ((1 / 2)[,]1)) ×t II) Cn 𝐽)) |
89 | 22, 23, 24, 25, 26, 27, 37, 39, 59, 74, 88 | cnmpt2pc 22535 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), ((2 · 𝑥)𝑀𝑦), (((2 · 𝑥) − 1)𝑁𝑦))) ∈ ((II ×t II) Cn
𝐽)) |
90 | 21, 89 | syl5eqel 2692 |
. 2
⊢ (𝜑 → 𝑃 ∈ ((II ×t II) Cn
𝐽)) |
91 | | simpll 786 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≤ (1 / 2)) → 𝜑) |
92 | | elii1 22542 |
. . . . . . . . 9
⊢ (𝑠 ∈ (0[,](1 / 2)) ↔
(𝑠 ∈ (0[,]1) ∧
𝑠 ≤ (1 /
2))) |
93 | | iihalf1 22538 |
. . . . . . . . 9
⊢ (𝑠 ∈ (0[,](1 / 2)) → (2
· 𝑠) ∈
(0[,]1)) |
94 | 92, 93 | sylbir 224 |
. . . . . . . 8
⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≤ (1 / 2)) → (2
· 𝑠) ∈
(0[,]1)) |
95 | 94 | adantll 746 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≤ (1 / 2)) → (2 · 𝑠) ∈
(0[,]1)) |
96 | 4, 11 | phtpyhtpy 22589 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹(PHtpy‘𝐽)𝐻) ⊆ (𝐹(II Htpy 𝐽)𝐻)) |
97 | 96, 13 | sseldd 3569 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ (𝐹(II Htpy 𝐽)𝐻)) |
98 | 39, 4, 11, 97 | htpyi 22581 |
. . . . . . 7
⊢ ((𝜑 ∧ (2 · 𝑠) ∈ (0[,]1)) → (((2
· 𝑠)𝑀0) = (𝐹‘(2 · 𝑠)) ∧ ((2 · 𝑠)𝑀1) = (𝐻‘(2 · 𝑠)))) |
99 | 91, 95, 98 | syl2anc 691 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≤ (1 / 2)) → (((2 · 𝑠)𝑀0) = (𝐹‘(2 · 𝑠)) ∧ ((2 · 𝑠)𝑀1) = (𝐻‘(2 · 𝑠)))) |
100 | 99 | simpld 474 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≤ (1 / 2)) → ((2 · 𝑠)𝑀0) = (𝐹‘(2 · 𝑠))) |
101 | | iftrue 4042 |
. . . . . 6
⊢ (𝑠 ≤ (1 / 2) → if(𝑠 ≤ (1 / 2), ((2 ·
𝑠)𝑀0), (((2 · 𝑠) − 1)𝑁0)) = ((2 · 𝑠)𝑀0)) |
102 | 101 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≤ (1 / 2)) → if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀0), (((2 · 𝑠) − 1)𝑁0)) = ((2 · 𝑠)𝑀0)) |
103 | | iftrue 4042 |
. . . . . 6
⊢ (𝑠 ≤ (1 / 2) → if(𝑠 ≤ (1 / 2), (𝐹‘(2 · 𝑠)), (𝐺‘((2 · 𝑠) − 1))) = (𝐹‘(2 · 𝑠))) |
104 | 103 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≤ (1 / 2)) → if(𝑠 ≤ (1 / 2), (𝐹‘(2 · 𝑠)), (𝐺‘((2 · 𝑠) − 1))) = (𝐹‘(2 · 𝑠))) |
105 | 100, 102,
104 | 3eqtr4d 2654 |
. . . 4
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≤ (1 / 2)) → if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀0), (((2 · 𝑠) − 1)𝑁0)) = if(𝑠 ≤ (1 / 2), (𝐹‘(2 · 𝑠)), (𝐺‘((2 · 𝑠) − 1)))) |
106 | | simpll 786 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → 𝜑) |
107 | | elii2 22543 |
. . . . . . . . 9
⊢ ((𝑠 ∈ (0[,]1) ∧ ¬
𝑠 ≤ (1 / 2)) →
𝑠 ∈ ((1 /
2)[,]1)) |
108 | 107 | adantll 746 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → 𝑠 ∈ ((1 /
2)[,]1)) |
109 | | iihalf2 22540 |
. . . . . . . 8
⊢ (𝑠 ∈ ((1 / 2)[,]1) → ((2
· 𝑠) − 1)
∈ (0[,]1)) |
110 | 108, 109 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → ((2
· 𝑠) − 1)
∈ (0[,]1)) |
111 | 8, 12 | phtpyhtpy 22589 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺(PHtpy‘𝐽)𝐾) ⊆ (𝐺(II Htpy 𝐽)𝐾)) |
112 | 111, 16 | sseldd 3569 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ (𝐺(II Htpy 𝐽)𝐾)) |
113 | 39, 8, 12, 112 | htpyi 22581 |
. . . . . . 7
⊢ ((𝜑 ∧ ((2 · 𝑠) − 1) ∈ (0[,]1))
→ ((((2 · 𝑠)
− 1)𝑁0) = (𝐺‘((2 · 𝑠) − 1)) ∧ (((2
· 𝑠) − 1)𝑁1) = (𝐾‘((2 · 𝑠) − 1)))) |
114 | 106, 110,
113 | syl2anc 691 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → ((((2
· 𝑠) − 1)𝑁0) = (𝐺‘((2 · 𝑠) − 1)) ∧ (((2 · 𝑠) − 1)𝑁1) = (𝐾‘((2 · 𝑠) − 1)))) |
115 | 114 | simpld 474 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → (((2
· 𝑠) − 1)𝑁0) = (𝐺‘((2 · 𝑠) − 1))) |
116 | | iffalse 4045 |
. . . . . 6
⊢ (¬
𝑠 ≤ (1 / 2) →
if(𝑠 ≤ (1 / 2), ((2
· 𝑠)𝑀0), (((2 · 𝑠) − 1)𝑁0)) = (((2 · 𝑠) − 1)𝑁0)) |
117 | 116 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → if(𝑠 ≤ (1 / 2), ((2 ·
𝑠)𝑀0), (((2 · 𝑠) − 1)𝑁0)) = (((2 · 𝑠) − 1)𝑁0)) |
118 | | iffalse 4045 |
. . . . . 6
⊢ (¬
𝑠 ≤ (1 / 2) →
if(𝑠 ≤ (1 / 2), (𝐹‘(2 · 𝑠)), (𝐺‘((2 · 𝑠) − 1))) = (𝐺‘((2 · 𝑠) − 1))) |
119 | 118 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → if(𝑠 ≤ (1 / 2), (𝐹‘(2 · 𝑠)), (𝐺‘((2 · 𝑠) − 1))) = (𝐺‘((2 · 𝑠) − 1))) |
120 | 115, 117,
119 | 3eqtr4d 2654 |
. . . 4
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → if(𝑠 ≤ (1 / 2), ((2 ·
𝑠)𝑀0), (((2 · 𝑠) − 1)𝑁0)) = if(𝑠 ≤ (1 / 2), (𝐹‘(2 · 𝑠)), (𝐺‘((2 · 𝑠) − 1)))) |
121 | 105, 120 | pm2.61dan 828 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀0), (((2 · 𝑠) − 1)𝑁0)) = if(𝑠 ≤ (1 / 2), (𝐹‘(2 · 𝑠)), (𝐺‘((2 · 𝑠) − 1)))) |
122 | | simpr 476 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → 𝑠 ∈ (0[,]1)) |
123 | | 0elunit 12161 |
. . . 4
⊢ 0 ∈
(0[,]1) |
124 | | simpl 472 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → 𝑥 = 𝑠) |
125 | 124 | breq1d 4593 |
. . . . . 6
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → (𝑥 ≤ (1 / 2) ↔ 𝑠 ≤ (1 / 2))) |
126 | 124 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → (2 · 𝑥) = (2 · 𝑠)) |
127 | | simpr 476 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → 𝑦 = 0) |
128 | 126, 127 | oveq12d 6567 |
. . . . . 6
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → ((2 · 𝑥)𝑀𝑦) = ((2 · 𝑠)𝑀0)) |
129 | 126 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → ((2 · 𝑥) − 1) = ((2 · 𝑠) − 1)) |
130 | 129, 127 | oveq12d 6567 |
. . . . . 6
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → (((2 · 𝑥) − 1)𝑁𝑦) = (((2 · 𝑠) − 1)𝑁0)) |
131 | 125, 128,
130 | ifbieq12d 4063 |
. . . . 5
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 0) → if(𝑥 ≤ (1 / 2), ((2 · 𝑥)𝑀𝑦), (((2 · 𝑥) − 1)𝑁𝑦)) = if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀0), (((2 · 𝑠) − 1)𝑁0))) |
132 | | ovex 6577 |
. . . . . 6
⊢ ((2
· 𝑠)𝑀0) ∈ V |
133 | | ovex 6577 |
. . . . . 6
⊢ (((2
· 𝑠) − 1)𝑁0) ∈ V |
134 | 132, 133 | ifex 4106 |
. . . . 5
⊢ if(𝑠 ≤ (1 / 2), ((2 ·
𝑠)𝑀0), (((2 · 𝑠) − 1)𝑁0)) ∈ V |
135 | 131, 21, 134 | ovmpt2a 6689 |
. . . 4
⊢ ((𝑠 ∈ (0[,]1) ∧ 0 ∈
(0[,]1)) → (𝑠𝑃0) = if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀0), (((2 · 𝑠) − 1)𝑁0))) |
136 | 122, 123,
135 | sylancl 693 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝑠𝑃0) = if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀0), (((2 · 𝑠) − 1)𝑁0))) |
137 | 4, 8 | pcovalg 22620 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((𝐹(*𝑝‘𝐽)𝐺)‘𝑠) = if(𝑠 ≤ (1 / 2), (𝐹‘(2 · 𝑠)), (𝐺‘((2 · 𝑠) − 1)))) |
138 | 121, 136,
137 | 3eqtr4d 2654 |
. 2
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝑠𝑃0) = ((𝐹(*𝑝‘𝐽)𝐺)‘𝑠)) |
139 | 99 | simprd 478 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≤ (1 / 2)) → ((2 · 𝑠)𝑀1) = (𝐻‘(2 · 𝑠))) |
140 | | iftrue 4042 |
. . . . . 6
⊢ (𝑠 ≤ (1 / 2) → if(𝑠 ≤ (1 / 2), ((2 ·
𝑠)𝑀1), (((2 · 𝑠) − 1)𝑁1)) = ((2 · 𝑠)𝑀1)) |
141 | 140 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≤ (1 / 2)) → if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀1), (((2 · 𝑠) − 1)𝑁1)) = ((2 · 𝑠)𝑀1)) |
142 | | iftrue 4042 |
. . . . . 6
⊢ (𝑠 ≤ (1 / 2) → if(𝑠 ≤ (1 / 2), (𝐻‘(2 · 𝑠)), (𝐾‘((2 · 𝑠) − 1))) = (𝐻‘(2 · 𝑠))) |
143 | 142 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≤ (1 / 2)) → if(𝑠 ≤ (1 / 2), (𝐻‘(2 · 𝑠)), (𝐾‘((2 · 𝑠) − 1))) = (𝐻‘(2 · 𝑠))) |
144 | 139, 141,
143 | 3eqtr4d 2654 |
. . . 4
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≤ (1 / 2)) → if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀1), (((2 · 𝑠) − 1)𝑁1)) = if(𝑠 ≤ (1 / 2), (𝐻‘(2 · 𝑠)), (𝐾‘((2 · 𝑠) − 1)))) |
145 | 114 | simprd 478 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → (((2
· 𝑠) − 1)𝑁1) = (𝐾‘((2 · 𝑠) − 1))) |
146 | | iffalse 4045 |
. . . . . 6
⊢ (¬
𝑠 ≤ (1 / 2) →
if(𝑠 ≤ (1 / 2), ((2
· 𝑠)𝑀1), (((2 · 𝑠) − 1)𝑁1)) = (((2 · 𝑠) − 1)𝑁1)) |
147 | 146 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → if(𝑠 ≤ (1 / 2), ((2 ·
𝑠)𝑀1), (((2 · 𝑠) − 1)𝑁1)) = (((2 · 𝑠) − 1)𝑁1)) |
148 | | iffalse 4045 |
. . . . . 6
⊢ (¬
𝑠 ≤ (1 / 2) →
if(𝑠 ≤ (1 / 2), (𝐻‘(2 · 𝑠)), (𝐾‘((2 · 𝑠) − 1))) = (𝐾‘((2 · 𝑠) − 1))) |
149 | 148 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → if(𝑠 ≤ (1 / 2), (𝐻‘(2 · 𝑠)), (𝐾‘((2 · 𝑠) − 1))) = (𝐾‘((2 · 𝑠) − 1))) |
150 | 145, 147,
149 | 3eqtr4d 2654 |
. . . 4
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → if(𝑠 ≤ (1 / 2), ((2 ·
𝑠)𝑀1), (((2 · 𝑠) − 1)𝑁1)) = if(𝑠 ≤ (1 / 2), (𝐻‘(2 · 𝑠)), (𝐾‘((2 · 𝑠) − 1)))) |
151 | 144, 150 | pm2.61dan 828 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀1), (((2 · 𝑠) − 1)𝑁1)) = if(𝑠 ≤ (1 / 2), (𝐻‘(2 · 𝑠)), (𝐾‘((2 · 𝑠) − 1)))) |
152 | | 1elunit 12162 |
. . . 4
⊢ 1 ∈
(0[,]1) |
153 | | simpl 472 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → 𝑥 = 𝑠) |
154 | 153 | breq1d 4593 |
. . . . . 6
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → (𝑥 ≤ (1 / 2) ↔ 𝑠 ≤ (1 / 2))) |
155 | 153 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → (2 · 𝑥) = (2 · 𝑠)) |
156 | | simpr 476 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → 𝑦 = 1) |
157 | 155, 156 | oveq12d 6567 |
. . . . . 6
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → ((2 · 𝑥)𝑀𝑦) = ((2 · 𝑠)𝑀1)) |
158 | 155 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → ((2 · 𝑥) − 1) = ((2 · 𝑠) − 1)) |
159 | 158, 156 | oveq12d 6567 |
. . . . . 6
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → (((2 · 𝑥) − 1)𝑁𝑦) = (((2 · 𝑠) − 1)𝑁1)) |
160 | 154, 157,
159 | ifbieq12d 4063 |
. . . . 5
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 1) → if(𝑥 ≤ (1 / 2), ((2 · 𝑥)𝑀𝑦), (((2 · 𝑥) − 1)𝑁𝑦)) = if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀1), (((2 · 𝑠) − 1)𝑁1))) |
161 | | ovex 6577 |
. . . . . 6
⊢ ((2
· 𝑠)𝑀1) ∈ V |
162 | | ovex 6577 |
. . . . . 6
⊢ (((2
· 𝑠) − 1)𝑁1) ∈ V |
163 | 161, 162 | ifex 4106 |
. . . . 5
⊢ if(𝑠 ≤ (1 / 2), ((2 ·
𝑠)𝑀1), (((2 · 𝑠) − 1)𝑁1)) ∈ V |
164 | 160, 21, 163 | ovmpt2a 6689 |
. . . 4
⊢ ((𝑠 ∈ (0[,]1) ∧ 1 ∈
(0[,]1)) → (𝑠𝑃1) = if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀1), (((2 · 𝑠) − 1)𝑁1))) |
165 | 122, 152,
164 | sylancl 693 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝑠𝑃1) = if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀1), (((2 · 𝑠) − 1)𝑁1))) |
166 | 11, 12 | pcovalg 22620 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((𝐻(*𝑝‘𝐽)𝐾)‘𝑠) = if(𝑠 ≤ (1 / 2), (𝐻‘(2 · 𝑠)), (𝐾‘((2 · 𝑠) − 1)))) |
167 | 151, 165,
166 | 3eqtr4d 2654 |
. 2
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝑠𝑃1) = ((𝐻(*𝑝‘𝐽)𝐾)‘𝑠)) |
168 | 4, 11, 13 | phtpyi 22591 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((0𝑀𝑠) = (𝐹‘0) ∧ (1𝑀𝑠) = (𝐹‘1))) |
169 | 168 | simpld 474 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (0𝑀𝑠) = (𝐹‘0)) |
170 | | simpl 472 |
. . . . . . . 8
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → 𝑥 = 0) |
171 | 170, 31 | syl6eqbr 4622 |
. . . . . . 7
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → 𝑥 ≤ (1 / 2)) |
172 | 171 | iftrued 4044 |
. . . . . 6
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → if(𝑥 ≤ (1 / 2), ((2 · 𝑥)𝑀𝑦), (((2 · 𝑥) − 1)𝑁𝑦)) = ((2 · 𝑥)𝑀𝑦)) |
173 | 170 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → (2 · 𝑥) = (2 · 0)) |
174 | | 2t0e0 11060 |
. . . . . . . 8
⊢ (2
· 0) = 0 |
175 | 173, 174 | syl6eq 2660 |
. . . . . . 7
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → (2 · 𝑥) = 0) |
176 | | simpr 476 |
. . . . . . 7
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → 𝑦 = 𝑠) |
177 | 175, 176 | oveq12d 6567 |
. . . . . 6
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → ((2 · 𝑥)𝑀𝑦) = (0𝑀𝑠)) |
178 | 172, 177 | eqtrd 2644 |
. . . . 5
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → if(𝑥 ≤ (1 / 2), ((2 · 𝑥)𝑀𝑦), (((2 · 𝑥) − 1)𝑁𝑦)) = (0𝑀𝑠)) |
179 | | ovex 6577 |
. . . . 5
⊢ (0𝑀𝑠) ∈ V |
180 | 178, 21, 179 | ovmpt2a 6689 |
. . . 4
⊢ ((0
∈ (0[,]1) ∧ 𝑠
∈ (0[,]1)) → (0𝑃𝑠) = (0𝑀𝑠)) |
181 | 123, 122,
180 | sylancr 694 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (0𝑃𝑠) = (0𝑀𝑠)) |
182 | 4, 8 | pco0 22622 |
. . . 4
⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐺)‘0) = (𝐹‘0)) |
183 | 182 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((𝐹(*𝑝‘𝐽)𝐺)‘0) = (𝐹‘0)) |
184 | 169, 181,
183 | 3eqtr4d 2654 |
. 2
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (0𝑃𝑠) = ((𝐹(*𝑝‘𝐽)𝐺)‘0)) |
185 | 8, 12, 16 | phtpyi 22591 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((0𝑁𝑠) = (𝐺‘0) ∧ (1𝑁𝑠) = (𝐺‘1))) |
186 | 185 | simprd 478 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (1𝑁𝑠) = (𝐺‘1)) |
187 | 28, 32 | ltnlei 10037 |
. . . . . . . . 9
⊢ ((1 / 2)
< 1 ↔ ¬ 1 ≤ (1 / 2)) |
188 | 33, 187 | mpbi 219 |
. . . . . . . 8
⊢ ¬ 1
≤ (1 / 2) |
189 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → 𝑥 = 1) |
190 | 189 | breq1d 4593 |
. . . . . . . 8
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → (𝑥 ≤ (1 / 2) ↔ 1 ≤ (1 /
2))) |
191 | 188, 190 | mtbiri 316 |
. . . . . . 7
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → ¬ 𝑥 ≤ (1 / 2)) |
192 | 191 | iffalsed 4047 |
. . . . . 6
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → if(𝑥 ≤ (1 / 2), ((2 · 𝑥)𝑀𝑦), (((2 · 𝑥) − 1)𝑁𝑦)) = (((2 · 𝑥) − 1)𝑁𝑦)) |
193 | 189 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → (2 · 𝑥) = (2 · 1)) |
194 | | 2t1e2 11053 |
. . . . . . . . . 10
⊢ (2
· 1) = 2 |
195 | 193, 194 | syl6eq 2660 |
. . . . . . . . 9
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → (2 · 𝑥) = 2) |
196 | 195 | oveq1d 6564 |
. . . . . . . 8
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → ((2 · 𝑥) − 1) = (2 −
1)) |
197 | | 2m1e1 11012 |
. . . . . . . 8
⊢ (2
− 1) = 1 |
198 | 196, 197 | syl6eq 2660 |
. . . . . . 7
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → ((2 · 𝑥) − 1) = 1) |
199 | | simpr 476 |
. . . . . . 7
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → 𝑦 = 𝑠) |
200 | 198, 199 | oveq12d 6567 |
. . . . . 6
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → (((2 · 𝑥) − 1)𝑁𝑦) = (1𝑁𝑠)) |
201 | 192, 200 | eqtrd 2644 |
. . . . 5
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → if(𝑥 ≤ (1 / 2), ((2 · 𝑥)𝑀𝑦), (((2 · 𝑥) − 1)𝑁𝑦)) = (1𝑁𝑠)) |
202 | | ovex 6577 |
. . . . 5
⊢ (1𝑁𝑠) ∈ V |
203 | 201, 21, 202 | ovmpt2a 6689 |
. . . 4
⊢ ((1
∈ (0[,]1) ∧ 𝑠
∈ (0[,]1)) → (1𝑃𝑠) = (1𝑁𝑠)) |
204 | 152, 122,
203 | sylancr 694 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (1𝑃𝑠) = (1𝑁𝑠)) |
205 | 4, 8 | pco1 22623 |
. . . 4
⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐺)‘1) = (𝐺‘1)) |
206 | 205 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → ((𝐹(*𝑝‘𝐽)𝐺)‘1) = (𝐺‘1)) |
207 | 186, 204,
206 | 3eqtr4d 2654 |
. 2
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (1𝑃𝑠) = ((𝐹(*𝑝‘𝐽)𝐺)‘1)) |
208 | 10, 20, 90, 138, 167, 184, 207 | isphtpy2d 22594 |
1
⊢ (𝜑 → 𝑃 ∈ ((𝐹(*𝑝‘𝐽)𝐺)(PHtpy‘𝐽)(𝐻(*𝑝‘𝐽)𝐾))) |