Proof of Theorem nmfnleub2
| Step | Hyp | Ref
| Expression |
| 1 | | normcl 31144 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℋ →
(normℎ‘𝑥) ∈ ℝ) |
| 2 | 1 | ad2antlr 727 |
. . . . . . . . . 10
⊢ ((((𝑇: ℋ⟶ℂ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) →
(normℎ‘𝑥) ∈ ℝ) |
| 3 | | simpllr 776 |
. . . . . . . . . 10
⊢ ((((𝑇: ℋ⟶ℂ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) |
| 4 | | simpr 484 |
. . . . . . . . . 10
⊢ ((((𝑇: ℋ⟶ℂ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) →
(normℎ‘𝑥) ≤ 1) |
| 5 | | 1re 11261 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
| 6 | | lemul2a 12122 |
. . . . . . . . . . 11
⊢
((((normℎ‘𝑥) ∈ ℝ ∧ 1 ∈ ℝ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧
(normℎ‘𝑥) ≤ 1) → (𝐴 ·
(normℎ‘𝑥)) ≤ (𝐴 · 1)) |
| 7 | 5, 6 | mp3anl2 1458 |
. . . . . . . . . 10
⊢
((((normℎ‘𝑥) ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) ∧
(normℎ‘𝑥) ≤ 1) → (𝐴 ·
(normℎ‘𝑥)) ≤ (𝐴 · 1)) |
| 8 | 2, 3, 4, 7 | syl21anc 838 |
. . . . . . . . 9
⊢ ((((𝑇: ℋ⟶ℂ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) → (𝐴 ·
(normℎ‘𝑥)) ≤ (𝐴 · 1)) |
| 9 | | ax-1rid 11225 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴) |
| 10 | 9 | ad2antrl 728 |
. . . . . . . . . 10
⊢ ((𝑇: ℋ⟶ℂ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) → (𝐴 · 1) = 𝐴) |
| 11 | 10 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝑇: ℋ⟶ℂ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) → (𝐴 · 1) = 𝐴) |
| 12 | 8, 11 | breqtrd 5169 |
. . . . . . . 8
⊢ ((((𝑇: ℋ⟶ℂ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) → (𝐴 ·
(normℎ‘𝑥)) ≤ 𝐴) |
| 13 | | ffvelcdm 7101 |
. . . . . . . . . . . 12
⊢ ((𝑇: ℋ⟶ℂ ∧
𝑥 ∈ ℋ) →
(𝑇‘𝑥) ∈ ℂ) |
| 14 | 13 | abscld 15475 |
. . . . . . . . . . 11
⊢ ((𝑇: ℋ⟶ℂ ∧
𝑥 ∈ ℋ) →
(abs‘(𝑇‘𝑥)) ∈
ℝ) |
| 15 | 14 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝑇: ℋ⟶ℂ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝑥 ∈ ℋ) →
(abs‘(𝑇‘𝑥)) ∈
ℝ) |
| 16 | | remulcl 11240 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧
(normℎ‘𝑥) ∈ ℝ) → (𝐴 ·
(normℎ‘𝑥)) ∈ ℝ) |
| 17 | 1, 16 | sylan2 593 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℋ) → (𝐴 ·
(normℎ‘𝑥)) ∈ ℝ) |
| 18 | 17 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℋ) → (𝐴 ·
(normℎ‘𝑥)) ∈ ℝ) |
| 19 | 18 | adantll 714 |
. . . . . . . . . 10
⊢ (((𝑇: ℋ⟶ℂ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝑥 ∈ ℋ) → (𝐴 ·
(normℎ‘𝑥)) ∈ ℝ) |
| 20 | | simplrl 777 |
. . . . . . . . . 10
⊢ (((𝑇: ℋ⟶ℂ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝑥 ∈ ℋ) → 𝐴 ∈
ℝ) |
| 21 | | letr 11355 |
. . . . . . . . . 10
⊢
(((abs‘(𝑇‘𝑥)) ∈ ℝ ∧ (𝐴 ·
(normℎ‘𝑥)) ∈ ℝ ∧ 𝐴 ∈ ℝ) → (((abs‘(𝑇‘𝑥)) ≤ (𝐴 ·
(normℎ‘𝑥)) ∧ (𝐴 ·
(normℎ‘𝑥)) ≤ 𝐴) → (abs‘(𝑇‘𝑥)) ≤ 𝐴)) |
| 22 | 15, 19, 20, 21 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝑇: ℋ⟶ℂ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝑥 ∈ ℋ) →
(((abs‘(𝑇‘𝑥)) ≤ (𝐴 ·
(normℎ‘𝑥)) ∧ (𝐴 ·
(normℎ‘𝑥)) ≤ 𝐴) → (abs‘(𝑇‘𝑥)) ≤ 𝐴)) |
| 23 | 22 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑇: ℋ⟶ℂ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) → (((abs‘(𝑇‘𝑥)) ≤ (𝐴 ·
(normℎ‘𝑥)) ∧ (𝐴 ·
(normℎ‘𝑥)) ≤ 𝐴) → (abs‘(𝑇‘𝑥)) ≤ 𝐴)) |
| 24 | 12, 23 | mpan2d 694 |
. . . . . . 7
⊢ ((((𝑇: ℋ⟶ℂ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) → ((abs‘(𝑇‘𝑥)) ≤ (𝐴 ·
(normℎ‘𝑥)) → (abs‘(𝑇‘𝑥)) ≤ 𝐴)) |
| 25 | 24 | ex 412 |
. . . . . 6
⊢ (((𝑇: ℋ⟶ℂ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝑥 ∈ ℋ) →
((normℎ‘𝑥) ≤ 1 → ((abs‘(𝑇‘𝑥)) ≤ (𝐴 ·
(normℎ‘𝑥)) → (abs‘(𝑇‘𝑥)) ≤ 𝐴))) |
| 26 | 25 | com23 86 |
. . . . 5
⊢ (((𝑇: ℋ⟶ℂ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝑥 ∈ ℋ) →
((abs‘(𝑇‘𝑥)) ≤ (𝐴 ·
(normℎ‘𝑥)) →
((normℎ‘𝑥) ≤ 1 → (abs‘(𝑇‘𝑥)) ≤ 𝐴))) |
| 27 | 26 | ralimdva 3167 |
. . . 4
⊢ ((𝑇: ℋ⟶ℂ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) →
(∀𝑥 ∈ ℋ
(abs‘(𝑇‘𝑥)) ≤ (𝐴 ·
(normℎ‘𝑥)) → ∀𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 → (abs‘(𝑇‘𝑥)) ≤ 𝐴))) |
| 28 | 27 | imp 406 |
. . 3
⊢ (((𝑇: ℋ⟶ℂ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧
∀𝑥 ∈ ℋ
(abs‘(𝑇‘𝑥)) ≤ (𝐴 ·
(normℎ‘𝑥))) → ∀𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 → (abs‘(𝑇‘𝑥)) ≤ 𝐴)) |
| 29 | | rexr 11307 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ*) |
| 30 | 29 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → 𝐴 ∈
ℝ*) |
| 31 | | nmfnleub 31944 |
. . . . 5
⊢ ((𝑇: ℋ⟶ℂ ∧
𝐴 ∈
ℝ*) → ((normfn‘𝑇) ≤ 𝐴 ↔ ∀𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 → (abs‘(𝑇‘𝑥)) ≤ 𝐴))) |
| 32 | 30, 31 | sylan2 593 |
. . . 4
⊢ ((𝑇: ℋ⟶ℂ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) →
((normfn‘𝑇) ≤ 𝐴 ↔ ∀𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 → (abs‘(𝑇‘𝑥)) ≤ 𝐴))) |
| 33 | 32 | biimpar 477 |
. . 3
⊢ (((𝑇: ℋ⟶ℂ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧
∀𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 → (abs‘(𝑇‘𝑥)) ≤ 𝐴)) → (normfn‘𝑇) ≤ 𝐴) |
| 34 | 28, 33 | syldan 591 |
. 2
⊢ (((𝑇: ℋ⟶ℂ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧
∀𝑥 ∈ ℋ
(abs‘(𝑇‘𝑥)) ≤ (𝐴 ·
(normℎ‘𝑥))) → (normfn‘𝑇) ≤ 𝐴) |
| 35 | 34 | 3impa 1110 |
1
⊢ ((𝑇: ℋ⟶ℂ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴) ∧ ∀𝑥 ∈ ℋ
(abs‘(𝑇‘𝑥)) ≤ (𝐴 ·
(normℎ‘𝑥))) → (normfn‘𝑇) ≤ 𝐴) |