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 \mathscr{H}\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)\leftrightarrow \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}\upharpoonright }_{\mathscr{H}}\right)\to T\left(A\right)=if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,{\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\left(A\right)$$
3	2	fveq2d	$$⊢T=if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,{\mathrm{I}\upharpoonright }_{\mathscr{H}}\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}\upharpoonright }_{\mathscr{H}}\right)\left(A\right)\right)$$
4		fveq2	$$⊢T=if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,{\mathrm{I}\upharpoonright }_{\mathscr{H}}\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}\upharpoonright }_{\mathscr{H}}\right)\right)$$
5	4	oveq1d	$$⊢T=if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,{\mathrm{I}\upharpoonright }_{\mathscr{H}}\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}\upharpoonright }_{\mathscr{H}}\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}\upharpoonright }_{\mathscr{H}}\right)\to \left({norm}_{ℎ}\left(T\left(A\right)\right)\le {norm}_{\mathrm{op}}\left(T\right){norm}_{ℎ}\left(A\right)\leftrightarrow {norm}_{ℎ}\left(if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,{\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\left(A\right)\right)\le {norm}_{\mathrm{op}}\left(if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,{\mathrm{I}\upharpoonright }_{\mathscr{H}}\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}\upharpoonright }_{\mathscr{H}}\right)\to \left(\left(A\in \mathscr{H}\to {norm}_{ℎ}\left(T\left(A\right)\right)\le {norm}_{\mathrm{op}}\left(T\right){norm}_{ℎ}\left(A\right)\right)\leftrightarrow \left(A\in \mathscr{H}\to {norm}_{ℎ}\left(if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,{\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\left(A\right)\right)\le {norm}_{\mathrm{op}}\left(if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,{\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\right){norm}_{ℎ}\left(A\right)\right)\right)$$
8		idlnop	$$⊢{\mathrm{I}\upharpoonright }_{\mathscr{H}}\in \mathrm{LinOp}$$
9		idcnop	$$⊢{\mathrm{I}\upharpoonright }_{\mathscr{H}}\in \mathrm{ContOp}$$
10		elin	$$⊢{\mathrm{I}\upharpoonright }_{\mathscr{H}}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\leftrightarrow \left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\in \mathrm{LinOp}\wedge {\mathrm{I}\upharpoonright }_{\mathscr{H}}\in \mathrm{ContOp}\right)$$
11	8 9 10	mpbir2an	$$⊢{\mathrm{I}\upharpoonright }_{\mathscr{H}}\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}\upharpoonright }_{\mathscr{H}}\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}\upharpoonright }_{\mathscr{H}}\right)\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\leftrightarrow \left(if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,{\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\in \mathrm{LinOp}\wedge if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,{\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\in \mathrm{ContOp}\right)$$
14	12 13	mpbi	$$⊢\left(if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,{\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\in \mathrm{LinOp}\wedge if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,{\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\in \mathrm{ContOp}\right)$$
15	14	simpli	$$⊢if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,{\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\in \mathrm{LinOp}$$
16	14	simpri	$$⊢if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,{\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\in \mathrm{ContOp}$$
17	15 16	nmcoplbi	$$⊢A\in \mathscr{H}\to {norm}_{ℎ}\left(if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,{\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\left(A\right)\right)\le {norm}_{\mathrm{op}}\left(if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,{\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\right){norm}_{ℎ}\left(A\right)$$
18	7 17	dedth	$$⊢T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\to \left(A\in \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\right)\to {norm}_{ℎ}\left(T\left(A\right)\right)\le {norm}_{\mathrm{op}}\left(T\right){norm}_{ℎ}\left(A\right)$$