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-10700 108 10701-10752

<

Statement List for Metamath Proof Explorer - 10001-10100 - Page 101 of 108

Type	Label	Description
Statement
Theorem	cnlnadjlem7 10001	Lemma for cnlnadj 10004. Helper lemma to show that F is continuous.
Theorem	cnlnadjlem8 10002	Lemma for cnlnadj 10004. F is continuous.
Theorem	cnlnadjlem9 10003	Lemma for cnlnadj 10004. F provides an example showing the existence of a continuous linear adjoint.
Theorem	cnlnadj 10004	Every continuous linear operator has an adjoint. Theorem 3.10 of [Beran] p. 104.
|- T e. LinOp   &   |- T e. ConOp   =>   |- E.t e. (LinOp i^i ConOp)A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y))
Theorem	cnlnadjeu 10005	Every continuous linear operator has a unique adjoint. Theorem 3.10 of [Beran] p. 104.
|- T e. LinOp   &   |- T e. ConOp   =>   |- E!t e. (LinOp i^i ConOp)A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y))
Theorem	cnlnadjeut 10006	Every continuous linear operator has a unique adjoint. Theorem 3.10 of [Beran] p. 104.
|- (T e. (LinOp i^i ConOp) -> E!t e. (LinOp i^i ConOp)A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y)))
Theorem	cnlnadjt 10007	Every continuous linear operator has an adjoint. Theorem 3.10 of [Beran] p. 104.
|- (T e. (LinOp i^i ConOp) -> E.t e. (LinOp i^i ConOp)A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y)))
Theorem	cnlnssadj 10008	Every continuous linear Hilbert space operator has an adjoint.
|- (LinOp i^i ConOp) (_ dom adjh
Theorem	bdopssadj 10009	Every bounded linear Hilbert space operator has an adjoint.
|- BndLinOp (_ dom adjh
Theorem	bdopadjt 10010	Every bounded linear Hilbert space operator has an adjoint.
|- (T e. BndLinOp -> T e. dom adjh)
Theorem	adjbdlnt 10011	The adjoint of a bounded linear operator is a bounded linear operator.
|- (T e. BndLinOp -> (adjh` T) e. BndLinOp)
Theorem	adjbdlnb 10012	An operator is bounded and linear iff its adjoint is.
|- (T e. BndLinOp <-> (adjh` T) e. BndLinOp)
Theorem	adjbd1o 10013	The mapping of adjoints of bounded linear operators is one-to-one onto.
|- (adjh |` BndLinOp):BndLinOp-1-1-onto->BndLinOp
Theorem	adjlnopt 10014	The adjoint of an operator is linear. Proposition 1 of [AkhiezerGlazman] p. 80.
|- (T e. dom adjh -> (adjh` T) e. LinOp)
Theorem	adjsslnop 10015	Every operator with an adjoint is linear.
|- dom adjh (_ LinOp
Theorem	nmopadjle 10016	Property of the norm of an adjoint. Part of proof of Theorem 3.10 of [Beran] p. 104.
|- T e. BndLinOp   =>   |- (A e. H~ -> (normh` ((adjh` T)` A)) <_ ((normop` T) x. (normh` A)))
Theorem	nmopadjlem 10017	Lemma for nmopadj 10018.
Theorem	nmopadj 10018	Property of the norm of an adjoint. Theorem 3.11(v) of [Beran] p. 106.
|- T e. BndLinOp   =>   |- (normop` (adjh` T)) = (normop` T)
Theorem	adjeq0 10019	An operator is zero iff its adjoint is zero. Theorem 3.11(i) of [Beran] p. 106.
|- (T = 0hop <-> (adjh` T) = 0hop)
Theorem	adjmult 10020	The adjoint of the scalar product of an operator. Theorem 3.11(ii) of [Beran] p. 106.
|- ((A e. CC /\ T e. dom adjh) -> (adjh` (A .op T)) = ((*` A) .op (adjh` T)))
Theorem	adjaddt 10021	The adjoint of the sum of two operators. Theorem 3.11(iii) of [Beran] p. 106.
|- ((S e. dom adjh /\ T e. dom adjh) -> (adjh` (S +op T)) = ((adjh` S) +op (adjh` T)))
Theorem	nmoptri 10022	Triangle inequality for the norms of bounded linear operators.
|- S e. BndLinOp   &   |- T e. BndLinOp   =>   |- (normop` (S +op T)) <_ ((normop` S) + (normop` T))
Theorem	nmopco 10023	Upper bound for the norm of the composition of two bounded linear operators.
|- S e. BndLinOp   &   |- T e. BndLinOp   =>   |- (normop` (S o. T)) <_ ((normop` S) x. (normop` T))
Theorem	bdophs 10024	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 10025	The difference between two bounded linear operators is bounded.
|- S e. BndLinOp   &   |- T e. BndLinOp   =>   |- (S -op T) e. BndLinOp
Theorem	bdopco 10026	The composition of two bounded linear operators is bounded.
|- S e. BndLinOp   &   |- T e. BndLinOp   =>   |- (S o. T) e. BndLinOp
Theorem	nmoptri2 10027	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 10028	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 10029	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 10030	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 10031	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 10032	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 10033	The norm of the bra function.
|- (A e. H~ -> (normfn` (bra` A)) = (normh` A))
Theorem	brabnt 10034	The bra of a vector is a bounded functional.
|- (A e. H~ -> (normfn` (bra` A)) e. RR)
Theorem	rnbra 10035	The set of bras equals the set of continuous linear functionals.
|- ran bra = (LinFn i^i ConFn)
Theorem	bra11 10036	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 10037	A bra is a continuous linear functional.
|- (A e. H~ -> (bra` A) e. (LinFn i^i ConFn))
Theorem	cnvbravalt 10038	Value of the converse of the bra function. Based on the Riesz Lemma riesz4t 9992, 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 10039	Closure of the converse of the bra function.
|- (T e. (LinFn i^i ConFn) -> (`'bra` T) e. H~)
Theorem	cnvbrabrat 10040	The converse bra of the bra of a vector is the vector itself.
|- (A e. H~ -> (`'bra` (bra` A)) = A)
Theorem	bracnvbrat 10041	The bra of the converse bra of a continuous linear functional.
|- (T e. (LinFn i^i ConFn) -> (bra` (`'bra` T)) = T)
Theorem	bracnlnvalt 10042	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 10043	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 10044	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 10045	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 10046	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 10047	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 10048	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 10049	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 10050	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 10051	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 10052	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 10053	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)))