mmtheorems100 - 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-10691

Statement List for Metamath Proof Explorer - 9901-10000 - Page 100 of 107

Type	Label	Description
Statement
Theorem	lnophmt 9901	A linear operator is Hermitian if x .ih (T` x) takes only real values. Remark in [ReedSimon] p. 195.
|- ((T e. LinOp /\ A.x e. H~ (x .ih (T` x)) e. RR) -> T e. HrmOp)
Theorem	hmopst 9902	The sum of two Hermitian operators is Hermitian.
|- ((T e. HrmOp /\ U e. HrmOp) -> (T +op U) e. HrmOp)
Theorem	hmopmt 9903	The scalar product of a Hermitian operator with a real is Hermitian.
|- ((A e. RR /\ T e. HrmOp) -> (A .op T) e. HrmOp)
Theorem	hmopdt 9904	The difference of two Hermitian operators is Hermitian.
|- ((T e. HrmOp /\ U e. HrmOp) -> (T -op U) e. HrmOp)
Theorem	hmopcot 9905	The composition of two commuting Hermitian operators is Hermitian.
|- ((T e. HrmOp /\ U e. HrmOp /\ (T o. U) = (U o. T)) -> (T o. U) e. HrmOp)
Theorem	nmbdoplb 9906	A lower bound for the norm of a bounded linear operator.
|- T e. BndLinOp   =>   |- (A e. H~ -> (normh` (T` A)) <_ ((normop` T) x. (normh` A)))
Theorem	nmbdoplbt 9907	A lower bound for the norm of a bounded linear Hilbert space operator.
|- ((T e. BndLinOp /\ A e. H~) -> (normh` (T` A)) <_ ((normop` T) x. (normh` A)))
Theorem	nmcopexlem1 9908	Lemma for nmcopex 9914 (Theorem 3.5(i) of [Beran] p. 99). A sufficient condition for the norm of an operator to be real, based on its definition and the properties of supremum. Compared to Beran, we use a direct proof instead of a proof by contradiction.
Theorem	nmcopexlem2 9909	Lemma for nmcopex 9914. Apply definition of continuity. Note that we use 1 instead of 0.5 that Beran uses for epsilon (e = 0.5 in his proof).
Theorem	nmcopexlem3 9910	Lemma for nmcopex 9914. Move 1 / n out of the norm, using linearity.
Theorem	nmcopexlem4 9911	Lemma for nmcopex 9914. Properties of the infimum of a collection of integers whose reciprocals are less than a real number y (which will later become the "epsilon" of the epsilon/delta continuity definition df-cnop 9724). Note that `' < in the fourth hypothesis signifies infimum. (This lemma involves only real numbers and is independent of Hilbert space. The first two hypotheses aren't used.)
Theorem	nmcopexlem5 9912	Lemma for nmcopex 9914.
Theorem	nmcopexlem6 9913	Lemma for nmcopex 9914. Combine lemmas to obtain the result (with hypotheses to be eliminated).
Theorem	nmcopex 9914	The norm of a continuous linear Hilbert space operator exists. Theorem 3.5(i) of [Beran] p. 99.
|- T e. LinOp   &   |- T e. ConOp   =>   |- (normop` T) e. RR
Theorem	nmcoplb 9915	A lower bound for the norm of a continuous linear operator. Theorem 3.5(ii) of [Beran] p. 99.
|- T e. LinOp   &   |- T e. ConOp   =>   |- (A e. H~ -> (normh` (T` A)) <_ ((normop` T) x. (normh` A)))
Theorem	nmcopext 9916	The norm of a continuous linear Hilbert space operator exists. Theorem 3.5(i) of [Beran] p. 99.
|- ((T e. LinOp /\ T e. ConOp) -> (normop` T) e. RR)
Theorem	nmcoplbt 9917	A lower bound for the norm of a continuous linear Hilbert space operator. Theorem 3.5(ii) of [Beran] p. 99.
|- ((T e. LinOp /\ T e. ConOp /\ A e. H~) -> (normh` (T` A)) <_ ((normop` T) x. (normh` A)))
Theorem	nmophm 9918	The norm of the scalar product of a bounded linear operator.
|- T e. BndLinOp   =>   |- (A e. CC -> (normop` (A .op T)) = ((abs` A) x. (normop` T)))
Theorem	bdophm 9919	The scalar product of a bounded linear operator is a bounded linear operator.
|- T e. BndLinOp   =>   |- (A e. CC -> (A .op T) e. BndLinOp)
Theorem	lnopcon 9920	A condition equivalent to "T is continuous" when T is linear. Theorem 3.5(iii) of [Beran] p. 99.
|- T e. LinOp   =>   |- (T e. ConOp <-> E.x e. RR A.y e. H~ (normh` (T` y)) <_ (x x. (normh` y)))
Theorem	lnopcont 9921	A condition equivalent to "T is continuous" when T is linear. Theorem 3.5(iii) of [Beran] p. 99.
|- (T e. LinOp -> (T e. ConOp <-> E.x e. RR A.y e. H~ (normh` (T` y)) <_ (x x. (normh` y))))
Theorem	lnopcnbdt 9922	A linear operator is continuous iff it is bounded.
|- (T e. LinOp -> (T e. ConOp <-> T e. BndLinOp))
Theorem	lncnopbd 9923	A continuous linear operator is a bounded linear operator. This theorem justifies our use of "bounded linear" as an interchangeable condition for "continuous linear" used in some textbook proofs.
|- (T e. (LinOp i^i ConOp) <-> T e. BndLinOp)
Theorem	lncnbd 9924	A continuous linear operator is a bounded linear operator.
|- (LinOp i^i ConOp) = BndLinOp
Theorem	lnopcnret 9925	A linear operator is continuous iff it is bounded.
|- (T e. LinOp -> (T e. ConOp <-> (normop` T) e. RR))
Theorem	lnfnl 9926	Basic property of a linear Hilbert space 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	lnfnf 9927	A linear Hilbert space functional is a functional.
|- T e. LinFn   =>   |- T:H~-->CC
Theorem	lnfn0 9928	The value of a linear Hilbert space functional at zero is zero. Remark in [Beran] p. 99.
|- T e. LinFn   =>   |- (T` 0h) = 0
Theorem	lnfnadd 9929	Additive property of a linear Hilbert space functional.
|- T e. LinFn   =>   |- ((A e. H~ /\ B e. H~) -> (T` (A +h B)) = ((T` A) + (T` B)))
Theorem	lnfnmul 9930	Multiplicative property of a linear Hilbert space functional.
|- T e. LinFn   =>   |- ((A e. CC /\ B e. H~) -> (T` (A .h B)) = (A x. (T` B)))
Theorem	lnfnaddmul 9931	Sum/product property of a linear Hilbert space functional.
|- T e. LinFn   =>   |- ((A e. CC /\ B e. H~ /\ C e. H~) -> (T` (B +h (A .h C))) = ((T` B) + (A x. (T` C))))
Theorem	lnfnsub 9932	Subtraction property for a linear Hilbert space functional.
|- T e. LinFn   =>   |- ((A e. H~ /\ B e. H~) -> (T` (A -h B)) = ((T` A) - (T` B)))
Theorem	lnfn0t 9933	The value of a linear Hilbert space functional at zero is zero. Remark in [Beran] p. 99.
|- (T e. LinFn -> (T` 0h) = 0)
Theorem	lnfnmult 9934	Multiplicative property of a linear Hilbert space functional.
|- ((T e. LinFn /\ A e. CC /\ B e. H~) -> (T` (A .h B)) = (A x. (T` B)))
Theorem	nmbdfnlb 9935	A lower bound for the norm of a bounded linear functional.
|- (T e. LinFn /\ (normfn` T) e. RR)   =>   |- (A e. H~ -> (abs` (T` A)) <_ ((normfn` T) x. (normh` A)))
Theorem	nmbdfnlbt 9936	A lower bound for the norm of a bounded linear functional.
|- ((T e. LinFn /\ (normfn` T) e. RR /\ A e. H~) -> (abs` (T` A)) <_ ((normfn` T) x. (normh` A)))
Theorem	nmcfnexlem1 9937	Lemma for nmcfnex 9943. Show a condition for the norm of a functional to exist, based on its definition and the properties of supremum. Compared to Beran, we use a direct proof instead of a proof by contradiction.
Theorem	nmcfnexlem2 9938	Lemma for nmcfnex 9943. Apply definition of continuity. Note that we use 1 instead of 0.5 that Beran uses for epsilon (e = 0.5 in his proof).
Theorem	nmcfnexlem3 9939	Lemma for nmcfnex 9943. Move 1 / n out of the norm, using linearity.
Theorem	nmcfnexlem4 9940	Lemma for nmcfnex 9943. Properties of the infimum of the collection of integers whose reciprocals are less than the delta of the continuity definition.
Theorem	nmcfnexlem5 9941	Lemma for nmcfnex 9943.
Theorem	nmcfnexlem6 9942	Lemma for nmcfnex 9943. Combine lemmas to obtain the result (with hypotheses to be eliminated).
Theorem	nmcfnex 9943	The norm of a continuous linear Hilbert space functional exists. Theorem 3.5(i) of [Beran] p. 99.
|- T e. LinFn   &   |- T e. ConFn   =>   |- (normfn` T) e. RR
Theorem	nmcfnlb 9944	A lower bound for the norm of a continuous linear functional. Theorem 3.5(ii) of [Beran] p. 99.
|- T e. LinFn   &   |- T e. ConFn   =>   |- (A e. H~ -> (abs` (T` A)) <_ ((normfn` T) x. (normh` A)))
Theorem	nmcfnext 9945	The norm of a continuous linear Hilbert space functional exists. Theorem 3.5(i) of [Beran] p. 99.
|- ((T e. LinFn /\ T e. ConFn) -> (normfn` T) e. RR)
Theorem	nmcfnlbt 9946	A lower bound of the norm of a continuous linear Hilbert space functional. Theorem 3.5(ii) of [Beran] p. 99.
|- ((T e. LinFn /\ T e. ConFn /\ A e. H~) -> (abs` (T` A)) <_ ((normfn` T) x. (normh` A)))
Theorem	lnfncon 9947	A condition equivalent to "T is continuous" when T is linear. Theorem 3.5(iii) of [Beran] p. 99.
|- T e. LinFn   =>   |- (T e. ConFn <-> E.x e. RR A.y e. H~ (abs` (T` y)) <_ (x x. (normh` y)))
Theorem	lnfncont 9948	A condition equivalent to "T is continuous" when T is linear. Theorem 3.5(iii) of [Beran] p. 99.
|- (T e. LinFn -> (T e. ConFn <-> E.x e. RR A.y e. H~ (abs` (T` y)) <_ (x x. (normh` y))))
Theorem	lnfncnbdt 9949	A linear functional is continuous iff it is bounded.
|- (T e. LinFn -> (T e. ConFn <-> (normfn` T) e. RR))
Theorem	nlelsh 9950	The null space of a linear functional is a subspace.
|- T e. LinFn   =>   |- (null` T) e. SH
Theorem	nlelch 9951	The null space of a continuous linear functional is a closed subspace. Remark 3.8 of [Beran] p. 103.
|- T e. LinFn   &   |- T e. ConFn   =>   |- (null` T) e. CH
Riesz lemma
Theorem	riesz3 9952	A continuous linear functional can be expressed as an inner product. Existence part of Theorem 3.9 of [Beran] p. 104.
|- T e. LinFn   &   |- T e. ConFn   =>   |- E.w e. H~ A.v e. H~ (T` v) = (v .ih w)
Theorem	riesz4 9953	A continuous linear functional can be expressed as an inner product. Uniqueness part of Theorem 3.9 of [Beran] p. 104.
|- T e. LinFn   &   |- T e. ConFn   =>   |- E!w e. H~ A.v e. H~ (T` v) = (v .ih w)
Theorem	riesz4t 9954	A continuous linear functional can be expressed as an inner product. Uniqueness part of Theorem 3.9 of [Beran] p. 104. See riesz2t 9956 for the bounded linear functional version.
|- (T e. (LinFn i^i ConFn) -> E!w e. H~ A.v e. H~ (T` v) = (v .ih w))
Theorem	riesz1t 9955	Part 1 of the Riesz representation theorem for bounded linear functionals. A linear functional is bounded iff its value can be expressed as an inner product. Part of Theorem 17.3 of [Halmos] p. 31. For part 2, see riesz2t 9956. For the continuous linear functional version, see riesz3 9952 and riesz4t 9954.
|- (T e. LinFn -> ((normfn` T) e. RR <-> E.y e. H~ A.x e. H~ (T` x) = (x .ih y)))
Theorem	riesz2t 9956	Part 2 of the Riesz representation theorem for bounded linear functionals. The value of a bounded linear functional corresponds to a unique inner product. Part of Theorem 17.3 of [Halmos] p. 31. For part 1, see riesz1t 9955.
|- ((T e. LinFn /\ (normfn` T) e. RR) -> E!y e. H~ A.x e. H~ (T` x) = (x .ih y))
Adjoints (cont.)
Theorem	cnlnadjlem1 9957	Lemma for cnlnadj 9966 (Theorem 3.10 of [Beran] p. 104: every continuous linear operator has an adjoint). The value of the auxiliary functional G.
Theorem	cnlnadjlem2 9958	Lemma for cnlnadj 9966. G is a continuous linear functional.
Theorem	cnlnadjlem3 9959	Lemma for cnlnadj 9966. By riesz4t 9954, B is the unique vector such that (T` v) .ih y) = (v .ih w) for all v.
Theorem	cnlnadjlem4 9960	Lemma for cnlnadj 9966. The values of auxiliary function F are vectors.
Theorem	cnlnadjlem5 9961	Lemma for cnlnadj 9966. F is an adjoint of T (later, we will show it is unique).
Theorem	cnlnadjlem6 9962	Lemma for cnlnadj 9966. F is linear.
Theorem	cnlnadjlem7 9963	Lemma for cnlnadj 9966. Helper lemma to show that F is continuous.
Theorem	cnlnadjlem8 9964	Lemma for cnlnadj 9966. F is continuous.
Theorem	cnlnadjlem9 9965	Lemma for cnlnadj 9966. F provides an example showing the existence of a continuous linear adjoint.
Theorem	cnlnadj 9966	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 9967	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 9968	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)))