 Home Metamath Proof ExplorerTheorem List (p. 295 of 435) < 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-28331) Hilbert Space Explorer (28332-29856) Users' Mathboxes (29857-43448)

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

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

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

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

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

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

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

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

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

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

Theoremnmlnop0iALT 29410 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 29411 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 29412 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 29413 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 29414 A linear operator with a nonzero norm is nonzero. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)
(𝑇 ∈ LinOp → ((normop𝑇) ≠ 0 ↔ 𝑇 ≠ 0hop ))

Theoremlnopmi 29415 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 29416 The sum of two linear operators is linear. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
𝑆 ∈ LinOp    &   𝑇 ∈ LinOp       (𝑆 +op 𝑇) ∈ LinOp

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

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

Theoremlnopco0i 29419 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 29420 Lemma for lnopeq0i 29422. Apply the generalized polarization identity polid2i 28570 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 29421 Lemma for lnopeq0i 29422. (Contributed by NM, 26-Jul-2006.) (New usage is discouraged.)
𝑇 ∈ LinOp       ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝑇𝐴) ·ih 𝐵) = (((((𝑇‘(𝐴 + 𝐵)) ·ih (𝐴 + 𝐵)) − ((𝑇‘(𝐴 𝐵)) ·ih (𝐴 𝐵))) + (i · (((𝑇‘(𝐴 + (i · 𝐵))) ·ih (𝐴 + (i · 𝐵))) − ((𝑇‘(𝐴 (i · 𝐵))) ·ih (𝐴 (i · 𝐵)))))) / 4))

Theoremlnopeq0i 29422* A condition implying that a linear Hilbert space operator is identically zero. Unlike ho01i 29243 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 29423* 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 29424* 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 29425* Lemma for lnopunii 29427. (Contributed by NM, 14-May-2005.) (New usage is discouraged.)
𝑇 ∈ LinOp    &   𝑥 ∈ ℋ (norm‘(𝑇𝑥)) = (norm𝑥)    &   𝐴 ∈ ℋ    &   𝐵 ∈ ℋ    &   𝐶 ∈ ℂ       (ℜ‘(𝐶 · ((𝑇𝐴) ·ih (𝑇𝐵)))) = (ℜ‘(𝐶 · (𝐴 ·ih 𝐵)))

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

Theoremlnopunii 29427* 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 29428* 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 29429 Norm of a unitary Hilbert space operator. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.)
(( ℋ ≠ 0𝑇 ∈ UniOp) → (normop𝑇) = 1)

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

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

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

Theoremlnophmi 29433* 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 29434* 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 29435 The sum of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 +op 𝑈) ∈ HrmOp)

Theoremhmopm 29436 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 29437 The difference of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇op 𝑈) ∈ HrmOp)

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

Theoremnmbdoplbi 29439 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 29440 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 29441* Lemma for nmcopexi 29442 and nmcfnexi 29466. 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 29442 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    &   𝑇 ∈ ContOp       (normop𝑇) ∈ ℝ

Theoremnmcoplbi 29443 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    &   𝑇 ∈ ContOp       (𝐴 ∈ ℋ → (norm‘(𝑇𝐴)) ≤ ((normop𝑇) · (norm𝐴)))

Theoremnmcopex 29444 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 ∧ 𝑇 ∈ ContOp) → (normop𝑇) ∈ ℝ)

Theoremnmcoplb 29445 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 ∧ 𝑇 ∈ ContOp ∧ 𝐴 ∈ ℋ) → (norm‘(𝑇𝐴)) ≤ ((normop𝑇) · (norm𝐴)))

Theoremnmophmi 29446 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 29447 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 29448* Lemma for lnopconi 29449 and lnfnconi 29470. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
(𝑇𝐶𝑆 ∈ ℝ)    &   ((𝑇𝐶𝑦 ∈ ℋ) → (𝑁‘(𝑇𝑦)) ≤ (𝑆 · (norm𝑦)))    &   (𝑇𝐶 ↔ ∀𝑥 ∈ ℋ ∀𝑧 ∈ ℝ+𝑦 ∈ ℝ+𝑤 ∈ ℋ ((norm‘(𝑤 𝑥)) < 𝑦 → (𝑁‘((𝑇𝑤)𝑀(𝑇𝑥))) < 𝑧))    &   (𝑦 ∈ ℋ → (𝑁‘(𝑇𝑦)) ∈ ℝ)    &   ((𝑤 ∈ ℋ ∧ 𝑥 ∈ ℋ) → (𝑇‘(𝑤 𝑥)) = ((𝑇𝑤)𝑀(𝑇𝑥)))       (𝑇𝐶 ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℋ (𝑁‘(𝑇𝑦)) ≤ (𝑥 · (norm𝑦)))

Theoremlnopconi 29449* 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       (𝑇 ∈ ContOp ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℋ (norm‘(𝑇𝑦)) ≤ (𝑥 · (norm𝑦)))

Theoremlnopcon 29450* 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 → (𝑇 ∈ ContOp ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℋ (norm‘(𝑇𝑦)) ≤ (𝑥 · (norm𝑦))))

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

Theoremlncnopbd 29452 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 ∩ ContOp) ↔ 𝑇 ∈ BndLinOp)

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

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

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

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

Theoremlnfn0i 29457 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 29458 Additive property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
𝑇 ∈ LinFn       ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 + 𝐵)) = ((𝑇𝐴) + (𝑇𝐵)))

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

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

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

Theoremlnfn0 29462 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 29463 Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
((𝑇 ∈ LinFn ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 · 𝐵)) = (𝐴 · (𝑇𝐵)))

Theoremnmbdfnlbi 29464 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 29465 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 29466 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    &   𝑇 ∈ ContFn       (normfn𝑇) ∈ ℝ

Theoremnmcfnlbi 29467 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    &   𝑇 ∈ ContFn       (𝐴 ∈ ℋ → (abs‘(𝑇𝐴)) ≤ ((normfn𝑇) · (norm𝐴)))

Theoremnmcfnex 29468 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 ∧ 𝑇 ∈ ContFn) → (normfn𝑇) ∈ ℝ)

Theoremnmcfnlb 29469 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 ∧ 𝑇 ∈ ContFn ∧ 𝐴 ∈ ℋ) → (abs‘(𝑇𝐴)) ≤ ((normfn𝑇) · (norm𝐴)))

Theoremlnfnconi 29470* 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       (𝑇 ∈ ContFn ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℋ (abs‘(𝑇𝑦)) ≤ (𝑥 · (norm𝑦)))

Theoremlnfncon 29471* 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 → (𝑇 ∈ ContFn ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℋ (abs‘(𝑇𝑦)) ≤ (𝑥 · (norm𝑦))))

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

Theoremimaelshi 29473 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 29474 The range of a linear operator is a subspace. (Contributed by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
𝑇 ∈ LinOp       ran 𝑇S

Theoremnlelshi 29475 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 29476 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    &   𝑇 ∈ ContFn       (null‘𝑇) ∈ C

19.6.11  Riesz lemma

Theoremriesz3i 29477* 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    &   𝑇 ∈ ContFn       𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇𝑣) = (𝑣 ·ih 𝑤)

Theoremriesz4i 29478* 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    &   𝑇 ∈ ContFn       ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇𝑣) = (𝑣 ·ih 𝑤)

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

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

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

Theoremcnlnadjlem1 29482* Lemma for cnlnadji 29491 (Theorem 3.10 of [Beran] p. 104: every continuous linear operator has an adjoint). The value of the auxiliary functional 𝐺. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.)
𝑇 ∈ LinOp    &   𝑇 ∈ ContOp    &   𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇𝑔) ·ih 𝑦))       (𝐴 ∈ ℋ → (𝐺𝐴) = ((𝑇𝐴) ·ih 𝑦))

Theoremcnlnadjlem2 29483* Lemma for cnlnadji 29491. 𝐺 is a continuous linear functional. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.)
𝑇 ∈ LinOp    &   𝑇 ∈ ContOp    &   𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇𝑔) ·ih 𝑦))       (𝑦 ∈ ℋ → (𝐺 ∈ LinFn ∧ 𝐺 ∈ ContFn))

Theoremcnlnadjlem3 29484* Lemma for cnlnadji 29491. By riesz4 29479, 𝐵 is the unique vector such that (𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤) for all 𝑣. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.)
𝑇 ∈ LinOp    &   𝑇 ∈ ContOp    &   𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇𝑔) ·ih 𝑦))    &   𝐵 = (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))       (𝑦 ∈ ℋ → 𝐵 ∈ ℋ)

Theoremcnlnadjlem4 29485* Lemma for cnlnadji 29491. The values of auxiliary function 𝐹 are vectors. (Contributed by NM, 17-Feb-2006.) (Proof shortened by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
𝑇 ∈ LinOp    &   𝑇 ∈ ContOp    &   𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇𝑔) ·ih 𝑦))    &   𝐵 = (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))    &   𝐹 = (𝑦 ∈ ℋ ↦ 𝐵)       (𝐴 ∈ ℋ → (𝐹𝐴) ∈ ℋ)

Theoremcnlnadjlem5 29486* Lemma for cnlnadji 29491. 𝐹 is an adjoint of 𝑇 (later, we will show it is unique). (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
𝑇 ∈ LinOp    &   𝑇 ∈ ContOp    &   𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇𝑔) ·ih 𝑦))    &   𝐵 = (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))    &   𝐹 = (𝑦 ∈ ℋ ↦ 𝐵)       ((𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝑇𝐶) ·ih 𝐴) = (𝐶 ·ih (𝐹𝐴)))

Theoremcnlnadjlem6 29487* Lemma for cnlnadji 29491. 𝐹 is linear. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.)
𝑇 ∈ LinOp    &   𝑇 ∈ ContOp    &   𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇𝑔) ·ih 𝑦))    &   𝐵 = (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))    &   𝐹 = (𝑦 ∈ ℋ ↦ 𝐵)       𝐹 ∈ LinOp

Theoremcnlnadjlem7 29488* Lemma for cnlnadji 29491. Helper lemma to show that 𝐹 is continuous. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
𝑇 ∈ LinOp    &   𝑇 ∈ ContOp    &   𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇𝑔) ·ih 𝑦))    &   𝐵 = (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))    &   𝐹 = (𝑦 ∈ ℋ ↦ 𝐵)       (𝐴 ∈ ℋ → (norm‘(𝐹𝐴)) ≤ ((normop𝑇) · (norm𝐴)))

Theoremcnlnadjlem8 29489* Lemma for cnlnadji 29491. 𝐹 is continuous. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.)
𝑇 ∈ LinOp    &   𝑇 ∈ ContOp    &   𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇𝑔) ·ih 𝑦))    &   𝐵 = (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))    &   𝐹 = (𝑦 ∈ ℋ ↦ 𝐵)       𝐹 ∈ ContOp

Theoremcnlnadjlem9 29490* Lemma for cnlnadji 29491. 𝐹 provides an example showing the existence of a continuous linear adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
𝑇 ∈ LinOp    &   𝑇 ∈ ContOp    &   𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇𝑔) ·ih 𝑦))    &   𝐵 = (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))    &   𝐹 = (𝑦 ∈ ℋ ↦ 𝐵)       𝑡 ∈ (LinOp ∩ ContOp)∀𝑥 ∈ ℋ ∀𝑧 ∈ ℋ ((𝑇𝑥) ·ih 𝑧) = (𝑥 ·ih (𝑡𝑧))

Theoremcnlnadji 29491* Every continuous linear operator has an adjoint. Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
𝑇 ∈ LinOp    &   𝑇 ∈ ContOp       𝑡 ∈ (LinOp ∩ ContOp)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑡𝑦))

Theoremcnlnadjeui 29492* Every continuous linear operator has a unique adjoint. Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
𝑇 ∈ LinOp    &   𝑇 ∈ ContOp       ∃!𝑡 ∈ (LinOp ∩ ContOp)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑡𝑦))

Theoremcnlnadjeu 29493* Every continuous linear operator has a unique adjoint. Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)
(𝑇 ∈ (LinOp ∩ ContOp) → ∃!𝑡 ∈ (LinOp ∩ ContOp)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑡𝑦)))

Theoremcnlnadj 29494* Every continuous linear operator has an adjoint. Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
(𝑇 ∈ (LinOp ∩ ContOp) → ∃𝑡 ∈ (LinOp ∩ ContOp)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑡𝑦)))

Theoremcnlnssadj 29495 Every continuous linear Hilbert space operator has an adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
(LinOp ∩ ContOp) ⊆ dom adj

Theorembdopssadj 29496 Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)

Theorembdopadj 29497 Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.)
(𝑇 ∈ BndLinOp → 𝑇 ∈ dom adj)

Theoremadjbdln 29498 The adjoint of a bounded linear operator is a bounded linear operator. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)
(𝑇 ∈ BndLinOp → (adj𝑇) ∈ BndLinOp)

Theoremadjbdlnb 29499 An operator is bounded and linear iff its adjoint is. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)
(𝑇 ∈ BndLinOp ↔ (adj𝑇) ∈ BndLinOp)

Theoremadjbd1o 29500 The mapping of adjoints of bounded linear operators is one-to-one onto. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)