mmtheorems115 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17411

Statement List for Metamath Proof Explorer - 11401-11500 - Page 115 of 175

Type	Label	Description
Statement
Theorem	eigorth 11401	A necessary and sufficient condition (that holds when T is a Hermitian operator) for two eigenvectors A and B to be orthogonal. Generalization of Equation 1.31 of [Hughes] p. 49.
|- ((((A e. ~H /\ B e. ~H) /\ (C e. CC /\ D e. CC)) /\ (((T` A) = (C .h A) /\ (T` B) = (D .h B)) /\ C =/= (*` D))) -> ((A .ih (T` B)) = ((T` A) .ih B) <-> (A .ih B) = 0))
Linear, continuous, bounded, Hermitian, unitary operators and norms
Definition	df-nmop 11402	Define the norm of a Hilbert space operator.
|- normop = {<.t, y>. | (t:~H-->~H /\ y = sup({x | E.z e. ~H ((normh` z) <_ 1 /\ x = (normh` (t` z)))}, RR*, < ))}
Definition	df-cnop 11403	Define the set of continuous operators on Hilbert space. For every "epsilon" (y) there is an "delta" (z) such that...
|- ConOp = {t | (t:~H-->~H /\ A.x e. ~H A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. ~H ((normh` (w -h x)) < z -> (normh` ((t` w) -h (t` x))) < y))))}
Definition	df-lnop 11404	Define the set of linear operators on Hilbert space. (See df-hosum 11139 for definition of operator.)
|- LinOp = {t | (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)))}
Definition	df-bdop 11405	Define the set of bounded linear Hilbert space operators. (See df-hosum 11139 for definition of operator.)
|- BndLinOp = (LinOp i^i {t | (t:~H-->~H /\ (normop` t) < +oo)})
Definition	df-unop 11406	Define the set of unitary operators on Hilbert space.
|- 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 11407	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.
|- HrmOp = {t | (t:~H-->~H /\ A.x e. ~H A.y e. ~H (x .ih (t` y)) = ((t` x) .ih y))}
Linear and continuous functionals and norms
Definition	df-nmfn 11408	Define the norm of a Hilbert space functional.
|- normfn = {<.t, y>. | (t:~H-->CC /\ y = sup({x | E.z e. ~H ((normh` z) <_ 1 /\ x = (abs` (t` z)))}, RR*, < ))}
Definition	df-nlfn 11409	Define the null space of a Hilbert space functional.
|- null = {<.t, y>. | (t:~H-->CC /\ y = {x e. ~H | (t` x) = 0})}
Definition	df-cnfn 11410	Define the set of continuous functionals on Hilbert space. For every "epsilon" (y) there is an "delta" (z) such that...
|- ConFn = {t | (t:~H-->CC /\ A.x e. ~H A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. ~H ((normh` (w -h x)) < z -> (abs` ((t` w) - (t` x))) < y))))}
Definition	df-lnfn 11411	Define the set of linear functionals on Hilbert space.
|- LinFn = {t | (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)))}
Adjoint
Definition	df-adjh 11412	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 11653) that the adjoint exists for a bounded linear operator.
|- 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)))}
Dirac bra-ket notation
Definition	df-bra 11413	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 bravalval 11505. The reversal of the inner product arguments not only makes the bra-ket behavior consistent with physics literature (see comments under ax-his3 10584) but is also required in order for the associative law kbass2 11688 to work. Our definition of bra and the associated outer product df-kb 11414 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 http://us.metamath.org/mpegif/mmnotes.txt, under the 17-May-2006 entry.
|- bra = {<.x, t>. | (x e. ~H /\ t = {<.y, z>. | (y e. ~H /\ z = (y .ih x))})}
Definition	df-kb 11414	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 11413, 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.
|- ketbra = {<.<.x, y>., t>. | ((x e. ~H /\ y e. ~H) /\ t = {<.w, v>. | (w e. ~H /\ v = ((w .ih y) .h x))})}
Positive operators
Definition	df-leop 11415	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.
|- <_op = {<.t, u>. | ((u -op t) e. HrmOp /\ A.x e. ~H 0 <_ (((u -op t)` x) .ih x))}
Eigenvectors, eigenvalues, spectrum
Definition	df-eigvec 11416	Define the eigenvector function. Theorem eleigveccl 11520 shows that eigvec` T, the set of eigenvectors of Hilbert space operator T, are Hilbert space vectors.
|- eigvec = {<.t, y>. | (t:~H-->~H /\ y = {x e. ~H | (x =/= 0h /\ E.z e. CC (t` x) = (z .h x))})}
Definition	df-eigval 11417	Define the eigenvalue function. The range of eigval` T is the set of eigenvalues of Hilbert space operator T. Theorem eigvalcl 11522 shows that (eigval` T)` A, the eigenvalue associated with eigenvector A, is a complex number.
|- eigval = {<.t, y>. | (t:~H-->~H /\ y = {<.x, z>. | (x e. (eigvec` t) /\ z = (((t` x) .ih x) / ((normh` x)^2)))})}
Definition	df-spec 11418	Define the spectrum of an operator. Definition of spectrum in [Halmos] p. 50.
|- Lambda = {<.t, y>. | (t:~H-->~H /\ y = {x e. CC | -. (t -op (x .op ( _I |` ~H))):~H-1-1->~H})}
Theorems about operators and functionals
Theorem	nmopval 11419	Value of the norm of a Hilbert space operator.
|- (T:~H-->~H -> (normop` T) = sup({x | E.y e. ~H ((normh` y) <_ 1 /\ x = (normh` (T` y)))}, RR*, < ))
Theorem	elcnop 11420	Property defining a continuous Hilbert space operator.
|- (T e. ConOp <-> (T:~H-->~H /\ A.x e. ~H A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. ~H ((normh` (w -h x)) < z -> (normh` ((T` w) -h (T` x))) < y)))))
Theorem	ellnop 11421	Property defining a linear Hilbert space operator.
|- (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 11422	A linear Hilbert space operator is a Hilbert space operator.
|- (T e. LinOp -> T:~H-->~H)
Theorem	dfbdop2 11423	Alternate definition of the set of bounded linear Hilbert space operators.
|- BndLinOp = {t e. LinOp | (normop` t) < +oo}
Theorem	elbdop 11424	Property defining a bounded linear Hilbert space operator.
|- (T e. BndLinOp <-> (T e. LinOp /\ (normop` T) < +oo))
Theorem	bdopln 11425	A bounded linear Hilbert space operator is a linear operator.
|- (T e. BndLinOp -> T e. LinOp)
Theorem	bdopf 11426	A bounded linear Hilbert space operator is a Hilbert space operator.
|- (T e. BndLinOp -> T:~H-->~H)
Theorem	nmopsetretALT 11427	The set in the supremum of the operator norm definition df-nmop 11402 is a set of reals.
|- (T:~H-->~H -> {x | E.y e. ~H ((normh` y) <_ 1 /\ x = (normh` (T` y)))} C_ RR)
Theorem	nmopsetretHIL 11428	The set in the supremum of the operator norm definition df-nmop 11402 is a set of reals.
|- (T:~H-->~H -> {x | E.y e. ~H ((normh` y) <_ 1 /\ x = (normh` (T` y)))} C_ RR)
Theorem	nmopsetn0 11429	The set in the supremum of the operator norm definition df-nmop 11402 is nonempty.
|- (normh` (T` 0h)) e. {x | E.y e. ~H ((normh` y) <_ 1 /\ x = (normh` (T` y)))}
Theorem	nmopxr 11430	The norm of a Hilbert space operator is an extended real.
|- (T:~H-->~H -> (normop` T) e. RR*)
Theorem	nmoprepnf 11431	The norm of a Hilbert space operator is either real or plus infinity.
|- (T:~H-->~H -> ((normop` T) e. RR <-> (normop` T) =/= +oo))
Theorem	nmopgtmnf 11432	The norm of a Hilbert space operator is not minus infinity.
|- (T:~H-->~H -> -oo < (normop` T))
Theorem	nmopreltpnf 11433	The norm of a Hilbert space operator is real iff it is less than infinity.
|- (T:~H-->~H -> ((normop` T) e. RR <-> (normop` T) < +oo))
Theorem	nmopre 11434	The norm of a bounded operator is a real number.
|- (T e. BndLinOp -> (normop` T) e. RR)
Theorem	elbdop2 11435	Property defining a bounded linear Hilbert space operator.
|- (T e. BndLinOp <-> (T e. LinOp /\ (normop` T) e. RR))
Theorem	elunop 11436	Property defining a unitary Hilbert space operator.
|- (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 11437	Property defining a Hermitian Hilbert space operator.
|- (T e. HrmOp <-> (T:~H-->~H /\ A.x e. ~H A.y e. ~H (x .ih (T` y)) = ((T` x) .ih y)))
Theorem	hmopf 11438	A Hermitian operator is a Hilbert space operator (mapping).
|- (T e. HrmOp -> T:~H-->~H)
Theorem	hmopex 11439	The class of Hermitian operators is a set.
|- HrmOp e. _V
Theorem	nmfnval 11440	Value of the norm of a Hilbert space functional.
|- (T:~H-->CC -> (normfn` T) = sup({x | E.y e. ~H ((normh` y) <_ 1 /\ x = (abs` (T` y)))}, RR*, < ))
Theorem	nmfnsetre 11441	The set in the supremum of the functional norm definition df-nmfn 11408 is a set of reals.
|- (T:~H-->CC -> {x | E.y e. ~H ((normh` y) <_ 1 /\ x = (abs` (T` y)))} C_ RR)
Theorem	nmfnsetn0 11442	The set in the supremum of the functional norm definition df-nmfn 11408 is nonempty.
|- (abs` (T` 0h)) e. {x | E.y e. ~H ((normh` y) <_ 1 /\ x = (abs` (T` y)))}
Theorem	nmfnxr 11443	The norm of any Hilbert space functional is an extended real.
|- (T:~H-->CC -> (normfn` T) e. RR*)
Theorem	nmfnrepnf 11444	The norm of a Hilbert space functional is either real or plus infinity.
|- (T:~H-->CC -> ((normfn` T) e. RR <-> (normfn` T) =/= +oo))
Theorem	nlfnval 11445	Value of the null space of a Hilbert space functional.
|- (T:~H-->CC -> (null` T) = {x e. ~H | (T` x) = 0})
Theorem	elcnfn 11446	Property defining a continuous functional.
|- (T e. ConFn <-> (T:~H-->CC /\ A.x e. ~H A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. ~H ((normh` (w -h x)) < z -> (abs` ((T` w) - (T` x))) < y)))))
Theorem	ellnfn 11447	Property defining a linear functional.
|- (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 11448	A linear Hilbert space functional is a functional.
|- (T e. LinFn -> T:~H-->CC)
Theorem	dfadj2 11449	Alternate definition of the adjoint of a Hilbert space operator.
|- 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 11450	Functionality of the adjoint function.
|- Fun adjh
Theorem	adjval 11451	Value of the adjoint function. By adjmo 11395 and euuni 3807, the union should be read "the unique u such that..." for T in the domain of adjh.
|- (T:~H-->~H -> (adjh` T) = U.{u | (u:~H-->~H /\ A.x e. ~H A.y e. ~H (x .ih (T` y)) = ((u` x) .ih y))})
Theorem	adjval2 11452	Value of the adjoint function.
|- (T:~H-->~H -> (adjh` T) = U.{u | (u:~H-->~H /\ A.x e. ~H A.y e. ~H ((T` x) .ih y) = (x .ih (u` y)))})
Theorem	cnvadj 11453	The adjoint function equals its converse.
|- `'adjh = adjh
Theorem	funcnvadj 11454	The converse of the adjoint function is a function.
|- Fun `'adjh
Theorem	adj1o 11455	The adjoint function maps one-to-one onto its domain.
|- adjh:dom adjh-1-1-onto->dom adjh
Theorem	dmadjss 11456	The domain of the adjoint function is a subset of the maps from ~H to ~H.
|- dom adjh C_ (~H ^m ~H)
Theorem	dmadjop 11457	A member of the domain of the adjoint function is a Hilbert space operator.
|- (T e. dom adjh -> T:~H-->~H)
Theorem	dmadjrn 11458	The adjoint of an operator belongs to the adjoint function's domain.
|- (T e. dom adjh -> (adjh` T) e. dom adjh)
Theorem	eigvecval 11459	The set of eigenvectors of a Hilbert space operator.
|- (T:~H-->~H -> (eigvec` T) = {x e. ~H | (x =/= 0h /\ E.y e. CC (T` x) = (y .h x))})
Theorem	eigvalval 11460	The eigenvalues of eigenvectors of a Hilbert space operator.
|- (T:~H-->~H -> (eigval` T) = {<.x, y>. | (x e. (eigvec` T) /\ y = (((T` x) .ih x) / ((normh` x)^2)))})
Theorem	specval 11461	The value of the spectrum of an operator.
|- (T:~H-->~H -> (Lambda` T) = {x e. CC | -. (T -op (x .op ( _I |` ~H))):~H-1-1->~H})
Theorem	speccl 11462	The spectrum of an operator is a set of complex numbers.
|- (T:~H-->~H -> (Lambda` T) C_ CC)
Theorem	hhlnoi 11463	The linear operators of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- L = (U LnOp U)   =>   |- LinOp = L
Theorem	hhnmoi 11464	The norm of an operator in Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- N = (UnormOpU)   =>   |- normop = N
Theorem	hhbloi 11465	A bounded linear operator in Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- B = (U BLnOp U)   =>   |- BndLinOp = B
Theorem	hh0oi 11466	The zero operator in Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- Z = (U 0op U)   =>   |- 0hop = Z
Theorem	dmadjrnb 11467	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 4702.)
|- (T e. dom adjh <-> (adjh` T) e. dom adjh)
Theorem	nmoplb 11468	A lower bound for an operator norm.
|- ((T:~H-->~H /\ A e. ~H /\ (normh` A) <_ 1) -> (normh` (T` A)) <_ (normop` T))
Theorem	nmopub 11469	An upper bound for an operator norm.
|- ((T:~H-->~H /\ A e. RR* /\ A.x e. ~H ((normh` x) <_ 1 -> (normh` (T` x)) <_ A)) -> (normop` T) <_ A)
Theorem	nmopub2tALT 11470	An upper bound for an operator norm.
|- ((T:~H-->~H /\ (A e. RR /\ 0 <_ A) /\ A.x e. ~H (normh` (T` x)) <_ (A x. (normh` x))) -> (normop` T) <_ A)
Theorem	nmopub2tHIL 11471	An upper bound for an operator norm.
|- ((T:~H-->~H /\ (A e. RR /\ 0 <_ A) /\ A.x e. ~H (normh` (T` x)) <_ (A x. (normh` x))) -> (normop` T) <_ A)
Theorem	nmopge0 11472	The norm of any Hilbert space operator is nonnegative.
|- (T:~H-->~H -> 0 <_ (normop` T))
Theorem	nmopgt0 11473	A linear Hilbert space operator that is not identically zero has a positive norm.
|- (T:~H-->~H -> ((normop` T) =/= 0 <-> 0 < (normop` T)))
Theorem	cnopc 11474	Basic continuity property of a continuous Hilbert space operator.
|- (((T e. ConOp /\ A e. ~H) /\ (B e. RR /\ 0 < B)) -> E.x e. RR (0 < x /\ A.y e. ~H ((normh` (y -h A)) < x -> (normh` ((T` y) -h (T` A))) < B)))
Theorem	lnopl 11475	Basic linearity property of a linear Hilbert space operator.
|- (((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 11476	Basic inner product property of a unitary operator.
|- ((T e. UniOp /\ A e. ~H /\ B e. ~H) -> ((T` A) .ih (T` B)) = (A .ih B))
Theorem	unopf1o 11477	A unitary operator in Hilbert space is one-to-one and onto.
|- (T e. UniOp -> T:~H-1-1-onto->~H)
Theorem	unopnorm 11478	A unitary operator is idempotent in the norm.
|- ((T e. UniOp /\ A e. ~H) -> (normh` (T` A)) = (normh` A))
Theorem	cnvunop 11479	The inverse (converse) of a unitary operator in Hilbert space is unitary. Theorem in [AkhiezerGlazman] p. 72.
|- (T e. UniOp -> `'T e. UniOp)
Theorem	unopadj 11480	The inverse (converse) of a unitary operator is its adjoint. Equation 2 of [AkhiezerGlazman] p. 72.
|- ((T e. UniOp /\ A e. ~H /\ B e. ~H) -> ((T` A) .ih B) = (A .ih (`'T` B)))
Theorem	unoplin 11481	A unitary operator is linear. Theorem in [AkhiezerGlazman] p. 72.
|- (T e. UniOp -> T e. LinOp)
Theorem	counop 11482	The composition of two unitary operators is unitary.
|- ((S e. UniOp /\ T e. UniOp) -> (S o. T) e. UniOp)
Theorem	hmop 11483	Basic inner product property of a Hermitian operator.
|- ((T e. HrmOp /\ A e. ~H /\ B e. ~H) -> (A .ih (T` B)) = ((T` A) .ih B))
Theorem	hmopre 11484	The inner product of the value and argument of a Hermitian operator is real.
|- ((T e. HrmOp /\ A e. ~H) -> ((T` A) .ih A) e. RR)
Theorem	nmfnlb 11485	A lower bound for a functional norm.
|- ((T:~H-->CC /\ A e. ~H /\ (normh` A) <_ 1) -> (abs` (T` A)) <_ (normfn` T))
Theorem	nmfnleub 11486	An upper bound for the norm of a functional.
|- ((T:~H-->CC /\ A e. RR* /\ A.x e. ~H ((normh` x) <_ 1 -> (abs` (T` x)) <_ A)) -> (normfn` T) <_ A)
Theorem	nmfnleub2 11487	An upper bound for the norm of a functional.
|- ((T:~H-->CC /\ (A e. RR /\ 0 <_ A) /\ A.x e. ~H (abs` (T` x)) <_ (A x. (normh` x))) -> (normfn` T) <_ A)
Theorem	nmfnge0 11488	The norm of any Hilbert space functional is nonnegative.
|- (T:~H-->CC -> 0 <_ (normfn` T))
Theorem	elnlfn 11489	Membership in the null space of a Hilbert space functional.
|- ((T:~H-->CC /\ A e. ~H) -> (A e. (null` T) <-> (T` A) = 0))
Theorem	elnlfn2 11490	Membership in the null space of a Hilbert space functional.
|- ((T:~H-->CC /\ A e. (null` T)) -> (T` A) = 0)
Theorem	cnfnc 11491	Basic continuity property of a continuous functional.
|- (((T e. ConFn /\ A e. ~H) /\ (B e. RR /\ 0 < B)) -> E.x e. RR (0 < x /\ A.y e. ~H ((normh` (y -h A)) < x -> (abs` ((T` y) - (T` A))) < B)))
Theorem	lnfnl 11492	Basic linearity property of a linear functional.
|- (((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 11493	Closure of the adjoint of a Hilbert space operator.
|- ((T e. dom adjh /\ A e. ~H) -> ((adjh` T)` A) e. ~H)
Theorem	adj1 11494	Property of an adjoint Hilbert space operator.
|- ((T e. dom adjh /\ A e. ~H /\ B e. ~H) -> (A .ih (T` B)) = (((adjh` T)` A) .ih B))
Theorem	adj2 11495	Property of an adjoint Hilbert space operator.
|- ((T e. dom adjh /\ A e. ~H /\ B e. ~H) -> ((T` A) .ih B) = (A .ih ((adjh` T)` B)))
Theorem	adjeq 11496	A property that determines the adjoint of a Hilbert space operator.
|- ((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 11497	Double adjoint. Theorem 3.11(iv) of [Beran] p. 106.
|- (T e. dom adjh -> (adjh` (adjh` T)) = T)
Theorem	adjvalval 11498	Value of the value of the adjoint function.
|- ((T e. dom adjh /\ A e. ~H) -> ((adjh` T)` A) = U.{w e. ~H | A.x e. ~H ((T` x) .ih A) = (x .ih w)})
Theorem	unopadj2 11499	The adjoint of a unitary operator is its inverse (converse). Equation 2 of [AkhiezerGlazman] p. 72.
|- (T e. UniOp -> (adjh` T) = `'T)
Theorem	hmopadj 11500	A Hermitian operator is self-adjoint.
|- (T e. HrmOp -> (adjh` T) = T)