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 ⊢ T ∈ BndLinOp ∧ A ∈ ℋ → norm ℎ ⁡ T ⁡ A ≤ norm op ⁡ T ⁢ norm ℎ ⁡ A

Proof

Step Hyp Ref Expression
1 fveq1 ⊢ T = if T ∈ BndLinOp T 0 hop → T ⁡ A = if T ∈ BndLinOp T 0 hop ⁡ A
2 1 fveq2d ⊢ T = if T ∈ BndLinOp T 0 hop → norm ℎ ⁡ T ⁡ A = norm ℎ ⁡ if T ∈ BndLinOp T 0 hop ⁡ A
3 fveq2 ⊢ T = if T ∈ BndLinOp T 0 hop → norm op ⁡ T = norm op ⁡ if T ∈ BndLinOp T 0 hop
4 3 oveq1d ⊢ T = if T ∈ BndLinOp T 0 hop → norm op ⁡ T ⁢ norm ℎ ⁡ A = norm op ⁡ if T ∈ BndLinOp T 0 hop ⁢ norm ℎ ⁡ A
5 2 4 breq12d ⊢ T = if T ∈ BndLinOp T 0 hop → norm ℎ ⁡ T ⁡ A ≤ norm op ⁡ T ⁢ norm ℎ ⁡ A ↔ norm ℎ ⁡ if T ∈ BndLinOp T 0 hop ⁡ A ≤ norm op ⁡ if T ∈ BndLinOp T 0 hop ⁢ norm ℎ ⁡ A
6 5 imbi2d ⊢ T = if T ∈ BndLinOp T 0 hop → A ∈ ℋ → norm ℎ ⁡ T ⁡ A ≤ norm op ⁡ T ⁢ norm ℎ ⁡ A ↔ A ∈ ℋ → norm ℎ ⁡ if T ∈ BndLinOp T 0 hop ⁡ A ≤ norm op ⁡ if T ∈ BndLinOp T 0 hop ⁢ norm ℎ ⁡ A
7 0bdop ⊢ 0 hop ∈ BndLinOp
8 7 elimel ⊢ if T ∈ BndLinOp T 0 hop ∈ BndLinOp
9 8 nmbdoplbi ⊢ A ∈ ℋ → norm ℎ ⁡ if T ∈ BndLinOp T 0 hop ⁡ A ≤ norm op ⁡ if T ∈ BndLinOp T 0 hop ⁢ norm ℎ ⁡ A
10 6 9 dedth ⊢ T ∈ BndLinOp → A ∈ ℋ → norm ℎ ⁡ T ⁡ A ≤ norm op ⁡ T ⁢ norm ℎ ⁡ A
11 10 imp ⊢ T ∈ BndLinOp ∧ A ∈ ℋ → norm ℎ ⁡ T ⁡ A ≤ norm op ⁡ T ⁢ norm ℎ ⁡ A