P. 288 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28701-28800   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-bdop 28701	Define the set of bounded linear Hilbert space operators. (See df-hosum 28589 for definition of operator.) (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
|- BndLinOp = { t e. LinOp | ( normop ` t ) < +oo }
Definition	df-unop 28702*	Define the set of unitary operators on Hilbert space. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
|- UniOp = { t | ( t : ~H -onto-> ~H /\ A. x e. ~H A. y e. ~H ( ( t ` x ) .ih ( t ` y ) ) = ( x .ih y ) ) }
Definition	df-hmop 28703*	Define the set of Hermitian operators on Hilbert space. Some books call these "symmetric operators" and others call them "self-adjoint operators," sometimes with slightly different technical meanings. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
|- HrmOp = { t e. ( ~H ^m ~H ) | A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( t ` x ) .ih y ) }
19.6.5  Linear and continuous functionals and norms
Definition	df-nmfn 28704*	Define the norm of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
|- normfn = ( t e. ( CC ^m ~H ) |-> sup ( { x | E. z e. ~H ( ( normh ` z ) <_ 1 /\ x = ( abs ` ( t ` z ) ) ) } , RR* , < ) )
Definition	df-nlfn 28705	Define the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
|- null = ( t e. ( CC ^m ~H ) |-> ( `' t " { 0 } ) )
Definition	df-cnfn 28706*	Define the set of continuous functionals on Hilbert space. For every "epsilon" ( y) there is a "delta" ( z) such that... (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
|- ContFn = { t e. ( CC ^m ~H ) | A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y ) }
Definition	df-lnfn 28707*	Define the set of linear functionals on Hilbert space. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
|- LinFn = { t e. ( CC ^m ~H ) | A. x e. CC A. y e. ~H A. z e. ~H ( t ` ( ( x .h y ) +h z ) ) = ( ( x x. ( t ` y ) ) + ( t ` z ) ) }
19.6.6  Adjoint
Definition	df-adjh 28708*	Define the adjoint of a Hilbert space operator (if it exists). The domain of adjh is the set of all adjoint operators. Definition of adjoint in [Kalmbach2] p. 8. Unlike Kalmbach (and most authors), we do not demand that the operator be linear, but instead show (in adjbdln 28942) that the adjoint exists for a bounded linear operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.)
|- adjh = { <. t , u >. | ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( t ` x ) .ih y ) = ( x .ih ( u ` y ) ) ) }
19.6.7  Dirac bra-ket notation
Definition	df-bra 28709*	Define the bra of a vector used by Dirac notation. Based on definition of bra in [Prugovecki] p. 186 (p. 180 in 1971 edition). In Dirac bra-ket notation, <. A | B >. is a complex number equal to the inner product ( B .ih A ). But physicists like to talk about the individual components <. A | and | B >., called bra and ket respectively. In order for their properties to make sense formally, we define the ket | B >. as the vector B itself, and the bra <. A | as a functional from ~H to CC. We represent the Dirac notation <. A | B >. by ( ( bra ` A ) ` B ); see braval 28803. The reversal of the inner product arguments not only makes the bra-ket behavior consistent with physics literature (see comments under ax-his3 27941) but is also required in order for the associative law kbass2 28976 to work. Our definition of bra and the associated outer product df-kb 28710 differs from, but is equivalent to, a common approach in the literature that makes use of mappings to a dual space. Our approach eliminates the need to have a parallel development of this dual space and instead keeps everything in Hilbert space. For an extensive discussion about how our notation maps to the bra-ket notation in physics textbooks, see mmnotes.txt, under the 17-May-2006 entry. (Contributed by NM, 15-May-2006.) (New usage is discouraged.)
|- bra = ( x e. ~H |-> ( y e. ~H |-> ( y .ih x ) ) )
Definition	df-kb 28710*	Define a commuted bra and ket juxtaposition used by Dirac notation. In Dirac notation, | A >. <. B | is an operator known as the outer product of A and B, which we represent by ( A ketbra B ). Based on Equation 8.1 of [Prugovecki] p. 376. This definition, combined with definition df-bra 28709, allows any legal juxtaposition of bras and kets to make sense formally and also to obey the associative law when mapped back to Dirac notation. (Contributed by NM, 15-May-2006.) (New usage is discouraged.)
|- ketbra = ( x e. ~H , y e. ~H |-> ( z e. ~H |-> ( ( z .ih y ) .h x ) ) )
19.6.8  Positive operators
Definition	df-leop 28711*	Define positive operator ordering. Definition VI.1 of [Retherford] p. 49. Note that ( ~H X. 0H ) <_op T means that T is a positive operator. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
|- <_op = { <. t , u >. | ( ( u -op t ) e. HrmOp /\ A. x e. ~H 0 <_ ( ( ( u -op t ) ` x ) .ih x ) ) }
19.6.9  Eigenvectors, eigenvalues, spectrum
Definition	df-eigvec 28712*	Define the eigenvector function. Theorem eleigveccl 28818 shows that eigvec ` T, the set of eigenvectors of Hilbert space operator T, are Hilbert space vectors. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
|- eigvec = ( t e. ( ~H ^m ~H ) |-> { x e. ( ~H \ 0H ) | E. z e. CC ( t ` x ) = ( z .h x ) } )
Definition	df-eigval 28713*	Define the eigenvalue function. The range of eigval ` T is the set of eigenvalues of Hilbert space operator T. Theorem eigvalcl 28820 shows that ( eigval ` T ) ` A, the eigenvalue associated with eigenvector A, is a complex number. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
|- eigval = ( t e. ( ~H ^m ~H ) |-> ( x e. ( eigvec ` t ) |-> ( ( ( t ` x ) .ih x ) / ( ( normh ` x ) ^ 2 ) ) ) )
Definition	df-spec 28714*	Define the spectrum of an operator. Definition of spectrum in [Halmos] p. 50. (Contributed by NM, 11-Apr-2006.) (New usage is discouraged.)
|- Lambda = ( t e. ( ~H ^m ~H ) |-> { x e. CC | -. ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H } )
19.6.10  Theorems about operators and functionals
Theorem	nmopval 28715*	Value of the norm of a Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- ( T : ~H --> ~H -> ( normop ` T ) = sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } , RR* , < ) )
Theorem	elcnop 28716*	Property defining a continuous Hilbert space operator. (Contributed by NM, 28-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- ( T e. ContOp <-> ( T : ~H --> ~H /\ A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( normh ` ( ( T ` w ) -h ( T ` x ) ) ) < y ) ) )
Theorem	ellnop 28717*	Property defining a linear Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- ( T e. LinOp <-> ( T : ~H --> ~H /\ A. x e. CC A. y e. ~H A. z e. ~H ( T ` ( ( x .h y ) +h z ) ) = ( ( x .h ( T ` y ) ) +h ( T ` z ) ) ) )
Theorem	lnopf 28718	A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
|- ( T e. LinOp -> T : ~H --> ~H )
Theorem	elbdop 28719	Property defining a bounded linear Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- ( T e. BndLinOp <-> ( T e. LinOp /\ ( normop ` T ) < +oo ) )
Theorem	bdopln 28720	A bounded linear Hilbert space operator is a linear operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
|- ( T e. BndLinOp -> T e. LinOp )
Theorem	bdopf 28721	A bounded linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.)
|- ( T e. BndLinOp -> T : ~H --> ~H )
Theorem	nmopsetretALT 28722*	The set in the supremum of the operator norm definition df-nmop 28698 is a set of reals. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( T : ~H --> ~H -> { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } C_ RR )
Theorem	nmopsetretHIL 28723*	The set in the supremum of the operator norm definition df-nmop 28698 is a set of reals. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.)
|- ( T : ~H --> ~H -> { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } C_ RR )
Theorem	nmopsetn0 28724*	The set in the supremum of the operator norm definition df-nmop 28698 is nonempty. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.)
|- ( normh ` ( T ` 0h ) ) e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) }
Theorem	nmopxr 28725	The norm of a Hilbert space operator is an extended real. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.)
|- ( T : ~H --> ~H -> ( normop ` T ) e. RR* )
Theorem	nmoprepnf 28726	The norm of a Hilbert space operator is either real or plus infinity. (Contributed by NM, 5-Feb-2006.) (New usage is discouraged.)
|- ( T : ~H --> ~H -> ( ( normop ` T ) e. RR <-> ( normop ` T ) =/= +oo ) )
Theorem	nmopgtmnf 28727	The norm of a Hilbert space operator is not minus infinity. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.)
|- ( T : ~H --> ~H -> -oo < ( normop ` T ) )
Theorem	nmopreltpnf 28728	The norm of a Hilbert space operator is real iff it is less than infinity. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
|- ( T : ~H --> ~H -> ( ( normop ` T ) e. RR <-> ( normop ` T ) < +oo ) )
Theorem	nmopre 28729	The norm of a bounded operator is a real number. (Contributed by NM, 29-Jan-2006.) (New usage is discouraged.)
|- ( T e. BndLinOp -> ( normop ` T ) e. RR )
Theorem	elbdop2 28730	Property defining a bounded linear Hilbert space operator. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
|- ( T e. BndLinOp <-> ( T e. LinOp /\ ( normop ` T ) e. RR ) )
Theorem	elunop 28731*	Property defining a unitary Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
|- ( T e. UniOp <-> ( T : ~H -onto-> ~H /\ A. x e. ~H A. y e. ~H ( ( T ` x ) .ih ( T ` y ) ) = ( x .ih y ) ) )
Theorem	elhmop 28732*	Property defining a Hermitian Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- ( T e. HrmOp <-> ( T : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( T ` x ) .ih y ) ) )
Theorem	hmopf 28733	A Hermitian operator is a Hilbert space operator (mapping). (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.)
|- ( T e. HrmOp -> T : ~H --> ~H )
Theorem	hmopex 28734	The class of Hermitian operators is a set. (Contributed by NM, 17-Aug-2006.) (New usage is discouraged.)
|- HrmOp e. _V
Theorem	nmfnval 28735*	Value of the norm of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- ( T : ~H --> CC -> ( normfn ` T ) = sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) } , RR* , < ) )
Theorem	nmfnsetre 28736*	The set in the supremum of the functional norm definition df-nmfn 28704 is a set of reals. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
|- ( T : ~H --> CC -> { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) } C_ RR )
Theorem	nmfnsetn0 28737*	The set in the supremum of the functional norm definition df-nmfn 28704 is nonempty. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
|- ( abs ` ( T ` 0h ) ) e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) }
Theorem	nmfnxr 28738	The norm of any Hilbert space functional is an extended real. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.)
|- ( T : ~H --> CC -> ( normfn ` T ) e. RR* )
Theorem	nmfnrepnf 28739	The norm of a Hilbert space functional is either real or plus infinity. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.)
|- ( T : ~H --> CC -> ( ( normfn ` T ) e. RR <-> ( normfn ` T ) =/= +oo ) )
Theorem	nlfnval 28740	Value of the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
|- ( T : ~H --> CC -> ( null ` T ) = ( `' T " { 0 } ) )
Theorem	elcnfn 28741*	Property defining a continuous functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- ( T e. ContFn <-> ( T : ~H --> CC /\ A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( T ` w ) - ( T ` x ) ) ) < y ) ) )
Theorem	ellnfn 28742*	Property defining a linear functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- ( T e. LinFn <-> ( T : ~H --> CC /\ A. x e. CC A. y e. ~H A. z e. ~H ( T ` ( ( x .h y ) +h z ) ) = ( ( x x. ( T ` y ) ) + ( T ` z ) ) ) )
Theorem	lnfnf 28743	A linear Hilbert space functional is a functional. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
|- ( T e. LinFn -> T : ~H --> CC )
Theorem	dfadj2 28744*	Alternate definition of the adjoint of a Hilbert space operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.)
|- adjh = { <. t , u >. | ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) }
Theorem	funadj 28745	Functionality of the adjoint function. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
|- Fun adjh
Theorem	dmadjss 28746	The domain of the adjoint function is a subset of the maps from ~H to ~H. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
|- dom adjh C_ ( ~H ^m ~H )
Theorem	dmadjop 28747	A member of the domain of the adjoint function is a Hilbert space operator. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
|- ( T e. dom adjh -> T : ~H --> ~H )
Theorem	adjeu 28748*	Elementhood in the domain of the adjoint function. (Contributed by Mario Carneiro, 11-Sep-2015.) (Revised by Mario Carneiro, 24-Dec-2016.) (New usage is discouraged.)
|- ( T : ~H --> ~H -> ( T e. dom adjh <-> E! u e. ( ~H ^m ~H ) A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) )
Theorem	adjval 28749*	Value of the adjoint function for T in the domain of adjh. (Contributed by NM, 19-Feb-2006.) (Revised by Mario Carneiro, 24-Dec-2016.) (New usage is discouraged.)
|- ( T e. dom adjh -> ( adjh ` T ) = ( iota_ u e. ( ~H ^m ~H ) A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) )
Theorem	adjval2 28750*	Value of the adjoint function. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)
|- ( T e. dom adjh -> ( adjh ` T ) = ( iota_ u e. ( ~H ^m ~H ) A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( u ` y ) ) ) )
Theorem	cnvadj 28751	The adjoint function equals its converse. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
|- `' adjh = adjh
Theorem	funcnvadj 28752	The converse of the adjoint function is a function. (Contributed by NM, 25-Jan-2006.) (New usage is discouraged.)
|- Fun `' adjh
Theorem	adj1o 28753	The adjoint function maps one-to-one onto its domain. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
|- adjh : dom adjh -1-1-onto-> dom adjh
Theorem	dmadjrn 28754	The adjoint of an operator belongs to the adjoint function's domain. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
|- ( T e. dom adjh -> ( adjh ` T ) e. dom adjh )
Theorem	eigvecval 28755*	The set of eigenvectors of a Hilbert space operator. (Contributed by NM, 11-Mar-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- ( T : ~H --> ~H -> ( eigvec ` T ) = { x e. ( ~H \ 0H ) | E. y e. CC ( T ` x ) = ( y .h x ) } )
Theorem	eigvalfval 28756*	The eigenvalues of eigenvectors of a Hilbert space operator. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
|- ( T : ~H --> ~H -> ( eigval ` T ) = ( x e. ( eigvec ` T ) |-> ( ( ( T ` x ) .ih x ) / ( ( normh ` x ) ^ 2 ) ) ) )
Theorem	specval 28757*	The value of the spectrum of an operator. (Contributed by NM, 11-Apr-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- ( T : ~H --> ~H -> ( Lambda ` T ) = { x e. CC | -. ( T -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H } )
Theorem	speccl 28758	The spectrum of an operator is a set of complex numbers. (Contributed by NM, 11-Apr-2006.) (New usage is discouraged.)
|- ( T : ~H --> ~H -> ( Lambda ` T ) C_ CC )
Theorem	hhlnoi 28759	The linear operators of Hilbert space. (Contributed by NM, 19-Nov-2007.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.)
|- U = <. <. +h , .h >. , normh >.   &    |- L = ( U LnOp U )   =>    |- LinOp = L
Theorem	hhnmoi 28760	The norm of an operator in Hilbert space. (Contributed by NM, 19-Nov-2007.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
|- U = <. <. +h , .h >. , normh >.   &    |- N = ( U normOpOLD U )   =>    |- normop = N
Theorem	hhbloi 28761	A bounded linear operator in Hilbert space. (Contributed by NM, 19-Nov-2007.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.)
|- U = <. <. +h , .h >. , normh >.   &    |- B = ( U BLnOp U )   =>    |- BndLinOp = B
Theorem	hh0oi 28762	The zero operator in Hilbert space. (Contributed by NM, 7-Dec-2007.) (New usage is discouraged.)
|- U = <. <. +h , .h >. , normh >.   &    |- Z = ( U 0op U )   =>    |- 0hop = Z
Theorem	hhcno 28763	The continuous operators of Hilbert space. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
|- D = ( normh o. -h )   &    |- J = ( MetOpen ` D )   =>    |- ContOp = ( J Cn J )
Theorem	hhcnf 28764	The continuous functionals of Hilbert space. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
|- D = ( normh o. -h )   &    |- J = ( MetOpen ` D )   &    |- K = ( TopOpen ` ℂfld )   =>    |- ContFn = ( J Cn K )
Theorem	dmadjrnb 28765	The adjoint of an operator belongs to the adjoint function's domain. (Note: the converse is dependent on our definition of function value, since it uses ndmfv 6218.) (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)
|- ( T e. dom adjh <-> ( adjh ` T ) e. dom adjh )
Theorem	nmoplb 28766	A lower bound for an operator norm. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
|- ( ( T : ~H --> ~H /\ A e. ~H /\ ( normh ` A ) <_ 1 ) -> ( normh ` ( T ` A ) ) <_ ( normop ` T ) )
Theorem	nmopub 28767*	An upper bound for an operator norm. (Contributed by NM, 7-Mar-2006.) (New usage is discouraged.)
|- ( ( T : ~H --> ~H /\ A e. RR* ) -> ( ( normop ` T ) <_ A <-> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( normh ` ( T ` x ) ) <_ A ) ) )
Theorem	nmopub2tALT 28768*	An upper bound for an operator norm. (Contributed by NM, 12-Apr-2006.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( T : ~H --> ~H /\ ( A e. RR /\ 0 <_ A ) /\ A. x e. ~H ( normh ` ( T ` x ) ) <_ ( A x. ( normh ` x ) ) ) -> ( normop ` T ) <_ A )
Theorem	nmopub2tHIL 28769*	An upper bound for an operator norm. (Contributed by NM, 13-Dec-2007.) (New usage is discouraged.)
|- ( ( T : ~H --> ~H /\ ( A e. RR /\ 0 <_ A ) /\ A. x e. ~H ( normh ` ( T ` x ) ) <_ ( A x. ( normh ` x ) ) ) -> ( normop ` T ) <_ A )
Theorem	nmopge0 28770	The norm of any Hilbert space operator is nonnegative. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.)
|- ( T : ~H --> ~H -> 0 <_ ( normop ` T ) )
Theorem	nmopgt0 28771	A linear Hilbert space operator that is not identically zero has a positive norm. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.)
|- ( T : ~H --> ~H -> ( ( normop ` T ) =/= 0 <-> 0 < ( normop ` T ) ) )
Theorem	cnopc 28772*	Basic continuity property of a continuous Hilbert space operator. (Contributed by NM, 2-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- ( ( T e. ContOp /\ A e. ~H /\ B e. RR+ ) -> E. x e. RR+ A. y e. ~H ( ( normh ` ( y -h A ) ) < x -> ( normh ` ( ( T ` y ) -h ( T ` A ) ) ) < B ) )
Theorem	lnopl 28773	Basic linearity property of a linear Hilbert space operator. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.)
|- ( ( ( T e. LinOp /\ A e. CC ) /\ ( B e. ~H /\ C e. ~H ) ) -> ( T ` ( ( A .h B ) +h C ) ) = ( ( A .h ( T ` B ) ) +h ( T ` C ) ) )
Theorem	unop 28774	Basic inner product property of a unitary operator. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.)
|- ( ( T e. UniOp /\ A e. ~H /\ B e. ~H ) -> ( ( T ` A ) .ih ( T ` B ) ) = ( A .ih B ) )
Theorem	unopf1o 28775	A unitary operator in Hilbert space is one-to-one and onto. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.)
|- ( T e. UniOp -> T : ~H -1-1-onto-> ~H )
Theorem	unopnorm 28776	A unitary operator is idempotent in the norm. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.)
|- ( ( T e. UniOp /\ A e. ~H ) -> ( normh ` ( T ` A ) ) = ( normh ` A ) )
Theorem	cnvunop 28777	The inverse (converse) of a unitary operator in Hilbert space is unitary. Theorem in [AkhiezerGlazman] p. 72. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.)
|- ( T e. UniOp -> `' T e. UniOp )
Theorem	unopadj 28778	The inverse (converse) of a unitary operator is its adjoint. Equation 2 of [AkhiezerGlazman] p. 72. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.)
|- ( ( T e. UniOp /\ A e. ~H /\ B e. ~H ) -> ( ( T ` A ) .ih B ) = ( A .ih ( `' T ` B ) ) )
Theorem	unoplin 28779	A unitary operator is linear. Theorem in [AkhiezerGlazman] p. 72. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.)
|- ( T e. UniOp -> T e. LinOp )
Theorem	counop 28780	The composition of two unitary operators is unitary. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.)
|- ( ( S e. UniOp /\ T e. UniOp ) -> ( S o. T ) e. UniOp )
Theorem	hmop 28781	Basic inner product property of a Hermitian operator. (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.)
|- ( ( T e. HrmOp /\ A e. ~H /\ B e. ~H ) -> ( A .ih ( T ` B ) ) = ( ( T ` A ) .ih B ) )
Theorem	hmopre 28782	The inner product of the value and argument of a Hermitian operator is real. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
|- ( ( T e. HrmOp /\ A e. ~H ) -> ( ( T ` A ) .ih A ) e. RR )
Theorem	nmfnlb 28783	A lower bound for a functional norm. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
|- ( ( T : ~H --> CC /\ A e. ~H /\ ( normh ` A ) <_ 1 ) -> ( abs ` ( T ` A ) ) <_ ( normfn ` T ) )
Theorem	nmfnleub 28784*	An upper bound for the norm of a functional. (Contributed by NM, 24-May-2006.) (Revised by Mario Carneiro, 7-Sep-2014.) (New usage is discouraged.)
|- ( ( T : ~H --> CC /\ A e. RR* ) -> ( ( normfn ` T ) <_ A <-> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( abs ` ( T ` x ) ) <_ A ) ) )
Theorem	nmfnleub2 28785*	An upper bound for the norm of a functional. (Contributed by NM, 24-May-2006.) (New usage is discouraged.)
|- ( ( T : ~H --> CC /\ ( A e. RR /\ 0 <_ A ) /\ A. x e. ~H ( abs ` ( T ` x ) ) <_ ( A x. ( normh ` x ) ) ) -> ( normfn ` T ) <_ A )
Theorem	nmfnge0 28786	The norm of any Hilbert space functional is nonnegative. (Contributed by NM, 24-May-2006.) (New usage is discouraged.)
|- ( T : ~H --> CC -> 0 <_ ( normfn ` T ) )
Theorem	elnlfn 28787	Membership in the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
|- ( T : ~H --> CC -> ( A e. ( null ` T ) <-> ( A e. ~H /\ ( T ` A ) = 0 ) ) )
Theorem	elnlfn2 28788	Membership in the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
|- ( ( T : ~H --> CC /\ A e. ( null ` T ) ) -> ( T ` A ) = 0 )
Theorem	cnfnc 28789*	Basic continuity property of a continuous functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- ( ( T e. ContFn /\ A e. ~H /\ B e. RR+ ) -> E. x e. RR+ A. y e. ~H ( ( normh ` ( y -h A ) ) < x -> ( abs ` ( ( T ` y ) - ( T ` A ) ) ) < B ) )
Theorem	lnfnl 28790	Basic linearity property of a linear functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
|- ( ( ( T e. LinFn /\ A e. CC ) /\ ( B e. ~H /\ C e. ~H ) ) -> ( T ` ( ( A .h B ) +h C ) ) = ( ( A x. ( T ` B ) ) + ( T ` C ) ) )
Theorem	adjcl 28791	Closure of the adjoint of a Hilbert space operator. (Contributed by NM, 17-Jun-2006.) (New usage is discouraged.)
|- ( ( T e. dom adjh /\ A e. ~H ) -> ( ( adjh ` T ) ` A ) e. ~H )
Theorem	adj1 28792	Property of an adjoint Hilbert space operator. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
|- ( ( T e. dom adjh /\ A e. ~H /\ B e. ~H ) -> ( A .ih ( T ` B ) ) = ( ( ( adjh ` T ) ` A ) .ih B ) )
Theorem	adj2 28793	Property of an adjoint Hilbert space operator. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
|- ( ( T e. dom adjh /\ A e. ~H /\ B e. ~H ) -> ( ( T ` A ) .ih B ) = ( A .ih ( ( adjh ` T ) ` B ) ) )
Theorem	adjeq 28794*	A property that determines the adjoint of a Hilbert space operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.)
|- ( ( T : ~H --> ~H /\ S : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( S ` y ) ) ) -> ( adjh ` T ) = S )
Theorem	adjadj 28795	Double adjoint. Theorem 3.11(iv) of [Beran] p. 106. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
|- ( T e. dom adjh -> ( adjh ` ( adjh ` T ) ) = T )
Theorem	adjvalval 28796*	Value of the value of the adjoint function. (Contributed by NM, 22-Feb-2006.) (Proof shortened by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
|- ( ( T e. dom adjh /\ A e. ~H ) -> ( ( adjh ` T ) ` A ) = ( iota_ w e. ~H A. x e. ~H ( ( T ` x ) .ih A ) = ( x .ih w ) ) )
Theorem	unopadj2 28797	The adjoint of a unitary operator is its inverse (converse). Equation 2 of [AkhiezerGlazman] p. 72. (Contributed by NM, 23-Feb-2006.) (New usage is discouraged.)
|- ( T e. UniOp -> ( adjh ` T ) = `' T )
Theorem	hmopadj 28798	A Hermitian operator is self-adjoint. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.)
|- ( T e. HrmOp -> ( adjh ` T ) = T )
Theorem	hmdmadj 28799	Every Hermitian operator has an adjoint. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.)
|- ( T e. HrmOp -> T e. dom adjh )
Theorem	hmopadj2 28800	An operator is Hermitian iff it is self-adjoint. Definition of Hermitian in [Halmos] p. 41. (Contributed by NM, 9-Apr-2006.) (New usage is discouraged.)
|- ( T e. dom adjh -> ( T e. HrmOp <-> ( adjh ` T ) = T ) )