mmtheorems99 - 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-10781

Statement List for Metamath Proof Explorer - 9801-9900 - Page 99 of 108

Type	Label	Description
Statement
Theorem	hmopft 9801	A Hermitian operator is a Hilbert space operator (mapping).
|- (T e. HrmOp -> T:H~-->H~)
Theorem	hmopex 9802	The class of Hermitian operators is a set.
|- HrmOp e. V
Theorem	nmfnvalt 9803	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	nmfnsetret 9804	The set in the supremum of the functional norm definition df-nmfn 9771 is a set of reals.
|- (T:H~-->CC -> {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (abs` (T` y)))} (_ RR)
Theorem	nmfnsetn0 9805	The set in the supremum of the functional norm definition df-nmfn 9771 is nonempty.
|- (abs` (T` 0h)) e. {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (abs` (T` y)))}
Theorem	nmfnxrt 9806	The norm of any Hilbert space functional is an extended real.
|- (T:H~-->CC -> (normfn` T) e. RR*)
Theorem	nmfnrepnf 9807	The norm of a Hilbert space functional is either real or plus infinity.
|- (T:H~-->CC -> ((normfn` T) e. RR <-> (normfn` T) =/= +oo))
Theorem	nlfnvalt 9808	Value of the null space of a Hilbert space functional.
|- (T:H~-->CC -> (null` T) = {x e. H~ | (T` x) = 0})
Theorem	elcnfnt 9809	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	ellnfnt 9810	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	lnfnft 9811	A linear Hilbert space functional is a functional.
|- (T e. LinFn -> T:H~-->CC)
Theorem	dfadj2 9812	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 9813	Functionality of the adjoint function.
|- Fun adjh
Theorem	adjvalt 9814	Value of the adjoint function. By adjmo 9758 and euuni 2881, 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	adjval2t 9815	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 9816	The adjoint function equals its converse.
|- `'adjh = adjh
Theorem	funcnvadj 9817	The converse of the adjoint function is a function.
|- Fun `'adjh
Theorem	adj1o 9818	The adjoint function maps one-to-one onto its domain.
|- adjh:dom adjh-1-1-onto->dom adjh
Theorem	dmadjss 9819	The domain of the adjoint function is a subset of the maps from H~ to H~.
|- dom adjh (_ (H~ ^m H~)
Theorem	dmadjopt 9820	A member of the domain of the adjoint function is a Hilbert space operator.
|- (T e. dom adjh -> T:H~-->H~)
Theorem	dmadjrnt 9821	The adjoint of an operator belongs to the adjoint function's domain.
|- (T e. dom adjh -> (adjh` T) e. dom adjh)
Theorem	eigvecvalt 9822	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	eigvalvalt 9823	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	specvalt 9824	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	specclt 9825	The spectrum of an operator is a set of complex numbers.
|- (T:H~-->H~ -> (Lambda` T) (_ CC)
Theorem	hhlno 9826	The linear operators of Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- L = (U LnOp U)   =>   |- LinOp = L
Theorem	hhnmo 9827	The norm of an operator in Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- N = (UnormOpU)   =>   |- normop = N
Theorem	hhblo 9828	A bounded linear operator in Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- B = (U BLnOp U)   =>   |- BndLinOp = B
Theorem	hh0o 9829	The zero operator in Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- Z = (U 0op U)   =>   |- 0hop = Z
Theorem	dmadjrnb 9830	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 3745.)
|- (T e. dom adjh <-> (adjh` T) e. dom adjh)
Theorem	nmoplbt 9831	A lower bound for an operator norm.
|- ((T:H~-->H~ /\ A e. H~ /\ (normh` A) <_ 1) -> (normh` (T` A)) <_ (normop` T))
Theorem	nmopubt 9832	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 9833	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 9834	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	nmopge0t 9835	The norm of any Hilbert space operator is nonnegative.
|- (T:H~-->H~ -> 0 <_ (normop` T))
Theorem	nmopgt0t 9836	A linear Hilbert space operator that is not identically zero has a positive norm.
|- (T:H~-->H~ -> ((normop` T) =/= 0 <-> 0 < (normop` T)))
Theorem	cnopct 9837	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	lnoplt 9838	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	unopt 9839	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	unopf1ot 9840	A unitary operator in Hilbert space is one-to-one and onto.
|- (T e. UniOp -> T:H~-1-1-onto->H~)
Theorem	unopnormt 9841	A unitary operator is idempotent in the norm.
|- ((T e. UniOp /\ A e. H~) -> (normh` (T` A)) = (normh` A))
Theorem	cnvunopt 9842	The inverse (converse) of a unitary operator in Hilbert space is unitary. Theorem in [AkhiezerGlazman] p. 72.
|- (T e. UniOp -> `'T e. UniOp)
Theorem	unopadjt 9843	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	unoplint 9844	A unitary operator is linear. Theorem in [AkhiezerGlazman] p. 72.
|- (T e. UniOp -> T e. LinOp)
Theorem	counopt 9845	The composition of two unitary operators is unitary.
|- ((S e. UniOp /\ T e. UniOp) -> (S o. T) e. UniOp)
Theorem	hmopt 9846	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	hmopret 9847	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	nmfnlbt 9848	A lower bound for a functional norm.
|- ((T:H~-->CC /\ A e. H~ /\ (normh` A) <_ 1) -> (abs` (T` A)) <_ (normfn` T))
Theorem	nmfnleubt 9849	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	nmfnleub2t 9850	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	nmfnge0t 9851	The norm of any Hilbert space functional is nonnegative.
|- (T:H~-->CC -> 0 <_ (normfn` T))
Theorem	elnlfnt 9852	Membership in the null space of a Hilbert space functional.
|- ((T:H~-->CC /\ A e. H~) -> (A e. (null` T) <-> (T` A) = 0))
Theorem	elnlfn2t 9853	Membership in the null space of a Hilbert space functional.
|-