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 )