Metamath Proof Explorer

Theorem nmfnleub2

Description: An upper bound for the norm of a functional. (Contributed by NM, 24-May-2006) (New usage is discouraged.)

Ref Expression
Assertion nmfnleub2 ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ ∀ x ∈ ℋ T ⁡ x ≤ A ⁢ norm ℎ ⁡ x → norm fn ⁡ T ≤ A

Proof

Step Hyp Ref Expression
1 normcl ⊢ x ∈ ℋ → norm ℎ ⁡ x ∈ ℝ
2 1 ad2antlr ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ x ∈ ℝ
3 simpllr ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → A ∈ ℝ ∧ 0 ≤ A
4 simpr ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → norm ℎ ⁡ x ≤ 1
5 1re ⊢ 1 ∈ ℝ
6 lemul2a ⊢ norm ℎ ⁡ x ∈ ℝ ∧ 1 ∈ ℝ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ norm ℎ ⁡ x ≤ 1 → A ⁢ norm ℎ ⁡ x ≤ A ⋅ 1
7 5 6 mp3anl2 ⊢ norm ℎ ⁡ x ∈ ℝ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ norm ℎ ⁡ x ≤ 1 → A ⁢ norm ℎ ⁡ x ≤ A ⋅ 1
8 2 3 4 7 syl21anc ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → A ⁢ norm ℎ ⁡ x ≤ A ⋅ 1
9 ax-1rid ⊢ A ∈ ℝ → A ⋅ 1 = A
10 9 ad2antrl ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℝ ∧ 0 ≤ A → A ⋅ 1 = A
11 10 ad2antrr ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → A ⋅ 1 = A
12 8 11 breqtrd ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → A ⁢ norm ℎ ⁡ x ≤ A
13 ffvelrn ⊢ T : ℋ ⟶ ℂ ∧ x ∈ ℋ → T ⁡ x ∈ ℂ
14 13 abscld ⊢ T : ℋ ⟶ ℂ ∧ x ∈ ℋ → T ⁡ x ∈ ℝ
15 14 adantlr ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ → T ⁡ x ∈ ℝ
16 remulcl ⊢ A ∈ ℝ ∧ norm ℎ ⁡ x ∈ ℝ → A ⁢ norm ℎ ⁡ x ∈ ℝ
17 1 16 sylan2 ⊢ A ∈ ℝ ∧ x ∈ ℋ → A ⁢ norm ℎ ⁡ x ∈ ℝ
18 17 adantlr ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ → A ⁢ norm ℎ ⁡ x ∈ ℝ
19 18 adantll ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ → A ⁢ norm ℎ ⁡ x ∈ ℝ
20 simplrl ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ → A ∈ ℝ
21 letr ⊢ T ⁡ x ∈ ℝ ∧ A ⁢ norm ℎ ⁡ x ∈ ℝ ∧ A ∈ ℝ → T ⁡ x ≤ A ⁢ norm ℎ ⁡ x ∧ A ⁢ norm ℎ ⁡ x ≤ A → T ⁡ x ≤ A
22 15 19 20 21 syl3anc ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ → T ⁡ x ≤ A ⁢ norm ℎ ⁡ x ∧ A ⁢ norm ℎ ⁡ x ≤ A → T ⁡ x ≤ A
23 22 adantr ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → T ⁡ x ≤ A ⁢ norm ℎ ⁡ x ∧ A ⁢ norm ℎ ⁡ x ≤ A → T ⁡ x ≤ A
24 12 23 mpan2d ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ ∧ norm ℎ ⁡ x ≤ 1 → T ⁡ x ≤ A ⁢ norm ℎ ⁡ x → T ⁡ x ≤ A
25 24 ex ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ → norm ℎ ⁡ x ≤ 1 → T ⁡ x ≤ A ⁢ norm ℎ ⁡ x → T ⁡ x ≤ A
26 25 com23 ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ x ∈ ℋ → T ⁡ x ≤ A ⁢ norm ℎ ⁡ x → norm ℎ ⁡ x ≤ 1 → T ⁡ x ≤ A
27 26 ralimdva ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℝ ∧ 0 ≤ A → ∀ x ∈ ℋ T ⁡ x ≤ A ⁢ norm ℎ ⁡ x → ∀ x ∈ ℋ norm ℎ ⁡ x ≤ 1 → T ⁡ x ≤ A
28 27 imp ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ ∀ x ∈ ℋ T ⁡ x ≤ A ⁢ norm ℎ ⁡ x → ∀ x ∈ ℋ norm ℎ ⁡ x ≤ 1 → T ⁡ x ≤ A
29 rexr ⊢ A ∈ ℝ → A ∈ ℝ *
30 29 adantr ⊢ A ∈ ℝ ∧ 0 ≤ A → A ∈ ℝ *
31 nmfnleub ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℝ * → norm fn ⁡ T ≤ A ↔ ∀ x ∈ ℋ norm ℎ ⁡ x ≤ 1 → T ⁡ x ≤ A
32 30 31 sylan2 ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℝ ∧ 0 ≤ A → norm fn ⁡ T ≤ A ↔ ∀ x ∈ ℋ norm ℎ ⁡ x ≤ 1 → T ⁡ x ≤ A
33 32 biimpar ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ ∀ x ∈ ℋ norm ℎ ⁡ x ≤ 1 → T ⁡ x ≤ A → norm fn ⁡ T ≤ A
34 28 33 syldan ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ ∀ x ∈ ℋ T ⁡ x ≤ A ⁢ norm ℎ ⁡ x → norm fn ⁡ T ≤ A
35 34 3impa ⊢ T : ℋ ⟶ ℂ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ ∀ x ∈ ℋ T ⁡ x ≤ A ⁢ norm ℎ ⁡ x → norm fn ⁡ T ≤ A