This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nmbdoplb

Description: A lower bound for the norm of a bounded linear Hilbert space operator. (Contributed by NM, 18-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmbdoplb ( ( 𝑇 ∈ BndLinOp ∧ 𝐴 ∈ ℋ ) → ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 fveq1 ⊢ ( 𝑇 = if ( 𝑇 ∈ BndLinOp , 𝑇 , 0hop ) → ( 𝑇 ‘ 𝐴 ) = ( if ( 𝑇 ∈ BndLinOp , 𝑇 , 0hop ) ‘ 𝐴 ) )
2 1 fveq2d ⊢ ( 𝑇 = if ( 𝑇 ∈ BndLinOp , 𝑇 , 0hop ) → ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) = ( normℎ ‘ ( if ( 𝑇 ∈ BndLinOp , 𝑇 , 0hop ) ‘ 𝐴 ) ) )
3 fveq2 ⊢ ( 𝑇 = if ( 𝑇 ∈ BndLinOp , 𝑇 , 0hop ) → ( normop ‘ 𝑇 ) = ( normop ‘ if ( 𝑇 ∈ BndLinOp , 𝑇 , 0hop ) ) )
4 3 oveq1d ⊢ ( 𝑇 = if ( 𝑇 ∈ BndLinOp , 𝑇 , 0hop ) → ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) = ( ( normop ‘ if ( 𝑇 ∈ BndLinOp , 𝑇 , 0hop ) ) · ( normℎ ‘ 𝐴 ) ) )
5 2 4 breq12d ⊢ ( 𝑇 = if ( 𝑇 ∈ BndLinOp , 𝑇 , 0hop ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) ↔ ( normℎ ‘ ( if ( 𝑇 ∈ BndLinOp , 𝑇 , 0hop ) ‘ 𝐴 ) ) ≤ ( ( normop ‘ if ( 𝑇 ∈ BndLinOp , 𝑇 , 0hop ) ) · ( normℎ ‘ 𝐴 ) ) ) )
6 5 imbi2d ⊢ ( 𝑇 = if ( 𝑇 ∈ BndLinOp , 𝑇 , 0hop ) → ( ( 𝐴 ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) ) ↔ ( 𝐴 ∈ ℋ → ( normℎ ‘ ( if ( 𝑇 ∈ BndLinOp , 𝑇 , 0hop ) ‘ 𝐴 ) ) ≤ ( ( normop ‘ if ( 𝑇 ∈ BndLinOp , 𝑇 , 0hop ) ) · ( normℎ ‘ 𝐴 ) ) ) ) )
7 0bdop ⊢ 0hop ∈ BndLinOp
8 7 elimel ⊢ if ( 𝑇 ∈ BndLinOp , 𝑇 , 0hop ) ∈ BndLinOp
9 8 nmbdoplbi ⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ ( if ( 𝑇 ∈ BndLinOp , 𝑇 , 0hop ) ‘ 𝐴 ) ) ≤ ( ( normop ‘ if ( 𝑇 ∈ BndLinOp , 𝑇 , 0hop ) ) · ( normℎ ‘ 𝐴 ) ) )
10 6 9 dedth ⊢ ( 𝑇 ∈ BndLinOp → ( 𝐴 ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) ) )
11 10 imp ⊢ ( ( 𝑇 ∈ BndLinOp ∧ 𝐴 ∈ ℋ ) → ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )