This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. HrmOp -> T e. BndLinOp )

Proof

Step Hyp Ref Expression
1 hmoplin 
 |-  ( T e. HrmOp -> T e. LinOp )
2 hmop 
 |-  ( ( T e. HrmOp /\ x e. ~H /\ y e. ~H ) -> ( x .ih ( T ` y ) ) = ( ( T ` x ) .ih y ) )
3 2 3expib 
 |-  ( T e. HrmOp -> ( ( x e. ~H /\ y e. ~H ) -> ( x .ih ( T ` y ) ) = ( ( T ` x ) .ih y ) ) )
4 3 ralrimivv 
 |-  ( T e. HrmOp -> A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( T ` x ) .ih y ) )
5 hilhl 
 |-  <. <. +h , .h >. , normh >. e. CHilOLD
6 df-hba 
 |-  ~H = ( BaseSet ` <. <. +h , .h >. , normh >. )
7 eqid 
 |-  <. <. +h , .h >. , normh >. = <. <. +h , .h >. , normh >.
8 7 hhip 
 |-  .ih = ( .iOLD ` <. <. +h , .h >. , normh >. )
9 eqid 
 |-  ( <. <. +h , .h >. , normh >. LnOp <. <. +h , .h >. , normh >. ) = ( <. <. +h , .h >. , normh >. LnOp <. <. +h , .h >. , normh >. )
10 7 9 hhlnoi 
 |-  LinOp = ( <. <. +h , .h >. , normh >. LnOp <. <. +h , .h >. , normh >. )
11 eqid 
 |-  ( <. <. +h , .h >. , normh >. BLnOp <. <. +h , .h >. , normh >. ) = ( <. <. +h , .h >. , normh >. BLnOp <. <. +h , .h >. , normh >. )
12 7 11 hhbloi 
 |-  BndLinOp = ( <. <. +h , .h >. , normh >. BLnOp <. <. +h , .h >. , normh >. )
13 6 8 10 12 htth 
 |-  ( ( <. <. +h , .h >. , normh >. e. CHilOLD /\ T e. LinOp /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( T ` x ) .ih y ) ) -> T e. BndLinOp )
14 5 13 mp3an1 
 |-  ( ( T e. LinOp /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( T ` x ) .ih y ) ) -> T e. BndLinOp )
15 1 4 14 syl2anc 
 |-  ( T e. HrmOp -> T e. BndLinOp )