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ℎ ‘ 𝐴 ) ) )