P. 289 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28801-28900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hmoplin 28801	A Hermitian operator is linear. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.)
|- ( T e. HrmOp -> T e. LinOp )
Theorem	brafval 28802*	The bra of a vector, expressed as <. A | in Dirac notation. See df-bra 28709. (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.)
|- ( A e. ~H -> ( bra ` A ) = ( x e. ~H |-> ( x .ih A ) ) )
Theorem	braval 28803	A bra-ket juxtaposition, expressed as <. A | B >. in Dirac notation, equals the inner product of the vectors. Based on definition of bra in [Prugovecki] p. 186. (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( bra ` A ) ` B ) = ( B .ih A ) )
Theorem	braadd 28804	Linearity property of bra for addition. (Contributed by NM, 23-May-2006.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( bra ` A ) ` ( B +h C ) ) = ( ( ( bra ` A ) ` B ) + ( ( bra ` A ) ` C ) ) )
Theorem	bramul 28805	Linearity property of bra for multiplication. (Contributed by NM, 23-May-2006.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. CC /\ C e. ~H ) -> ( ( bra ` A ) ` ( B .h C ) ) = ( B x. ( ( bra ` A ) ` C ) ) )
Theorem	brafn 28806	The bra function is a functional. (Contributed by NM, 23-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- ( A e. ~H -> ( bra ` A ) : ~H --> CC )
Theorem	bralnfn 28807	The Dirac bra function is a linear functional. (Contributed by NM, 23-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- ( A e. ~H -> ( bra ` A ) e. LinFn )
Theorem	bracl 28808	Closure of the bra function. (Contributed by NM, 23-May-2006.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( bra ` A ) ` B ) e. CC )
Theorem	bra0 28809	The Dirac bra of the zero vector. (Contributed by NM, 25-May-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.)
|- ( bra ` 0h ) = ( ~H X. { 0 } )
Theorem	brafnmul 28810	Anti-linearity property of bra functional for multiplication. (Contributed by NM, 31-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. ~H ) -> ( bra ` ( A .h B ) ) = ( ( * ` A ) .fn ( bra ` B ) ) )
Theorem	kbfval 28811*	The outer product of two vectors, expressed as | A >. <. B | in Dirac notation. See df-kb 28710. (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H ) -> ( A ketbra B ) = ( x e. ~H |-> ( ( x .ih B ) .h A ) ) )
Theorem	kbop 28812	The outer product of two vectors, expressed as | A >. <. B | in Dirac notation, is an operator. (Contributed by NM, 30-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H ) -> ( A ketbra B ) : ~H --> ~H )
Theorem	kbval 28813	The value of the operator resulting from the outer product | A >. <. B | of two vectors. Equation 8.1 of [Prugovecki] p. 376. (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A ketbra B ) ` C ) = ( ( C .ih B ) .h A ) )
Theorem	kbmul 28814	Multiplication property of outer product. (Contributed by NM, 31-May-2006.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( ( A .h B ) ketbra C ) = ( B ketbra ( ( * ` A ) .h C ) ) )
Theorem	kbpj 28815	If a vector A has norm 1, the outer product | A >. <. A | is the projector onto the subspace spanned by A. http://en.wikipedia.org/wiki/Bra-ket#Linear%5Foperators. (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
|- ( ( A e. ~H /\ ( normh ` A ) = 1 ) -> ( A ketbra A ) = ( proj h ` ( span ` { A } ) ) )
Theorem	eleigvec 28816*	Membership in 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 -> ( A e. ( eigvec ` T ) <-> ( A e. ~H /\ A =/= 0h /\ E. x e. CC ( T ` A ) = ( x .h A ) ) ) )
Theorem	eleigvec2 28817	Membership in the set of eigenvectors of a Hilbert space operator. (Contributed by NM, 18-Mar-2006.) (New usage is discouraged.)
|- ( T : ~H --> ~H -> ( A e. ( eigvec ` T ) <-> ( A e. ~H /\ A =/= 0h /\ ( T ` A ) e. ( span ` { A } ) ) ) )
Theorem	eleigveccl 28818	Closure of an eigenvector of a Hilbert space operator. (Contributed by NM, 23-Mar-2006.) (New usage is discouraged.)
|- ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> A e. ~H )
Theorem	eigvalval 28819	The eigenvalue of an eigenvector of a Hilbert space operator. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
|- ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> ( ( eigval ` T ) ` A ) = ( ( ( T ` A ) .ih A ) / ( ( normh ` A ) ^ 2 ) ) )
Theorem	eigvalcl 28820	An eigenvalue is a complex number. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
|- ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> ( ( eigval ` T ) ` A ) e. CC )
Theorem	eigvec1 28821	Property of an eigenvector. (Contributed by NM, 12-Mar-2006.) (New usage is discouraged.)
|- ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> ( ( T ` A ) = ( ( ( eigval ` T ) ` A ) .h A ) /\ A =/= 0h ) )
Theorem	eighmre 28822	The eigenvalues of a Hermitian operator are real. Equation 1.30 of [Hughes] p. 49. (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.)
|- ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) -> ( ( eigval ` T ) ` A ) e. RR )
Theorem	eighmorth 28823	Eigenvectors of a Hermitian operator with distinct eigenvalues are orthogonal. Equation 1.31 of [Hughes] p. 49. (Contributed by NM, 23-Mar-2006.) (New usage is discouraged.)
|- ( ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) /\ ( B e. ( eigvec ` T ) /\ ( ( eigval ` T ) ` A ) =/= ( ( eigval ` T ) ` B ) ) ) -> ( A .ih B ) = 0 )
Theorem	nmopnegi 28824	Value of the norm of the negative of a Hilbert space operator. Unlike nmophmi 28890, the operator does not have to be bounded. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
|- T : ~H --> ~H   =>    |- ( normop ` ( -u 1 .op T ) ) = ( normop ` T )
Theorem	lnop0 28825	The value of a linear Hilbert space operator at zero is zero. Remark in [Beran] p. 99. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.)
|- ( T e. LinOp -> ( T ` 0h ) = 0h )
Theorem	lnopmul 28826	Multiplicative property of a linear Hilbert space operator. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.)
|- ( ( T e. LinOp /\ A e. CC /\ B e. ~H ) -> ( T ` ( A .h B ) ) = ( A .h ( T ` B ) ) )
Theorem	lnopli 28827	Basic scalar product property of a linear Hilbert space operator. (Contributed by NM, 23-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	lnopfi 28828	A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 23-Jan-2006.) (New usage is discouraged.)
|- T e. LinOp   =>    |- T : ~H --> ~H
Theorem	lnop0i 28829	The value of a linear Hilbert space operator at zero is zero. Remark in [Beran] p. 99. (Contributed by NM, 11-May-2005.) (New usage is discouraged.)
|- T e. LinOp   =>    |- ( T ` 0h ) = 0h
Theorem	lnopaddi 28830	Additive property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005.) (New usage is discouraged.)
|- T e. LinOp   =>    |- ( ( A e. ~H /\ B e. ~H ) -> ( T ` ( A +h B ) ) = ( ( T ` A ) +h ( T ` B ) ) )
Theorem	lnopmuli 28831	Multiplicative property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005.) (New usage is discouraged.)
|- T e. LinOp   =>    |- ( ( A e. CC /\ B e. ~H ) -> ( T ` ( A .h B ) ) = ( A .h ( T ` B ) ) )
Theorem	lnopaddmuli 28832	Sum/product property of a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.)
|- T e. LinOp   =>    |- ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( T ` ( B +h ( A .h C ) ) ) = ( ( T ` B ) +h ( A .h ( T ` C ) ) ) )
Theorem	lnopsubi 28833	Subtraction property for a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.)
|- T e. LinOp   =>    |- ( ( A e. ~H /\ B e. ~H ) -> ( T ` ( A -h B ) ) = ( ( T ` A ) -h ( T ` B ) ) )
Theorem	lnopsubmuli 28834	Subtraction/product property of a linear Hilbert space operator. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.)
|- T e. LinOp   =>    |- ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( T ` ( B -h ( A .h C ) ) ) = ( ( T ` B ) -h ( A .h ( T ` C ) ) ) )
Theorem	lnopmulsubi 28835	Product/subtraction property of a linear Hilbert space operator. (Contributed by NM, 2-Jul-2005.) (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	homco2 28836	Move a scalar product out of a composition of operators. The operator T must be linear, unlike homco1 28660 that works for any operators. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.)
|- ( ( A e. CC /\ T e. LinOp /\ U : ~H --> ~H ) -> ( T o. ( A .op U ) ) = ( A .op ( T o. U ) ) )
Theorem	idunop 28837	The identity function (restricted to Hilbert space) is a unitary operator. (Contributed by NM, 21-Jan-2006.) (New usage is discouraged.)
|- ( _I |` ~H ) e. UniOp
Theorem	0cnop 28838	The identically zero function is a continuous Hilbert space operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
|- 0hop e. ContOp
Theorem	0cnfn 28839	The identically zero function is a continuous Hilbert space functional. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
|- ( ~H X. { 0 } ) e. ContFn
Theorem	idcnop 28840	The identity function (restricted to Hilbert space) is a continuous operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
|- ( _I |` ~H ) e. ContOp
Theorem	idhmop 28841	The Hilbert space identity operator is a Hermitian operator. (Contributed by NM, 22-Apr-2006.) (New usage is discouraged.)
|- Iop e. HrmOp
Theorem	0hmop 28842	The identically zero function is a Hermitian operator. (Contributed by NM, 8-Aug-2006.) (New usage is discouraged.)
|- 0hop e. HrmOp
Theorem	0lnop 28843	The identically zero function is a linear Hilbert space operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
|- 0hop e. LinOp
Theorem	0lnfn 28844	The identically zero function is a linear Hilbert space functional. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
|- ( ~H X. { 0 } ) e. LinFn
Theorem	nmop0 28845	The norm of the zero operator is zero. (Contributed by NM, 8-Feb-2006.) (New usage is discouraged.)
|- ( normop ` 0hop ) = 0
Theorem	nmfn0 28846	The norm of the identically zero functional is zero. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
|- ( normfn ` ( ~H X. { 0 } ) ) = 0
Theorem	hmopbdoptHIL 28847	A Hermitian operator is a bounded linear operator (Hellinger-Toeplitz Theorem). (Contributed by NM, 18-Jan-2008.) (New usage is discouraged.)
|- ( T e. HrmOp -> T e. BndLinOp )
Theorem	hoddii 28848	Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri 28639 does not require linearity.) (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
|- R e. LinOp   &    |- S : ~H --> ~H   &    |- T : ~H --> ~H   =>    |- ( R o. ( S -op T ) ) = ( ( R o. S ) -op ( R o. T ) )
Theorem	hoddi 28849	Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri 28639 does not require linearity.) (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.)
|- ( ( R e. LinOp /\ S : ~H --> ~H /\ T : ~H --> ~H ) -> ( R o. ( S -op T ) ) = ( ( R o. S ) -op ( R o. T ) ) )
Theorem	nmop0h 28850	The norm of any operator on the trivial Hilbert space is zero. (This is the reason we need ~H =/= 0H in nmopun 28873.) (Contributed by NM, 24-Feb-2006.) (New usage is discouraged.)
|- ( ( ~H = 0H /\ T : ~H --> ~H ) -> ( normop ` T ) = 0 )
Theorem	idlnop 28851	The identity function (restricted to Hilbert space) is a linear operator. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.)
|- ( _I |` ~H ) e. LinOp
Theorem	0bdop 28852	The identically zero operator is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
|- 0hop e. BndLinOp
Theorem	adj0 28853	Adjoint of the zero operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.)
|- ( adjh ` 0hop ) = 0hop
Theorem	nmlnop0iALT 28854	A linear operator with a zero norm is identically zero. (Contributed by NM, 8-Feb-2006.) (New usage is discouraged.) (Proof modification is discouraged.)
|- T e. LinOp   =>    |- ( ( normop ` T ) = 0 <-> T = 0hop )
Theorem	nmlnop0iHIL 28855	A linear operator with a zero norm is identically zero. (Contributed by NM, 18-Jan-2008.) (New usage is discouraged.)
|- T e. LinOp   =>    |- ( ( normop ` T ) = 0 <-> T = 0hop )
Theorem	nmlnopgt0i 28856	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 e. LinOp   =>    |- ( T =/= 0hop <-> 0 < ( normop ` T ) )
Theorem	nmlnop0 28857	A linear operator with a zero norm is identically zero. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)
|- ( T e. LinOp -> ( ( normop ` T ) = 0 <-> T = 0hop ) )
Theorem	nmlnopne0 28858	A linear operator with a nonzero norm is nonzero. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)
|- ( T e. LinOp -> ( ( normop ` T ) =/= 0 <-> T =/= 0hop ) )
Theorem	lnopmi 28859	The scalar product of a linear operator is a linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
|- T e. LinOp   =>    |- ( A e. CC -> ( A .op T ) e. LinOp )
Theorem	lnophsi 28860	The sum of two linear operators is linear. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
|- S e. LinOp   &    |- T e. LinOp   =>    |- ( S +op T ) e. LinOp
Theorem	lnophdi 28861	The difference of two linear operators is linear. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.)
|- S e. LinOp   &    |- T e. LinOp   =>    |- ( S -op T ) e. LinOp
Theorem	lnopcoi 28862	The composition of two linear operators is linear. (Contributed by NM, 8-Mar-2006.) (New usage is discouraged.)
|- S e. LinOp   &    |- T e. LinOp   =>    |- ( S o. T ) e. LinOp
Theorem	lnopco0i 28863	The composition of a linear operator with one whose norm is zero. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
|- S e. LinOp   &    |- T e. LinOp   =>    |- ( ( normop ` T ) = 0 -> ( normop ` ( S o. T ) ) = 0 )
Theorem	lnopeq0lem1 28864	Lemma for lnopeq0i 28866. Apply the generalized polarization identity polid2i 28014 to the quadratic form ( ( T ` x ) , x ). (Contributed by NM, 26-Jul-2006.) (New usage is discouraged.)
|- T e. LinOp   &    |- A e. ~H   &    |- B e. ~H   =>    |- ( ( T ` A ) .ih B ) = ( ( ( ( ( T ` ( A +h B ) ) .ih ( A +h B ) ) - ( ( T ` ( A -h B ) ) .ih ( A -h B ) ) ) + ( _i x. ( ( ( T ` ( A +h ( _i .h B ) ) ) .ih ( A +h ( _i .h B ) ) ) - ( ( T ` ( A -h ( _i .h B ) ) ) .ih ( A -h ( _i .h B ) ) ) ) ) ) / 4 )
Theorem	lnopeq0lem2 28865	Lemma for lnopeq0i 28866. (Contributed by NM, 26-Jul-2006.) (New usage is discouraged.)
|- T e. LinOp   =>    |- ( ( A e. ~H /\ B e. ~H ) -> ( ( T ` A ) .ih B ) = ( ( ( ( ( T ` ( A +h B ) ) .ih ( A +h B ) ) - ( ( T ` ( A -h B ) ) .ih ( A -h B ) ) ) + ( _i x. ( ( ( T ` ( A +h ( _i .h B ) ) ) .ih ( A +h ( _i .h B ) ) ) - ( ( T ` ( A -h ( _i .h B ) ) ) .ih ( A -h ( _i .h B ) ) ) ) ) ) / 4 ) )
Theorem	lnopeq0i 28866*	A condition implying that a linear Hilbert space operator is identically zero. Unlike ho01i 28687 for arbitrary operators, when the operator is linear we need to consider only the values of the quadratic form ( T ` x ) .ih x ). (Contributed by NM, 26-Jul-2006.) (New usage is discouraged.)
|- T e. LinOp   =>    |- ( A. x e. ~H ( ( T ` x ) .ih x ) = 0 <-> T = 0hop )
Theorem	lnopeqi 28867*	Two linear Hilbert space operators are equal iff their quadratic forms are equal. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.)
|- T e. LinOp   &    |- U e. LinOp   =>    |- ( A. x e. ~H ( ( T ` x ) .ih x ) = ( ( U ` x ) .ih x ) <-> T = U )
Theorem	lnopeq 28868*	Two linear Hilbert space operators are equal iff their quadratic forms are equal. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.)
|- ( ( T e. LinOp /\ U e. LinOp ) -> ( A. x e. ~H ( ( T ` x ) .ih x ) = ( ( U ` x ) .ih x ) <-> T = U ) )
Theorem	lnopunilem1 28869*	Lemma for lnopunii 28871. (Contributed by NM, 14-May-2005.) (New usage is discouraged.)
|- T e. LinOp   &    |- A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x )   &    |- A e. ~H   &    |- B e. ~H   &    |- C e. CC   =>    |- ( Re ` ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) ) = ( Re ` ( C x. ( A .ih B ) ) )
Theorem	lnopunilem2 28870*	Lemma for lnopunii 28871. (Contributed by NM, 12-May-2005.) (New usage is discouraged.)
|- T e. LinOp   &    |- A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x )   &    |- A e. ~H   &    |- B e. ~H   =>    |- ( ( T ` A ) .ih ( T ` B ) ) = ( A .ih B )
Theorem	lnopunii 28871*	If a linear operator (whose range is ~H) is idempotent in the norm, the operator is unitary. Similar to theorem in [AkhiezerGlazman] p. 73. (Contributed by NM, 23-Jan-2006.) (New usage is discouraged.)
|- T e. LinOp   &    |- T : ~H -onto-> ~H   &    |- A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x )   =>    |- T e. UniOp
Theorem	elunop2 28872*	An operator is unitary iff it is linear, onto, and idempotent in the norm. Similar to theorem in [AkhiezerGlazman] p. 73, and its converse. (Contributed by NM, 24-Feb-2006.) (New usage is discouraged.)
|- ( T e. UniOp <-> ( T e. LinOp /\ T : ~H -onto-> ~H /\ A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) ) )
Theorem	nmopun 28873	Norm of a unitary Hilbert space operator. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.)
|- ( ( ~H =/= 0H /\ T e. UniOp ) -> ( normop ` T ) = 1 )
Theorem	unopbd 28874	A unitary operator is a bounded linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
|- ( T e. UniOp -> T e. BndLinOp )
Theorem	lnophmlem1 28875*	Lemma for lnophmi 28877. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.)
|- A e. ~H   &    |- B e. ~H   &    |- T e. LinOp   &    |- A. x e. ~H ( x .ih ( T ` x ) ) e. RR   =>    |- ( A .ih ( T ` A ) ) e. RR
Theorem	lnophmlem2 28876*	Lemma for lnophmi 28877. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.)
|- A e. ~H   &    |- B e. ~H   &    |- T e. LinOp   &    |- A. x e. ~H ( x .ih ( T ` x ) ) e. RR   =>    |- ( A .ih ( T ` B ) ) = ( ( T ` A ) .ih B )
Theorem	lnophmi 28877*	A linear operator is Hermitian if x .ih ( T ` x ) takes only real values. Remark in [ReedSimon] p. 195. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.)
|- T e. LinOp   &    |- A. x e. ~H ( x .ih ( T ` x ) ) e. RR   =>    |- T e. HrmOp
Theorem	lnophm 28878*	A linear operator is Hermitian if x .ih ( T ` x ) takes only real values. Remark in [ReedSimon] p. 195. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.)
|- ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) -> T e. HrmOp )
Theorem	hmops 28879	The sum of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
|- ( ( T e. HrmOp /\ U e. HrmOp ) -> ( T +op U ) e. HrmOp )
Theorem	hmopm 28880	The scalar product of a Hermitian operator with a real is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
|- ( ( A e. RR /\ T e. HrmOp ) -> ( A .op T ) e. HrmOp )
Theorem	hmopd 28881	The difference of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
|- ( ( T e. HrmOp /\ U e. HrmOp ) -> ( T -op U ) e. HrmOp )
Theorem	hmopco 28882	The composition of two commuting Hermitian operators is Hermitian. (Contributed by NM, 22-Aug-2006.) (New usage is discouraged.)
|- ( ( T e. HrmOp /\ U e. HrmOp /\ ( T o. U ) = ( U o. T ) ) -> ( T o. U ) e. HrmOp )
Theorem	nmbdoplbi 28883	A lower bound for the norm of a bounded linear operator. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
|- T e. BndLinOp   =>    |- ( A e. ~H -> ( normh ` ( T ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )
Theorem	nmbdoplb 28884	A lower bound for the norm of a bounded linear Hilbert space operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
|- ( ( T e. BndLinOp /\ A e. ~H ) -> ( normh ` ( T ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )
Theorem	nmcexi 28885*	Lemma for nmcopexi 28886 and nmcfnexi 28910. The norm of a continuous linear Hilbert space operator or functional exists. Theorem 3.5(i) of [Beran] p. 99. (Contributed by Mario Carneiro, 17-Nov-2013.) (Proof shortened by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
|- E. y e. RR+ A. z e. ~H ( ( normh ` z ) < y -> ( N ` ( T ` z ) ) < 1 )   &    |- ( S ` T ) = sup ( { m | E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( N ` ( T ` x ) ) ) } , RR* , < )   &    |- ( x e. ~H -> ( N ` ( T ` x ) ) e. RR )   &    |- ( N ` ( T ` 0h ) ) = 0   &    |- ( ( ( y / 2 ) e. RR+ /\ x e. ~H ) -> ( ( y / 2 ) x. ( N ` ( T ` x ) ) ) = ( N ` ( T ` ( ( y / 2 ) .h x ) ) ) )   =>    |- ( S ` T ) e. RR
Theorem	nmcopexi 28886	The norm of a continuous linear Hilbert space operator exists. Theorem 3.5(i) of [Beran] p. 99. (Contributed by NM, 5-Feb-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
|- T e. LinOp   &    |- T e. ContOp   =>    |- ( normop ` T ) e. RR
Theorem	nmcoplbi 28887	A lower bound for the norm of a continuous linear operator. Theorem 3.5(ii) of [Beran] p. 99. (Contributed by NM, 7-Feb-2006.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
|- T e. LinOp   &    |- T e. ContOp   =>    |- ( A e. ~H -> ( normh ` ( T ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )
Theorem	nmcopex 28888	The norm of a continuous linear Hilbert space operator exists. Theorem 3.5(i) of [Beran] p. 99. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
|- ( ( T e. LinOp /\ T e. ContOp ) -> ( normop ` T ) e. RR )
Theorem	nmcoplb 28889	A lower bound for the norm of a continuous linear Hilbert space operator. Theorem 3.5(ii) of [Beran] p. 99. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
|- ( ( T e. LinOp /\ T e. ContOp /\ A e. ~H ) -> ( normh ` ( T ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )
Theorem	nmophmi 28890	The norm of the scalar product of a bounded linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
|- T e. BndLinOp   =>    |- ( A e. CC -> ( normop ` ( A .op T ) ) = ( ( abs ` A ) x. ( normop ` T ) ) )
Theorem	bdophmi 28891	The scalar product of a bounded linear operator is a bounded linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
|- T e. BndLinOp   =>    |- ( A e. CC -> ( A .op T ) e. BndLinOp )
Theorem	lnconi 28892*	Lemma for lnopconi 28893 and lnfnconi 28914. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
|- ( T e. C -> S e. RR )   &    |- ( ( T e. C /\ y e. ~H ) -> ( N ` ( T ` y ) ) <_ ( S x. ( normh ` y ) ) )   &    |- ( T e. C <-> A. x e. ~H A. z e. RR+ E. y e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < y -> ( N ` ( ( T ` w ) M ( T ` x ) ) ) < z ) )   &    |- ( y e. ~H -> ( N ` ( T ` y ) ) e. RR )   &    |- ( ( w e. ~H /\ x e. ~H ) -> ( T ` ( w -h x ) ) = ( ( T ` w ) M ( T ` x ) ) )   =>    |- ( T e. C <-> E. x e. RR A. y e. ~H ( N ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) )
Theorem	lnopconi 28893*	A condition equivalent to " T is continuous" when T is linear. Theorem 3.5(iii) of [Beran] p. 99. (Contributed by NM, 7-Feb-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
|- T e. LinOp   =>    |- ( T e. ContOp <-> E. x e. RR A. y e. ~H ( normh ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) )
Theorem	lnopcon 28894*	A condition equivalent to " T is continuous" when T is linear. Theorem 3.5(iii) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
|- ( T e. LinOp -> ( T e. ContOp <-> E. x e. RR A. y e. ~H ( normh ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) ) )
Theorem	lnopcnbd 28895	A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
|- ( T e. LinOp -> ( T e. ContOp <-> T e. BndLinOp ) )
Theorem	lncnopbd 28896	A continuous linear operator is a bounded linear operator. This theorem justifies our use of "bounded linear" as an interchangeable condition for "continuous linear" used in some textbook proofs. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
|- ( T e. ( LinOp i^i ContOp ) <-> T e. BndLinOp )
Theorem	lncnbd 28897	A continuous linear operator is a bounded linear operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
|- ( LinOp i^i ContOp ) = BndLinOp
Theorem	lnopcnre 28898	A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
|- ( T e. LinOp -> ( T e. ContOp <-> ( normop ` T ) e. RR ) )
Theorem	lnfnli 28899	Basic property of a linear Hilbert space 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	lnfnfi 28900	A linear Hilbert space functional is a functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
|- T e. LinFn   =>    |- T : ~H --> CC