P. 290 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28901-29000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lnfn0i 28901	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 28902	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 28903	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 ) ) )
Theorem	lnfnaddmuli 28904	Sum/product property of a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.)
|- T e. LinFn   =>    |- ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( T ` ( B +h ( A .h C ) ) ) = ( ( T ` B ) + ( A x. ( T ` C ) ) ) )
Theorem	lnfnsubi 28905	Subtraction property for a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.)
|- T e. LinFn   =>    |- ( ( A e. ~H /\ B e. ~H ) -> ( T ` ( A -h B ) ) = ( ( T ` A ) - ( T ` B ) ) )
Theorem	lnfn0 28906	The value of a linear Hilbert space functional at zero is zero. Remark in [Beran] p. 99. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
|- ( T e. LinFn -> ( T ` 0h ) = 0 )
Theorem	lnfnmul 28907	Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
|- ( ( T e. LinFn /\ A e. CC /\ B e. ~H ) -> ( T ` ( A .h B ) ) = ( A x. ( T ` B ) ) )
Theorem	nmbdfnlbi 28908	A lower bound for the norm of a bounded linear functional. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
|- ( T e. LinFn /\ ( normfn ` T ) e. RR )   =>    |- ( A e. ~H -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) )
Theorem	nmbdfnlb 28909	A lower bound for the norm of a bounded linear functional. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
|- ( ( T e. LinFn /\ ( normfn ` T ) e. RR /\ A e. ~H ) -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) )
Theorem	nmcfnexi 28910	The norm of a continuous linear Hilbert space functional exists. Theorem 3.5(i) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
|- T e. LinFn   &    |- T e. ContFn   =>    |- ( normfn ` T ) e. RR
Theorem	nmcfnlbi 28911	A lower bound for the norm of a continuous linear functional. Theorem 3.5(ii) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
|- T e. LinFn   &    |- T e. ContFn   =>    |- ( A e. ~H -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) )
Theorem	nmcfnex 28912	The norm of a continuous linear Hilbert space functional exists. Theorem 3.5(i) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
|- ( ( T e. LinFn /\ T e. ContFn ) -> ( normfn ` T ) e. RR )
Theorem	nmcfnlb 28913	A lower bound of the norm of a continuous linear Hilbert space functional. Theorem 3.5(ii) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
|- ( ( T e. LinFn /\ T e. ContFn /\ A e. ~H ) -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) )
Theorem	lnfnconi 28914*	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.) (Proof shortened by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
|- T e. LinFn   =>    |- ( T e. ContFn <-> E. x e. RR A. y e. ~H ( abs ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) )
Theorem	lnfncon 28915*	A condition equivalent to " T is continuous" when T is linear. Theorem 3.5(iii) of [Beran] p. 99. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.)
|- ( T e. LinFn -> ( T e. ContFn <-> E. x e. RR A. y e. ~H ( abs ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) ) )
Theorem	lnfncnbd 28916	A linear functional is continuous iff it is bounded. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
|- ( T e. LinFn -> ( T e. ContFn <-> ( normfn ` T ) e. RR ) )
Theorem	imaelshi 28917	The image of a subspace under a linear operator is a subspace. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
|- T e. LinOp   &    |- A e. SH   =>    |- ( T " A ) e. SH
Theorem	rnelshi 28918	The range of a linear operator is a subspace. (Contributed by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
|- T e. LinOp   =>    |- ran T e. SH
Theorem	nlelshi 28919	The null space of a linear functional is a subspace. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
|- T e. LinFn   =>    |- ( null ` T ) e. SH
Theorem	nlelchi 28920	The null space of a continuous linear functional is a closed subspace. Remark 3.8 of [Beran] p. 103. (Contributed by NM, 11-Feb-2006.) (Proof shortened by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
|- T e. LinFn   &    |- T e. ContFn   =>    |- ( null ` T ) e. CH
19.6.11  Riesz lemma
Theorem	riesz3i 28921*	A continuous linear functional can be expressed as an inner product. Existence part of Theorem 3.9 of [Beran] p. 104. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.)
|- T e. LinFn   &    |- T e. ContFn   =>    |- E. w e. ~H A. v e. ~H ( T ` v ) = ( v .ih w )
Theorem	riesz4i 28922*	A continuous linear functional can be expressed as an inner product. Uniqueness part of Theorem 3.9 of [Beran] p. 104. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.)
|- T e. LinFn   &    |- T e. ContFn   =>    |- E! w e. ~H A. v e. ~H ( T ` v ) = ( v .ih w )
Theorem	riesz4 28923*	A continuous linear functional can be expressed as an inner product. Uniqueness part of Theorem 3.9 of [Beran] p. 104. See riesz2 28925 for the bounded linear functional version. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.)
|- ( T e. ( LinFn i^i ContFn ) -> E! w e. ~H A. v e. ~H ( T ` v ) = ( v .ih w ) )
Theorem	riesz1 28924*	Part 1 of the Riesz representation theorem for bounded linear functionals. A linear functional is bounded iff its value can be expressed as an inner product. Part of Theorem 17.3 of [Halmos] p. 31. For part 2, see riesz2 28925. For the continuous linear functional version, see riesz3i 28921 and riesz4 28923. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
|- ( T e. LinFn -> ( ( normfn ` T ) e. RR <-> E. y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) ) )
Theorem	riesz2 28925*	Part 2 of the Riesz representation theorem for bounded linear functionals. The value of a bounded linear functional corresponds to a unique inner product. Part of Theorem 17.3 of [Halmos] p. 31. For part 1, see riesz1 28924. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
|- ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) -> E! y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) )
19.6.12  Adjoints (cont.)
Theorem	cnlnadjlem1 28926*	Lemma for cnlnadji 28935 (Theorem 3.10 of [Beran] p. 104: every continuous linear operator has an adjoint). The value of the auxiliary functional G. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.)
|- T e. LinOp   &    |- T e. ContOp   &    |- G = ( g e. ~H |-> ( ( T ` g ) .ih y ) )   =>    |- ( A e. ~H -> ( G ` A ) = ( ( T ` A ) .ih y ) )
Theorem	cnlnadjlem2 28927*	Lemma for cnlnadji 28935. G is a continuous linear functional. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.)
|- T e. LinOp   &    |- T e. ContOp   &    |- G = ( g e. ~H |-> ( ( T ` g ) .ih y ) )   =>    |- ( y e. ~H -> ( G e. LinFn /\ G e. ContFn ) )
Theorem	cnlnadjlem3 28928*	Lemma for cnlnadji 28935. By riesz4 28923, B is the unique vector such that ( T ` v ) .ih y ) = ( v .ih w ) for all v. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.)
|- T e. LinOp   &    |- T e. ContOp   &    |- G = ( g e. ~H |-> ( ( T ` g ) .ih y ) )   &    |- B = ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) )   =>    |- ( y e. ~H -> B e. ~H )
Theorem	cnlnadjlem4 28929*	Lemma for cnlnadji 28935. The values of auxiliary function F are vectors. (Contributed by NM, 17-Feb-2006.) (Proof shortened by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
|- T e. LinOp   &    |- T e. ContOp   &    |- G = ( g e. ~H |-> ( ( T ` g ) .ih y ) )   &    |- B = ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) )   &    |- F = ( y e. ~H |-> B )   =>    |- ( A e. ~H -> ( F ` A ) e. ~H )
Theorem	cnlnadjlem5 28930*	Lemma for cnlnadji 28935. F is an adjoint of T (later, we will show it is unique). (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
|- T e. LinOp   &    |- T e. ContOp   &    |- G = ( g e. ~H |-> ( ( T ` g ) .ih y ) )   &    |- B = ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) )   &    |- F = ( y e. ~H |-> B )   =>    |- ( ( A e. ~H /\ C e. ~H ) -> ( ( T ` C ) .ih A ) = ( C .ih ( F ` A ) ) )
Theorem	cnlnadjlem6 28931*	Lemma for cnlnadji 28935. F is linear. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.)
|- T e. LinOp   &    |- T e. ContOp   &    |- G = ( g e. ~H |-> ( ( T ` g ) .ih y ) )   &    |- B = ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) )   &    |- F = ( y e. ~H |-> B )   =>    |- F e. LinOp
Theorem	cnlnadjlem7 28932*	Lemma for cnlnadji 28935. Helper lemma to show that F is continuous. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
|- T e. LinOp   &    |- T e. ContOp   &    |- G = ( g e. ~H |-> ( ( T ` g ) .ih y ) )   &    |- B = ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) )   &    |- F = ( y e. ~H |-> B )   =>    |- ( A e. ~H -> ( normh ` ( F ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )
Theorem	cnlnadjlem8 28933*	Lemma for cnlnadji 28935. F is continuous. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.)
|- T e. LinOp   &    |- T e. ContOp   &    |- G = ( g e. ~H |-> ( ( T ` g ) .ih y ) )   &    |- B = ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) )   &    |- F = ( y e. ~H |-> B )   =>    |- F e. ContOp
Theorem	cnlnadjlem9 28934*	Lemma for cnlnadji 28935. F provides an example showing the existence of a continuous linear adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
|- T e. LinOp   &    |- T e. ContOp   &    |- G = ( g e. ~H |-> ( ( T ` g ) .ih y ) )   &    |- B = ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) )   &    |- F = ( y e. ~H |-> B )   =>    |- E. t e. ( LinOp i^i ContOp ) A. x e. ~H A. z e. ~H ( ( T ` x ) .ih z ) = ( x .ih ( t ` z ) )
Theorem	cnlnadji 28935*	Every continuous linear operator has an adjoint. Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
|- T e. LinOp   &    |- T e. ContOp   =>    |- E. t e. ( LinOp i^i ContOp ) A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( t ` y ) )
Theorem	cnlnadjeui 28936*	Every continuous linear operator has a unique adjoint. Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
|- T e. LinOp   &    |- T e. ContOp   =>    |- E! t e. ( LinOp i^i ContOp ) A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( t ` y ) )
Theorem	cnlnadjeu 28937*	Every continuous linear operator has a unique adjoint. Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)
|- ( T e. ( LinOp i^i ContOp ) -> E! t e. ( LinOp i^i ContOp ) A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( t ` y ) ) )
Theorem	cnlnadj 28938*	Every continuous linear operator has an adjoint. Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
|- ( T e. ( LinOp i^i ContOp ) -> E. t e. ( LinOp i^i ContOp ) A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = ( x .ih ( t ` y ) ) )
Theorem	cnlnssadj 28939	Every continuous linear Hilbert space operator has an adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
|- ( LinOp i^i ContOp ) C_ dom adjh
Theorem	bdopssadj 28940	Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)
|- BndLinOp C_ dom adjh
Theorem	bdopadj 28941	Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.)
|- ( T e. BndLinOp -> T e. dom adjh )
Theorem	adjbdln 28942	The adjoint of a bounded linear operator is a bounded linear operator. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)
|- ( T e. BndLinOp -> ( adjh ` T ) e. BndLinOp )
Theorem	adjbdlnb 28943	An operator is bounded and linear iff its adjoint is. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)
|- ( T e. BndLinOp <-> ( adjh ` T ) e. BndLinOp )
Theorem	adjbd1o 28944	The mapping of adjoints of bounded linear operators is one-to-one onto. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)
|- ( adjh |` BndLinOp ) : BndLinOp -1-1-onto-> BndLinOp
Theorem	adjlnop 28945	The adjoint of an operator is linear. Proposition 1 of [AkhiezerGlazman] p. 80. (Contributed by NM, 17-Jun-2006.) (New usage is discouraged.)
|- ( T e. dom adjh -> ( adjh ` T ) e. LinOp )
Theorem	adjsslnop 28946	Every operator with an adjoint is linear. (Contributed by NM, 17-Jun-2006.) (New usage is discouraged.)
|- dom adjh C_ LinOp
Theorem	nmopadjlei 28947	Property of the norm of an adjoint. Part of proof of Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.)
|- T e. BndLinOp   =>    |- ( A e. ~H -> ( normh ` ( ( adjh ` T ) ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )
Theorem	nmopadjlem 28948	Lemma for nmopadji 28949. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.)
|- T e. BndLinOp   =>    |- ( normop ` ( adjh ` T ) ) <_ ( normop ` T )
Theorem	nmopadji 28949	Property of the norm of an adjoint. Theorem 3.11(v) of [Beran] p. 106. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.)
|- T e. BndLinOp   =>    |- ( normop ` ( adjh ` T ) ) = ( normop ` T )
Theorem	adjeq0 28950	An operator is zero iff its adjoint is zero. Theorem 3.11(i) of [Beran] p. 106. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.)
|- ( T = 0hop <-> ( adjh ` T ) = 0hop )
Theorem	adjmul 28951	The adjoint of the scalar product of an operator. Theorem 3.11(ii) of [Beran] p. 106. (Contributed by NM, 21-Feb-2006.) (New usage is discouraged.)
|- ( ( A e. CC /\ T e. dom adjh ) -> ( adjh ` ( A .op T ) ) = ( ( * ` A ) .op ( adjh ` T ) ) )
Theorem	adjadd 28952	The adjoint of the sum of two operators. Theorem 3.11(iii) of [Beran] p. 106. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.)
|- ( ( S e. dom adjh /\ T e. dom adjh ) -> ( adjh ` ( S +op T ) ) = ( ( adjh ` S ) +op ( adjh ` T ) ) )
Theorem	nmoptrii 28953	Triangle inequality for the norms of bounded linear operators. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
|- S e. BndLinOp   &    |- T e. BndLinOp   =>    |- ( normop ` ( S +op T ) ) <_ ( ( normop ` S ) + ( normop ` T ) )
Theorem	nmopcoi 28954	Upper bound for the norm of the composition of two bounded linear operators. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
|- S e. BndLinOp   &    |- T e. BndLinOp   =>    |- ( normop ` ( S o. T ) ) <_ ( ( normop ` S ) x. ( normop ` T ) )
Theorem	bdophsi 28955	The sum of two bounded linear operators is a bounded linear operator. (Contributed by NM, 9-Mar-2006.) (New usage is discouraged.)
|- S e. BndLinOp   &    |- T e. BndLinOp   =>    |- ( S +op T ) e. BndLinOp
Theorem	bdophdi 28956	The difference between two bounded linear operators is bounded. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
|- S e. BndLinOp   &    |- T e. BndLinOp   =>    |- ( S -op T ) e. BndLinOp
Theorem	bdopcoi 28957	The composition of two bounded linear operators is bounded. (Contributed by NM, 9-Mar-2006.) (New usage is discouraged.)
|- S e. BndLinOp   &    |- T e. BndLinOp   =>    |- ( S o. T ) e. BndLinOp
Theorem	nmoptri2i 28958	Triangle-type inequality for the norms of bounded linear operators. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
|- S e. BndLinOp   &    |- T e. BndLinOp   =>    |- ( ( normop ` S ) - ( normop ` T ) ) <_ ( normop ` ( S +op T ) )
Theorem	adjcoi 28959	The adjoint of a composition of bounded linear operators. Theorem 3.11(viii) of [Beran] p. 106. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
|- S e. BndLinOp   &    |- T e. BndLinOp   =>    |- ( adjh ` ( S o. T ) ) = ( ( adjh ` T ) o. ( adjh ` S ) )
Theorem	nmopcoadji 28960	The norm of an operator composed with its adjoint. Part of Theorem 3.11(vi) of [Beran] p. 106. (Contributed by NM, 8-Mar-2006.) (New usage is discouraged.)
|- T e. BndLinOp   =>    |- ( normop ` ( ( adjh ` T ) o. T ) ) = ( ( normop ` T ) ^ 2 )
Theorem	nmopcoadj2i 28961	The norm of an operator composed with its adjoint. Part of Theorem 3.11(vi) of [Beran] p. 106. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
|- T e. BndLinOp   =>    |- ( normop ` ( T o. ( adjh ` T ) ) ) = ( ( normop ` T ) ^ 2 )
Theorem	nmopcoadj0i 28962	An operator composed with its adjoint is zero iff the operator is zero. Theorem 3.11(vii) of [Beran] p. 106. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
|- T e. BndLinOp   =>    |- ( ( T o. ( adjh ` T ) ) = 0hop <-> T = 0hop )
19.6.13  Quantum computation error bound theorem
Theorem	unierri 28963	If we approximate a chain of unitary transformations (quantum computer gates) F, G by other unitary transformations S, T, the error increases at most additively. Equation 4.73 of [NielsenChuang] p. 195. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
|- F e. UniOp   &    |- G e. UniOp   &    |- S e. UniOp   &    |- T e. UniOp   =>    |- ( normop ` ( ( F o. G ) -op ( S o. T ) ) ) <_ ( ( normop ` ( F -op S ) ) + ( normop ` ( G -op T ) ) )
19.6.14  Dirac bra-ket notation (cont.)
Theorem	branmfn 28964	The norm of the bra function. (Contributed by NM, 24-May-2006.) (New usage is discouraged.)
|- ( A e. ~H -> ( normfn ` ( bra ` A ) ) = ( normh ` A ) )
Theorem	brabn 28965	The bra of a vector is a bounded functional. (Contributed by NM, 26-May-2006.) (New usage is discouraged.)
|- ( A e. ~H -> ( normfn ` ( bra ` A ) ) e. RR )
Theorem	rnbra 28966	The set of bras equals the set of continuous linear functionals. (Contributed by NM, 26-May-2006.) (New usage is discouraged.)
|- ran bra = ( LinFn i^i ContFn )
Theorem	bra11 28967	The bra function maps vectors one-to-one onto the set of continuous linear functionals. (Contributed by NM, 26-May-2006.) (Proof shortened by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- bra : ~H -1-1-onto-> ( LinFn i^i ContFn )
Theorem	bracnln 28968	A bra is a continuous linear functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
|- ( A e. ~H -> ( bra ` A ) e. ( LinFn i^i ContFn ) )
Theorem	cnvbraval 28969*	Value of the converse of the bra function. Based on the Riesz Lemma riesz4 28923, this very important theorem not only justifies the Dirac bra-ket notation, but allows us to extract a unique vector from any continuous linear functional from which the functional can be recovered; i.e. a single vector can "store" all of the information contained in any entire continuous linear functional (mapping from ~H to CC). (Contributed by NM, 26-May-2006.) (New usage is discouraged.)
|- ( T e. ( LinFn i^i ContFn ) -> ( `' bra ` T ) = ( iota_ y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) ) )
Theorem	cnvbracl 28970	Closure of the converse of the bra function. (Contributed by NM, 26-May-2006.) (New usage is discouraged.)
|- ( T e. ( LinFn i^i ContFn ) -> ( `' bra ` T ) e. ~H )
Theorem	cnvbrabra 28971	The converse bra of the bra of a vector is the vector itself. (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
|- ( A e. ~H -> ( `' bra ` ( bra ` A ) ) = A )
Theorem	bracnvbra 28972	The bra of the converse bra of a continuous linear functional. (Contributed by NM, 31-May-2006.) (New usage is discouraged.)
|- ( T e. ( LinFn i^i ContFn ) -> ( bra ` ( `' bra ` T ) ) = T )
Theorem	bracnlnval 28973*	The vector that a continuous linear functional is the bra of. (Contributed by NM, 26-May-2006.) (New usage is discouraged.)
|- ( T e. ( LinFn i^i ContFn ) -> T = ( bra ` ( iota_ y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) ) ) )
Theorem	cnvbramul 28974	Multiplication property of the converse bra function. (Contributed by NM, 31-May-2006.) (New usage is discouraged.)
|- ( ( A e. CC /\ T e. ( LinFn i^i ContFn ) ) -> ( `' bra ` ( A .fn T ) ) = ( ( * ` A ) .h ( `' bra ` T ) ) )
Theorem	kbass1 28975	Dirac bra-ket associative law ( | A >. <. B | ) | C >. = | A >. ( <. B | C >. ) i.e. the juxtaposition of an outer product with a ket equals a bra juxtaposed with an inner product. Since <. B | C >. is a complex number, it is the first argument in the inner product .h that it is mapped to, although in Dirac notation it is placed after the ket. (Contributed by NM, 15-May-2006.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A ketbra B ) ` C ) = ( ( ( bra ` B ) ` C ) .h A ) )
Theorem	kbass2 28976	Dirac bra-ket associative law ( <. A | B >. ) <. C | = <. A | ( | B >. <. C | ) i.e. the juxtaposition of an inner product with a bra equals a ket juxtaposed with an outer product. (Contributed by NM, 23-May-2006.) (New usage is discouraged.)
|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( ( bra ` A ) ` B ) .fn ( bra ` C ) ) = ( ( bra ` A ) o. ( B ketbra C ) ) )
Theorem	kbass3 28977	Dirac bra-ket associative law <. A | B >. <. C | D >. = ( <. A | B >. <. C | ) | D >.. (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( ( bra ` A ) ` B ) x. ( ( bra ` C ) ` D ) ) = ( ( ( ( bra ` A ) ` B ) .fn ( bra ` C ) ) ` D ) )
Theorem	kbass4 28978	Dirac bra-ket associative law <. A | B >. <. C | D >. = <. A | ( | B >. <. C | D >. ). (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( ( bra ` A ) ` B ) x. ( ( bra ` C ) ` D ) ) = ( ( bra ` A ) ` ( ( ( bra ` C ) ` D ) .h B ) ) )
Theorem	kbass5 28979	Dirac bra-ket associative law ( | A >. <. B | ) ( | C >. <. D | ) = ( ( | A >. <. B | ) | C >. ) <. D |. (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A ketbra B ) o. ( C ketbra D ) ) = ( ( ( A ketbra B ) ` C ) ketbra D ) )
Theorem	kbass6 28980	Dirac bra-ket associative law ( | A >. <. B | ) ( | C >. <. D | ) = | A >. ( <. B | ( | C >. <. D | ) ). (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A ketbra B ) o. ( C ketbra D ) ) = ( A ketbra ( `' bra ` ( ( bra ` B ) o. ( C ketbra D ) ) ) ) )
19.6.15  Positive operators (cont.)
Theorem	leopg 28981*	Ordering relation for positive operators. Definition of positive operator ordering in [Kreyszig] p. 470. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
|- ( ( T e. A /\ U e. B ) -> ( T <_op U <-> ( ( U -op T ) e. HrmOp /\ A. x e. ~H 0 <_ ( ( ( U -op T ) ` x ) .ih x ) ) ) )
Theorem	leop 28982*	Ordering relation for operators. Definition of positive operator ordering in [Kreyszig] p. 470. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
|- ( ( T e. HrmOp /\ U e. HrmOp ) -> ( T <_op U <-> A. x e. ~H 0 <_ ( ( ( U -op T ) ` x ) .ih x ) ) )
Theorem	leop2 28983*	Ordering relation for operators. Definition of operator ordering in [Young] p. 141. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
|- ( ( T e. HrmOp /\ U e. HrmOp ) -> ( T <_op U <-> A. x e. ~H ( ( T ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) ) )
Theorem	leop3 28984	Operator ordering in terms of a positive operator. Definition of operator ordering in [Retherford] p. 49. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
|- ( ( T e. HrmOp /\ U e. HrmOp ) -> ( T <_op U <-> 0hop <_op ( U -op T ) ) )
Theorem	leoppos 28985*	Binary relation defining a positive operator. Definition VI.1 of [Retherford] p. 49. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.)
|- ( T e. HrmOp -> ( 0hop <_op T <-> A. x e. ~H 0 <_ ( ( T ` x ) .ih x ) ) )
Theorem	leoprf2 28986	The ordering relation for operators is reflexive. (Contributed by NM, 24-Jul-2006.) (New usage is discouraged.)
|- ( T : ~H --> ~H -> T <_op T )
Theorem	leoprf 28987	The ordering relation for operators is reflexive. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
|- ( T e. HrmOp -> T <_op T )
Theorem	leopsq 28988	The square of a Hermitian operator is positive. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.)
|- ( T e. HrmOp -> 0hop <_op ( T o. T ) )
Theorem	0leop 28989	The zero operator is a positive operator. (The literature calls it "positive," even though in some sense it is really "nonnegative.") Part of Example 12.2(i) in [Young] p. 142. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
|- 0hop <_op 0hop
Theorem	idleop 28990	The identity operator is a positive operator. Part of Example 12.2(i) in [Young] p. 142. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
|- 0hop <_op Iop
Theorem	leopadd 28991	The sum of two positive operators is positive. Exercise 1(i) of [Retherford] p. 49. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.)
|- ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ ( 0hop <_op T /\ 0hop <_op U ) ) -> 0hop <_op ( T +op U ) )
Theorem	leopmuli 28992	The scalar product of a nonnegative real and a positive operator is a positive operator. Exercise 1(ii) of [Retherford] p. 49. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.)
|- ( ( ( A e. RR /\ T e. HrmOp ) /\ ( 0 <_ A /\ 0hop <_op T ) ) -> 0hop <_op ( A .op T ) )
Theorem	leopmul 28993	The scalar product of a positive real and a positive operator is a positive operator. Exercise 1(ii) of [Retherford] p. 49. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.)
|- ( ( A e. RR /\ T e. HrmOp /\ 0 < A ) -> ( 0hop <_op T <-> 0hop <_op ( A .op T ) ) )
Theorem	leopmul2i 28994	Scalar product applied to operator ordering. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)
|- ( ( ( A e. RR /\ T e. HrmOp /\ U e. HrmOp ) /\ ( 0 <_ A /\ T <_op U ) ) -> ( A .op T ) <_op ( A .op U ) )
Theorem	leoptri 28995	The positive operator ordering relation satisfies trichotomy. Exercise 1(iii) of [Retherford] p. 49. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.)
|- ( ( T e. HrmOp /\ U e. HrmOp ) -> ( ( T <_op U /\ U <_op T ) <-> T = U ) )
Theorem	leoptr 28996	The positive operator ordering relation is transitive. Exercise 1(iv) of [Retherford] p. 49. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.)
|- ( ( ( S e. HrmOp /\ T e. HrmOp /\ U e. HrmOp ) /\ ( S <_op T /\ T <_op U ) ) -> S <_op U )
Theorem	leopnmid 28997	A bounded Hermitian operator is less than or equal to its norm times the identity operator. (Contributed by NM, 11-Aug-2006.) (New usage is discouraged.)
|- ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) -> T <_op ( ( normop ` T ) .op Iop ) )
Theorem	nmopleid 28998	A nonzero, bounded Hermitian operator divided by its norm is less than or equal to the identity operator. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)
|- ( ( T e. HrmOp /\ ( normop ` T ) e. RR /\ T =/= 0hop ) -> ( ( 1 / ( normop ` T ) ) .op T ) <_op Iop )
Theorem	opsqrlem1 28999*	Lemma for opsqri . (Contributed by NM, 9-Aug-2006.) (New usage is discouraged.)
|- T e. HrmOp   &    |- ( normop ` T ) e. RR   &    |- 0hop <_op T   &    |- R = ( ( 1 / ( normop ` T ) ) .op T )   &    |- ( T =/= 0hop -> E. u e. HrmOp ( 0hop <_op u /\ ( u o. u ) = R ) )   =>    |- ( T =/= 0hop -> E. v e. HrmOp ( 0hop <_op v /\ ( v o. v ) = T ) )
Theorem	opsqrlem2 29000*	Lemma for opsqri . F ` N is the recursive function An (starting at n=1 instead of 0) of Theorem 9.4-2 of [Kreyszig] p. 476. (Contributed by NM, 17-Aug-2006.) (New usage is discouraged.)
|- T e. HrmOp   &    |- S = ( x e. HrmOp , y e. HrmOp |-> ( x +op ( ( 1 / 2 ) .op ( T -op ( x o. x ) ) ) ) )   &    |- F = seq 1 ( S , ( NN X. { 0hop } ) )   =>    |- ( F ` 1 ) = 0hop