# Metamath Proof Explorer

## Theorem nmcoplb

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

Ref Expression
Assertion nmcoplb ${⊢}\left({T}\in \mathrm{LinOp}\wedge {T}\in \mathrm{ContOp}\wedge {A}\in ℋ\right)\to {norm}_{ℎ}\left({T}\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)$

### Proof

Step Hyp Ref Expression
1 elin ${⊢}{T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)↔\left({T}\in \mathrm{LinOp}\wedge {T}\in \mathrm{ContOp}\right)$
2 fveq1 ${⊢}{T}=if\left({T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to {T}\left({A}\right)=if\left({T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({A}\right)$
3 2 fveq2d ${⊢}{T}=if\left({T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to {norm}_{ℎ}\left({T}\left({A}\right)\right)={norm}_{ℎ}\left(if\left({T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({A}\right)\right)$
4 fveq2 ${⊢}{T}=if\left({T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to {norm}_{\mathrm{op}}\left({T}\right)={norm}_{\mathrm{op}}\left(if\left({T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),{T},{\mathrm{I}↾}_{ℋ}\right)\right)$
5 4 oveq1d ${⊢}{T}=if\left({T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)={norm}_{\mathrm{op}}\left(if\left({T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),{T},{\mathrm{I}↾}_{ℋ}\right)\right){norm}_{ℎ}\left({A}\right)$
6 3 5 breq12d ${⊢}{T}=if\left({T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to \left({norm}_{ℎ}\left({T}\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)↔{norm}_{ℎ}\left(if\left({T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left(if\left({T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),{T},{\mathrm{I}↾}_{ℋ}\right)\right){norm}_{ℎ}\left({A}\right)\right)$
7 6 imbi2d ${⊢}{T}=if\left({T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to \left(\left({A}\in ℋ\to {norm}_{ℎ}\left({T}\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)\right)↔\left({A}\in ℋ\to {norm}_{ℎ}\left(if\left({T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left(if\left({T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),{T},{\mathrm{I}↾}_{ℋ}\right)\right){norm}_{ℎ}\left({A}\right)\right)\right)$
8 idlnop ${⊢}{\mathrm{I}↾}_{ℋ}\in \mathrm{LinOp}$
9 idcnop ${⊢}{\mathrm{I}↾}_{ℋ}\in \mathrm{ContOp}$
10 elin ${⊢}{\mathrm{I}↾}_{ℋ}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)↔\left({\mathrm{I}↾}_{ℋ}\in \mathrm{LinOp}\wedge {\mathrm{I}↾}_{ℋ}\in \mathrm{ContOp}\right)$
11 8 9 10 mpbir2an ${⊢}{\mathrm{I}↾}_{ℋ}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)$
12 11 elimel ${⊢}if\left({T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),{T},{\mathrm{I}↾}_{ℋ}\right)\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)$
13 elin ${⊢}if\left({T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),{T},{\mathrm{I}↾}_{ℋ}\right)\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)↔\left(if\left({T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),{T},{\mathrm{I}↾}_{ℋ}\right)\in \mathrm{LinOp}\wedge if\left({T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),{T},{\mathrm{I}↾}_{ℋ}\right)\in \mathrm{ContOp}\right)$
14 12 13 mpbi ${⊢}\left(if\left({T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),{T},{\mathrm{I}↾}_{ℋ}\right)\in \mathrm{LinOp}\wedge if\left({T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),{T},{\mathrm{I}↾}_{ℋ}\right)\in \mathrm{ContOp}\right)$
15 14 simpli ${⊢}if\left({T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),{T},{\mathrm{I}↾}_{ℋ}\right)\in \mathrm{LinOp}$
16 14 simpri ${⊢}if\left({T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),{T},{\mathrm{I}↾}_{ℋ}\right)\in \mathrm{ContOp}$
17 15 16 nmcoplbi ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left(if\left({T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left(if\left({T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),{T},{\mathrm{I}↾}_{ℋ}\right)\right){norm}_{ℎ}\left({A}\right)$
18 7 17 dedth ${⊢}{T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\to \left({A}\in ℋ\to {norm}_{ℎ}\left({T}\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)\right)$
19 18 imp ${⊢}\left({T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\wedge {A}\in ℋ\right)\to {norm}_{ℎ}\left({T}\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)$
20 1 19 sylanbr ${⊢}\left(\left({T}\in \mathrm{LinOp}\wedge {T}\in \mathrm{ContOp}\right)\wedge {A}\in ℋ\right)\to {norm}_{ℎ}\left({T}\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)$
21 20 3impa ${⊢}\left({T}\in \mathrm{LinOp}\wedge {T}\in \mathrm{ContOp}\wedge {A}\in ℋ\right)\to {norm}_{ℎ}\left({T}\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)$