Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pcohtpylem Structured version   Visualization version   GIF version

Theorem pcohtpylem 23713
 Description: Lemma for pcohtpy 23714. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 24-Feb-2015.)
Hypotheses
Ref Expression
pcohtpy.4 (𝜑 → (𝐹‘1) = (𝐺‘0))
pcohtpy.5 (𝜑𝐹( ≃ph𝐽)𝐻)
pcohtpy.6 (𝜑𝐺( ≃ph𝐽)𝐾)
pcohtpylem.7 𝑃 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), ((2 · 𝑥)𝑀𝑦), (((2 · 𝑥) − 1)𝑁𝑦)))
pcohtpylem.8 (𝜑𝑀 ∈ (𝐹(PHtpy‘𝐽)𝐻))
pcohtpylem.9 (𝜑𝑁 ∈ (𝐺(PHtpy‘𝐽)𝐾))
Assertion
Ref Expression
pcohtpylem (𝜑𝑃 ∈ ((𝐹(*𝑝𝐽)𝐺)(PHtpy‘𝐽)(𝐻(*𝑝𝐽)𝐾)))
Distinct variable groups:   𝑥,𝑦,𝐹   𝑥,𝑀,𝑦   𝑥,𝑁,𝑦   𝜑,𝑥,𝑦   𝑥,𝐺,𝑦   𝑥,𝐻,𝑦   𝑥,𝐽,𝑦   𝑥,𝐾,𝑦
Allowed substitution hints:   𝑃(𝑥,𝑦)

