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→normfn⁡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 ffvelcdm ⊢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∈ℝ*→normfn⁡T≤A↔∀x∈ℋnormℎ⁡x≤1→T⁡x≤A
32 30 31 sylan2 ⊢T:ℋ⟶ℂ∧A∈ℝ∧0≤A→normfn⁡T≤A↔∀x∈ℋnormℎ⁡x≤1→T⁡x≤A
33 32 biimpar ⊢T:ℋ⟶ℂ∧A∈ℝ∧0≤A∧∀x∈ℋnormℎ⁡x≤1→T⁡x≤A→normfn⁡T≤A
34 28 33 syldan ⊢T:ℋ⟶ℂ∧A∈ℝ∧0≤A∧∀x∈ℋT⁡x≤A⁢normℎ⁡x→normfn⁡T≤A
35 34 3impa ⊢T:ℋ⟶ℂ∧A∈ℝ∧0≤A∧∀x∈ℋT⁡x≤A⁢normℎ⁡x→normfn⁡T≤A