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

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

Type	Label	Description
Statement
Theorem	hmopdt 9901	The difference of two Hermitian operators is Hermitian.
|- ((T e. HrmOp /\ U e. HrmOp) -> (T -op U) e. HrmOp)
Theorem	hmopcot 9902	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 9903	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 9904	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 9905	Lemma for nmcopex 9911 (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 9906	Lemma for nmcopex 9911. 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 9907	Lemma for nmcopex 9911. Move 1 / n out of the norm, using linearity.
Theorem	nmcopexlem4 9908	Lemma for nmcopex 9911. 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 9721). 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 9909	Lemma for nmcopex 9911.
Theorem	nmcopexlem6 9910	Lemma for nmcopex 9911. Combine lemmas to obtain the result (with hypotheses to be eliminated).
Theorem	nmcopex 9911	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 9912	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 9913	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 9914	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 9915	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 9916	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 9917	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 9918	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 9919	A linear operator is continuous iff it is bounded.
|- (T e. LinOp -> (T e. ConOp <-> T e. BndLinOp))
Theorem	lncnopbd 9920	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 9921	A continuous linear operator is a bounded linear operator.
|- (LinOp i^i ConOp) = BndLinOp
Theorem	lnopcnret 9922	A linear operator is continuous iff it is bounded.
|- (T e. LinOp -> (T e. ConOp <-> (normop` T) e. RR))
Theorem	lnfnl 9923	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 9924	A linear Hilbert space functional is a functional.
|- T e. LinFn   =>   |- T:H~-->CC
Theorem	lnfn0 9925	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 9926	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 9927	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 9928	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 9929	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 9930	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 9931	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 9932	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 9933	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 9934	Lemma for nmcfnex 9940. 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 9935	Lemma for nmcfnex 9940. 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 9936	Lemma for nmcfnex 9940. Move 1 / n out of the norm, using linearity.
Theorem	nmcfnexlem4 9937	Lemma for nmcfnex 9940. Properties of the infimum of the collection of integers whose reciprocals are less than the delta of the continuity definition.
Theorem	nmcfnexlem5 9938	Lemma for nmcfnex 9940.
Theorem	nmcfnexlem6 9939	Lemma for nmcfnex 9940. Combine lemmas to obtain the result (with hypotheses to be eliminated).
Theorem	nmcfnex 9940	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 9941	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 9942	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 9943	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 9944	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 9945	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 9946	A linear functional is continuous iff it is bounded.
|- (T e. LinFn -> (T e. ConFn <-> (normfn` T) e. RR))
Theorem	nlelsh 9947	The null space of a linear functional is a subspace.
|- T e. LinFn   =>   |- (null` T) e. SH
Theorem	nlelch 9948	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 9949	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 9950	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 9951	A continuous linear functional can be expressed as an inner product. Uniqueness part of Theorem 3.9 of [Beran] p. 104. See riesz2t 9953 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 9952	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 9953. For the continuous linear functional version, see riesz3 9949 and riesz4t 9951.
|- (T e. LinFn -> ((normfn` T) e. RR <-> E.y e. H~ A.x e. H~ (T` x) = (x .ih y)))
Theorem	riesz2t 9953	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 9952.
|- ((T e. LinFn /\ (normfn` T) e. RR) -> E!y e. H~ A.x e. H~ (T` x) = (x .ih y))
Adjoints (cont.)
Theorem	cnlnadjlem1 9954	Lemma for cnlnadj 9963 (Theorem 3.10 of [Beran] p. 104: every continuous linear operator has an adjoint). The value of the auxiliary functional G.
Theorem	cnlnadjlem2 9955	Lemma for cnlnadj 9963. G is a continuous linear functional.
Theorem	cnlnadjlem3 9956	Lemma for cnlnadj 9963. By riesz4t 9951, B is the unique vector such that (T` v) .ih y) = (v .ih w) for all v.
Theorem	cnlnadjlem4 9957	Lemma for cnlnadj 9963. The values of auxiliary function F are vectors.
Theorem	cnlnadjlem5 9958	Lemma for cnlnadj 9963. F is an adjoint of T (later, we will show it is unique).
Theorem	cnlnadjlem6 9959	Lemma for cnlnadj 9963. F is linear.
Theorem	cnlnadjlem7 9960	Lemma for cnlnadj 9963. Helper lemma to show that F is continuous.
Theorem	cnlnadjlem8 9961	Lemma for cnlnadj 9963. F is continuous.
Theorem	cnlnadjlem9 9962	Lemma for cnlnadj 9963. F provides an example showing the existence of a continuous linear adjoint.
Theorem	cnlnadj 9963	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 9964	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 9965	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 9966	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 9967	Every continuous linear Hilbert space operator has an adjoint.
|- (LinOp i^i ConOp) (_ dom adjh
Theorem	bdopssadj 9968	Every bounded linear Hilbert space operator has an adjoint.
|- BndLinOp (_ dom adjh
Theorem	bdopadjt 9969	Every bounded linear Hilbert space operator has an adjoint.
|- (T e. BndLinOp -> T e. dom adjh)