Metamath Proof Explorer

Theorem nmbdfnlb

Description: A lower bound for the norm of a bounded linear functional. (Contributed by NM, 25-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion nmbdfnlb ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ∧ 𝐴 ∈ ℋ ) → ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 fveq1 ⊢ ( 𝑇 = if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) → ( 𝑇 ‘ 𝐴 ) = ( if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝐴 ) )
2 1 fveq2d ⊢ ( 𝑇 = if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) → ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) = ( abs ‘ ( if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝐴 ) ) )
3 fveq2 ⊢ ( 𝑇 = if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) → ( normfn ‘ 𝑇 ) = ( normfn ‘ if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) ) )
4 3 oveq1d ⊢ ( 𝑇 = if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) → ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) = ( ( normfn ‘ if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) ) · ( normℎ ‘ 𝐴 ) ) )
5 2 4 breq12d ⊢ ( 𝑇 = if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) → ( ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) ↔ ( abs ‘ ( if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝐴 ) ) ≤ ( ( normfn ‘ if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) ) · ( normℎ ‘ 𝐴 ) ) ) )
6 5 imbi2d ⊢ ( 𝑇 = if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) → ( ( 𝐴 ∈ ℋ → ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) ) ↔ ( 𝐴 ∈ ℋ → ( abs ‘ ( if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝐴 ) ) ≤ ( ( normfn ‘ if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) ) · ( normℎ ‘ 𝐴 ) ) ) ) )
7 eleq1 ⊢ ( 𝑇 = if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) → ( 𝑇 ∈ LinFn ↔ if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ LinFn ) )
8 3 eleq1d ⊢ ( 𝑇 = if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) → ( ( normfn ‘ 𝑇 ) ∈ ℝ ↔ ( normfn ‘ if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) ) ∈ ℝ ) )
9 7 8 anbi12d ⊢ ( 𝑇 = if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) → ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) ↔ ( if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ LinFn ∧ ( normfn ‘ if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) ) ∈ ℝ ) ) )
10 eleq1 ⊢ ( ( ℋ × { 0 } ) = if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) → ( ( ℋ × { 0 } ) ∈ LinFn ↔ if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ LinFn ) )
11 fveq2 ⊢ ( ( ℋ × { 0 } ) = if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) → ( normfn ‘ ( ℋ × { 0 } ) ) = ( normfn ‘ if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) ) )
12 11 eleq1d ⊢ ( ( ℋ × { 0 } ) = if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) → ( ( normfn ‘ ( ℋ × { 0 } ) ) ∈ ℝ ↔ ( normfn ‘ if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) ) ∈ ℝ ) )
13 10 12 anbi12d ⊢ ( ( ℋ × { 0 } ) = if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) → ( ( ( ℋ × { 0 } ) ∈ LinFn ∧ ( normfn ‘ ( ℋ × { 0 } ) ) ∈ ℝ ) ↔ ( if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ LinFn ∧ ( normfn ‘ if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) ) ∈ ℝ ) ) )
14 0lnfn ⊢ ( ℋ × { 0 } ) ∈ LinFn
15 nmfn0 ⊢ ( normfn ‘ ( ℋ × { 0 } ) ) = 0
16 0re ⊢ 0 ∈ ℝ
17 15 16 eqeltri ⊢ ( normfn ‘ ( ℋ × { 0 } ) ) ∈ ℝ
18 14 17 pm3.2i ⊢ ( ( ℋ × { 0 } ) ∈ LinFn ∧ ( normfn ‘ ( ℋ × { 0 } ) ) ∈ ℝ )
19 9 13 18 elimhyp ⊢ ( if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ LinFn ∧ ( normfn ‘ if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) ) ∈ ℝ )
20 19 nmbdfnlbi ⊢ ( 𝐴 ∈ ℋ → ( abs ‘ ( if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝐴 ) ) ≤ ( ( normfn ‘ if ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) , 𝑇 , ( ℋ × { 0 } ) ) ) · ( normℎ ‘ 𝐴 ) ) )
21 6 20 dedth ⊢ ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) → ( 𝐴 ∈ ℋ → ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) ) )
22 21 3impia ⊢ ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ∧ 𝐴 ∈ ℋ ) → ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )