HomeTheorem List (p. 290 of 429)
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. 290 of 429) | < 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-27903) |
Hilbert Space Explorer
(27904-29428) |
Users' Mathboxes
(29429-42879) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | lnopl 28901 | Basic linearity property of a linear Hilbert space operator. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
| ⊢ (((𝑇 ∈ LinOp ∧ 𝐴 ∈ ℂ) ∧ (𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)) → (𝑇‘((𝐴 ·ℎ 𝐵) +ℎ 𝐶)) = ((𝐴 ·ℎ (𝑇‘𝐵)) +ℎ (𝑇‘𝐶))) | ||
| Theorem | unop 28902 | Basic inner product property of a unitary operator. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ UniOp ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝑇‘𝐴) ·ih (𝑇‘𝐵)) = (𝐴 ·ih 𝐵)) | ||
| Theorem | unopf1o 28903 | A unitary operator in Hilbert space is one-to-one and onto. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ UniOp → 𝑇: ℋ–1-1-onto→ ℋ) | ||
| Theorem | unopnorm 28904 | A unitary operator is idempotent in the norm. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ UniOp ∧ 𝐴 ∈ ℋ) → (normℎ‘(𝑇‘𝐴)) = (normℎ‘𝐴)) | ||
| Theorem | cnvunop 28905 | The inverse (converse) of a unitary operator in Hilbert space is unitary. Theorem in [AkhiezerGlazman] p. 72. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ UniOp → ◡𝑇 ∈ UniOp) | ||
| Theorem | unopadj 28906 | The inverse (converse) of a unitary operator is its adjoint. Equation 2 of [AkhiezerGlazman] p. 72. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ UniOp ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝑇‘𝐴) ·ih 𝐵) = (𝐴 ·ih (◡𝑇‘𝐵))) | ||
| Theorem | unoplin 28907 | A unitary operator is linear. Theorem in [AkhiezerGlazman] p. 72. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ UniOp → 𝑇 ∈ LinOp) | ||
| Theorem | counop 28908 | The composition of two unitary operators is unitary. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
| ⊢ ((𝑆 ∈ UniOp ∧ 𝑇 ∈ UniOp) → (𝑆 ∘ 𝑇) ∈ UniOp) | ||
| Theorem | hmop 28909 | Basic inner product property of a Hermitian operator. (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ HrmOp ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih (𝑇‘𝐵)) = ((𝑇‘𝐴) ·ih 𝐵)) | ||
| Theorem | hmopre 28910 | The inner product of the value and argument of a Hermitian operator is real. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ HrmOp ∧ 𝐴 ∈ ℋ) → ((𝑇‘𝐴) ·ih 𝐴) ∈ ℝ) | ||
| Theorem | nmfnlb 28911 | A lower bound for a functional norm. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ℂ ∧ 𝐴 ∈ ℋ ∧ (normℎ‘𝐴) ≤ 1) → (abs‘(𝑇‘𝐴)) ≤ (normfn‘𝑇)) | ||
| Theorem | nmfnleub 28912* | An upper bound for the norm of a functional. (Contributed by NM, 24-May-2006.) (Revised by Mario Carneiro, 7-Sep-2014.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ℂ ∧ 𝐴 ∈ ℝ*) → ((normfn‘𝑇) ≤ 𝐴 ↔ ∀𝑥 ∈ ℋ ((normℎ‘𝑥) ≤ 1 → (abs‘(𝑇‘𝑥)) ≤ 𝐴))) | ||
| Theorem | nmfnleub2 28913* | An upper bound for the norm of a functional. (Contributed by NM, 24-May-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ℂ ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ ∀𝑥 ∈ ℋ (abs‘(𝑇‘𝑥)) ≤ (𝐴 · (normℎ‘𝑥))) → (normfn‘𝑇) ≤ 𝐴) | ||
| Theorem | nmfnge0 28914 | The norm of any Hilbert space functional is nonnegative. (Contributed by NM, 24-May-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ℂ → 0 ≤ (normfn‘𝑇)) | ||
| Theorem | elnlfn 28915 | Membership in the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ℂ → (𝐴 ∈ (null‘𝑇) ↔ (𝐴 ∈ ℋ ∧ (𝑇‘𝐴) = 0))) | ||
| Theorem | elnlfn2 28916 | Membership in the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ℂ ∧ 𝐴 ∈ (null‘𝑇)) → (𝑇‘𝐴) = 0) | ||
| Theorem | cnfnc 28917* | Basic continuity property of a continuous functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ ContFn ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℝ+) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ ℋ ((normℎ‘(𝑦 −ℎ 𝐴)) < 𝑥 → (abs‘((𝑇‘𝑦) − (𝑇‘𝐴))) < 𝐵)) | ||
| Theorem | lnfnl 28918 | Basic linearity property of a linear functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
| ⊢ (((𝑇 ∈ LinFn ∧ 𝐴 ∈ ℂ) ∧ (𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)) → (𝑇‘((𝐴 ·ℎ 𝐵) +ℎ 𝐶)) = ((𝐴 · (𝑇‘𝐵)) + (𝑇‘𝐶))) | ||
| Theorem | adjcl 28919 | Closure of the adjoint of a Hilbert space operator. (Contributed by NM, 17-Jun-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ) → ((adjℎ‘𝑇)‘𝐴) ∈ ℋ) | ||
| Theorem | adj1 28920 | Property of an adjoint Hilbert space operator. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih (𝑇‘𝐵)) = (((adjℎ‘𝑇)‘𝐴) ·ih 𝐵)) | ||
| Theorem | adj2 28921 | Property of an adjoint Hilbert space operator. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝑇‘𝐴) ·ih 𝐵) = (𝐴 ·ih ((adjℎ‘𝑇)‘𝐵))) | ||
| Theorem | adjeq 28922* | A property that determines the adjoint of a Hilbert space operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑆: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑆‘𝑦))) → (adjℎ‘𝑇) = 𝑆) | ||
| Theorem | adjadj 28923 | Double adjoint. Theorem 3.11(iv) of [Beran] p. 106. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ dom adjℎ → (adjℎ‘(adjℎ‘𝑇)) = 𝑇) | ||
| Theorem | adjvalval 28924* | Value of the value of the adjoint function. (Contributed by NM, 22-Feb-2006.) (Proof shortened by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ) → ((adjℎ‘𝑇)‘𝐴) = (℩𝑤 ∈ ℋ ∀𝑥 ∈ ℋ ((𝑇‘𝑥) ·ih 𝐴) = (𝑥 ·ih 𝑤))) | ||
| Theorem | unopadj2 28925 | The adjoint of a unitary operator is its inverse (converse). Equation 2 of [AkhiezerGlazman] p. 72. (Contributed by NM, 23-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ UniOp → (adjℎ‘𝑇) = ◡𝑇) | ||
| Theorem | hmopadj 28926 | A Hermitian operator is self-adjoint. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ HrmOp → (adjℎ‘𝑇) = 𝑇) | ||
| Theorem | hmdmadj 28927 | Every Hermitian operator has an adjoint. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ HrmOp → 𝑇 ∈ dom adjℎ) | ||
| Theorem | hmopadj2 28928 | An operator is Hermitian iff it is self-adjoint. Definition of Hermitian in [Halmos] p. 41. (Contributed by NM, 9-Apr-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ dom adjℎ → (𝑇 ∈ HrmOp ↔ (adjℎ‘𝑇) = 𝑇)) | ||
| Theorem | hmoplin 28929 | A Hermitian operator is linear. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ HrmOp → 𝑇 ∈ LinOp) | ||
| Theorem | brafval 28930* | The bra of a vector, expressed as ⟨𝐴 ∣ in Dirac notation. See df-bra 28837. (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (bra‘𝐴) = (𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐴))) | ||
| Theorem | braval 28931 | A bra-ket juxtaposition, expressed as ⟨𝐴 ∣ 𝐵⟩ in Dirac notation, equals the inner product of the vectors. Based on definition of bra in [Prugovecki] p. 186. (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((bra‘𝐴)‘𝐵) = (𝐵 ·ih 𝐴)) | ||
| Theorem | braadd 28932 | Linearity property of bra for addition. (Contributed by NM, 23-May-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((bra‘𝐴)‘(𝐵 +ℎ 𝐶)) = (((bra‘𝐴)‘𝐵) + ((bra‘𝐴)‘𝐶))) | ||
| Theorem | bramul 28933 | Linearity property of bra for multiplication. (Contributed by NM, 23-May-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((bra‘𝐴)‘(𝐵 ·ℎ 𝐶)) = (𝐵 · ((bra‘𝐴)‘𝐶))) | ||
| Theorem | brafn 28934 | The bra function is a functional. (Contributed by NM, 23-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (bra‘𝐴): ℋ⟶ℂ) | ||
| Theorem | bralnfn 28935 | The Dirac bra function is a linear functional. (Contributed by NM, 23-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (bra‘𝐴) ∈ LinFn) | ||
| Theorem | bracl 28936 | Closure of the bra function. (Contributed by NM, 23-May-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((bra‘𝐴)‘𝐵) ∈ ℂ) | ||
| Theorem | bra0 28937 | The Dirac bra of the zero vector. (Contributed by NM, 25-May-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.) |
| ⊢ (bra‘0ℎ) = ( ℋ × {0}) | ||
| Theorem | brafnmul 28938 | Anti-linearity property of bra functional for multiplication. (Contributed by NM, 31-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (bra‘(𝐴 ·ℎ 𝐵)) = ((∗‘𝐴) ·fn (bra‘𝐵))) | ||
| Theorem | kbfval 28939* | The outer product of two vectors, expressed as ∣ 𝐴⟩ ⟨𝐵 ∣ in Dirac notation. See df-kb 28838. (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ketbra 𝐵) = (𝑥 ∈ ℋ ↦ ((𝑥 ·ih 𝐵) ·ℎ 𝐴))) | ||
| Theorem | kbop 28940 | 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 28941 | 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 28942 | Multiplication property of outer product. (Contributed by NM, 31-May-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ketbra 𝐶) = (𝐵 ketbra ((∗‘𝐴) ·ℎ 𝐶))) | ||
| Theorem | kbpj 28943 | 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 28944* | 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 28945 | 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 28946 | Closure of an eigenvector of a Hilbert space operator. (Contributed by NM, 23-Mar-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ (eigvec‘𝑇)) → 𝐴 ∈ ℋ) | ||
| Theorem | eigvalval 28947 | 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 28948 | An eigenvalue is a complex number. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ (eigvec‘𝑇)) → ((eigval‘𝑇)‘𝐴) ∈ ℂ) | ||
| Theorem | eigvec1 28949 | Property of an eigenvector. (Contributed by NM, 12-Mar-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ (eigvec‘𝑇)) → ((𝑇‘𝐴) = (((eigval‘𝑇)‘𝐴) ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) | ||
| Theorem | eighmre 28950 | 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 28951 | 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 28952 | Value of the norm of the negative of a Hilbert space operator. Unlike nmophmi 29018, the operator does not have to be bounded. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (normop‘(-1 ·op 𝑇)) = (normop‘𝑇) | ||
| Theorem | lnop0 28953 | 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 28954 | Multiplicative property of a linear Hilbert space operator. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇 ∈ LinOp ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 ·ℎ 𝐵)) = (𝐴 ·ℎ (𝑇‘𝐵))) | ||
| Theorem | lnopli 28955 | Basic scalar product property of a linear Hilbert space operator. (Contributed by NM, 23-Jan-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘((𝐴 ·ℎ 𝐵) +ℎ 𝐶)) = ((𝐴 ·ℎ (𝑇‘𝐵)) +ℎ (𝑇‘𝐶))) | ||
| Theorem | lnopfi 28956 | A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 23-Jan-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp ⇒ ⊢ 𝑇: ℋ⟶ ℋ | ||
| Theorem | lnop0i 28957 | 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 28958 | Additive property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 +ℎ 𝐵)) = ((𝑇‘𝐴) +ℎ (𝑇‘𝐵))) | ||
| Theorem | lnopmuli 28959 | Multiplicative property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 ·ℎ 𝐵)) = (𝐴 ·ℎ (𝑇‘𝐵))) | ||
| Theorem | lnopaddmuli 28960 | Sum/product property of a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘(𝐵 +ℎ (𝐴 ·ℎ 𝐶))) = ((𝑇‘𝐵) +ℎ (𝐴 ·ℎ (𝑇‘𝐶)))) | ||
| Theorem | lnopsubi 28961 | Subtraction property for a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 −ℎ 𝐵)) = ((𝑇‘𝐴) −ℎ (𝑇‘𝐵))) | ||
| Theorem | lnopsubmuli 28962 | Subtraction/product property of a linear Hilbert space operator. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘(𝐵 −ℎ (𝐴 ·ℎ 𝐶))) = ((𝑇‘𝐵) −ℎ (𝐴 ·ℎ (𝑇‘𝐶)))) | ||
| Theorem | lnopmulsubi 28963 | Product/subtraction property of a linear Hilbert space operator. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘((𝐴 ·ℎ 𝐵) −ℎ 𝐶)) = ((𝐴 ·ℎ (𝑇‘𝐵)) −ℎ (𝑇‘𝐶))) | ||
| Theorem | homco2 28964 | Move a scalar product out of a composition of operators. The operator 𝑇 must be linear, unlike homco1 28788 that works for any operators. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈: ℋ⟶ ℋ) → (𝑇 ∘ (𝐴 ·op 𝑈)) = (𝐴 ·op (𝑇 ∘ 𝑈))) | ||
| Theorem | idunop 28965 | 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 28966 | The identically zero function is a continuous Hilbert space operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
| ⊢ 0hop ∈ ContOp | ||
| Theorem | 0cnfn 28967 | The identically zero function is a continuous Hilbert space functional. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
| ⊢ ( ℋ × {0}) ∈ ContFn | ||
| Theorem | idcnop 28968 | 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 28969 | The Hilbert space identity operator is a Hermitian operator. (Contributed by NM, 22-Apr-2006.) (New usage is discouraged.) |
| ⊢ Iop ∈ HrmOp | ||
| Theorem | 0hmop 28970 | The identically zero function is a Hermitian operator. (Contributed by NM, 8-Aug-2006.) (New usage is discouraged.) |
| ⊢ 0hop ∈ HrmOp | ||
| Theorem | 0lnop 28971 | The identically zero function is a linear Hilbert space operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
| ⊢ 0hop ∈ LinOp | ||
| Theorem | 0lnfn 28972 | The identically zero function is a linear Hilbert space functional. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
| ⊢ ( ℋ × {0}) ∈ LinFn | ||
| Theorem | nmop0 28973 | The norm of the zero operator is zero. (Contributed by NM, 8-Feb-2006.) (New usage is discouraged.) |
| ⊢ (normop‘ 0hop ) = 0 | ||
| Theorem | nmfn0 28974 | The norm of the identically zero functional is zero. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
| ⊢ (normfn‘( ℋ × {0})) = 0 | ||
| Theorem | hmopbdoptHIL 28975 | 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 28976 | Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri 28767 does not require linearity.) (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑅 ∈ LinOp & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑅 ∘ (𝑆 −op 𝑇)) = ((𝑅 ∘ 𝑆) −op (𝑅 ∘ 𝑇)) | ||
| Theorem | hoddi 28977 | Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri 28767 does not require linearity.) (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑅 ∈ LinOp ∧ 𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑅 ∘ (𝑆 −op 𝑇)) = ((𝑅 ∘ 𝑆) −op (𝑅 ∘ 𝑇))) | ||
| Theorem | nmop0h 28978 | The norm of any operator on the trivial Hilbert space is zero. (This is the reason we need ℋ ≠ 0ℋ in nmopun 29001.) (Contributed by NM, 24-Feb-2006.) (New usage is discouraged.) |
| ⊢ (( ℋ = 0ℋ ∧ 𝑇: ℋ⟶ ℋ) → (normop‘𝑇) = 0) | ||
| Theorem | idlnop 28979 | 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 28980 | The identically zero operator is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
| ⊢ 0hop ∈ BndLinOp | ||
| Theorem | adj0 28981 | Adjoint of the zero operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
| ⊢ (adjℎ‘ 0hop ) = 0hop | ||
| Theorem | nmlnop0iALT 28982 | 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 28983 | 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 28984 | 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 28985 | 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 28986 | 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 28987 | 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 28988 | The sum of two linear operators is linear. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑆 ∈ LinOp & ⊢ 𝑇 ∈ LinOp ⇒ ⊢ (𝑆 +op 𝑇) ∈ LinOp | ||
| Theorem | lnophdi 28989 | The difference of two linear operators is linear. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.) |
| ⊢ 𝑆 ∈ LinOp & ⊢ 𝑇 ∈ LinOp ⇒ ⊢ (𝑆 −op 𝑇) ∈ LinOp | ||
| Theorem | lnopcoi 28990 | The composition of two linear operators is linear. (Contributed by NM, 8-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑆 ∈ LinOp & ⊢ 𝑇 ∈ LinOp ⇒ ⊢ (𝑆 ∘ 𝑇) ∈ LinOp | ||
| Theorem | lnopco0i 28991 | 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 28992 | Lemma for lnopeq0i 28994. Apply the generalized polarization identity polid2i 28142 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 28993 | Lemma for lnopeq0i 28994. (Contributed by NM, 26-Jul-2006.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝑇‘𝐴) ·ih 𝐵) = (((((𝑇‘(𝐴 +ℎ 𝐵)) ·ih (𝐴 +ℎ 𝐵)) − ((𝑇‘(𝐴 −ℎ 𝐵)) ·ih (𝐴 −ℎ 𝐵))) + (i · (((𝑇‘(𝐴 +ℎ (i ·ℎ 𝐵))) ·ih (𝐴 +ℎ (i ·ℎ 𝐵))) − ((𝑇‘(𝐴 −ℎ (i ·ℎ 𝐵))) ·ih (𝐴 −ℎ (i ·ℎ 𝐵)))))) / 4)) | ||
| Theorem | lnopeq0i 28994* | A condition implying that a linear Hilbert space operator is identically zero. Unlike ho01i 28815 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 28995* | 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 28996* | 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 28997* | Lemma for lnopunii 28999. (Contributed by NM, 14-May-2005.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp & ⊢ ∀𝑥 ∈ ℋ (normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥) & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ (ℜ‘(𝐶 · ((𝑇‘𝐴) ·ih (𝑇‘𝐵)))) = (ℜ‘(𝐶 · (𝐴 ·ih 𝐵))) | ||
| Theorem | lnopunilem2 28998* | Lemma for lnopunii 28999. (Contributed by NM, 12-May-2005.) (New usage is discouraged.) |
| ⊢ 𝑇 ∈ LinOp & ⊢ ∀𝑥 ∈ ℋ (normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥) & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ ((𝑇‘𝐴) ·ih (𝑇‘𝐵)) = (𝐴 ·ih 𝐵) | ||
| Theorem | lnopunii 28999* | 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 29000* | 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ℎ‘𝑥))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |