 Home Metamath Proof ExplorerTheorem List (p. 281 of 425) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

 Color key: Metamath Proof Explorer (1-26947) Hilbert Space Explorer (26948-28472) Users' Mathboxes (28473-42426)

Theorem List for Metamath Proof Explorer - 28001-28100   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremlnop0i 28001 The value of a linear Hilbert space operator at zero is zero. Remark in [Beran] p. 99. (Contributed by NM, 11-May-2005.) (New usage is discouraged.)
𝑇 ∈ LinOp       (𝑇‘0) = 0

Theoremlnopaddi 28002 Additive property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005.) (New usage is discouraged.)
𝑇 ∈ LinOp       ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 + 𝐵)) = ((𝑇𝐴) + (𝑇𝐵)))

Theoremlnopmuli 28003 Multiplicative property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005.) (New usage is discouraged.)
𝑇 ∈ LinOp       ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 · 𝐵)) = (𝐴 · (𝑇𝐵)))

Theoremlnopaddmuli 28004 Sum/product property of a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.)
𝑇 ∈ LinOp       ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘(𝐵 + (𝐴 · 𝐶))) = ((𝑇𝐵) + (𝐴 · (𝑇𝐶))))

Theoremlnopsubi 28005 Subtraction property for a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.)
𝑇 ∈ LinOp       ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 𝐵)) = ((𝑇𝐴) − (𝑇𝐵)))

Theoremlnopsubmuli 28006 Subtraction/product property of a linear Hilbert space operator. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.)
𝑇 ∈ LinOp       ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘(𝐵 (𝐴 · 𝐶))) = ((𝑇𝐵) − (𝐴 · (𝑇𝐶))))

Theoremlnopmulsubi 28007 Product/subtraction property of a linear Hilbert space operator. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.)
𝑇 ∈ LinOp       ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘((𝐴 · 𝐵) − 𝐶)) = ((𝐴 · (𝑇𝐵)) − (𝑇𝐶)))

Theoremhomco2 28008 Move a scalar product out of a composition of operators. The operator 𝑇 must be linear, unlike homco1 27832 that works for any operators. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.)
((𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈: ℋ⟶ ℋ) → (𝑇 ∘ (𝐴 ·op 𝑈)) = (𝐴 ·op (𝑇𝑈)))

Theoremidunop 28009 The identity function (restricted to Hilbert space) is a unitary operator. (Contributed by NM, 21-Jan-2006.) (New usage is discouraged.)
( I ↾ ℋ) ∈ UniOp

Theorem0cnop 28010 The identically zero function is a continuous Hilbert space operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
0hop ∈ ConOp

Theorem0cnfn 28011 The identically zero function is a continuous Hilbert space functional. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
( ℋ × {0}) ∈ ConFn

Theoremidcnop 28012 The identity function (restricted to Hilbert space) is a continuous operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
( I ↾ ℋ) ∈ ConOp

Theoremidhmop 28013 The Hilbert space identity operator is a Hermitian operator. (Contributed by NM, 22-Apr-2006.) (New usage is discouraged.)
Iop ∈ HrmOp

Theorem0hmop 28014 The identically zero function is a Hermitian operator. (Contributed by NM, 8-Aug-2006.) (New usage is discouraged.)
0hop ∈ HrmOp

Theorem0lnop 28015 The identically zero function is a linear Hilbert space operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
0hop ∈ LinOp

Theorem0lnfn 28016 The identically zero function is a linear Hilbert space functional. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
( ℋ × {0}) ∈ LinFn

Theoremnmop0 28017 The norm of the zero operator is zero. (Contributed by NM, 8-Feb-2006.) (New usage is discouraged.)
(normop‘ 0hop ) = 0

Theoremnmfn0 28018 The norm of the identically zero functional is zero. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
(normfn‘( ℋ × {0})) = 0

TheoremhmopbdoptHIL 28019 A Hermitian operator is a bounded linear operator (Hellinger-Toeplitz Theorem). (Contributed by NM, 18-Jan-2008.) (New usage is discouraged.)
(𝑇 ∈ HrmOp → 𝑇 ∈ BndLinOp)

Theoremhoddii 28020 Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri 27811 does not require linearity.) (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
𝑅 ∈ LinOp    &   𝑆: ℋ⟶ ℋ    &   𝑇: ℋ⟶ ℋ       (𝑅 ∘ (𝑆op 𝑇)) = ((𝑅𝑆) −op (𝑅𝑇))

Theoremhoddi 28021 Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri 27811 does not require linearity.) (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.)
((𝑅 ∈ LinOp ∧ 𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑅 ∘ (𝑆op 𝑇)) = ((𝑅𝑆) −op (𝑅𝑇)))

Theoremnmop0h 28022 The norm of any operator on the trivial Hilbert space is zero. (This is the reason we need ℋ ≠ 0 in nmopun 28045.) (Contributed by NM, 24-Feb-2006.) (New usage is discouraged.)
(( ℋ = 0𝑇: ℋ⟶ ℋ) → (normop𝑇) = 0)

Theoremidlnop 28023 The identity function (restricted to Hilbert space) is a linear operator. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.)
( I ↾ ℋ) ∈ LinOp

Theorem0bdop 28024 The identically zero operator is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
0hop ∈ BndLinOp

Theoremadj0 28025 Adjoint of the zero operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.)

Theoremnmlnop0iALT 28026 A linear operator with a zero norm is identically zero. (Contributed by NM, 8-Feb-2006.) (New usage is discouraged.) (Proof modification is discouraged.)
𝑇 ∈ LinOp       ((normop𝑇) = 0 ↔ 𝑇 = 0hop )

Theoremnmlnop0iHIL 28027 A linear operator with a zero norm is identically zero. (Contributed by NM, 18-Jan-2008.) (New usage is discouraged.)
𝑇 ∈ LinOp       ((normop𝑇) = 0 ↔ 𝑇 = 0hop )

Theoremnmlnopgt0i 28028 A linear Hilbert space operator that is not identically zero has a positive norm. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.)
𝑇 ∈ LinOp       (𝑇 ≠ 0hop ↔ 0 < (normop𝑇))

Theoremnmlnop0 28029 A linear operator with a zero norm is identically zero. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)
(𝑇 ∈ LinOp → ((normop𝑇) = 0 ↔ 𝑇 = 0hop ))

Theoremnmlnopne0 28030 A linear operator with a nonzero norm is nonzero. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)
(𝑇 ∈ LinOp → ((normop𝑇) ≠ 0 ↔ 𝑇 ≠ 0hop ))

Theoremlnopmi 28031 The scalar product of a linear operator is a linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
𝑇 ∈ LinOp       (𝐴 ∈ ℂ → (𝐴 ·op 𝑇) ∈ LinOp)

Theoremlnophsi 28032 The sum of two linear operators is linear. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
𝑆 ∈ LinOp    &   𝑇 ∈ LinOp       (𝑆 +op 𝑇) ∈ LinOp

Theoremlnophdi 28033 The difference of two linear operators is linear. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.)
𝑆 ∈ LinOp    &   𝑇 ∈ LinOp       (𝑆op 𝑇) ∈ LinOp

Theoremlnopcoi 28034 The composition of two linear operators is linear. (Contributed by NM, 8-Mar-2006.) (New usage is discouraged.)
𝑆 ∈ LinOp    &   𝑇 ∈ LinOp       (𝑆𝑇) ∈ LinOp

Theoremlnopco0i 28035 The composition of a linear operator with one whose norm is zero. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
𝑆 ∈ LinOp    &   𝑇 ∈ LinOp       ((normop𝑇) = 0 → (normop‘(𝑆𝑇)) = 0)

Theoremlnopeq0lem1 28036 Lemma for lnopeq0i 28038. Apply the generalized polarization identity polid2i 27186 to the quadratic form ((𝑇𝑥), 𝑥). (Contributed by NM, 26-Jul-2006.) (New usage is discouraged.)
𝑇 ∈ LinOp    &   𝐴 ∈ ℋ    &   𝐵 ∈ ℋ       ((𝑇𝐴) ·ih 𝐵) = (((((𝑇‘(𝐴 + 𝐵)) ·ih (𝐴 + 𝐵)) − ((𝑇‘(𝐴 𝐵)) ·ih (𝐴 𝐵))) + (i · (((𝑇‘(𝐴 + (i · 𝐵))) ·ih (𝐴 + (i · 𝐵))) − ((𝑇‘(𝐴 (i · 𝐵))) ·ih (𝐴 (i · 𝐵)))))) / 4)

Theoremlnopeq0lem2 28037 Lemma for lnopeq0i 28038. (Contributed by NM, 26-Jul-2006.) (New usage is discouraged.)
𝑇 ∈ LinOp       ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝑇𝐴) ·ih 𝐵) = (((((𝑇‘(𝐴 + 𝐵)) ·ih (𝐴 + 𝐵)) − ((𝑇‘(𝐴 𝐵)) ·ih (𝐴 𝐵))) + (i · (((𝑇‘(𝐴 + (i · 𝐵))) ·ih (𝐴 + (i · 𝐵))) − ((𝑇‘(𝐴 (i · 𝐵))) ·ih (𝐴 (i · 𝐵)))))) / 4))

Theoremlnopeq0i 28038* A condition implying that a linear Hilbert space operator is identically zero. Unlike ho01i 27859 for arbitrary operators, when the operator is linear we need to consider only the values of the quadratic form (𝑇𝑥) ·ih 𝑥). (Contributed by NM, 26-Jul-2006.) (New usage is discouraged.)
𝑇 ∈ LinOp       (∀𝑥 ∈ ℋ ((𝑇𝑥) ·ih 𝑥) = 0 ↔ 𝑇 = 0hop )

Theoremlnopeqi 28039* Two linear Hilbert space operators are equal iff their quadratic forms are equal. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.)
𝑇 ∈ LinOp    &   𝑈 ∈ LinOp       (∀𝑥 ∈ ℋ ((𝑇𝑥) ·ih 𝑥) = ((𝑈𝑥) ·ih 𝑥) ↔ 𝑇 = 𝑈)

Theoremlnopeq 28040* Two linear Hilbert space operators are equal iff their quadratic forms are equal. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.)
((𝑇 ∈ LinOp ∧ 𝑈 ∈ LinOp) → (∀𝑥 ∈ ℋ ((𝑇𝑥) ·ih 𝑥) = ((𝑈𝑥) ·ih 𝑥) ↔ 𝑇 = 𝑈))

Theoremlnopunilem1 28041* Lemma for lnopunii 28043. (Contributed by NM, 14-May-2005.) (New usage is discouraged.)
𝑇 ∈ LinOp    &   𝑥 ∈ ℋ (norm‘(𝑇𝑥)) = (norm𝑥)    &   𝐴 ∈ ℋ    &   𝐵 ∈ ℋ    &   𝐶 ∈ ℂ       (ℜ‘(𝐶 · ((𝑇𝐴) ·ih (𝑇𝐵)))) = (ℜ‘(𝐶 · (𝐴 ·ih 𝐵)))

Theoremlnopunilem2 28042* Lemma for lnopunii 28043. (Contributed by NM, 12-May-2005.) (New usage is discouraged.)
𝑇 ∈ LinOp    &   𝑥 ∈ ℋ (norm‘(𝑇𝑥)) = (norm𝑥)    &   𝐴 ∈ ℋ    &   𝐵 ∈ ℋ       ((𝑇𝐴) ·ih (𝑇𝐵)) = (𝐴 ·ih 𝐵)

Theoremlnopunii 28043* If a linear operator (whose range is ) is idempotent in the norm, the operator is unitary. Similar to theorem in [AkhiezerGlazman] p. 73. (Contributed by NM, 23-Jan-2006.) (New usage is discouraged.)
𝑇 ∈ LinOp    &   𝑇: ℋ–onto→ ℋ    &   𝑥 ∈ ℋ (norm‘(𝑇𝑥)) = (norm𝑥)       𝑇 ∈ UniOp

Theoremelunop2 28044* An operator is unitary iff it is linear, onto, and idempotent in the norm. Similar to theorem in [AkhiezerGlazman] p. 73, and its converse. (Contributed by NM, 24-Feb-2006.) (New usage is discouraged.)
(𝑇 ∈ UniOp ↔ (𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ (norm‘(𝑇𝑥)) = (norm𝑥)))

Theoremnmopun 28045 Norm of a unitary Hilbert space operator. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.)
(( ℋ ≠ 0𝑇 ∈ UniOp) → (normop𝑇) = 1)

Theoremunopbd 28046 A unitary operator is a bounded linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
(𝑇 ∈ UniOp → 𝑇 ∈ BndLinOp)

Theoremlnophmlem1 28047* Lemma for lnophmi 28049. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.)
𝐴 ∈ ℋ    &   𝐵 ∈ ℋ    &   𝑇 ∈ LinOp    &   𝑥 ∈ ℋ (𝑥 ·ih (𝑇𝑥)) ∈ ℝ       (𝐴 ·ih (𝑇𝐴)) ∈ ℝ

Theoremlnophmlem2 28048* Lemma for lnophmi 28049. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.)
𝐴 ∈ ℋ    &   𝐵 ∈ ℋ    &   𝑇 ∈ LinOp    &   𝑥 ∈ ℋ (𝑥 ·ih (𝑇𝑥)) ∈ ℝ       (𝐴 ·ih (𝑇𝐵)) = ((𝑇𝐴) ·ih 𝐵)

Theoremlnophmi 28049* A linear operator is Hermitian if 𝑥 ·ih (𝑇𝑥) takes only real values. Remark in [ReedSimon] p. 195. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.)
𝑇 ∈ LinOp    &   𝑥 ∈ ℋ (𝑥 ·ih (𝑇𝑥)) ∈ ℝ       𝑇 ∈ HrmOp

Theoremlnophm 28050* A linear operator is Hermitian if 𝑥 ·ih (𝑇𝑥) takes only real values. Remark in [ReedSimon] p. 195. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.)
((𝑇 ∈ LinOp ∧ ∀𝑥 ∈ ℋ (𝑥 ·ih (𝑇𝑥)) ∈ ℝ) → 𝑇 ∈ HrmOp)

Theoremhmops 28051 The sum of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 +op 𝑈) ∈ HrmOp)

Theoremhmopm 28052 The scalar product of a Hermitian operator with a real is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
((𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp) → (𝐴 ·op 𝑇) ∈ HrmOp)

Theoremhmopd 28053 The difference of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇op 𝑈) ∈ HrmOp)

Theoremhmopco 28054 The composition of two commuting Hermitian operators is Hermitian. (Contributed by NM, 22-Aug-2006.) (New usage is discouraged.)
((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇𝑈) = (𝑈𝑇)) → (𝑇𝑈) ∈ HrmOp)

Theoremnmbdoplbi 28055 A lower bound for the norm of a bounded linear operator. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
𝑇 ∈ BndLinOp       (𝐴 ∈ ℋ → (norm‘(𝑇𝐴)) ≤ ((normop𝑇) · (norm𝐴)))

Theoremnmbdoplb 28056 A lower bound for the norm of a bounded linear Hilbert space operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
((𝑇 ∈ BndLinOp ∧ 𝐴 ∈ ℋ) → (norm‘(𝑇𝐴)) ≤ ((normop𝑇) · (norm𝐴)))

Theoremnmcexi 28057* Lemma for nmcopexi 28058 and nmcfnexi 28082. The norm of a continuous linear Hilbert space operator or functional exists. Theorem 3.5(i) of [Beran] p. 99. (Contributed by Mario Carneiro, 17-Nov-2013.) (Proof shortened by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
𝑦 ∈ ℝ+𝑧 ∈ ℋ ((norm𝑧) < 𝑦 → (𝑁‘(𝑇𝑧)) < 1)    &   (𝑆𝑇) = sup({𝑚 ∣ ∃𝑥 ∈ ℋ ((norm𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇𝑥)))}, ℝ*, < )    &   (𝑥 ∈ ℋ → (𝑁‘(𝑇𝑥)) ∈ ℝ)    &   (𝑁‘(𝑇‘0)) = 0    &   (((𝑦 / 2) ∈ ℝ+𝑥 ∈ ℋ) → ((𝑦 / 2) · (𝑁‘(𝑇𝑥))) = (𝑁‘(𝑇‘((𝑦 / 2) · 𝑥))))       (𝑆𝑇) ∈ ℝ

Theoremnmcopexi 28058 The norm of a continuous linear Hilbert space operator exists. Theorem 3.5(i) of [Beran] p. 99. (Contributed by NM, 5-Feb-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
𝑇 ∈ LinOp    &   𝑇 ∈ ConOp       (normop𝑇) ∈ ℝ

Theoremnmcoplbi 28059 A lower bound for the norm of a continuous linear operator. Theorem 3.5(ii) of [Beran] p. 99. (Contributed by NM, 7-Feb-2006.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
𝑇 ∈ LinOp    &   𝑇 ∈ ConOp       (𝐴 ∈ ℋ → (norm‘(𝑇𝐴)) ≤ ((normop𝑇) · (norm𝐴)))

Theoremnmcopex 28060 The norm of a continuous linear Hilbert space operator exists. Theorem 3.5(i) of [Beran] p. 99. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
((𝑇 ∈ LinOp ∧ 𝑇 ∈ ConOp) → (normop𝑇) ∈ ℝ)

Theoremnmcoplb 28061 A lower bound for the norm of a continuous linear Hilbert space operator. Theorem 3.5(ii) of [Beran] p. 99. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
((𝑇 ∈ LinOp ∧ 𝑇 ∈ ConOp ∧ 𝐴 ∈ ℋ) → (norm‘(𝑇𝐴)) ≤ ((normop𝑇) · (norm𝐴)))

Theoremnmophmi 28062 The norm of the scalar product of a bounded linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
𝑇 ∈ BndLinOp       (𝐴 ∈ ℂ → (normop‘(𝐴 ·op 𝑇)) = ((abs‘𝐴) · (normop𝑇)))

Theorembdophmi 28063 The scalar product of a bounded linear operator is a bounded linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
𝑇 ∈ BndLinOp       (𝐴 ∈ ℂ → (𝐴 ·op 𝑇) ∈ BndLinOp)

Theoremlnconi 28064* Lemma for lnopconi 28065 and lnfnconi 28086. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
(𝑇𝐶𝑆 ∈ ℝ)    &   ((𝑇𝐶𝑦 ∈ ℋ) → (𝑁‘(𝑇𝑦)) ≤ (𝑆 · (norm𝑦)))    &   (𝑇𝐶 ↔ ∀𝑥 ∈ ℋ ∀𝑧 ∈ ℝ+𝑦 ∈ ℝ+𝑤 ∈ ℋ ((norm‘(𝑤 𝑥)) < 𝑦 → (𝑁‘((𝑇𝑤)𝑀(𝑇𝑥))) < 𝑧))    &   (𝑦 ∈ ℋ → (𝑁‘(𝑇𝑦)) ∈ ℝ)    &   ((𝑤 ∈ ℋ ∧ 𝑥 ∈ ℋ) → (𝑇‘(𝑤 𝑥)) = ((𝑇𝑤)𝑀(𝑇𝑥)))       (𝑇𝐶 ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℋ (𝑁‘(𝑇𝑦)) ≤ (𝑥 · (norm𝑦)))

Theoremlnopconi 28065* A condition equivalent to "𝑇 is continuous" when 𝑇 is linear. Theorem 3.5(iii) of [Beran] p. 99. (Contributed by NM, 7-Feb-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
𝑇 ∈ LinOp       (𝑇 ∈ ConOp ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℋ (norm‘(𝑇𝑦)) ≤ (𝑥 · (norm𝑦)))

Theoremlnopcon 28066* A condition equivalent to "𝑇 is continuous" when 𝑇 is linear. Theorem 3.5(iii) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
(𝑇 ∈ LinOp → (𝑇 ∈ ConOp ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℋ (norm‘(𝑇𝑦)) ≤ (𝑥 · (norm𝑦))))

Theoremlnopcnbd 28067 A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
(𝑇 ∈ LinOp → (𝑇 ∈ ConOp ↔ 𝑇 ∈ BndLinOp))

Theoremlncnopbd 28068 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. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
(𝑇 ∈ (LinOp ∩ ConOp) ↔ 𝑇 ∈ BndLinOp)

Theoremlncnbd 28069 A continuous linear operator is a bounded linear operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
(LinOp ∩ ConOp) = BndLinOp

Theoremlnopcnre 28070 A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
(𝑇 ∈ LinOp → (𝑇 ∈ ConOp ↔ (normop𝑇) ∈ ℝ))

Theoremlnfnli 28071 Basic property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
𝑇 ∈ LinFn       ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘((𝐴 · 𝐵) + 𝐶)) = ((𝐴 · (𝑇𝐵)) + (𝑇𝐶)))

Theoremlnfnfi 28072 A linear Hilbert space functional is a functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
𝑇 ∈ LinFn       𝑇: ℋ⟶ℂ

Theoremlnfn0i 28073 The value of a linear Hilbert space functional at zero is zero. Remark in [Beran] p. 99. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
𝑇 ∈ LinFn       (𝑇‘0) = 0

Theoremlnfnaddi 28074 Additive property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
𝑇 ∈ LinFn       ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 + 𝐵)) = ((𝑇𝐴) + (𝑇𝐵)))

Theoremlnfnmuli 28075 Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
𝑇 ∈ LinFn       ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 · 𝐵)) = (𝐴 · (𝑇𝐵)))

Theoremlnfnaddmuli 28076 Sum/product property of a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.)
𝑇 ∈ LinFn       ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘(𝐵 + (𝐴 · 𝐶))) = ((𝑇𝐵) + (𝐴 · (𝑇𝐶))))

Theoremlnfnsubi 28077 Subtraction property for a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.)
𝑇 ∈ LinFn       ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 𝐵)) = ((𝑇𝐴) − (𝑇𝐵)))

Theoremlnfn0 28078 The value of a linear Hilbert space functional at zero is zero. Remark in [Beran] p. 99. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
(𝑇 ∈ LinFn → (𝑇‘0) = 0)

Theoremlnfnmul 28079 Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
((𝑇 ∈ LinFn ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 · 𝐵)) = (𝐴 · (𝑇𝐵)))

Theoremnmbdfnlbi 28080 A lower bound for the norm of a bounded linear functional. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
(𝑇 ∈ LinFn ∧ (normfn𝑇) ∈ ℝ)       (𝐴 ∈ ℋ → (abs‘(𝑇𝐴)) ≤ ((normfn𝑇) · (norm𝐴)))

Theoremnmbdfnlb 28081 A lower bound for the norm of a bounded linear functional. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
((𝑇 ∈ LinFn ∧ (normfn𝑇) ∈ ℝ ∧ 𝐴 ∈ ℋ) → (abs‘(𝑇𝐴)) ≤ ((normfn𝑇) · (norm𝐴)))

Theoremnmcfnexi 28082 The norm of a continuous linear Hilbert space functional exists. Theorem 3.5(i) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
𝑇 ∈ LinFn    &   𝑇 ∈ ConFn       (normfn𝑇) ∈ ℝ

Theoremnmcfnlbi 28083 A lower bound for the norm of a continuous linear functional. Theorem 3.5(ii) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
𝑇 ∈ LinFn    &   𝑇 ∈ ConFn       (𝐴 ∈ ℋ → (abs‘(𝑇𝐴)) ≤ ((normfn𝑇) · (norm𝐴)))

Theoremnmcfnex 28084 The norm of a continuous linear Hilbert space functional exists. Theorem 3.5(i) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
((𝑇 ∈ LinFn ∧ 𝑇 ∈ ConFn) → (normfn𝑇) ∈ ℝ)

Theoremnmcfnlb 28085 A lower bound of the norm of a continuous linear Hilbert space functional. Theorem 3.5(ii) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
((𝑇 ∈ LinFn ∧ 𝑇 ∈ ConFn ∧ 𝐴 ∈ ℋ) → (abs‘(𝑇𝐴)) ≤ ((normfn𝑇) · (norm𝐴)))

Theoremlnfnconi 28086* A condition equivalent to "𝑇 is continuous" when 𝑇 is linear. Theorem 3.5(iii) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
𝑇 ∈ LinFn       (𝑇 ∈ ConFn ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℋ (abs‘(𝑇𝑦)) ≤ (𝑥 · (norm𝑦)))

Theoremlnfncon 28087* A condition equivalent to "𝑇 is continuous" when 𝑇 is linear. Theorem 3.5(iii) of [Beran] p. 99. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.)
(𝑇 ∈ LinFn → (𝑇 ∈ ConFn ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℋ (abs‘(𝑇𝑦)) ≤ (𝑥 · (norm𝑦))))

Theoremlnfncnbd 28088 A linear functional is continuous iff it is bounded. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
(𝑇 ∈ LinFn → (𝑇 ∈ ConFn ↔ (normfn𝑇) ∈ ℝ))

Theoremimaelshi 28089 The image of a subspace under a linear operator is a subspace. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
𝑇 ∈ LinOp    &   𝐴S       (𝑇𝐴) ∈ S

Theoremrnelshi 28090 The range of a linear operator is a subspace. (Contributed by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
𝑇 ∈ LinOp       ran 𝑇S

Theoremnlelshi 28091 The null space of a linear functional is a subspace. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
𝑇 ∈ LinFn       (null‘𝑇) ∈ S

Theoremnlelchi 28092 The null space of a continuous linear functional is a closed subspace. Remark 3.8 of [Beran] p. 103. (Contributed by NM, 11-Feb-2006.) (Proof shortened by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
𝑇 ∈ LinFn    &   𝑇 ∈ ConFn       (null‘𝑇) ∈ C

19.6.11  Riesz lemma

Theoremriesz3i 28093* A continuous linear functional can be expressed as an inner product. Existence part of Theorem 3.9 of [Beran] p. 104. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.)
𝑇 ∈ LinFn    &   𝑇 ∈ ConFn       𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇𝑣) = (𝑣 ·ih 𝑤)

Theoremriesz4i 28094* A continuous linear functional can be expressed as an inner product. Uniqueness part of Theorem 3.9 of [Beran] p. 104. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.)
𝑇 ∈ LinFn    &   𝑇 ∈ ConFn       ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇𝑣) = (𝑣 ·ih 𝑤)

Theoremriesz4 28095* A continuous linear functional can be expressed as an inner product. Uniqueness part of Theorem 3.9 of [Beran] p. 104. See riesz2 28097 for the bounded linear functional version. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.)
(𝑇 ∈ (LinFn ∩ ConFn) → ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇𝑣) = (𝑣 ·ih 𝑤))

Theoremriesz1 28096* 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 riesz2 28097. For the continuous linear functional version, see riesz3i 28093 and riesz4 28095. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
(𝑇 ∈ LinFn → ((normfn𝑇) ∈ ℝ ↔ ∃𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇𝑥) = (𝑥 ·ih 𝑦)))

Theoremriesz2 28097* 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 riesz1 28096. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
((𝑇 ∈ LinFn ∧ (normfn𝑇) ∈ ℝ) → ∃!𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇𝑥) = (𝑥 ·ih 𝑦))