Step | Hyp | Ref
| Expression |
1 | | elcnop 29938 |
. . . 4
⊢ (𝑇 ∈ ContOp ↔ (𝑇: ℋ⟶ ℋ ∧
∀𝑧 ∈ ℋ
∀𝑤 ∈
ℝ+ ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ ℋ
((normℎ‘(𝑦 −ℎ 𝑧)) < 𝑥 →
(normℎ‘((𝑇‘𝑦) −ℎ (𝑇‘𝑧))) < 𝑤))) |
2 | 1 | simprbi 500 |
. . 3
⊢ (𝑇 ∈ ContOp →
∀𝑧 ∈ ℋ
∀𝑤 ∈
ℝ+ ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ ℋ
((normℎ‘(𝑦 −ℎ 𝑧)) < 𝑥 →
(normℎ‘((𝑇‘𝑦) −ℎ (𝑇‘𝑧))) < 𝑤)) |
3 | | oveq2 7221 |
. . . . . . . 8
⊢ (𝑧 = 𝐴 → (𝑦 −ℎ 𝑧) = (𝑦 −ℎ 𝐴)) |
4 | 3 | fveq2d 6721 |
. . . . . . 7
⊢ (𝑧 = 𝐴 →
(normℎ‘(𝑦 −ℎ 𝑧)) =
(normℎ‘(𝑦 −ℎ 𝐴))) |
5 | 4 | breq1d 5063 |
. . . . . 6
⊢ (𝑧 = 𝐴 →
((normℎ‘(𝑦 −ℎ 𝑧)) < 𝑥 ↔ (normℎ‘(𝑦 −ℎ
𝐴)) < 𝑥)) |
6 | | fveq2 6717 |
. . . . . . . . 9
⊢ (𝑧 = 𝐴 → (𝑇‘𝑧) = (𝑇‘𝐴)) |
7 | 6 | oveq2d 7229 |
. . . . . . . 8
⊢ (𝑧 = 𝐴 → ((𝑇‘𝑦) −ℎ (𝑇‘𝑧)) = ((𝑇‘𝑦) −ℎ (𝑇‘𝐴))) |
8 | 7 | fveq2d 6721 |
. . . . . . 7
⊢ (𝑧 = 𝐴 →
(normℎ‘((𝑇‘𝑦) −ℎ (𝑇‘𝑧))) = (normℎ‘((𝑇‘𝑦) −ℎ (𝑇‘𝐴)))) |
9 | 8 | breq1d 5063 |
. . . . . 6
⊢ (𝑧 = 𝐴 →
((normℎ‘((𝑇‘𝑦) −ℎ (𝑇‘𝑧))) < 𝑤 ↔
(normℎ‘((𝑇‘𝑦) −ℎ (𝑇‘𝐴))) < 𝑤)) |
10 | 5, 9 | imbi12d 348 |
. . . . 5
⊢ (𝑧 = 𝐴 →
(((normℎ‘(𝑦 −ℎ 𝑧)) < 𝑥 →
(normℎ‘((𝑇‘𝑦) −ℎ (𝑇‘𝑧))) < 𝑤) ↔
((normℎ‘(𝑦 −ℎ 𝐴)) < 𝑥 →
(normℎ‘((𝑇‘𝑦) −ℎ (𝑇‘𝐴))) < 𝑤))) |
11 | 10 | rexralbidv 3220 |
. . . 4
⊢ (𝑧 = 𝐴 → (∃𝑥 ∈ ℝ+ ∀𝑦 ∈ ℋ
((normℎ‘(𝑦 −ℎ 𝑧)) < 𝑥 →
(normℎ‘((𝑇‘𝑦) −ℎ (𝑇‘𝑧))) < 𝑤) ↔ ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ ℋ
((normℎ‘(𝑦 −ℎ 𝐴)) < 𝑥 →
(normℎ‘((𝑇‘𝑦) −ℎ (𝑇‘𝐴))) < 𝑤))) |
12 | | breq2 5057 |
. . . . . 6
⊢ (𝑤 = 𝐵 →
((normℎ‘((𝑇‘𝑦) −ℎ (𝑇‘𝐴))) < 𝑤 ↔
(normℎ‘((𝑇‘𝑦) −ℎ (𝑇‘𝐴))) < 𝐵)) |
13 | 12 | imbi2d 344 |
. . . . 5
⊢ (𝑤 = 𝐵 →
(((normℎ‘(𝑦 −ℎ 𝐴)) < 𝑥 →
(normℎ‘((𝑇‘𝑦) −ℎ (𝑇‘𝐴))) < 𝑤) ↔
((normℎ‘(𝑦 −ℎ 𝐴)) < 𝑥 →
(normℎ‘((𝑇‘𝑦) −ℎ (𝑇‘𝐴))) < 𝐵))) |
14 | 13 | rexralbidv 3220 |
. . . 4
⊢ (𝑤 = 𝐵 → (∃𝑥 ∈ ℝ+ ∀𝑦 ∈ ℋ
((normℎ‘(𝑦 −ℎ 𝐴)) < 𝑥 →
(normℎ‘((𝑇‘𝑦) −ℎ (𝑇‘𝐴))) < 𝑤) ↔ ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ ℋ
((normℎ‘(𝑦 −ℎ 𝐴)) < 𝑥 →
(normℎ‘((𝑇‘𝑦) −ℎ (𝑇‘𝐴))) < 𝐵))) |
15 | 11, 14 | rspc2v 3547 |
. . 3
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℝ+)
→ (∀𝑧 ∈
ℋ ∀𝑤 ∈
ℝ+ ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ ℋ
((normℎ‘(𝑦 −ℎ 𝑧)) < 𝑥 →
(normℎ‘((𝑇‘𝑦) −ℎ (𝑇‘𝑧))) < 𝑤) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ ℋ
((normℎ‘(𝑦 −ℎ 𝐴)) < 𝑥 →
(normℎ‘((𝑇‘𝑦) −ℎ (𝑇‘𝐴))) < 𝐵))) |
16 | 2, 15 | syl5com 31 |
. 2
⊢ (𝑇 ∈ ContOp → ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℝ+)
→ ∃𝑥 ∈
ℝ+ ∀𝑦 ∈ ℋ
((normℎ‘(𝑦 −ℎ 𝐴)) < 𝑥 →
(normℎ‘((𝑇‘𝑦) −ℎ (𝑇‘𝐴))) < 𝐵))) |
17 | 16 | 3impib 1118 |
1
⊢ ((𝑇 ∈ ContOp ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℝ+)
→ ∃𝑥 ∈
ℝ+ ∀𝑦 ∈ ℋ
((normℎ‘(𝑦 −ℎ 𝐴)) < 𝑥 →
(normℎ‘((𝑇‘𝑦) −ℎ (𝑇‘𝐴))) < 𝐵)) |