# Metamath Proof Explorer

## 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 ℋ\wedge {y}\in ℋ\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 ℋ\wedge {y}\in ℋ\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 ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{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 ${⊢}ℋ=\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 ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{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 ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{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}$