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 ( ( 𝑇 : ℋ ⟶ ℂ ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ∀ 𝑥 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( normℎ ‘ 𝑥 ) ) ) → ( normfn ‘ 𝑇 ) ≤ 𝐴 )

Proof

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