mmtheorems123 - 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-17500 176 17501-17600 177 17601-17700 178 17701-17800 179 17801-17900 180 17901-18000 181 18001-18100 182 18101-18200 183 18201-18300 184 18301-18400 185 18401-18500 186 18501-18600 187 18601-18700 188 18701-18800 189 18801-18900 190 18901-19000 191 19001-19026

Statement List for Metamath Proof Explorer - 12201-12300 - Page 123 of 191

Type	Label	Description
Statement
Theorem	honegneg 12201	Double negative of a Hilbert space operator.
|- (T:~H-->~H -> (-u1 .op (-u1 .op T)) = T)
Theorem	hosubneg 12202	Relationship between operator subtraction and negative.
|- ((T:~H-->~H /\ U:~H-->~H) -> (T -op (-u1 .op U)) = (T +op U))
Theorem	hosubdi 12203	Scalar product distributive law for operator difference.
|- ((A e. CC /\ T:~H-->~H /\ U:~H-->~H) -> (A .op (T -op U)) = ((A .op T) -op (A .op U)))
Theorem	honegdi 12204	Distribution of negative over addition.
|- ((T:~H-->~H /\ U:~H-->~H) -> (-u1 .op (T +op U)) = ((-u1 .op T) +op (-u1 .op U)))
Theorem	honegsubdi 12205	Distribution of negative over subtraction.
|- ((T:~H-->~H /\ U:~H-->~H) -> (-u1 .op (T -op U)) = ((-u1 .op T) +op U))
Theorem	honegsubdi2 12206	Distribution of negative over subtraction.
|- ((T:~H-->~H /\ U:~H-->~H) -> (-u1 .op (T -op U)) = (U -op T))
Theorem	hosubsub2 12207	Law for double subtraction of Hilbert space operators.
|- ((S:~H-->~H /\ T:~H-->~H /\ U:~H-->~H) -> (S -op (T -op U)) = (S +op (U -op T)))
Theorem	hosub4 12208	Rearrangement of 4 terms in a mixed addition and subtraction of Hilbert space operators.
|- (((R:~H-->~H /\ S:~H-->~H) /\ (T:~H-->~H /\ U:~H-->~H)) -> ((R +op S) -op (T +op U)) = ((R -op T) +op (S -op U)))
Theorem	hosubadd4 12209	Rearrangement of 4 terms in a mixed addition and subtraction of Hilbert space operators.
|- (((R:~H-->~H /\ S:~H-->~H) /\ (T:~H-->~H /\ U:~H-->~H)) -> ((R -op S) -op (T -op U)) = ((R +op U) -op (S +op T)))
Theorem	hoaddsubass 12210	Associative-type law for addition and subtraction of Hilbert space operators.
|- ((S:~H-->~H /\ T:~H-->~H /\ U:~H-->~H) -> ((S +op T) -op U) = (S +op (T -op U)))
Theorem	hoaddsub 12211	Law for operator addition and subtraction of Hilbert space operators.
|- ((S:~H-->~H /\ T:~H-->~H /\ U:~H-->~H) -> ((S +op T) -op U) = ((S -op U) +op T))
Theorem	hosubsub 12212	Law for double subtraction of Hilbert space operators.
|- ((S:~H-->~H /\ T:~H-->~H /\ U:~H-->~H) -> (S -op (T -op U)) = ((S -op T) +op U))
Theorem	hosubsub4 12213	Law for double subtraction of Hilbert space operators.
|- ((S:~H-->~H /\ T:~H-->~H /\ U:~H-->~H) -> ((S -op T) -op U) = (S -op (T +op U)))
Theorem	ho2times 12214	Two times a Hilbert space operator.
|- (T:~H-->~H -> (2 .op T) = (T +op T))
Theorem	hoaddsubassi 12215	Associativity of sum and difference of Hilbert space operators.
|- R:~H-->~H   &   |- S:~H-->~H   &   |- T:~H-->~H   =>   |- ((R +op S) -op T) = (R +op (S -op T))
Theorem	hoaddsubi 12216	Law for sum and difference of Hilbert space operators.
|- R:~H-->~H   &   |- S:~H-->~H   &   |- T:~H-->~H   =>   |- ((R +op S) -op T) = ((R -op T) +op S)
Theorem	hosd1i 12217	Hilbert space operator sum expressed in terms of difference.
|- T:~H-->~H   &   |- U:~H-->~H   =>   |- (T +op U) = (T -op (0hop -op U))
Theorem	hosd2i 12218	Hilbert space operator sum expressed in terms of difference.
|- T:~H-->~H   &   |- U:~H-->~H   =>   |- (T +op U) = (T -op ((U -op U) -op U))
Theorem	hopncani 12219	Hilbert space operator cancellation law.
|- T:~H-->~H   &   |- U:~H-->~H   =>   |- ((T +op U) -op U) = T
Theorem	honpcani 12220	Hilbert space operator cancellation law.
|- T:~H-->~H   &   |- U:~H-->~H   =>   |- ((T -op U) +op U) = T
Theorem	hosubeq0i 12221	If the difference between two operators is zero, they are equal.
|- T:~H-->~H   &   |- U:~H-->~H   =>   |- ((T -op U) = 0hop <-> T = U)
Theorem	honpncani 12222	Hilbert space operator cancellation law.
|- R:~H-->~H   &   |- S:~H-->~H   &   |- T:~H-->~H   =>   |- ((R -op S) +op (S -op T)) = (R -op T)
Theorem	ho01i 12223	A condition implying that a Hilbert space operator is identically zero. Lemma 3.2(S8) of [Beran] p. 95.
|- T:~H-->~H   =>   |- (A.x e. ~H A.y e. ~H ((T` x) .ih y) = 0 <-> T = 0hop)
Theorem	ho02i 12224	A condition implying that a Hilbert space operator is identically zero. Lemma 3.2(S10) of [Beran] p. 95.
|- T:~H-->~H   =>   |- (A.x e. ~H A.y e. ~H (x .ih (T` y)) = 0 <-> T = 0hop)
Theorem	hoeq1 12225	A condition implying that two Hilbert space operators are equal. Lemma 3.2(S9) of [Beran] p. 95.
|- ((S:~H-->~H /\ T:~H-->~H) -> (A.x e. ~H A.y e. ~H ((S` x) .ih y) = ((T` x) .ih y) <-> S = T))
Theorem	hoeq2 12226	A condition implying that two Hilbert space operators are equal. Lemma 3.2(S11) of [Beran] p. 95.
|- ((S:~H-->~H /\ T:~H-->~H) -> (A.x e. ~H A.y e. ~H (x .ih (S` y)) = (x .ih (T` y)) <-> S = T))
Theorem	adjmo 12227	Every Hilbert space operator has at most one adjoint.
|- E*u(u:~H-->~H /\ A.x e. ~H A.y e. ~H (x .ih (T` y)) = ((u` x) .ih y))
Theorem	adjsym 12228	Symmetry property of an adjoint.
|- ((S:~H-->~H /\ T:~H-->~H) -> (A.x e. ~H A.y e. ~H (x .ih (S` y)) = ((T` x) .ih y) <-> A.x e. ~H A.y e. ~H (x .ih (T` y)) = ((S` x) .ih y)))
Theorem	eigrei 12229	A necessary and sufficient condition (that holds when T is a Hermitian operator) for an eigenvalue B to be real. Generalization of Equation 1.30 of [Hughes] p. 49.
|- A e. ~H   &   |- B e. CC   =>   |- (((T` A) = (B .h A) /\ A =/= 0h) -> ((A .ih (T` A)) = ((T` A) .ih A) <-> B e. RR))
Theorem	eigre 12230	A necessary and sufficient condition (that holds when T is a Hermitian operator) for an eigenvalue B to be real. Generalization of Equation 1.30 of [Hughes] p. 49.
|- (((A e. ~H /\ B e. CC) /\ ((T` A) = (B .h A) /\ A =/= 0h)) -> ((A .ih (T` A)) = ((T` A) .ih A) <-> B e. RR))
Theorem	eigposi 12231	A sufficient condition (first conjunct pair, that holds when T is a positive operator) for an eigenvalue B (second conjunct pair) to be nonnegative. Remark (ii) in [Hughes] p. 137.
|- A e. ~H   &   |- B e. CC   =>   |- ((((A .ih (T` A)) e. RR /\ 0 <_ (A .ih (T` A))) /\ ((T` A) = (B .h A) /\ A =/= 0h)) -> (B e. RR /\ 0 <_ B))
Theorem	eigorthi 12232	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))
Theorem	eigorth 12233	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 12234	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 12235	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 12236	Define the set of linear operators on Hilbert space. (See df-hosum 11973 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 12237	Define the set of bounded linear Hilbert space operators. (See df-hosum 11973 for definition of operator.)
|- BndLinOp = (LinOp i^i {t | (t:~H-->~H /\ (normop` t) < +oo)})
Definition	df-unop 12238	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 12239	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 12240	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 12241	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 12242	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 12243	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 12244	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 12485) 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 12245	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 12337. The reversal of the inner product arguments not only makes the bra-ket behavior consistent with physics literature (see comments under ax-his3 11421) but is also required in order for the associative law kbass2 12519 to work. Our definition of bra and the associated outer product df-kb 12246 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 12246	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 12245, 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 12247	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 12248	Define the eigenvector function. Theorem eleigveccl 12352 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 12249	Define the eigenvalue function. The range of eigval` T is the set of eigenvalues of Hilbert space operator T. Theorem eigvalcl 12354 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 12250	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 12251	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 12252	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 12253	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 12254	A linear Hilbert space operator is a Hilbert space operator.
|- (T e. LinOp -> T:~H-->~H)
Theorem	dfbdop2 12255	Alternate definition of the set of bounded linear Hilbert space operators.
|- BndLinOp = {t e. LinOp | (normop` t) < +oo}
Theorem	elbdop 12256	Property defining a bounded linear Hilbert space operator.
|- (T e. BndLinOp <-> (T e. LinOp /\ (normop` T) < +oo))
Theorem	bdopln 12257	A bounded linear Hilbert space operator is a linear operator.
|- (T e. BndLinOp -> T e. LinOp)
Theorem	bdopf 12258	A bounded linear Hilbert space operator is a Hilbert space operator.
|- (T e. BndLinOp -> T:~H-->~H)
Theorem	nmopsetretALT 12259	The set in the supremum of the operator norm definition df-nmop 12234 is a set of reals.
|- (T:~H-->~H -> {x | E.y e. ~H ((normh` y) <_ 1 /\ x = (normh` (T` y)))} C_ RR)
Theorem	nmopsetretHIL 12260	The set in the supremum of the operator norm definition df-nmop 12234 is a set of reals.
|- (T:~H-->~H -> {x | E.y e. ~H ((normh` y) <_ 1 /\ x = (normh` (T` y)))} C_ RR)
Theorem	nmopsetn0 12261	The set in the supremum of the operator norm definition df-nmop 12234 is nonempty.
|- (normh` (T` 0h)) e. {x | E.y e. ~H ((normh` y) <_ 1 /\ x = (normh` (T` y)))}
Theorem	nmopxr 12262	The norm of a Hilbert space operator is an extended real.
|- (T:~H-->~H -> (normop` T) e. RR*)
Theorem	nmoprepnf 12263	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 12264	The norm of a Hilbert space operator is not minus infinity.
|- (T:~H-->~H -> -oo < (normop` T))
Theorem	nmopreltpnf 12265	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 12266	The norm of a bounded operator is a real number.
|- (T e. BndLinOp -> (normop` T) e. RR)
Theorem	elbdop2 12267	Property defining a bounded linear Hilbert space operator.
|- (T e. BndLinOp <-> (T e. LinOp /\ (normop` T) e. RR))
Theorem	elunop 12268	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 12269	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 12270	A Hermitian operator is a Hilbert space operator (mapping).
|- (T e. HrmOp -> T:~H-->~H)
Theorem	hmopex 12271	The class of Hermitian operators is a set.
|- HrmOp e. _V
Theorem	nmfnval 12272	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 12273	The set in the supremum of the functional norm definition df-nmfn 12240 is a set of reals.
|- (T:~H-->CC -> {x | E.y e. ~H ((normh` y) <_ 1 /\ x = (abs` (T` y)))} C_ RR)
Theorem	nmfnsetn0 12274	The set in the supremum of the functional norm definition df-nmfn 12240 is nonempty.
|- (abs` (T` 0h)) e. {x | E.y e. ~H ((normh` y) <_ 1 /\ x = (abs` (T` y)))}
Theorem	nmfnxr 12275	The norm of any Hilbert space functional is an extended real.
|- (T:~H-->CC -> (normfn` T) e. RR*)
Theorem	nmfnrepnf 12276	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 12277	Value of the null space of a Hilbert space functional.
|- (T:~H-->CC -> (null` T) = {x e. ~H | (T` x) = 0})
Theorem	elcnfn 12278	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 12279	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 12280	A linear Hilbert space functional is a functional.
|- (T e. LinFn -> T:~H-->CC)
Theorem	dfadj2 12281	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 12282	Functionality of the adjoint function.
|- Fun adjh
Theorem	adjval 12283	Value of the adjoint function. By adjmo 12227 and euuni 3945, 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 12284	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 12285	The adjoint function equals its converse.
|- `'adjh = adjh
Theorem	funcnvadj 12286	The converse of the adjoint function is a function.
|- Fun `'adjh
Theorem	adj1o 12287	The adjoint function maps one-to-one onto its domain.
|- adjh:dom adjh-1-1-onto->dom adjh
Theorem	dmadjss 12288	The domain of the adjoint function is a subset of the maps from ~H to ~H.
|- dom adjh C_ (~H ^m ~H)
Theorem	dmadjop 12289	A member of the domain of the adjoint function is a Hilbert space operator.
|- (T e. dom adjh -> T:~H-->~H)
Theorem	dmadjrn 12290	The adjoint of an operator belongs to the adjoint function's domain.
|- (T e. dom adjh -> (adjh` T) e. dom adjh)
Theorem	eigvecval 12291	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 12292	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 12293	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 12294	The spectrum of an operator is a set of complex numbers.
|- (T:~H-->~H -> (Lambda` T) C_ CC)
Theorem	hhlnoi 12295	The linear operators of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- L = (U LnOp U)   =>   |- LinOp = L
Theorem	hhnmoi 12296	The norm of an operator in Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- N = (UnormOpU)   =>   |- normop = N
Theorem	hhbloi 12297	A bounded linear operator in Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- B = (U BLnOp U)   =>   |- BndLinOp = B
Theorem	hh0oi 12298	The zero operator in Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- Z = (U 0op U)   =>   |- 0hop = Z
Theorem	dmadjrnb 12299	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 4788.)
|- (T e. dom adjh <-> (adjh` T) e. dom adjh)
Theorem	nmoplb 12300	A lower bound for an operator norm.
|- ((T:~H-->~H /\ A e. ~H /\ (normh` A) <_ 1) -> (normh` (T` A)) <_ (normop` T))