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

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

Type	Label	Description
Statement
Theorem	counopt 9801	The composition of two unitary operators is unitary.
|- ((S e. UniOp /\ T e. UniOp) -> (S o. T) e. UniOp)
Theorem	hmopt 9802	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 9803	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 9804	A lower bound for a functional norm.
|- ((T:H~-->CC /\ A e. H~ /\ (normh` A) <_ 1) -> (abs` (T` A)) <_ (normfn` T))
Theorem	nmfnleubt 9805	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 9806	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 9807	The norm of any Hilbert space functional is nonnegative.
|- (T:H~-->CC -> 0 <_ (normfn` T))
Theorem	elnlfnt 9808	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 9809	Membership in the null space of a Hilbert space functional.
|- ((T:H~-->CC /\ A e. (null` T)) -> (T` A) = 0)
Theorem	cnfnct 9810	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 9811	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 9812	Closure of the adjoint of a Hilbert space operator.
|- ((T e. dom adjh /\ A e. H~) -> ((adjh` T)` A) e. H~)
Theorem	adjt 9813	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 9814	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 9815	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 9816	Double adjoint. Theorem 3.11(iv) of [Beran] p. 106.
|- (T e. dom adjh -> (adjh` (adjh` T)) = T)
Theorem	adjvalvalt 9817	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 9818	The adjoint of a unitary operator is its inverse (converse). Equation 2 of [AkhiezerGlazman] p. 72.
|- (T e. UniOp -> (adjh` T) = `'T)
Theorem	hmopadjt 9819	A Hermitian operator is self-adjoint.
|- (T e. HrmOp -> (adjh` T) = T)
Theorem	hmdmadjt 9820	Every Hermitian operator has an adjoint.
|- (T e. HrmOp -> T e. dom adjh)
Theorem	hmopadj2t 9821	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 9822	A Hermitian operator is linear.
|- (T e. HrmOp -> T e. LinOp)
Theorem	bravalt 9823	The bra of a vector, expressed as <.A | in Dirac notation. See df-bra 9732.
|- (A e. H~ -> (bra` A) = {<.x, y>. | (x e. H~ /\ y = (x .ih A))})
Theorem	bravalvalt 9824	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 9825	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 9826	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 9827	The bra function is a functional.
|- (A e. H~ -> (bra` A):H~-->CC)
Theorem	bralnfnt 9828	The Dirac bra function is a linear functional.
|- (A e. H~ -> (bra` A) e. LinFn)
Theorem	braclt 9829	Closure of the bra function.
|- ((A e. H~ /\ B e. H~) -> ((bra` A)` B) e. CC)
Theorem	bra0 9830	The Dirac bra of the zero vector.
|- (bra` 0h) = (H~ X. {0})
Theorem	brafnmult 9831	Anti-linearity property of bra functional for multiplication.
|- ((A e. CC /\ B e. H~) -> (bra` (A .h B)) = ((*` A) .fn (bra` B)))
Theorem	kbvalt 9832	The outer product of two vectors, expressed as | A>. <.B | in Dirac notation. See df-kb 9733.
|- ((A e. H~ /\ B e. H~) -> (A ketbra B) = {<.x, y>. | (x e. H~ /\ y = ((x .ih B) .h A))})
Theorem	kbopt 9833	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 9834	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 9835	Multiplication property of outer product.
|- ((A e. CC /\ B e. H~ /\ C e. H~) -> ((A .h B) ketbra C) = (B ketbra ((*` A) .h C)))
Theorem	kbpjt 9836	If a vector A has norm 1, the outer product | A>. <.A | is the projector onto the subspace spanned by A. http://en.wikipedia.org/wiki/Bra-ket#Linear%5Foperators.
|- ((A e. H~ /\ (normh` A) = 1) -> (A ketbra A) = (proj` (span` {A})))
Theorem	eleigvect 9837	Membership in the set of eigenvectors of a Hilbert space operator.
|- (T:H~-->H~ -> (A e. (eigvec` T) <-> (A e. H~ /\ A =/= 0h /\ E.x e. CC (T` A) = (x .h A))))
Theorem	eleigvec2t 9838	Membership in the set of eigenvectors of a Hilbert space operator.
|- (T:H~-->H~ -> (A e. (eigvec` T) <-> (A e. H~ /\ A =/= 0h /\ (T` A) e. (span` {A}))))
Theorem	eleigvecclt 9839	Closure of an eigenvector of a Hilbert space operator.
|- ((T:H~-->H~ /\ A e. (eigvec` T)) -> A e. H~)
Theorem	eigvalt 9840	The eigenvalue of an eigenvector of a Hilbert space operator.
|- ((T:H~-->H~ /\ A e. (eigvec` T)) -> ((eigval` T)` A) = (((T` A) .ih A) / ((normh` A)^2)))
Theorem	eigvalclt 9841	An eigenvalue is a complex number.
|- ((T:H~-->H~ /\ A e. (eigvec` T)) -> ((eigval` T)` A) e. CC)
Theorem	eigvect 9842	Property of an eigenvector.
|- ((T:H~-->H~ /\ A e. (eigvec` T)) -> ((T` A) = (((eigval` T)` A) .h A) /\ A =/= 0h))
Theorem	eighmret 9843	The eigenvalues of a Hermitian operator are real. Equation 1.30 of [Hughes] p. 49.
|- ((T e. HrmOp /\ A e. (eigvec` T)) -> ((eigval` T)` A) e. RR)
Theorem	eighmortht 9844	Eigenvectors of a Hermitian operator with distinct eigenvalues are orthogonal. Equation 1.31 of [Hughes] p. 49.
|- (((T e. HrmOp /\ A e. (eigvec` T)) /\ (B e. (eigvec` T) /\ -. ((eigval` T)` A) = ((eigval` T)` B))) -> (A .ih B) = 0)
Theorem	nmopneg 9845	Value of the norm of the negative of a Hilbert space operator. Unlike nmophm 9916, the operator does not have to be bounded.
|- T:H~-->H~   =>   |- (normop` (-u1 .op T)) = (normop` T)
Theorem	lnop0t 9846	The value of a linear Hilbert space operator at zero is zero. Remark in [Beran] p. 99.
|- (T e. LinOp -> (T` 0h) = 0h)
Theorem	lnopmult 9847	Multiplicative property of a linear Hilbert space operator.
|- ((T e. LinOp /\ A e. CC /\ B e. H~) -> (T` (A .h B)) = (A .h (T` B)))
Theorem	lnopl 9848	Basic scalar product 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	lnopf 9849	A linear Hilbert space operator is a Hilbert space operator.
|- T e. LinOp   =>   |- T:H~-->H~
Theorem	lnop0 9850	The value of a linear Hilbert space operator at zero is zero. Remark in [Beran] p. 99.
|- T e. LinOp   =>   |- (T` 0h) = 0h
Theorem	lnopadd 9851	Additive property of a linear Hilbert space operator.
|- T e. LinOp   =>   |- ((A e. H~ /\