Proof of Theorem pcohtpylem
Dummy variables 𝑠 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pcohtpy.5 . . . . 5 (𝜑𝐹( ≃ph𝐽)𝐻)
2 isphtpc 23688 . . . . 5 (𝐹( ≃ph𝐽)𝐻 ↔ (𝐹 ∈ (II Cn 𝐽) ∧ 𝐻 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐻) ≠ ∅))
31, 2sylib 221 . . . 4 (𝜑 → (𝐹 ∈ (II Cn 𝐽) ∧ 𝐻 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐻) ≠ ∅))
43simp1d 1140 . . 3 (𝜑𝐹 ∈ (II Cn 𝐽))
5 pcohtpy.6 . . . . 5 (𝜑𝐺( ≃ph𝐽)𝐾)
6 isphtpc 23688 . . . . 5 (𝐺( ≃ph𝐽)𝐾 ↔ (𝐺 ∈ (II Cn 𝐽) ∧ 𝐾 ∈ (II Cn 𝐽) ∧ (𝐺(PHtpy‘𝐽)𝐾) ≠ ∅))
75, 6sylib 221 . . . 4 (𝜑 → (𝐺 ∈ (II Cn 𝐽) ∧ 𝐾 ∈ (II Cn 𝐽) ∧ (𝐺(PHtpy‘𝐽)𝐾) ≠ ∅))
87simp1d 1140 . . 3 (𝜑𝐺 ∈ (II Cn 𝐽))
9 pcohtpy.4 . . 3 (𝜑 → (𝐹‘1) = (𝐺‘0))
104, 8, 9pcocn 23711 . 2 (𝜑 → (𝐹(*𝑝𝐽)𝐺) ∈ (II Cn 𝐽))
113simp2d 1141 . . 3 (𝜑𝐻 ∈ (II Cn 𝐽))
127simp2d 1141 . . 3 (𝜑𝐾 ∈ (II Cn 𝐽))
13 pcohtpylem.8 . . . . . 6 (𝜑𝑀 ∈ (𝐹(PHtpy‘𝐽)𝐻))
144, 11, 13phtpy01 23679 . . . . 5 (𝜑 → ((𝐹‘0) = (𝐻‘0) ∧ (𝐹‘1) = (𝐻‘1)))
1514simprd 500 . . . 4 (𝜑 → (𝐹‘1) = (𝐻‘1))
16 pcohtpylem.9 . . . . . 6 (𝜑𝑁 ∈ (𝐺(PHtpy‘𝐽)𝐾))
178, 12, 16phtpy01 23679 . . . . 5 (𝜑 → ((𝐺‘0) = (𝐾‘0) ∧ (𝐺‘1) = (𝐾‘1)))
1817simpld 499 . . . 4 (𝜑 → (𝐺‘0) = (𝐾‘0))
199, 15, 183eqtr3d 2802 . . 3 (𝜑 → (𝐻‘1) = (𝐾‘0))
2011, 12, 19pcocn 23711 . 2 (𝜑 → (𝐻(*𝑝𝐽)𝐾) ∈ (II Cn 𝐽))
21 pcohtpylem.7 . . 3 𝑃 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), ((2 · 𝑥)𝑀𝑦), (((2 · 𝑥) − 1)𝑁𝑦)))
22 eqid 2759 . . . 4 (topGen‘ran (,)) = (topGen‘ran (,))
23 eqid 2759 . . . 4 ((topGen‘ran (,)) ↾t (0[,](1 / 2))) = ((topGen‘ran (,)) ↾t (0[,](1 / 2)))
24 eqid 2759 . . . 4 ((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) = ((topGen‘ran (,)) ↾t ((1 / 2)[,]1))
25 dfii2 23576 . . . 4 II = ((topGen‘ran (,)) ↾t (0[,]1))
26 0red 10675 . . . 4 (𝜑 → 0 ∈ ℝ)
27 1red 10673 . . . 4 (𝜑 → 1 ∈ ℝ)
28 halfre 11881 . . . . . 6 (1 / 2) ∈ ℝ
29 halfge0 11884 . . . . . 6 0 ≤ (1 / 2)
30 1re 10672 . . . . . . 7 1 ∈ ℝ
31 halflt1 11885 . . . . . . 7 (1 / 2) < 1
3228, 30, 31ltleii 10794 . . . . . 6 (1 / 2) ≤ 1
33 elicc01 12891 . . . . . 6 ((1 / 2) ∈ (0[,]1) ↔ ((1 / 2) ∈ ℝ ∧ 0 ≤ (1 / 2) ∧ (1 / 2) ≤ 1))
3428, 29, 32, 33mpbir3an 1339 . . . . 5 (1 / 2) ∈ (0[,]1)
3534a1i 11 . . . 4 (𝜑 → (1 / 2) ∈ (0[,]1))
36 iitopon 23573 . . . . 5 II ∈ (TopOn‘(0[,]1))
3736a1i 11 . . . 4 (𝜑 → II ∈ (TopOn‘(0[,]1)))
389adantr 485 . . . . . 6 ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → (𝐹‘1) = (𝐺‘0))
394, 11, 13phtpyi 23678 . . . . . . . 8 ((𝜑𝑦 ∈ (0[,]1)) → ((0𝑀𝑦) = (𝐹‘0) ∧ (1𝑀𝑦) = (𝐹‘1)))
4039simprd 500 . . . . . . 7 ((𝜑𝑦 ∈ (0[,]1)) → (1𝑀𝑦) = (𝐹‘1))
4140adantrl 716 . . . . . 6 ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → (1𝑀𝑦) = (𝐹‘1))
428, 12, 16phtpyi 23678 . . . . . . . 8 ((𝜑𝑦 ∈ (0[,]1)) → ((0𝑁𝑦) = (𝐺‘0) ∧ (1𝑁𝑦) = (𝐺‘1)))
4342simpld 499 . . . . . . 7 ((𝜑𝑦 ∈ (0[,]1)) → (0𝑁𝑦) = (𝐺‘0))
4443adantrl 716 . . . . . 6 ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → (0𝑁𝑦) = (𝐺‘0))
4538, 41, 443eqtr4d 2804 . . . . 5 ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → (1𝑀𝑦) = (0𝑁𝑦))
46 simprl 771 . . . . . . . 8 ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → 𝑥 = (1 / 2))
4746oveq2d 7167 . . . . . . 7 ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → (2 · 𝑥) = (2 · (1 / 2)))
48 2cn 11742 . . . . . . . 8 2 ∈ ℂ
49 2ne0 11771 . . . . . . . 8 2 ≠ 0
5048, 49recidi 11402 . . . . . . 7 (2 · (1 / 2)) = 1
5147, 50eqtrdi 2810 . . . . . 6 ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → (2 · 𝑥) = 1)
5251oveq1d 7166 . . . . 5 ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → ((2 · 𝑥)𝑀𝑦) = (1𝑀𝑦))
5351oveq1d 7166 . . . . . . 7 ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → ((2 · 𝑥) − 1) = (1 − 1))
54 1m1e0 11739 . . . . . . 7 (1 − 1) = 0
5553, 54eqtrdi 2810 . . . . . 6 ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → ((2 · 𝑥) − 1) = 0)
5655oveq1d 7166 . . . . 5 ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → (((2 · 𝑥) − 1)𝑁𝑦) = (0𝑁𝑦))
5745, 52, 563eqtr4d 2804 . . . 4 ((𝜑 ∧ (𝑥 = (1 / 2) ∧ 𝑦 ∈ (0[,]1))) → ((2 · 𝑥)𝑀𝑦) = (((2 · 𝑥) − 1)𝑁𝑦))
58 retopon 23458 . . . . . . 7 (topGen‘ran (,)) ∈ (TopOn‘ℝ)
59 0re 10674 . . . . . . . 8 0 ∈ ℝ
60 iccssre 12854 . . . . . . . 8 ((0 ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (0[,](1 / 2)) ⊆ ℝ)
6159, 28, 60mp2an 692 . . . . . . 7 (0[,](1 / 2)) ⊆ ℝ
62 resttopon 21854 . . . . . . 7 (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (0[,](1 / 2)) ⊆ ℝ) → ((topGen‘ran (,)) ↾t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 / 2))))
6358, 61, 62mp2an 692 . . . . . 6 ((topGen‘ran (,)) ↾t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 / 2)))
6463a1i 11 . . . . 5 (𝜑 → ((topGen‘ran (,)) ↾t (0[,](1 / 2))) ∈ (TopOn‘(0[,](1 / 2))))
6564, 37cnmpt1st 22361 . . . . . 6 (𝜑 → (𝑥 ∈ (0[,](1 / 2)), 𝑦 ∈ (0[,]1) ↦ 𝑥) ∈ ((((topGen‘ran (,)) ↾t (0[,](1 / 2))) ×t II) Cn ((topGen‘ran (,)) ↾t (0[,](1 / 2)))))
6623iihalf1cn 23626 . . . . . . 7 (𝑧 ∈ (0[,](1 / 2)) ↦ (2 · 𝑧)) ∈ (((topGen‘ran (,)) ↾t (0[,](1 / 2))) Cn II)
6766a1i 11 . . . . . 6 (𝜑 → (𝑧 ∈ (0[,](1 / 2)) ↦ (2 · 𝑧)) ∈ (((topGen‘ran (,)) ↾t (0[,](1 / 2))) Cn II))
68 oveq2 7159 . . . . . 6 (𝑧 = 𝑥 → (2 · 𝑧) = (2 · 𝑥))
6964, 37, 65, 64, 67, 68cnmpt21 22364 . . . . 5 (𝜑 → (𝑥 ∈ (0[,](1 / 2)), 𝑦 ∈ (0[,]1) ↦ (2 · 𝑥)) ∈ ((((topGen‘ran (,)) ↾t (0[,](1 / 2))) ×t II) Cn II))
7064, 37cnmpt2nd 22362 . . . . 5 (𝜑 → (𝑥 ∈ (0[,](1 / 2)), 𝑦 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,)) ↾t (0[,](1 / 2))) ×t II) Cn II))
714, 11phtpycn 23677 . . . . . 6 (𝜑 → (𝐹(PHtpy‘𝐽)𝐻) ⊆ ((II ×t II) Cn 𝐽))
7271, 13sseldd 3894 . . . . 5 (𝜑𝑀 ∈ ((II ×t II) Cn 𝐽))
7364, 37, 69, 70, 72cnmpt22f 22368 . . . 4 (𝜑 → (𝑥 ∈ (0[,](1 / 2)), 𝑦 ∈ (0[,]1) ↦ ((2 · 𝑥)𝑀𝑦)) ∈ ((((topGen‘ran (,)) ↾t (0[,](1 / 2))) ×t II) Cn 𝐽))
74 iccssre 12854 . . . . . . . 8 (((1 / 2) ∈ ℝ ∧ 1 ∈ ℝ) → ((1 / 2)[,]1) ⊆ ℝ)
7528, 30, 74mp2an 692 . . . . . . 7 ((1 / 2)[,]1) ⊆ ℝ
76 resttopon 21854 . . . . . . 7 (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((1 / 2)[,]1) ⊆ ℝ) → ((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1)))
7758, 75, 76mp2an 692 . . . . . 6 ((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1))
7877a1i 11 . . . . 5 (𝜑 → ((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ∈ (TopOn‘((1 / 2)[,]1)))
7978, 37cnmpt1st 22361 . . . . . 6 (𝜑 → (𝑥 ∈ ((1 / 2)[,]1), 𝑦 ∈ (0[,]1) ↦ 𝑥) ∈ ((((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ×t II) Cn ((topGen‘ran (,)) ↾t ((1 / 2)[,]1))))
8024iihalf2cn 23628 . . . . . . 7 (𝑧 ∈ ((1 / 2)[,]1) ↦ ((2 · 𝑧) − 1)) ∈ (((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) Cn II)
8180a1i 11 . . . . . 6 (𝜑 → (𝑧 ∈ ((1 / 2)[,]1) ↦ ((2 · 𝑧) − 1)) ∈ (((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) Cn II))
8268oveq1d 7166 . . . . . 6 (𝑧 = 𝑥 → ((2 · 𝑧) − 1) = ((2 · 𝑥) − 1))
8378, 37, 79, 78, 81, 82cnmpt21 22364 . . . . 5 (𝜑 → (𝑥 ∈ ((1 / 2)[,]1), 𝑦 ∈ (0[,]1) ↦ ((2 · 𝑥) − 1)) ∈ ((((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ×t II) Cn II))
8478, 37cnmpt2nd 22362 . . . . 5 (𝜑 → (𝑥 ∈ ((1 / 2)[,]1), 𝑦 ∈ (0[,]1) ↦ 𝑦) ∈ ((((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ×t II) Cn II))
858, 12phtpycn 23677 . . . . . 6 (𝜑 → (𝐺(PHtpy‘𝐽)𝐾) ⊆ ((II ×t II) Cn 𝐽))
8685, 16sseldd 3894 . . . . 5 (𝜑𝑁 ∈ ((II ×t II) Cn 𝐽))
8778, 37, 83, 84, 86cnmpt22f 22368 . . . 4 (𝜑 → (𝑥 ∈ ((1 / 2)[,]1), 𝑦 ∈ (0[,]1) ↦ (((2 · 𝑥) − 1)𝑁𝑦)) ∈ ((((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ×t II) Cn 𝐽))
8822, 23, 24, 25, 26, 27, 35, 37, 57, 73, 87cnmpopc 23622 . . 3 (𝜑 → (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), ((2 · 𝑥)𝑀𝑦), (((2 · 𝑥) − 1)𝑁𝑦))) ∈ ((II ×t II) Cn 𝐽))
8921, 88eqeltrid 2857 . 2 (𝜑𝑃 ∈ ((II ×t II) Cn 𝐽))
90 simpll 767 . . . . . 6 (((𝜑𝑠 ∈ (0[,]1)) ∧ 𝑠 ≤ (1 / 2)) → 𝜑)
91 elii1 23629 . . . . . . . 8 (𝑠 ∈ (0[,](1 / 2)) ↔ (𝑠 ∈ (0[,]1) ∧ 𝑠 ≤ (1 / 2)))
92 iihalf1 23625 . . . . . . . 8 (𝑠 ∈ (0[,](1 / 2)) → (2 · 𝑠) ∈ (0[,]1))
9391, 92sylbir 238 . . . . . . 7 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≤ (1 / 2)) → (2 · 𝑠) ∈ (0[,]1))
9493adantll 714 . . . . . 6 (((𝜑𝑠 ∈ (0[,]1)) ∧ 𝑠 ≤ (1 / 2)) → (2 · 𝑠) ∈ (0[,]1))
954, 11phtpyhtpy 23676 . . . . . . . 8 (𝜑 → (𝐹(PHtpy‘𝐽)𝐻) ⊆ (𝐹(II Htpy 𝐽)𝐻))
9695, 13sseldd 3894 . . . . . . 7 (𝜑𝑀 ∈ (𝐹(II Htpy 𝐽)𝐻))
9737, 4, 11, 96htpyi 23668 . . . . . 6 ((𝜑 ∧ (2 · 𝑠) ∈ (0[,]1)) → (((2 · 𝑠)𝑀0) = (𝐹‘(2 · 𝑠)) ∧ ((2 · 𝑠)𝑀1) = (𝐻‘(2 · 𝑠))))
9890, 94, 97syl2anc 588 . . . . 5 (((𝜑𝑠 ∈ (0[,]1)) ∧ 𝑠 ≤ (1 / 2)) → (((2 · 𝑠)𝑀0) = (𝐹‘(2 · 𝑠)) ∧ ((2 · 𝑠)𝑀1) = (𝐻‘(2 · 𝑠))))
9998simpld 499 . . . 4 (((𝜑𝑠 ∈ (0[,]1)) ∧ 𝑠 ≤ (1 / 2)) → ((2 · 𝑠)𝑀0) = (𝐹‘(2 · 𝑠)))
100 simpll 767 . . . . . 6 (((𝜑𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → 𝜑)
101 elii2 23630 . . . . . . . 8 ((𝑠 ∈ (0[,]1) ∧ ¬ 𝑠 ≤ (1 / 2)) → 𝑠 ∈ ((1 / 2)[,]1))
102101adantll 714 . . . . . . 7 (((𝜑𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → 𝑠 ∈ ((1 / 2)[,]1))
103 iihalf2 23627 . . . . . . 7 (𝑠 ∈ ((1 / 2)[,]1) → ((2 · 𝑠) − 1) ∈ (0[,]1))
104102, 103syl 17 . . . . . 6 (((𝜑𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → ((2 · 𝑠) − 1) ∈ (0[,]1))
1058, 12phtpyhtpy 23676 . . . . . . . 8 (𝜑 → (𝐺(PHtpy‘𝐽)𝐾) ⊆ (𝐺(II Htpy 𝐽)𝐾))
106105, 16sseldd 3894 . . . . . . 7 (𝜑𝑁 ∈ (𝐺(II Htpy 𝐽)𝐾))
10737, 8, 12, 106htpyi 23668 . . . . . 6 ((𝜑 ∧ ((2 · 𝑠) − 1) ∈ (0[,]1)) → ((((2 · 𝑠) − 1)𝑁0) = (𝐺‘((2 · 𝑠) − 1)) ∧ (((2 · 𝑠) − 1)𝑁1) = (𝐾‘((2 · 𝑠) − 1))))
108100, 104, 107syl2anc 588 . . . . 5 (((𝜑𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → ((((2 · 𝑠) − 1)𝑁0) = (𝐺‘((2 · 𝑠) − 1)) ∧ (((2 · 𝑠) − 1)𝑁1) = (𝐾‘((2 · 𝑠) − 1))))
109108simpld 499 . . . 4 (((𝜑𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → (((2 · 𝑠) − 1)𝑁0) = (𝐺‘((2 · 𝑠) − 1)))
11099, 109ifeq12da 4454 . . 3 ((𝜑𝑠 ∈ (0[,]1)) → if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀0), (((2 · 𝑠) − 1)𝑁0)) = if(𝑠 ≤ (1 / 2), (𝐹‘(2 · 𝑠)), (𝐺‘((2 · 𝑠) − 1))))
111 simpr 489 . . . 4 ((𝜑𝑠 ∈ (0[,]1)) → 𝑠 ∈ (0[,]1))
112 0elunit 12894 . . . 4 0 ∈ (0[,]1)
113 simpl 487 . . . . . . 7 ((𝑥 = 𝑠𝑦 = 0) → 𝑥 = 𝑠)
114113breq1d 5043 . . . . . 6 ((𝑥 = 𝑠𝑦 = 0) → (𝑥 ≤ (1 / 2) ↔ 𝑠 ≤ (1 / 2)))
115113oveq2d 7167 . . . . . . 7 ((𝑥 = 𝑠𝑦 = 0) → (2 · 𝑥) = (2 · 𝑠))
116 simpr 489 . . . . . . 7 ((𝑥 = 𝑠𝑦 = 0) → 𝑦 = 0)
117115, 116oveq12d 7169 . . . . . 6 ((𝑥 = 𝑠𝑦 = 0) → ((2 · 𝑥)𝑀𝑦) = ((2 · 𝑠)𝑀0))
118115oveq1d 7166 . . . . . . 7 ((𝑥 = 𝑠𝑦 = 0) → ((2 · 𝑥) − 1) = ((2 · 𝑠) − 1))
119118, 116oveq12d 7169 . . . . . 6 ((𝑥 = 𝑠𝑦 = 0) → (((2 · 𝑥) − 1)𝑁𝑦) = (((2 · 𝑠) − 1)𝑁0))
120114, 117, 119ifbieq12d 4449 . . . . 5 ((𝑥 = 𝑠𝑦 = 0) → if(𝑥 ≤ (1 / 2), ((2 · 𝑥)𝑀𝑦), (((2 · 𝑥) − 1)𝑁𝑦)) = if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀0), (((2 · 𝑠) − 1)𝑁0)))
121 ovex 7184 . . . . . 6 ((2 · 𝑠)𝑀0) ∈ V
122 ovex 7184 . . . . . 6 (((2 · 𝑠) − 1)𝑁0) ∈ V
123121, 122ifex 4471 . . . . 5 if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀0), (((2 · 𝑠) − 1)𝑁0)) ∈ V
124120, 21, 123ovmpoa 7301 . . . 4 ((𝑠 ∈ (0[,]1) ∧ 0 ∈ (0[,]1)) → (𝑠𝑃0) = if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀0), (((2 · 𝑠) − 1)𝑁0)))
125111, 112, 124sylancl 590 . . 3 ((𝜑𝑠 ∈ (0[,]1)) → (𝑠𝑃0) = if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀0), (((2 · 𝑠) − 1)𝑁0)))
1264, 8pcovalg 23706 . . 3 ((𝜑𝑠 ∈ (0[,]1)) → ((𝐹(*𝑝𝐽)𝐺)‘𝑠) = if(𝑠 ≤ (1 / 2), (𝐹‘(2 · 𝑠)), (𝐺‘((2 · 𝑠) − 1))))
127110, 125, 1263eqtr4d 2804 . 2 ((𝜑𝑠 ∈ (0[,]1)) → (𝑠𝑃0) = ((𝐹(*𝑝𝐽)𝐺)‘𝑠))
12898simprd 500 . . . 4 (((𝜑𝑠 ∈ (0[,]1)) ∧ 𝑠 ≤ (1 / 2)) → ((2 · 𝑠)𝑀1) = (𝐻‘(2 · 𝑠)))
129108simprd 500 . . . 4 (((𝜑𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → (((2 · 𝑠) − 1)𝑁1) = (𝐾‘((2 · 𝑠) − 1)))
130128, 129ifeq12da 4454 . . 3 ((𝜑𝑠 ∈ (0[,]1)) → if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀1), (((2 · 𝑠) − 1)𝑁1)) = if(𝑠 ≤ (1 / 2), (𝐻‘(2 · 𝑠)), (𝐾‘((2 · 𝑠) − 1))))
131 1elunit 12895 . . . 4 1 ∈ (0[,]1)
132 simpl 487 . . . . . . 7 ((𝑥 = 𝑠𝑦 = 1) → 𝑥 = 𝑠)
133132breq1d 5043 . . . . . 6 ((𝑥 = 𝑠𝑦 = 1) → (𝑥 ≤ (1 / 2) ↔ 𝑠 ≤ (1 / 2)))
134132oveq2d 7167 . . . . . . 7 ((𝑥 = 𝑠𝑦 = 1) → (2 · 𝑥) = (2 · 𝑠))
135 simpr 489 . . . . . . 7 ((𝑥 = 𝑠𝑦 = 1) → 𝑦 = 1)
136134, 135oveq12d 7169 . . . . . 6 ((𝑥 = 𝑠𝑦 = 1) → ((2 · 𝑥)𝑀𝑦) = ((2 · 𝑠)𝑀1))
137134oveq1d 7166 . . . . . . 7 ((𝑥 = 𝑠𝑦 = 1) → ((2 · 𝑥) − 1) = ((2 · 𝑠) − 1))
138137, 135oveq12d 7169 . . . . . 6 ((𝑥 = 𝑠𝑦 = 1) → (((2 · 𝑥) − 1)𝑁𝑦) = (((2 · 𝑠) − 1)𝑁1))
139133, 136, 138ifbieq12d 4449 . . . . 5 ((𝑥 = 𝑠𝑦 = 1) → if(𝑥 ≤ (1 / 2), ((2 · 𝑥)𝑀𝑦), (((2 · 𝑥) − 1)𝑁𝑦)) = if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀1), (((2 · 𝑠) − 1)𝑁1)))
140 ovex 7184 . . . . . 6 ((2 · 𝑠)𝑀1) ∈ V
141 ovex 7184 . . . . . 6 (((2 · 𝑠) − 1)𝑁1) ∈ V
142140, 141ifex 4471 . . . . 5 if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀1), (((2 · 𝑠) − 1)𝑁1)) ∈ V
143139, 21, 142ovmpoa 7301 . . . 4 ((𝑠 ∈ (0[,]1) ∧ 1 ∈ (0[,]1)) → (𝑠𝑃1) = if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀1), (((2 · 𝑠) − 1)𝑁1)))
144111, 131, 143sylancl 590 . . 3 ((𝜑𝑠 ∈ (0[,]1)) → (𝑠𝑃1) = if(𝑠 ≤ (1 / 2), ((2 · 𝑠)𝑀1), (((2 · 𝑠) − 1)𝑁1)))
14511, 12pcovalg 23706 . . 3 ((𝜑𝑠 ∈ (0[,]1)) → ((𝐻(*𝑝𝐽)𝐾)‘𝑠) = if(𝑠 ≤ (1 / 2), (𝐻‘(2 · 𝑠)), (𝐾‘((2 · 𝑠) − 1))))
146130, 144, 1453eqtr4d 2804 . 2 ((𝜑𝑠 ∈ (0[,]1)) → (𝑠𝑃1) = ((𝐻(*𝑝𝐽)𝐾)‘𝑠))
1474, 11, 13phtpyi 23678 . . . 4 ((𝜑𝑠 ∈ (0[,]1)) → ((0𝑀𝑠) = (𝐹‘0) ∧ (1𝑀𝑠) = (𝐹‘1)))
148147simpld 499 . . 3 ((𝜑𝑠 ∈ (0[,]1)) → (0𝑀𝑠) = (𝐹‘0))
149 simpl 487 . . . . . . . 8 ((𝑥 = 0 ∧ 𝑦 = 𝑠) → 𝑥 = 0)
150149, 29eqbrtrdi 5072 . . . . . . 7 ((𝑥 = 0 ∧ 𝑦 = 𝑠) → 𝑥 ≤ (1 / 2))
151150iftrued 4429 . . . . . 6 ((𝑥 = 0 ∧ 𝑦 = 𝑠) → if(𝑥 ≤ (1 / 2), ((2 · 𝑥)𝑀𝑦), (((2 · 𝑥) − 1)𝑁𝑦)) = ((2 · 𝑥)𝑀𝑦))
152149oveq2d 7167 . . . . . . . 8 ((𝑥 = 0 ∧ 𝑦 = 𝑠) → (2 · 𝑥) = (2 · 0))
153 2t0e0 11836 . . . . . . . 8 (2 · 0) = 0
154152, 153eqtrdi 2810 . . . . . . 7 ((𝑥 = 0 ∧ 𝑦 = 𝑠) → (2 · 𝑥) = 0)
155 simpr 489 . . . . . . 7 ((𝑥 = 0 ∧ 𝑦 = 𝑠) → 𝑦 = 𝑠)
156154, 155oveq12d 7169 . . . . . 6 ((𝑥 = 0 ∧ 𝑦 = 𝑠) → ((2 · 𝑥)𝑀𝑦) = (0𝑀𝑠))
157151, 156eqtrd 2794 . . . . 5 ((𝑥 = 0 ∧ 𝑦 = 𝑠) → if(𝑥 ≤ (1 / 2), ((2 · 𝑥)𝑀𝑦), (((2 · 𝑥) − 1)𝑁𝑦)) = (0𝑀𝑠))
158 ovex 7184 . . . . 5 (0𝑀𝑠) ∈ V
159157, 21, 158ovmpoa 7301 . . . 4 ((0 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) → (0𝑃𝑠) = (0𝑀𝑠))
160112, 111, 159sylancr 591 . . 3 ((𝜑𝑠 ∈ (0[,]1)) → (0𝑃𝑠) = (0𝑀𝑠))
1614, 8pco0 23708 . . . 4 (𝜑 → ((𝐹(*𝑝𝐽)𝐺)‘0) = (𝐹‘0))
162161adantr 485 . . 3 ((𝜑𝑠 ∈ (0[,]1)) → ((𝐹(*𝑝𝐽)𝐺)‘0) = (𝐹‘0))
163148, 160, 1623eqtr4d 2804 . 2 ((𝜑𝑠 ∈ (0[,]1)) → (0𝑃𝑠) = ((𝐹(*𝑝𝐽)𝐺)‘0))
1648, 12, 16phtpyi 23678 . . . 4 ((𝜑𝑠 ∈ (0[,]1)) → ((0𝑁𝑠) = (𝐺‘0) ∧ (1𝑁𝑠) = (𝐺‘1)))
165164simprd 500 . . 3 ((𝜑𝑠 ∈ (0[,]1)) → (1𝑁𝑠) = (𝐺‘1))
16628, 30ltnlei 10792 . . . . . . . . 9 ((1 / 2) < 1 ↔ ¬ 1 ≤ (1 / 2))
16731, 166mpbi 233 . . . . . . . 8 ¬ 1 ≤ (1 / 2)
168 simpl 487 . . . . . . . . 9 ((𝑥 = 1 ∧ 𝑦 = 𝑠) → 𝑥 = 1)
169168breq1d 5043 . . . . . . . 8 ((𝑥 = 1 ∧ 𝑦 = 𝑠) → (𝑥 ≤ (1 / 2) ↔ 1 ≤ (1 / 2)))
170167, 169mtbiri 331 . . . . . . 7 ((𝑥 = 1 ∧ 𝑦 = 𝑠) → ¬ 𝑥 ≤ (1 / 2))
171170iffalsed 4432 . . . . . 6 ((𝑥 = 1 ∧ 𝑦 = 𝑠) → if(𝑥 ≤ (1 / 2), ((2 · 𝑥)𝑀𝑦), (((2 · 𝑥) − 1)𝑁𝑦)) = (((2 · 𝑥) − 1)𝑁𝑦))
172168oveq2d 7167 . . . . . . . . . 10 ((𝑥 = 1 ∧ 𝑦 = 𝑠) → (2 · 𝑥) = (2 · 1))
173 2t1e2 11830 . . . . . . . . . 10 (2 · 1) = 2
174172, 173eqtrdi 2810 . . . . . . . . 9 ((𝑥 = 1 ∧ 𝑦 = 𝑠) → (2 · 𝑥) = 2)
175174oveq1d 7166 . . . . . . . 8 ((𝑥 = 1 ∧ 𝑦 = 𝑠) → ((2 · 𝑥) − 1) = (2 − 1))
176 2m1e1 11793 . . . . . . . 8 (2 − 1) = 1
177175, 176eqtrdi 2810 . . . . . . 7 ((𝑥 = 1 ∧ 𝑦 = 𝑠) → ((2 · 𝑥) − 1) = 1)
178 simpr 489 . . . . . . 7 ((𝑥 = 1 ∧ 𝑦 = 𝑠) → 𝑦 = 𝑠)
179177, 178oveq12d 7169 . . . . . 6 ((𝑥 = 1 ∧ 𝑦 = 𝑠) → (((2 · 𝑥) − 1)𝑁𝑦) = (1𝑁𝑠))
180171, 179eqtrd 2794 . . . . 5 ((𝑥 = 1 ∧ 𝑦 = 𝑠) → if(𝑥 ≤ (1 / 2), ((2 · 𝑥)𝑀𝑦), (((2 · 𝑥) − 1)𝑁𝑦)) = (1𝑁𝑠))
181 ovex 7184 . . . . 5 (1𝑁𝑠) ∈ V
182180, 21, 181ovmpoa 7301 . . . 4 ((1 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) → (1𝑃𝑠) = (1𝑁𝑠))
183131, 111, 182sylancr 591 . . 3 ((𝜑𝑠 ∈ (0[,]1)) → (1𝑃𝑠) = (1𝑁𝑠))
1844, 8pco1 23709 . . . 4 (𝜑 → ((𝐹(*𝑝𝐽)𝐺)‘1) = (𝐺‘1))
185184adantr 485 . . 3 ((𝜑𝑠 ∈ (0[,]1)) → ((𝐹(*𝑝𝐽)𝐺)‘1) = (𝐺‘1))
186165, 183, 1853eqtr4d 2804 . 2 ((𝜑𝑠 ∈ (0[,]1)) → (1𝑃𝑠) = ((𝐹(*𝑝𝐽)𝐺)‘1))
18710, 20, 89, 127, 146, 163, 186isphtpy2d 23681 1 (𝜑𝑃 ∈ ((𝐹(*𝑝𝐽)𝐺)(PHtpy‘𝐽)(𝐻(*𝑝𝐽)𝐾)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112   ≠ wne 2952   ⊆ wss 3859  ∅c0 4226  ifcif 4421   class class class wbr 5033   ↦ cmpt 5113  ran crn 5526  ‘cfv 6336  (class class class)co 7151   ∈ cmpo 7153  ℝcr 10567  0cc0 10568  1c1 10569   · cmul 10573   < clt 10706   ≤ cle 10707   − cmin 10901   / cdiv 11328  2c2 11722  (,)cioo 12772  [,]cicc 12775   ↾t crest 16745  topGenctg 16762  TopOnctopon 21603   Cn ccn 21917   ×t ctx 22253  IIcii 23569   Htpy chtpy 23661  PHtpycphtpy 23662   ≃phcphtpc 23663  *𝑝cpco 23694 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460  ax-cnex 10624  ax-resscn 10625  ax-1cn 10626  ax-icn 10627  ax-addcl 10628  ax-addrcl 10629  ax-mulcl 10630  ax-mulrcl 10631  ax-mulcom 10632  ax-addass 10633  ax-mulass 10634  ax-distr 10635  ax-i2m1 10636  ax-1ne0 10637  ax-1rid 10638  ax-rnegex 10639  ax-rrecex 10640  ax-cnre 10641  ax-pre-lttri 10642  ax-pre-lttrn 10643  ax-pre-ltadd 10644  ax-pre-mulgt0 10645  ax-pre-sup 10646  ax-mulf 10648 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-tp 4528  df-op 4530  df-uni 4800  df-int 4840  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5431  df-eprel 5436  df-po 5444  df-so 5445  df-fr 5484  df-se 5485  df-we 5486  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6127  df-ord 6173  df-on 6174  df-lim 6175  df-suc 6176  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-isom 6345  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-of 7406  df-om 7581  df-1st 7694  df-2nd 7695  df-supp 7837  df-wrecs 7958  df-recs 8019  df-rdg 8057  df-1o 8113  df-2o 8114  df-oadd 8117  df-er 8300  df-map 8419  df-ixp 8481  df-en 8529  df-dom 8530  df-sdom 8531  df-fin 8532  df-fsupp 8860  df-fi 8901  df-sup 8932  df-inf 8933  df-oi 9000  df-card 9394  df-pnf 10708  df-mnf 10709  df-xr 10710  df-ltxr 10711  df-le 10712  df-sub 10903  df-neg 10904  df-div 11329  df-nn 11668  df-2 11730  df-3 11731  df-4 11732  df-5 11733  df-6 11734  df-7 11735  df-8 11736  df-9 11737  df-n0 11928  df-z 12014  df-dec 12131  df-uz 12276  df-q 12382  df-rp 12424  df-xneg 12541  df-xadd 12542  df-xmul 12543  df-ioo 12776  df-icc 12779  df-fz 12933  df-fzo 13076  df-seq 13412  df-exp 13473  df-hash 13734  df-cj 14499  df-re 14500  df-im 14501  df-sqrt 14635  df-abs 14636  df-struct 16536  df-ndx 16537  df-slot 16538  df-base 16540  df-sets 16541  df-ress 16542  df-plusg 16629  df-mulr 16630  df-starv 16631  df-sca 16632  df-vsca 16633  df-ip 16634  df-tset 16635  df-ple 16636  df-ds 16638  df-unif 16639  df-hom 16640  df-cco 16641  df-rest 16747  df-topn 16748  df-0g 16766  df-gsum 16767  df-topgen 16768  df-pt 16769  df-prds 16772  df-xrs 16826  df-qtop 16831  df-imas 16832  df-xps 16834  df-mre 16908  df-mrc 16909  df-acs 16911  df-mgm 17911  df-sgrp 17960  df-mnd 17971  df-submnd 18016  df-mulg 18285  df-cntz 18507  df-cmn 18968  df-psmet 20151  df-xmet 20152  df-met 20153  df-bl 20154  df-mopn 20155  df-cnfld 20160  df-top 21587  df-topon 21604  df-topsp 21626  df-bases 21639  df-cld 21712  df-cn 21920  df-cnp 21921  df-tx 22255  df-hmeo 22448  df-xms 23015  df-ms 23016  df-tms 23017  df-ii 23571  df-htpy 23664  df-phtpy 23665  df-phtpc 23686  df-pco 23699 This theorem is referenced by:  pcohtpy  23714
 Copyright terms: Public domain W3C validator