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-10688

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

Type	Label	Description
Statement
Theorem	hhnmo 9801	The norm of an operator in Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- N = (UnormOpU)   =>   |- normop = N
Theorem	hhblo 9802	A bounded linear operator in Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- B = (U BLnOp U)   =>   |- BndLinOp = B
Theorem	hh0o 9803	The zero operator in Hilbert space.
|- U = <.<. +h , .h >., normh>.   &   |- Z = (U 0op U)   =>   |- 0hop = Z
Theorem	dmadjrnb 9804	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 3746.)
|- (T e. dom adjh <-> (adjh` T) e. dom adjh)
Theorem	nmoplbt 9805	A lower bound for an operator norm.
|- ((T:H~-->H~ /\ A e. H~ /\ (normh` A) <_ 1) -> (normh` (T` A)) <_ (normop` T))
Theorem	nmopubt 9806	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 9807	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 9808	The norm of any Hilbert space operator is nonnegative.
|- (T:H~-->H~ -> 0 <_ (normop` T))
Theorem	nmopgt0t 9809	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 9810	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 9811	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 9812	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 9813	A unitary operator in Hilbert space is one-to-one and onto.
|- (T e. UniOp -> T:H~-1-1-onto->H~)
Theorem	unopnormt 9814	A unitary operator is idempotent in the norm.
|- ((T e. UniOp /\ A e. H~) -> (normh` (T` A)) = (normh` A))
Theorem	cnvunopt 9815	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 9816	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 9817	A unitary operator is linear. Theorem in [AkhiezerGlazman] p. 72.
|- (T e. UniOp -> T e. LinOp)
Theorem	counopt 9818	The composition of two unitary operators is unitary.
|- ((S e. UniOp /\ T e. UniOp) -> (S o. T) e. UniOp)
Theorem	hmopt 9819	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 9820	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 9821	A lower bound for a functional norm.
|- ((T:H~-->CC /\ A e. H~ /\ (normh` A) <_ 1) -> (abs` (T` A)) <_ (normfn` T))
Theorem	nmfnleubt 9822	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 9823	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 9824	The norm of any Hilbert space functional is nonnegative.
|- (T:H~-->CC -> 0 <_ (normfn` T))
Theorem	elnlfnt 9825	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 9826	Membership in the null space of a Hilbert space functional.
|- ((T:H~-->CC /\ A e. (null` T)) -> (T` A) = 0)
Theorem	cnfnct 9827	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	lnfnlt 9828	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	adjclt 9829	Closure of the adjoint of a Hilbert space operator.
|- ((T e. dom adjh /\ A e. H~) -> ((adjh` T)` A) e. H~)
Theorem	adjt 9830	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	adj2t 9831	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	adjeqt 9832	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	adjadjt 9833	Double adjoint. Theorem 3.11(iv) of [Beran] p. 106.
|- (T e. dom adjh -> (adjh` (adjh` T)) = T)
Theorem	adjvalvalt 9834	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	unopadj2t 9835	The adjoint of a unitary operator is its inverse (converse). Equation 2 of [AkhiezerGlazman] p. 72.
|- (T e. UniOp -> (adjh` T) = `'T)
Theorem	hmopadjt 9836	A Hermitian operator is self-adjoint.
|- (T e. HrmOp -> (adjh` T) = T)
Theorem	hmdmadjt 9837	Every Hermitian operator has an adjoint.
|- (T e. HrmOp -> T e. dom adjh)
Theorem	hmopadj2t 9838	An operator is Hermitian iff it is self-adjoint. Definition of Hermitian in [Halmos] p. 41.
|- (T e. dom adjh -> (T e. HrmOp <-> (adjh` T) = T))
Theorem	hmoplint 9839	A Hermitian operator is linear.
|- (T e. HrmOp -> T e. LinOp)
Theorem	bravalt 9840	The bra of a vector, expressed as <.A | in Dirac notation. See df-bra 9750.
|- (A e. H~ -> (bra` A) = {<.x, y>. | (x e. H~ /\ y = (x .ih A))})
Theorem	bravalvalt 9841	A bra-ket juxtaposition, expressed as <.A | B>. in Dirac notation, equals the inner product of the vectors. Based on definition of bra in [Prugovecki] p. 186.
|- ((A e. H~ /\ B e. H~) -> ((bra` A)` B) = (B .ih A))
Theorem	braaddt 9842	Linearity property of bra for addition.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((bra` A)` (B +h C)) = (((bra` A)` B) + ((bra` A)` C)))
Theorem	bramult 9843	Linearity property of bra for multiplication.
|- ((A e. H~ /\ B e. CC /\ C e. H~) -> ((bra` A)` (B .h C)) = (B x. ((bra` A)` C)))
Theorem	brafnt 9844	The bra function is a functional.
|- (A e. H~ -> (bra` A):H~-->CC)
Theorem	bralnfnt 9845	The Dirac bra function is a linear functional.
|- (A e. H~ -> (bra` A) e. LinFn)
Theorem	braclt 9846	Closure of the bra function.
|- ((A e. H~ /\ B e. H~) -> ((bra` A)` B) e. CC)
Theorem	bra0 9847	The Dirac bra of the zero vector.
|- (bra` 0h) = (H~ X. {0})
Theorem	brafnmult 9848	Anti-linearity property of bra functional for multiplication.
|- ((A e. CC /\ B e. H~) -> (bra` (A .h B)) = ((*` A) .fn (bra` B)))
Theorem	kbvalt 9849	The outer product of two vectors, expressed as | A>. <.B | in Dirac notation. See df-kb 9751.
|- ((A e. H~ /\ B e. H~) -> (A ketbra B) = {<.x, y>. | (x e. H~ /\ y = ((x .ih B) .h A))})
Theorem	kbopt 9850	The outer product of two vectors, expressed as | A>. <.B | in Dirac notation, is an operator.
|- ((A e. H~ /\ B e. H~) -> (A ketbra B):H~-->H~)
Theorem	kbvalvalt 9851	The value of the operator resulting from the outer product | A>. <.B | of two vectors. Equation 8.1 of [Prugovecki] p. 376.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((A ketbra B)` C) = ((C .ih B) .h A))
Theorem	kbmult 9852	Multiplication property of outer product.
|- ((A e. CC /\ B e. H~ /\ C e. H~