P. 235 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 23401-23500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	braadd 23401	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 23402	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 23403	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 23404	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 23405	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 23406	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 23407	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 23408*	The outer product of two vectors, expressed as | A >. <. B | in Dirac notation. See df-kb 23307. (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 23409	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 23410	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 23411	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 23412	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 23413*	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 23414	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 23415	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 23416	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 23417	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 23418	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 23419	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 23420	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 23421	Value of the norm of the negative of a Hilbert space operator. Unlike nmophmi 23487, 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 23422	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 23423	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 23424	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 23425	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 23426	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 23427	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 23428	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 23429	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 23430	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 23431	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 23432	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 23433	Move a scalar product out of a composition of operators. The operator T must be linear, unlike homco1 23257 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 23434	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 23435	The identically zero function is a continuous Hilbert space operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
|- 0hop e. ConOp
Theorem	0cnfn 23436	The identically zero function is a continuous Hilbert space functional. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
|- ( ~H X. { 0 } ) e. ConFn
Theorem	idcnop 23437	The identity function (restricted to Hilbert space) is a continuous operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
|- ( _I |` ~H ) e. ConOp
Theorem	idhmop 23438	The Hilbert space identity operator is a Hermitian operator. (Contributed by NM, 22-Apr-2006.) (New usage is discouraged.)
|- Iop e. HrmOp
Theorem	0hmop 23439	The identically zero function is a Hermitian operator. (Contributed by NM, 8-Aug-2006.) (New usage is discouraged.)
|- 0hop e. HrmOp
Theorem	0lnop 23440	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 23441	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 23442	The norm of the zero operator is zero. (Contributed by NM, 8-Feb-2006.) (New usage is discouraged.)
|- ( normop ` 0hop ) = 0
Theorem	nmfn0 23443	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 23444	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 23445	Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri 23236 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 23446	Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri 23236 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 23447	The norm of any operator on the trivial Hilbert space is zero. (This is the reason we need ~H =/= 0H in nmopun 23470.) (Contributed by NM, 24-Feb-2006.) (New usage is discouraged.)
|- ( ( ~H = 0H /\ T : ~H --> ~H ) -> ( normop ` T ) = 0 )
Theorem	idlnop 23448	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 23449	The identically zero operator is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
|- 0hop e. BndLinOp
Theorem	adj0 23450	Adjoint of the zero operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.)
|- ( adjh ` 0hop ) = 0hop
Theorem	nmlnop0iALT 23451	A linear operator with a zero norm is identically zero. (Contributed by NM, 8-Feb-2006.) (New usage is discouraged.)
|- T e. LinOp   =>    |- ( ( normop ` T ) = 0 <-> T = 0hop )
Theorem	nmlnop0iHIL 23452	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 23453	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 23454	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 23455	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 23456	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 23457	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 23458	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 23459	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 23460	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 23461	Lemma for lnopeq0i 23463. Apply the generalized polarization identity polid2i 22612 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 23462	Lemma for lnopeq0i 23463. (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 23463*	A condition implying that a linear Hilbert space operator is identically zero. Unlike ho01i 23284 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 23464*	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 23465*	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 23466*	Lemma for lnopunii 23468. (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 23467*	Lemma for lnopunii 23468. (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 23468*	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 23469*	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 23470	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 23471	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 23472*	Lemma for lnophmi 23474. (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 23473*	Lemma for lnophmi 23474. (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 23474*	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 23475*	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 23476	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 23477	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 23478	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 23479	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 23480	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 23481	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 23482*	Lemma for nmcopexi 23483 and nmcfnexi 23507. 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 23483	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. ConOp   =>    |- ( normop ` T ) e. RR
Theorem	nmcoplbi 23484	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. ConOp   =>    |- ( A e. ~H -> ( normh ` ( T ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )
Theorem	nmcopex 23485	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. ConOp ) -> ( normop ` T ) e. RR )
Theorem	nmcoplb 23486	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. ConOp /\ A e. ~H ) -> ( normh ` ( T ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )
Theorem	nmophmi 23487	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 23488	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 23489*	Lemma for lnopconi 23490 and lnfnconi 23511. (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 23490*	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. ConOp <-> E. x e. RR A. y e. ~H ( normh ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) )
Theorem	lnopcon 23491*	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. ConOp <-> E. x e. RR A. y e. ~H ( normh ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) ) )
Theorem	lnopcnbd 23492	A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
|- ( T e. LinOp -> ( T e. ConOp <-> T e. BndLinOp ) )
Theorem	lncnopbd 23493	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 ConOp ) <-> T e. BndLinOp )
Theorem	lncnbd 23494	A continuous linear operator is a bounded linear operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
|- ( LinOp i^i ConOp ) = BndLinOp
Theorem	lnopcnre 23495	A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
|- ( T e. LinOp -> ( T e. ConOp <-> ( normop ` T ) e. RR ) )
Theorem	lnfnli 23496	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 23497	A linear Hilbert space functional is a functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
|- T e. LinFn   =>    |- T : ~H --> CC
Theorem	lnfn0i 23498	The value of a linear Hilbert space functional at zero is zero. Remark in [Beran] p. 99. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
|- T e. LinFn   =>    |- ( T ` 0h ) = 0
Theorem	lnfnaddi 23499	Additive property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
|- T e. LinFn   =>    |- ( ( A e. ~H /\ B e. ~H ) -> ( T ` ( A +h B ) ) = ( ( T ` A ) + ( T ` B ) ) )
Theorem	lnfnmuli 23500	Multiplicative 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 ) -> ( T ` ( A .h B ) ) = ( A x. ( T ` B ) ) )