![]() |
Metamath
Proof Explorer Theorem List (p. 321 of 491) | < 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: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lnopaddmuli 32001 | Sum/product property of a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘(𝐵 +ℎ (𝐴 ·ℎ 𝐶))) = ((𝑇‘𝐵) +ℎ (𝐴 ·ℎ (𝑇‘𝐶)))) | ||
Theorem | lnopsubi 32002 | Subtraction property for a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 −ℎ 𝐵)) = ((𝑇‘𝐴) −ℎ (𝑇‘𝐵))) | ||
Theorem | lnopsubmuli 32003 | Subtraction/product property of a linear Hilbert space operator. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘(𝐵 −ℎ (𝐴 ·ℎ 𝐶))) = ((𝑇‘𝐵) −ℎ (𝐴 ·ℎ (𝑇‘𝐶)))) | ||
Theorem | lnopmulsubi 32004 | Product/subtraction property of a linear Hilbert space operator. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘((𝐴 ·ℎ 𝐵) −ℎ 𝐶)) = ((𝐴 ·ℎ (𝑇‘𝐵)) −ℎ (𝑇‘𝐶))) | ||
Theorem | homco2 32005 | Move a scalar product out of a composition of operators. The operator 𝑇 must be linear, unlike homco1 31829 that works for any operators. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈: ℋ⟶ ℋ) → (𝑇 ∘ (𝐴 ·op 𝑈)) = (𝐴 ·op (𝑇 ∘ 𝑈))) | ||
Theorem | idunop 32006 | The identity function (restricted to Hilbert space) is a unitary operator. (Contributed by NM, 21-Jan-2006.) (New usage is discouraged.) |
⊢ ( I ↾ ℋ) ∈ UniOp | ||
Theorem | 0cnop 32007 | The identically zero function is a continuous Hilbert space operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
⊢ 0hop ∈ ContOp | ||
Theorem | 0cnfn 32008 | The identically zero function is a continuous Hilbert space functional. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
⊢ ( ℋ × {0}) ∈ ContFn | ||
Theorem | idcnop 32009 | The identity function (restricted to Hilbert space) is a continuous operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
⊢ ( I ↾ ℋ) ∈ ContOp | ||
Theorem | idhmop 32010 | The Hilbert space identity operator is a Hermitian operator. (Contributed by NM, 22-Apr-2006.) (New usage is discouraged.) |
⊢ Iop ∈ HrmOp | ||
Theorem | 0hmop 32011 | The identically zero function is a Hermitian operator. (Contributed by NM, 8-Aug-2006.) (New usage is discouraged.) |
⊢ 0hop ∈ HrmOp | ||
Theorem | 0lnop 32012 | The identically zero function is a linear Hilbert space operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
⊢ 0hop ∈ LinOp | ||
Theorem | 0lnfn 32013 | The identically zero function is a linear Hilbert space functional. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
⊢ ( ℋ × {0}) ∈ LinFn | ||
Theorem | nmop0 32014 | The norm of the zero operator is zero. (Contributed by NM, 8-Feb-2006.) (New usage is discouraged.) |
⊢ (normop‘ 0hop ) = 0 | ||
Theorem | nmfn0 32015 | The norm of the identically zero functional is zero. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
⊢ (normfn‘( ℋ × {0})) = 0 | ||
Theorem | hmopbdoptHIL 32016 | A Hermitian operator is a bounded linear operator (Hellinger-Toeplitz Theorem). (Contributed by NM, 18-Jan-2008.) (New usage is discouraged.) |
⊢ (𝑇 ∈ HrmOp → 𝑇 ∈ BndLinOp) | ||
Theorem | hoddii 32017 | Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri 31808 does not require linearity.) (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
⊢ 𝑅 ∈ LinOp & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑅 ∘ (𝑆 −op 𝑇)) = ((𝑅 ∘ 𝑆) −op (𝑅 ∘ 𝑇)) | ||
Theorem | hoddi 32018 | Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri 31808 does not require linearity.) (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
⊢ ((𝑅 ∈ LinOp ∧ 𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑅 ∘ (𝑆 −op 𝑇)) = ((𝑅 ∘ 𝑆) −op (𝑅 ∘ 𝑇))) | ||
Theorem | nmop0h 32019 | The norm of any operator on the trivial Hilbert space is zero. (This is the reason we need ℋ ≠ 0ℋ in nmopun 32042.) (Contributed by NM, 24-Feb-2006.) (New usage is discouraged.) |
⊢ (( ℋ = 0ℋ ∧ 𝑇: ℋ⟶ ℋ) → (normop‘𝑇) = 0) | ||
Theorem | idlnop 32020 | The identity function (restricted to Hilbert space) is a linear operator. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.) |
⊢ ( I ↾ ℋ) ∈ LinOp | ||
Theorem | 0bdop 32021 | The identically zero operator is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
⊢ 0hop ∈ BndLinOp | ||
Theorem | adj0 32022 | Adjoint of the zero operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
⊢ (adjℎ‘ 0hop ) = 0hop | ||
Theorem | nmlnop0iALT 32023 | 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 ) | ||
Theorem | nmlnop0iHIL 32024 | A linear operator with a zero norm is identically zero. (Contributed by NM, 18-Jan-2008.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((normop‘𝑇) = 0 ↔ 𝑇 = 0hop ) | ||
Theorem | nmlnopgt0i 32025 | 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‘𝑇)) | ||
Theorem | nmlnop0 32026 | A linear operator with a zero norm is identically zero. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ LinOp → ((normop‘𝑇) = 0 ↔ 𝑇 = 0hop )) | ||
Theorem | nmlnopne0 32027 | A linear operator with a nonzero norm is nonzero. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ LinOp → ((normop‘𝑇) ≠ 0 ↔ 𝑇 ≠ 0hop )) | ||
Theorem | lnopmi 32028 | The scalar product of a linear operator is a linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp ⇒ ⊢ (𝐴 ∈ ℂ → (𝐴 ·op 𝑇) ∈ LinOp) | ||
Theorem | lnophsi 32029 | The sum of two linear operators is linear. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
⊢ 𝑆 ∈ LinOp & ⊢ 𝑇 ∈ LinOp ⇒ ⊢ (𝑆 +op 𝑇) ∈ LinOp | ||
Theorem | lnophdi 32030 | The difference of two linear operators is linear. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.) |
⊢ 𝑆 ∈ LinOp & ⊢ 𝑇 ∈ LinOp ⇒ ⊢ (𝑆 −op 𝑇) ∈ LinOp | ||
Theorem | lnopcoi 32031 | The composition of two linear operators is linear. (Contributed by NM, 8-Mar-2006.) (New usage is discouraged.) |
⊢ 𝑆 ∈ LinOp & ⊢ 𝑇 ∈ LinOp ⇒ ⊢ (𝑆 ∘ 𝑇) ∈ LinOp | ||
Theorem | lnopco0i 32032 | 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) | ||
Theorem | lnopeq0lem1 32033 | Lemma for lnopeq0i 32035. Apply the generalized polarization identity polid2i 31185 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) | ||
Theorem | lnopeq0lem2 32034 | Lemma for lnopeq0i 32035. (Contributed by NM, 26-Jul-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝑇‘𝐴) ·ih 𝐵) = (((((𝑇‘(𝐴 +ℎ 𝐵)) ·ih (𝐴 +ℎ 𝐵)) − ((𝑇‘(𝐴 −ℎ 𝐵)) ·ih (𝐴 −ℎ 𝐵))) + (i · (((𝑇‘(𝐴 +ℎ (i ·ℎ 𝐵))) ·ih (𝐴 +ℎ (i ·ℎ 𝐵))) − ((𝑇‘(𝐴 −ℎ (i ·ℎ 𝐵))) ·ih (𝐴 −ℎ (i ·ℎ 𝐵)))))) / 4)) | ||
Theorem | lnopeq0i 32035* | A condition implying that a linear Hilbert space operator is identically zero. Unlike ho01i 31856 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 ) | ||
Theorem | lnopeqi 32036* | 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 𝑥) ↔ 𝑇 = 𝑈) | ||
Theorem | lnopeq 32037* | 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 𝑥) ↔ 𝑇 = 𝑈)) | ||
Theorem | lnopunilem1 32038* | Lemma for lnopunii 32040. (Contributed by NM, 14-May-2005.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp & ⊢ ∀𝑥 ∈ ℋ (normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥) & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ (ℜ‘(𝐶 · ((𝑇‘𝐴) ·ih (𝑇‘𝐵)))) = (ℜ‘(𝐶 · (𝐴 ·ih 𝐵))) | ||
Theorem | lnopunilem2 32039* | Lemma for lnopunii 32040. (Contributed by NM, 12-May-2005.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp & ⊢ ∀𝑥 ∈ ℋ (normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥) & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ ((𝑇‘𝐴) ·ih (𝑇‘𝐵)) = (𝐴 ·ih 𝐵) | ||
Theorem | lnopunii 32040* | 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 | ||
Theorem | elunop2 32041* | 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ℎ‘𝑥))) | ||
Theorem | nmopun 32042 | Norm of a unitary Hilbert space operator. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.) |
⊢ (( ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → (normop‘𝑇) = 1) | ||
Theorem | unopbd 32043 | A unitary operator is a bounded linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ UniOp → 𝑇 ∈ BndLinOp) | ||
Theorem | lnophmlem1 32044* | Lemma for lnophmi 32046. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝑇 ∈ LinOp & ⊢ ∀𝑥 ∈ ℋ (𝑥 ·ih (𝑇‘𝑥)) ∈ ℝ ⇒ ⊢ (𝐴 ·ih (𝑇‘𝐴)) ∈ ℝ | ||
Theorem | lnophmlem2 32045* | Lemma for lnophmi 32046. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝑇 ∈ LinOp & ⊢ ∀𝑥 ∈ ℋ (𝑥 ·ih (𝑇‘𝑥)) ∈ ℝ ⇒ ⊢ (𝐴 ·ih (𝑇‘𝐵)) = ((𝑇‘𝐴) ·ih 𝐵) | ||
Theorem | lnophmi 32046* | 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 | ||
Theorem | lnophm 32047* | 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) | ||
Theorem | hmops 32048 | The sum of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 +op 𝑈) ∈ HrmOp) | ||
Theorem | hmopm 32049 | 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) | ||
Theorem | hmopd 32050 | The difference of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 −op 𝑈) ∈ HrmOp) | ||
Theorem | hmopco 32051 | The composition of two commuting Hermitian operators is Hermitian. (Contributed by NM, 22-Aug-2006.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) → (𝑇 ∘ 𝑈) ∈ HrmOp) | ||
Theorem | nmbdoplbi 32052 | 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ℎ‘𝐴))) | ||
Theorem | nmbdoplb 32053 | 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ℎ‘𝐴))) | ||
Theorem | nmcexi 32054* | Lemma for nmcopexi 32055 and nmcfnexi 32079. 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) ·ℎ 𝑥)))) ⇒ ⊢ (𝑆‘𝑇) ∈ ℝ | ||
Theorem | nmcopexi 32055 | 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‘𝑇) ∈ ℝ | ||
Theorem | nmcoplbi 32056 | 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ℎ‘𝐴))) | ||
Theorem | nmcopex 32057 | 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‘𝑇) ∈ ℝ) | ||
Theorem | nmcoplb 32058 | 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ℎ‘𝐴))) | ||
Theorem | nmophmi 32059 | 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‘𝑇))) | ||
Theorem | bdophmi 32060 | 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) | ||
Theorem | lnconi 32061* | Lemma for lnopconi 32062 and lnfnconi 32083. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ 𝐶 → 𝑆 ∈ ℝ) & ⊢ ((𝑇 ∈ 𝐶 ∧ 𝑦 ∈ ℋ) → (𝑁‘(𝑇‘𝑦)) ≤ (𝑆 · (normℎ‘𝑦))) & ⊢ (𝑇 ∈ 𝐶 ↔ ∀𝑥 ∈ ℋ ∀𝑧 ∈ ℝ+ ∃𝑦 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑦 → (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥))) < 𝑧)) & ⊢ (𝑦 ∈ ℋ → (𝑁‘(𝑇‘𝑦)) ∈ ℝ) & ⊢ ((𝑤 ∈ ℋ ∧ 𝑥 ∈ ℋ) → (𝑇‘(𝑤 −ℎ 𝑥)) = ((𝑇‘𝑤)𝑀(𝑇‘𝑥))) ⇒ ⊢ (𝑇 ∈ 𝐶 ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 · (normℎ‘𝑦))) | ||
Theorem | lnopconi 32062* | 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ℎ‘𝑦))) | ||
Theorem | lnopcon 32063* | 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ℎ‘𝑦)))) | ||
Theorem | lnopcnbd 32064 | A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ LinOp → (𝑇 ∈ ContOp ↔ 𝑇 ∈ BndLinOp)) | ||
Theorem | lncnopbd 32065 | 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) | ||
Theorem | lncnbd 32066 | A continuous linear operator is a bounded linear operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
⊢ (LinOp ∩ ContOp) = BndLinOp | ||
Theorem | lnopcnre 32067 | A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ LinOp → (𝑇 ∈ ContOp ↔ (normop‘𝑇) ∈ ℝ)) | ||
Theorem | lnfnli 32068 | Basic property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinFn ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘((𝐴 ·ℎ 𝐵) +ℎ 𝐶)) = ((𝐴 · (𝑇‘𝐵)) + (𝑇‘𝐶))) | ||
Theorem | lnfnfi 32069 | A linear Hilbert space functional is a functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinFn ⇒ ⊢ 𝑇: ℋ⟶ℂ | ||
Theorem | lnfn0i 32070 | 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 | ||
Theorem | lnfnaddi 32071 | Additive property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinFn ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 +ℎ 𝐵)) = ((𝑇‘𝐴) + (𝑇‘𝐵))) | ||
Theorem | lnfnmuli 32072 | Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinFn ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 ·ℎ 𝐵)) = (𝐴 · (𝑇‘𝐵))) | ||
Theorem | lnfnaddmuli 32073 | Sum/product property of a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinFn ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘(𝐵 +ℎ (𝐴 ·ℎ 𝐶))) = ((𝑇‘𝐵) + (𝐴 · (𝑇‘𝐶)))) | ||
Theorem | lnfnsubi 32074 | Subtraction property for a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinFn ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 −ℎ 𝐵)) = ((𝑇‘𝐴) − (𝑇‘𝐵))) | ||
Theorem | lnfn0 32075 | 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) | ||
Theorem | lnfnmul 32076 | Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ LinFn ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 ·ℎ 𝐵)) = (𝐴 · (𝑇‘𝐵))) | ||
Theorem | nmbdfnlbi 32077 | 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ℎ‘𝐴))) | ||
Theorem | nmbdfnlb 32078 | 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ℎ‘𝐴))) | ||
Theorem | nmcfnexi 32079 | 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‘𝑇) ∈ ℝ | ||
Theorem | nmcfnlbi 32080 | 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ℎ‘𝐴))) | ||
Theorem | nmcfnex 32081 | 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‘𝑇) ∈ ℝ) | ||
Theorem | nmcfnlb 32082 | 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ℎ‘𝐴))) | ||
Theorem | lnfnconi 32083* | 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ℎ‘𝑦))) | ||
Theorem | lnfncon 32084* | 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ℎ‘𝑦)))) | ||
Theorem | lnfncnbd 32085 | A linear functional is continuous iff it is bounded. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ LinFn → (𝑇 ∈ ContFn ↔ (normfn‘𝑇) ∈ ℝ)) | ||
Theorem | imaelshi 32086 | 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ℋ | ||
Theorem | rnelshi 32087 | The range of a linear operator is a subspace. (Contributed by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp ⇒ ⊢ ran 𝑇 ∈ Sℋ | ||
Theorem | nlelshi 32088 | 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ℋ | ||
Theorem | nlelchi 32089 | 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ℋ | ||
Theorem | riesz3i 32090* | 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 𝑤) | ||
Theorem | riesz4i 32091* | 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 𝑤) | ||
Theorem | riesz4 32092* | A continuous linear functional can be expressed as an inner product. Uniqueness part of Theorem 3.9 of [Beran] p. 104. See riesz2 32094 for the bounded linear functional version. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ (LinFn ∩ ContFn) → ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih 𝑤)) | ||
Theorem | riesz1 32093* | 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 32094. For the continuous linear functional version, see riesz3i 32090 and riesz4 32092. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ LinFn → ((normfn‘𝑇) ∈ ℝ ↔ ∃𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑥 ·ih 𝑦))) | ||
Theorem | riesz2 32094* | 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 32093. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ LinFn ∧ (normfn‘𝑇) ∈ ℝ) → ∃!𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑥 ·ih 𝑦)) | ||
Theorem | cnlnadjlem1 32095* | Lemma for cnlnadji 32104 (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 𝑦)) | ||
Theorem | cnlnadjlem2 32096* | Lemma for cnlnadji 32104. 𝐺 is a continuous linear functional. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ContOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) ⇒ ⊢ (𝑦 ∈ ℋ → (𝐺 ∈ LinFn ∧ 𝐺 ∈ ContFn)) | ||
Theorem | cnlnadjlem3 32097* | Lemma for cnlnadji 32104. By riesz4 32092, 𝐵 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 𝑤)) ⇒ ⊢ (𝑦 ∈ ℋ → 𝐵 ∈ ℋ) | ||
Theorem | cnlnadjlem4 32098* | Lemma for cnlnadji 32104. 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 𝑤)) & ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵) ⇒ ⊢ (𝐴 ∈ ℋ → (𝐹‘𝐴) ∈ ℋ) | ||
Theorem | cnlnadjlem5 32099* | Lemma for cnlnadji 32104. 𝐹 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 (𝐹‘𝐴))) | ||
Theorem | cnlnadjlem6 32100* | Lemma for cnlnadji 32104. 𝐹 is linear. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp & ⊢ 𝑇 ∈ ContOp & ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) & ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) & ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵) ⇒ ⊢ 𝐹 ∈ LinOp |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |