mmtheorems101 - 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 - 10001-10100 - Page 101 of 107

Type	Label	Description
Statement
Theorem	bdophs 10001	The sum of two bounded linear operators is a bounded linear operator.
|- S e. BndLinOp   &   |- T e. BndLinOp   =>   |- (S +op T) e. BndLinOp
Theorem	bdophd 10002	The difference between two bounded linear operators is bounded.
|- S e. BndLinOp   &   |- T e. BndLinOp   =>   |- (S -op T) e. BndLinOp
Theorem	bdopco 10003	The composition of two bounded linear operators is bounded.
|- S e. BndLinOp   &   |- T e. BndLinOp   =>   |- (S o. T) e. BndLinOp
Theorem	nmoptri2 10004	Triangle-type inequality for the norms of bounded linear operators.
|- S e. BndLinOp   &   |- T e. BndLinOp   =>   |- ((normop` S) - (normop` T)) <_ (normop` (S +op T))
Theorem	adjco 10005	The adjoint of a composition of bounded linear operators. Theorem 3.11(viii) of [Beran] p. 106.
|- S e. BndLinOp   &   |- T e. BndLinOp   =>   |- (adjh` (S o. T)) = ((adjh` T) o. (adjh` S))
Theorem	nmopcoadj 10006	The norm of an operator composed with its adjoint. Part of Theorem 3.11(vi) of [Beran] p. 106.
|- T e. BndLinOp   =>   |- (normop` ((adjh` T) o. T)) = ((normop` T)^2)
Theorem	nmopcoadj2 10007	The norm of an operator composed with its adjoint. Part of Theorem 3.11(vi) of [Beran] p. 106.
|- T e. BndLinOp   =>   |- (normop` (T o. (adjh` T))) = ((normop` T)^2)
Theorem	nmopcoadj0 10008	An operator composed with its adjoint is zero iff the operator is zero. Theorem 3.11(vii) of [Beran] p. 106.
|- T e. BndLinOp   =>   |- ((T o. (adjh` T)) = 0hop <-> T = 0hop)
Quantum computation error bound theorem
Theorem	unierr 10009	If we approximate a chain of unitary transformations (quantum computer gates) F, G by other unitary transformations S, T, the error increases at most additively. Equation 4.73 of [NielsenChuang] p. 195.
|- F e. UniOp   &   |- G e. UniOp   &   |- S e. UniOp   &   |- T e. UniOp   =>   |- (normop` ((F o. G) -op (S o. T))) <_ ((normop` (F -op S)) + (normop` (G -op T)))
Dirac bra-ket notation (cont.)
Theorem	branmfnt 10010	The norm of the bra function.
|- (A e. H~ -> (normfn` (bra` A)) = (normh` A))
Theorem	brabnt 10011	The bra of a vector is a bounded functional.
|- (A e. H~ -> (normfn` (bra` A)) e. RR)
Theorem	rnbra 10012	The set of bras equals the set of continuous linear functionals.
|- ran bra = (LinFn i^i ConFn)
Theorem	bra11 10013	The bra function maps vectors one-to-one onto the set of continuous linear functionals.
|- bra:H~-1-1-onto->(LinFn i^i ConFn)
Theorem	bracnlnt 10014	A bra is a continuous linear functional.
|- (A e. H~ -> (bra` A) e. (LinFn i^i ConFn))
Theorem	cnvbravalt 10015	Value of the converse of the bra function. Based on the Riesz Lemma riesz4t 9969, this very important theorem not only justifies the Dirac bra-ket notation, but allows us to extract a unique vector from any continuous linear functional from which the functional can be recovered; i.e. a single vector can "store" all of the information contained in any entire continuous linear functional (mapping from H~ to CC).
|- (T e. (LinFn i^i ConFn) -> (`'bra` T) = U.{y e. H~ | A.x e. H~ (T` x) = (x .ih y)})
Theorem	cnvbraclt 10016	Closure of the converse of the bra function.
|- (T e. (LinFn i^i ConFn) -> (`'bra` T) e. H~)
Theorem	cnvbrabrat 10017	The converse bra of the bra of a vector is the vector itself.
|- (A e. H~ -> (`'bra` (bra` A)) = A)
Theorem	bracnvbrat 10018	The bra of the converse bra of a continuous linear functional.
|- (T e. (LinFn i^i ConFn) -> (bra` (`'bra` T)) = T)
Theorem	bracnlnvalt 10019	The vector that a continuous linear functional is the bra of.
|- (T e. (LinFn i^i ConFn) -> T = (bra` U.{y e. H~ | A.x e. H~ (T` x) = (x .ih y)}))
Theorem	cnvbramult 10020	Multiplication property of the converse bra function.
|- ((A e. CC /\ T e. (LinFn i^i ConFn)) -> (`'bra` (A .fn T)) = ((*` A) .h (`'bra` T)))
Theorem	kbass1t 10021	Dirac bra-ket associative law ( | A>. <.B | ) | C>. = | A>.(<.B | C>.) i.e. the juxtaposition of an outer product with a ket equals a bra juxtaposed with an inner product. Since <.B | C>. is a complex number, it is the first argument in the inner product .h that it is mapped to, although in Dirac notation it is placed after the ket.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((A ketbra B)` C) = (((bra` B)` C) .h A))
Theorem	kbass2t 10022	Dirac bra-ket associative law (<.A | B>.)<.C | = <.A | ( | B>. <.C | ) i.e. the juxtaposition of an inner product with a bra equals a ket juxtaposed with an outer product.
|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> (((bra` A)` B) .fn (bra` C)) = ((bra` A) o. (B ketbra C)))
Theorem	kbass3t 10023	Dirac bra-ket associative law <.A | B>. <.C | D>. = (<.A | B>. <.C | ) | D>..
|- (((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) -> (((bra` A)` B) x. ((bra` C)` D)) = ((((bra` A)` B) .fn (bra` C))` D))
Theorem	kbass4t 10024	Dirac bra-ket associative law <.A | B>. <.C | D>. = <.A | ( | B>. <.C | D>.).
|- (((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) -> (((bra` A)` B) x. ((bra` C)` D)) = ((bra` A)` (((bra` C)` D) .h B)))
Theorem	kbass5t 10025	Dirac bra-ket associative law ( | A>. <.B | )( | C>. <.D | ) = (( | A>. <.B | ) | C>.)<.D |.
|- (((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) -> ((A ketbra B) o. (C ketbra D)) = (((A ketbra B)` C) ketbra D))
Theorem	kbass6t 10026	Dirac bra-ket associative law ( | A>. <.B | )( | C>. <.D | ) = | A>. (<.B | ( | C>. <.D | )).
|- (((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) -> ((A ketbra B) o. (C ketbra D)) = (A ketbra (`'bra` ((bra` B) o. (C ketbra D)))))
Positive operators (cont.)
Theorem	leopg 10027	Ordering relation for positive operators. Definition of positive operator ordering in [Kreyszig] p. 470.
|- ((T e. A /\ U e. B) -> (T <_op U <-> ((U -op T) e. HrmOp /\ A.x e. H~ 0 <_ (((U -op T)` x) .ih x))))
Theorem	leopt 10028	Ordering relation for operators. Definition of positive operator ordering in [Kreyszig] p. 470.
|- ((T e. HrmOp /\ U e. HrmOp) -> (T <_op U <-> A.x e. H~ 0 <_ (((U -op T)` x) .ih x)))
Theorem	leop2t 10029	Ordering relation for operators. Definition of operator ordering in [Young] p. 141.
|- ((T e. HrmOp /\ U e. HrmOp) -> (T <_op U <-> A.x e. H~ ((T` x) .ih x) <_ ((U` x) .ih x)))
Theorem	leop3t 10030	Operator ordering in terms of a positive operator. Definition of operator ordering in [Retherford] p. 49.
|- ((T e. HrmOp /\ U e. HrmOp) -> (T <_op U <-> 0hop <_op (U -op T)))
Theorem	leoppost 10031	Binary relation defining a positive operator. Definition VI.1 of [Retherford] p. 49.
|- (T e. HrmOp -> (0hop <_op T <-> A.x e. H~ 0 <_ ((T` x) .ih x)))
Theorem	leoprf2t 10032	The ordering relation for operators is reflexive.
|- (T:H~-->H~ -> T <_op T)
Theorem	leoprft 10033	The ordering relation for operators is reflexive.
|- (T e. HrmOp -> T <_op T)
Theorem	leopsqt 10034	The square of a Hermitian operator is positive.
|- (T e. HrmOp -> 0hop <_op (T o. T))
Theorem	0leop 10035	The zero operator is a positive operator. (The literature calls it "positive," even though in some sense it is really "nonnegative.") Part of Example 12.2(i) in [Young] p. 142.
|- 0hop <_op 0hop
Theorem	idleop 10036	The identity operator is a positive operator. Part of Example 12.2(i) in [Young] p. 142.
|- 0hop <_op Iop
Theorem	leopaddt 10037	The sum of two positive operators is positive. Exercise 1(i) of [Retherford] p. 49.
|- (((T e. HrmOp /\ U e. HrmOp) /\ (0hop <_op T /\ 0hop <_op U)) -> 0hop <_op (T +op U))
Theorem	leopmulit 10038	The scalar product of a nonnegative real and a positive operator is a positive operator. Exercise 1(ii) of [Retherford] p. 49.
|- (((A e. RR /\ T e. HrmOp) /\ (0 <_ A /\ 0hop <_op T)) -> 0hop <_op (A .op T))
Theorem	leopmult 10039	The scalar product of a positive real and a positive operator is a positive operator. Exercise 1(ii) of [Retherford] p. 49.
|- ((A e. RR /\ T e. HrmOp /\ 0 < A) -> (0hop <_op T <-> 0hop <_op (A .op T)))
Theorem	leopmul2it 10040	Scalar product applied to operator ordering.
|- (((A e. RR /\ T e. HrmOp /\ U e. HrmOp) /\ (0 <_ A /\ T <_op U)) -> (A .op T) <_op (A .op U))
Theorem	leoptrit 10041	The positive operator ordering relation satisfies trichotomy. Exercise 1(iii) of [Retherford] p. 49.
|- ((T e. HrmOp /\ U e. HrmOp) -> ((T <_op U /\ U <_op T) <-> T = U))
Theorem	leoptrt 10042	The positive operator ordering relation is transitive. Exercise 1(iv) of [Retherford] p. 49.
|- (((S e. HrmOp /\ T e. HrmOp /\ U e. HrmOp) /\ (S <_op T /\ T <_op U)) -> S <_op U)
Theorem	leopnmidt 10043	A bounded Hermitian operator is less than or equal to its norm times the identity operator.
|- ((T e. HrmOp /\ (normop` T) e. RR) -> T <_op ((normop` T) .op Iop ))
Theorem	nmopleidt 10044	A nonzero, bounded Hermitian operator divided by its norm is less than or equal to the identity operator.
|- ((T e. HrmOp /\ (normop` T) e. RR /\ T =/= 0hop) -> ((1 / (normop` T)) .op T) <_op Iop )
Projectors as operators
Theorem	pjhmop 10045	A projector is a Hermitian operator.
|- H e. CH   =>   |- (proj` H) e. HrmOp
Theorem	pjlnop 10046	A projector is a linear operator.
|- H e. CH   =>   |- (proj` H) e. LinOp
Theorem	pjnmop 10047	The operator norm of a projector on a non-zero closed subspace is one. Part of Theorem 26.1 of [Halmos] p. 43.
|- H e. CH   =>   |- (H =/= 0H -> (normop` (proj` H)) = 1)
Theorem	pjbdln 10048	A projector is a bounded linear operator.
|- H e. CH   =>   |- (proj` H) e. BndLinOp
Theorem	pjhmopt 10049	A projection is a Hermitian operator.
|- (H e. CH -> (proj` H) e. HrmOp)
Theorem	hmopidmchlem 10050	Lemma for hmopidmch 10051.
Theorem	hmopidmch 10051	An idempotent Hermitian operator generates a closed subspace. Part of proof of Theorem of [AkhiezerGlazman] p. 64.
|- H = {x e. H~ | (T` x) = x}   &   |- (T e. HrmOp /\ (T o. T) = T)   =>   |- H e. CH
Theorem	hmopidmpj 10052	An idempotent Hermitian operator is a projection operator. Theorem 26.4 of [Halmos] p. 44. (Halmos seems to omit the proof that H is a closed subspace, which is not trivial as hmopidmch 10051 shows.)
|- H = {x e. H~ | (T` x) = x}   &   |- (T e. HrmOp /\ (T o. T) = T)   =>   |-