Theorem hmopbdoptHIL

Description: A Hermitian operator is a bounded linear operator (Hellinger-Toeplitz Theorem). (Contributed by NM, 18-Jan-2008) (New usage is discouraged.)

	Ref	Expression
Assertion	hmopbdoptHIL	$$⊢T\in \mathrm{HrmOp}\to T\in \mathrm{BndLinOp}$$

Proof

Step	Hyp	Ref	Expression
1		hmoplin	$$⊢T\in \mathrm{HrmOp}\to T\in \mathrm{LinOp}$$
2		hmop	$$⊢\left(T\in \mathrm{HrmOp}\wedge x\in \mathscr{H}\wedge y\in \mathscr{H}\right)\to x{\cdot }_{\mathrm{ih}}T\left(y\right)=T\left(x\right){\cdot }_{\mathrm{ih}}y$$
3	2	3expib	$$⊢T\in \mathrm{HrmOp}\to \left(\left(x\in \mathscr{H}\wedge y\in \mathscr{H}\right)\to x{\cdot }_{\mathrm{ih}}T\left(y\right)=T\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$
4	3	ralrimivv	$$⊢T\in \mathrm{HrmOp}\to \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=T\left(x\right){\cdot }_{\mathrm{ih}}y$$
5		hilhl	$$⊢⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\in {CHil}_{\mathrm{OLD}}$$
6		df-hba	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
7		eqid	$$⊢⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
8	7	hhip	$$⊢{\cdot }_{\mathrm{ih}}={\cdot }_{\mathrm{𝑖OLD}}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
9		eqid	$$⊢⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\mathrm{LnOp}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\mathrm{LnOp}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
10	7 9	hhlnoi	$$⊢\mathrm{LinOp}=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\mathrm{LnOp}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
11		eqid	$$⊢⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\mathrm{BLnOp}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\mathrm{BLnOp}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
12	7 11	hhbloi	$$⊢\mathrm{BndLinOp}=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\mathrm{BLnOp}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
13	6 8 10 12	htth	$$⊢\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\in {CHil}_{\mathrm{OLD}}\wedge T\in \mathrm{LinOp}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=T\left(x\right){\cdot }_{\mathrm{ih}}y\right)\to T\in \mathrm{BndLinOp}$$
14	5 13	mp3an1	$$⊢\left(T\in \mathrm{LinOp}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=T\left(x\right){\cdot }_{\mathrm{ih}}y\right)\to T\in \mathrm{BndLinOp}$$
15	1 4 14	syl2anc	$$⊢T\in \mathrm{HrmOp}\to T\in \mathrm{BndLinOp}$$