Metamath Proof Explorer

Theorem nmcfnlb

Description: A lower bound of the norm of a continuous linear Hilbert space functional. Theorem 3.5(ii) of Beran p. 99. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 elin ⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) ↔ ( 𝑇 ∈ LinFn ∧ 𝑇 ∈ ContFn ) )
2 fveq1 ⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) → ( 𝑇 ‘ 𝐴 ) = ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝐴 ) )
3 2 fveq2d ⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) → ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) = ( abs ‘ ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝐴 ) ) )
4 fveq2 ⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) → ( normfn ‘ 𝑇 ) = ( normfn ‘ if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ) )
5 4 oveq1d ⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) → ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) = ( ( normfn ‘ if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ) · ( normℎ ‘ 𝐴 ) ) )
6 3 5 breq12d ⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) → ( ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) ↔ ( abs ‘ ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝐴 ) ) ≤ ( ( normfn ‘ if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ) · ( normℎ ‘ 𝐴 ) ) ) )
7 6 imbi2d ⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) → ( ( 𝐴 ∈ ℋ → ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) ) ↔ ( 𝐴 ∈ ℋ → ( abs ‘ ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝐴 ) ) ≤ ( ( normfn ‘ if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ) · ( normℎ ‘ 𝐴 ) ) ) ) )
8 0lnfn ⊢ ( ℋ × { 0 } ) ∈ LinFn
9 0cnfn ⊢ ( ℋ × { 0 } ) ∈ ContFn
10 elin ⊢ ( ( ℋ × { 0 } ) ∈ ( LinFn ∩ ContFn ) ↔ ( ( ℋ × { 0 } ) ∈ LinFn ∧ ( ℋ × { 0 } ) ∈ ContFn ) )
11 8 9 10 mpbir2an ⊢ ( ℋ × { 0 } ) ∈ ( LinFn ∩ ContFn )
12 11 elimel ⊢ if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ ( LinFn ∩ ContFn )
13 elin ⊢ ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ ( LinFn ∩ ContFn ) ↔ ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ LinFn ∧ if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ ContFn ) )
14 12 13 mpbi ⊢ ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ LinFn ∧ if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ ContFn )
15 14 simpli ⊢ if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ LinFn
16 14 simpri ⊢ if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ∈ ContFn
17 15 16 nmcfnlbi ⊢ ( 𝐴 ∈ ℋ → ( abs ‘ ( if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝐴 ) ) ≤ ( ( normfn ‘ if ( 𝑇 ∈ ( LinFn ∩ ContFn ) , 𝑇 , ( ℋ × { 0 } ) ) ) · ( normℎ ‘ 𝐴 ) ) )
18 7 17 dedth ⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ( 𝐴 ∈ ℋ → ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) ) )
19 18 imp ⊢ ( ( 𝑇 ∈ ( LinFn ∩ ContFn ) ∧ 𝐴 ∈ ℋ ) → ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )
20 1 19 sylanbr ⊢ ( ( ( 𝑇 ∈ LinFn ∧ 𝑇 ∈ ContFn ) ∧ 𝐴 ∈ ℋ ) → ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )
21 20 3impa ⊢ ( ( 𝑇 ∈ LinFn ∧ 𝑇 ∈ ContFn ∧ 𝐴 ∈ ℋ ) → ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )