HomeTheorem List (p. 320 of 499)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 320 of 499) | < 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-30866) |
Hilbert Space Explorer
(30867-32389) |
Users' Mathboxes
(32390-49810) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | kbop 31901 | The outer product of two vectors, expressed as ∣ 𝐴⟩⟨𝐵 ∣ in Dirac notation, is an operator. (Contributed by NM, 30-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ketbra 𝐵): ℋ⟶ ℋ) | ||
| Theorem | kbval 31902 | The value of the operator resulting from the outer product ∣ 𝐴⟩ ⟨𝐵 ∣ of two vectors. Equation 8.1 of [Prugovecki] p. 376. (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ketbra 𝐵)‘𝐶) = ((𝐶 ·ih 𝐵) ·ℎ 𝐴)) | ||
| Theorem | kbmul 31903 | Multiplication property of outer product. (Contributed by NM, 31-May-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ketbra 𝐶) = (𝐵 ketbra ((∗‘𝐴) ·ℎ 𝐶))) | ||
| Theorem | kbpj 31904 | If a vector 𝐴 has norm 1, the outer product ∣ 𝐴⟩⟨𝐴 ∣ is the projector onto the subspace spanned by 𝐴. http://en.wikipedia.org/wiki/Bra-ket#Linear%5Foperators. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ (normℎ‘𝐴) = 1) → (𝐴 ketbra 𝐴) = (projℎ‘(span‘{𝐴}))) | ||
| Theorem | eleigvec 31905* | Membership in the set of eigenvectors of a Hilbert space operator. (Contributed by NM, 11-Mar-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (𝐴 ∈ (eigvec‘𝑇) ↔ (𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ∧ ∃𝑥 ∈ ℂ (𝑇‘𝐴) = (𝑥 ·ℎ 𝐴)))) | ||
| Theorem | eleigvec2 31906 | Membership in the set of eigenvectors of a Hilbert space operator. (Contributed by NM, 18-Mar-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (𝐴 ∈ (eigvec‘𝑇) ↔ (𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ∧ (𝑇‘𝐴) ∈ (span‘{𝐴})))) | ||
| Theorem | eleigveccl 31907 | Closure of an eigenvector of a Hilbert space operator. (Contributed by NM, 23-Mar-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ (eigvec‘𝑇)) → 𝐴 ∈ ℋ) | ||
| Theorem | eigvalval 31908 | The eigenvalue of an eigenvector of a Hilbert space operator. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ (eigvec‘𝑇)) → ((eigval‘𝑇)‘𝐴) = (((𝑇‘𝐴) ·ih 𝐴) / ((normℎ‘𝐴)↑2))) | ||
| Theorem | eigvalcl 31909 | An eigenvalue is a complex number. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ (eigvec‘𝑇)) → ((eigval‘𝑇)‘𝐴) ∈ ℂ) | ||
| Theorem | eigvec1 31910 | Property of an eigenvector. (Contributed by NM, 12-Mar-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ (eigvec‘𝑇)) → ((𝑇‘𝐴) = (((eigval‘𝑇)‘𝐴) ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) | ||
| Theorem | eighmre 31911 | The eigenvalues of a Hermitian operator are real. Equation 1.30 of [Hughes] p. 49. (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ HrmOp ∧ 𝐴 ∈ (eigvec‘𝑇)) → ((eigval‘𝑇)‘𝐴) ∈ ℝ) | ||
| Theorem | eighmorth 31912 | Eigenvectors of a Hermitian operator with distinct eigenvalues are orthogonal. Equation 1.31 of [Hughes] p. 49. (Contributed by NM, 23-Mar-2006.) (New usage is discouraged.) |
| ⊢ (((𝑇 ∈ HrmOp ∧ 𝐴 ∈ (eigvec‘𝑇)) ∧ (𝐵 ∈ (eigvec‘𝑇) ∧ ((eigval‘𝑇)‘𝐴) ≠ ((eigval‘𝑇)‘𝐵))) → (𝐴 ·ih 𝐵) = 0) | ||
| Theorem | nmopnegi 31913 | Value of the norm of the negative of a Hilbert space operator. Unlike nmophmi 31979, the operator does not have to be bounded. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (normop‘(-1 ·op 𝑇)) = (normop‘𝑇) | ||
| Theorem | lnop0 31914 | The value of a linear Hilbert space operator at zero is zero. Remark in [Beran] p. 99. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ LinOp → (𝑇‘0ℎ) = 0ℎ) | ||
| Theorem | lnopmul 31915 | Multiplicative property of a linear Hilbert space operator. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ LinOp ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 ·ℎ 𝐵)) = (𝐴 ·ℎ (𝑇‘𝐵))) | ||
| Theorem | lnopli 31916 | Basic scalar product property of a linear Hilbert space operator. (Contributed by NM, 23-Jan-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘((𝐴 ·ℎ 𝐵) +ℎ 𝐶)) = ((𝐴 ·ℎ (𝑇‘𝐵)) +ℎ (𝑇‘𝐶))) | ||
| Theorem | lnopfi 31917 | A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 23-Jan-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp ⇒ ⊢ 𝑇: ℋ⟶ ℋ | ||
| Theorem | lnop0i 31918 | 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ℎ | ||
| Theorem | lnopaddi 31919 | Additive property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 +ℎ 𝐵)) = ((𝑇‘𝐴) +ℎ (𝑇‘𝐵))) | ||
| Theorem | lnopmuli 31920 | Multiplicative property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 ·ℎ 𝐵)) = (𝐴 ·ℎ (𝑇‘𝐵))) | ||
| Theorem | lnopaddmuli 31921 | Sum/product property of a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘(𝐵 +ℎ (𝐴 ·ℎ 𝐶))) = ((𝑇‘𝐵) +ℎ (𝐴 ·ℎ (𝑇‘𝐶)))) | ||
| Theorem | lnopsubi 31922 | Subtraction property for a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 −ℎ 𝐵)) = ((𝑇‘𝐴) −ℎ (𝑇‘𝐵))) | ||
| Theorem | lnopsubmuli 31923 | Subtraction/product property of a linear Hilbert space operator. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘(𝐵 −ℎ (𝐴 ·ℎ 𝐶))) = ((𝑇‘𝐵) −ℎ (𝐴 ·ℎ (𝑇‘𝐶)))) | ||
| Theorem | lnopmulsubi 31924 | Product/subtraction property of a linear Hilbert space operator. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘((𝐴 ·ℎ 𝐵) −ℎ 𝐶)) = ((𝐴 ·ℎ (𝑇‘𝐵)) −ℎ (𝑇‘𝐶))) | ||
| Theorem | homco2 31925 | Move a scalar product out of a composition of operators. The operator 𝑇 must be linear, unlike homco1 31749 that works for any operators. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈: ℋ⟶ ℋ) → (𝑇 ∘ (𝐴 ·op 𝑈)) = (𝐴 ·op (𝑇 ∘ 𝑈))) | ||
| Theorem | idunop 31926 | 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 31927 | The identically zero function is a continuous Hilbert space operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
| ⊢ 0hop ∈ ContOp | ||
| Theorem | 0cnfn 31928 | The identically zero function is a continuous Hilbert space functional. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
| ⊢ ( ℋ × {0}) ∈ ContFn | ||
| Theorem | idcnop 31929 | 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 31930 | The Hilbert space identity operator is a Hermitian operator. (Contributed by NM, 22-Apr-2006.) (New usage is discouraged.) |
| ⊢ Iop ∈ HrmOp | ||
| Theorem | 0hmop 31931 | The identically zero function is a Hermitian operator. (Contributed by NM, 8-Aug-2006.) (New usage is discouraged.) |
| ⊢ 0hop ∈ HrmOp | ||
| Theorem | 0lnop 31932 | The identically zero function is a linear Hilbert space operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
| ⊢ 0hop ∈ LinOp | ||
| Theorem | 0lnfn 31933 | The identically zero function is a linear Hilbert space functional. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
| ⊢ ( ℋ × {0}) ∈ LinFn | ||
| Theorem | nmop0 31934 | The norm of the zero operator is zero. (Contributed by NM, 8-Feb-2006.) (New usage is discouraged.) |
| ⊢ (normop‘ 0hop ) = 0 | ||
| Theorem | nmfn0 31935 | The norm of the identically zero functional is zero. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
| ⊢ (normfn‘( ℋ × {0})) = 0 | ||
| Theorem | hmopbdoptHIL 31936 | 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 31937 | Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri 31728 does not require linearity.) (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑅 ∈ LinOp & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑅 ∘ (𝑆 −op 𝑇)) = ((𝑅 ∘ 𝑆) −op (𝑅 ∘ 𝑇)) | ||
| Theorem | hoddi 31938 | Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri 31728 does not require linearity.) (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑅 ∈ LinOp ∧ 𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑅 ∘ (𝑆 −op 𝑇)) = ((𝑅 ∘ 𝑆) −op (𝑅 ∘ 𝑇))) | ||
| Theorem | nmop0h 31939 | The norm of any operator on the trivial Hilbert space is zero. (This is the reason we need ℋ ≠ 0ℋ in nmopun 31962.) (Contributed by NM, 24-Feb-2006.) (New usage is discouraged.) |
| ⊢ (( ℋ = 0ℋ ∧ 𝑇: ℋ⟶ ℋ) → (normop‘𝑇) = 0) | ||
| Theorem | idlnop 31940 | 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 31941 | The identically zero operator is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
| ⊢ 0hop ∈ BndLinOp | ||
| Theorem | adj0 31942 | Adjoint of the zero operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
| ⊢ (adjℎ‘ 0hop ) = 0hop | ||
| Theorem | nmlnop0iALT 31943 | 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 31944 | 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 31945 | 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 31946 | 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 31947 | 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 31948 | 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 31949 | The sum of two linear operators is linear. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑆 ∈ LinOp & ⊢ 𝑇 ∈ LinOp ⇒ ⊢ (𝑆 +op 𝑇) ∈ LinOp | ||
| Theorem | lnophdi 31950 | The difference of two linear operators is linear. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.) |
| ⊢ 𝑆 ∈ LinOp & ⊢ 𝑇 ∈ LinOp ⇒ ⊢ (𝑆 −op 𝑇) ∈ LinOp | ||
| Theorem | lnopcoi 31951 | The composition of two linear operators is linear. (Contributed by NM, 8-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑆 ∈ LinOp & ⊢ 𝑇 ∈ LinOp ⇒ ⊢ (𝑆 ∘ 𝑇) ∈ LinOp | ||
| Theorem | lnopco0i 31952 | 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 31953 | Lemma for lnopeq0i 31955. Apply the generalized polarization identity polid2i 31105 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 31954 | Lemma for lnopeq0i 31955. (Contributed by NM, 26-Jul-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝑇‘𝐴) ·ih 𝐵) = (((((𝑇‘(𝐴 +ℎ 𝐵)) ·ih (𝐴 +ℎ 𝐵)) − ((𝑇‘(𝐴 −ℎ 𝐵)) ·ih (𝐴 −ℎ 𝐵))) + (i · (((𝑇‘(𝐴 +ℎ (i ·ℎ 𝐵))) ·ih (𝐴 +ℎ (i ·ℎ 𝐵))) − ((𝑇‘(𝐴 −ℎ (i ·ℎ 𝐵))) ·ih (𝐴 −ℎ (i ·ℎ 𝐵)))))) / 4)) | ||
| Theorem | lnopeq0i 31955* | A condition implying that a linear Hilbert space operator is identically zero. Unlike ho01i 31776 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 31956* | 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 31957* | 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 31958* | Lemma for lnopunii 31960. (Contributed by NM, 14-May-2005.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp & ⊢ ∀𝑥 ∈ ℋ (normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥) & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ (ℜ‘(𝐶 · ((𝑇‘𝐴) ·ih (𝑇‘𝐵)))) = (ℜ‘(𝐶 · (𝐴 ·ih 𝐵))) | ||
| Theorem | lnopunilem2 31959* | Lemma for lnopunii 31960. (Contributed by NM, 12-May-2005.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp & ⊢ ∀𝑥 ∈ ℋ (normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥) & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ ((𝑇‘𝐴) ·ih (𝑇‘𝐵)) = (𝐴 ·ih 𝐵) | ||
| Theorem | lnopunii 31960* | 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 31961* | 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 31962 | Norm of a unitary Hilbert space operator. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.) |
| ⊢ (( ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → (normop‘𝑇) = 1) | ||
| Theorem | unopbd 31963 | A unitary operator is a bounded linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ UniOp → 𝑇 ∈ BndLinOp) | ||
| Theorem | lnophmlem1 31964* | Lemma for lnophmi 31966. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝑇 ∈ LinOp & ⊢ ∀𝑥 ∈ ℋ (𝑥 ·ih (𝑇‘𝑥)) ∈ ℝ ⇒ ⊢ (𝐴 ·ih (𝑇‘𝐴)) ∈ ℝ | ||
| Theorem | lnophmlem2 31965* | Lemma for lnophmi 31966. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝑇 ∈ LinOp & ⊢ ∀𝑥 ∈ ℋ (𝑥 ·ih (𝑇‘𝑥)) ∈ ℝ ⇒ ⊢ (𝐴 ·ih (𝑇‘𝐵)) = ((𝑇‘𝐴) ·ih 𝐵) | ||
| Theorem | lnophmi 31966* | 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 31967* | 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 31968 | The sum of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 +op 𝑈) ∈ HrmOp) | ||
| Theorem | hmopm 31969 | 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 31970 | The difference of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 −op 𝑈) ∈ HrmOp) | ||
| Theorem | hmopco 31971 | The composition of two commuting Hermitian operators is Hermitian. (Contributed by NM, 22-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) → (𝑇 ∘ 𝑈) ∈ HrmOp) | ||
| Theorem | nmbdoplbi 31972 | 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 31973 | 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 31974* | Lemma for nmcopexi 31975 and nmcfnexi 31999. 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 31975 | 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 31976 | 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 31977 | 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 31978 | 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 31979 | 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 31980 | 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 31981* | Lemma for lnopconi 31982 and lnfnconi 32003. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ 𝐶 → 𝑆 ∈ ℝ) & ⊢ ((𝑇 ∈ 𝐶 ∧ 𝑦 ∈ ℋ) → (𝑁‘(𝑇‘𝑦)) ≤ (𝑆 · (normℎ‘𝑦))) & ⊢ (𝑇 ∈ 𝐶 ↔ ∀𝑥 ∈ ℋ ∀𝑧 ∈ ℝ+ ∃𝑦 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑦 → (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥))) < 𝑧)) & ⊢ (𝑦 ∈ ℋ → (𝑁‘(𝑇‘𝑦)) ∈ ℝ) & ⊢ ((𝑤 ∈ ℋ ∧ 𝑥 ∈ ℋ) → (𝑇‘(𝑤 −ℎ 𝑥)) = ((𝑇‘𝑤)𝑀(𝑇‘𝑥))) ⇒ ⊢ (𝑇 ∈ 𝐶 ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 · (normℎ‘𝑦))) | ||
| Theorem | lnopconi 31982* | 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 31983* | 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 31984 | A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ LinOp → (𝑇 ∈ ContOp ↔ 𝑇 ∈ BndLinOp)) | ||
| Theorem | lncnopbd 31985 | 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 31986 | A continuous linear operator is a bounded linear operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
| ⊢ (LinOp ∩ ContOp) = BndLinOp | ||
| Theorem | lnopcnre 31987 | A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ LinOp → (𝑇 ∈ ContOp ↔ (normop‘𝑇) ∈ ℝ)) | ||
| Theorem | lnfnli 31988 | Basic property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinFn ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘((𝐴 ·ℎ 𝐵) +ℎ 𝐶)) = ((𝐴 · (𝑇‘𝐵)) + (𝑇‘𝐶))) | ||
| Theorem | lnfnfi 31989 | A linear Hilbert space functional is a functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinFn ⇒ ⊢ 𝑇: ℋ⟶ℂ | ||
| Theorem | lnfn0i 31990 | 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 31991 | Additive property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinFn ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 +ℎ 𝐵)) = ((𝑇‘𝐴) + (𝑇‘𝐵))) | ||
| Theorem | lnfnmuli 31992 | Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinFn ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 ·ℎ 𝐵)) = (𝐴 · (𝑇‘𝐵))) | ||
| Theorem | lnfnaddmuli 31993 | Sum/product property of a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinFn ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘(𝐵 +ℎ (𝐴 ·ℎ 𝐶))) = ((𝑇‘𝐵) + (𝐴 · (𝑇‘𝐶)))) | ||
| Theorem | lnfnsubi 31994 | Subtraction property for a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinFn ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 −ℎ 𝐵)) = ((𝑇‘𝐴) − (𝑇‘𝐵))) | ||
| Theorem | lnfn0 31995 | 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 31996 | Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ LinFn ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 ·ℎ 𝐵)) = (𝐴 · (𝑇‘𝐵))) | ||
| Theorem | nmbdfnlbi 31997 | 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 31998 | 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 31999 | 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 32000 | 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ℎ‘𝐴))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |