Home | Metamath
Proof Explorer Theorem List (p. 298 of 450) | < 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-28698) |
Hilbert Space Explorer
(28699-30221) |
Users' Mathboxes
(30222-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | counop 29701 | The composition of two unitary operators is unitary. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.) |
⊢ ((𝑆 ∈ UniOp ∧ 𝑇 ∈ UniOp) → (𝑆 ∘ 𝑇) ∈ UniOp) | ||
Theorem | hmop 29702 | Basic inner product property of a Hermitian operator. (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ HrmOp ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih (𝑇‘𝐵)) = ((𝑇‘𝐴) ·ih 𝐵)) | ||
Theorem | hmopre 29703 | 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 29704 | A lower bound for a functional norm. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
⊢ ((𝑇: ℋ⟶ℂ ∧ 𝐴 ∈ ℋ ∧ (normℎ‘𝐴) ≤ 1) → (abs‘(𝑇‘𝐴)) ≤ (normfn‘𝑇)) | ||
Theorem | nmfnleub 29705* | 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 29706* | 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 29707 | The norm of any Hilbert space functional is nonnegative. (Contributed by NM, 24-May-2006.) (New usage is discouraged.) |
⊢ (𝑇: ℋ⟶ℂ → 0 ≤ (normfn‘𝑇)) | ||
Theorem | elnlfn 29708 | 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 29709 | 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 29710* | 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 29711 | Basic linearity property of a linear functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
⊢ (((𝑇 ∈ LinFn ∧ 𝐴 ∈ ℂ) ∧ (𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)) → (𝑇‘((𝐴 ·ℎ 𝐵) +ℎ 𝐶)) = ((𝐴 · (𝑇‘𝐵)) + (𝑇‘𝐶))) | ||
Theorem | adjcl 29712 | Closure of the adjoint of a Hilbert space operator. (Contributed by NM, 17-Jun-2006.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ) → ((adjℎ‘𝑇)‘𝐴) ∈ ℋ) | ||
Theorem | adj1 29713 | Property of an adjoint Hilbert space operator. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih (𝑇‘𝐵)) = (((adjℎ‘𝑇)‘𝐴) ·ih 𝐵)) | ||
Theorem | adj2 29714 | Property of an adjoint Hilbert space operator. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝑇‘𝐴) ·ih 𝐵) = (𝐴 ·ih ((adjℎ‘𝑇)‘𝐵))) | ||
Theorem | adjeq 29715* | 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 29716 | 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 29717* | 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 29718 | 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 29719 | A Hermitian operator is self-adjoint. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ HrmOp → (adjℎ‘𝑇) = 𝑇) | ||
Theorem | hmdmadj 29720 | Every Hermitian operator has an adjoint. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ HrmOp → 𝑇 ∈ dom adjℎ) | ||
Theorem | hmopadj2 29721 | 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 29722 | A Hermitian operator is linear. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ HrmOp → 𝑇 ∈ LinOp) | ||
Theorem | brafval 29723* | The bra of a vector, expressed as 〈𝐴 ∣ in Dirac notation. See df-bra 29630. (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (bra‘𝐴) = (𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐴))) | ||
Theorem | braval 29724 | 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 29725 | Linearity property of bra for addition. (Contributed by NM, 23-May-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((bra‘𝐴)‘(𝐵 +ℎ 𝐶)) = (((bra‘𝐴)‘𝐵) + ((bra‘𝐴)‘𝐶))) | ||
Theorem | bramul 29726 | Linearity property of bra for multiplication. (Contributed by NM, 23-May-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((bra‘𝐴)‘(𝐵 ·ℎ 𝐶)) = (𝐵 · ((bra‘𝐴)‘𝐶))) | ||
Theorem | brafn 29727 | 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 29728 | 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 29729 | Closure of the bra function. (Contributed by NM, 23-May-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((bra‘𝐴)‘𝐵) ∈ ℂ) | ||
Theorem | bra0 29730 | 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 29731 | 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 29732* | The outer product of two vectors, expressed as ∣ 𝐴〉 〈𝐵 ∣ in Dirac notation. See df-kb 29631. (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ketbra 𝐵) = (𝑥 ∈ ℋ ↦ ((𝑥 ·ih 𝐵) ·ℎ 𝐴))) | ||
Theorem | kbop 29733 | 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 29734 | 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 29735 | Multiplication property of outer product. (Contributed by NM, 31-May-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ketbra 𝐶) = (𝐵 ketbra ((∗‘𝐴) ·ℎ 𝐶))) | ||
Theorem | kbpj 29736 | 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 29737* | 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 29738 | 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 29739 | Closure of an eigenvector of a Hilbert space operator. (Contributed by NM, 23-Mar-2006.) (New usage is discouraged.) |
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ (eigvec‘𝑇)) → 𝐴 ∈ ℋ) | ||
Theorem | eigvalval 29740 | 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 29741 | An eigenvalue is a complex number. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ (eigvec‘𝑇)) → ((eigval‘𝑇)‘𝐴) ∈ ℂ) | ||
Theorem | eigvec1 29742 | Property of an eigenvector. (Contributed by NM, 12-Mar-2006.) (New usage is discouraged.) |
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ (eigvec‘𝑇)) → ((𝑇‘𝐴) = (((eigval‘𝑇)‘𝐴) ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) | ||
Theorem | eighmre 29743 | 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 29744 | 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 29745 | Value of the norm of the negative of a Hilbert space operator. Unlike nmophmi 29811, the operator does not have to be bounded. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (normop‘(-1 ·op 𝑇)) = (normop‘𝑇) | ||
Theorem | lnop0 29746 | 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 29747 | Multiplicative property of a linear Hilbert space operator. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ LinOp ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 ·ℎ 𝐵)) = (𝐴 ·ℎ (𝑇‘𝐵))) | ||
Theorem | lnopli 29748 | Basic scalar product property of a linear Hilbert space operator. (Contributed by NM, 23-Jan-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘((𝐴 ·ℎ 𝐵) +ℎ 𝐶)) = ((𝐴 ·ℎ (𝑇‘𝐵)) +ℎ (𝑇‘𝐶))) | ||
Theorem | lnopfi 29749 | A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 23-Jan-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp ⇒ ⊢ 𝑇: ℋ⟶ ℋ | ||
Theorem | lnop0i 29750 | 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 29751 | Additive property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 +ℎ 𝐵)) = ((𝑇‘𝐴) +ℎ (𝑇‘𝐵))) | ||
Theorem | lnopmuli 29752 | Multiplicative property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 ·ℎ 𝐵)) = (𝐴 ·ℎ (𝑇‘𝐵))) | ||
Theorem | lnopaddmuli 29753 | Sum/product property of a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘(𝐵 +ℎ (𝐴 ·ℎ 𝐶))) = ((𝑇‘𝐵) +ℎ (𝐴 ·ℎ (𝑇‘𝐶)))) | ||
Theorem | lnopsubi 29754 | Subtraction property for a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 −ℎ 𝐵)) = ((𝑇‘𝐴) −ℎ (𝑇‘𝐵))) | ||
Theorem | lnopsubmuli 29755 | Subtraction/product property of a linear Hilbert space operator. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘(𝐵 −ℎ (𝐴 ·ℎ 𝐶))) = ((𝑇‘𝐵) −ℎ (𝐴 ·ℎ (𝑇‘𝐶)))) | ||
Theorem | lnopmulsubi 29756 | Product/subtraction property of a linear Hilbert space operator. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘((𝐴 ·ℎ 𝐵) −ℎ 𝐶)) = ((𝐴 ·ℎ (𝑇‘𝐵)) −ℎ (𝑇‘𝐶))) | ||
Theorem | homco2 29757 | Move a scalar product out of a composition of operators. The operator 𝑇 must be linear, unlike homco1 29581 that works for any operators. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈: ℋ⟶ ℋ) → (𝑇 ∘ (𝐴 ·op 𝑈)) = (𝐴 ·op (𝑇 ∘ 𝑈))) | ||
Theorem | idunop 29758 | 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 29759 | The identically zero function is a continuous Hilbert space operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
⊢ 0hop ∈ ContOp | ||
Theorem | 0cnfn 29760 | The identically zero function is a continuous Hilbert space functional. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
⊢ ( ℋ × {0}) ∈ ContFn | ||
Theorem | idcnop 29761 | 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 29762 | The Hilbert space identity operator is a Hermitian operator. (Contributed by NM, 22-Apr-2006.) (New usage is discouraged.) |
⊢ Iop ∈ HrmOp | ||
Theorem | 0hmop 29763 | The identically zero function is a Hermitian operator. (Contributed by NM, 8-Aug-2006.) (New usage is discouraged.) |
⊢ 0hop ∈ HrmOp | ||
Theorem | 0lnop 29764 | The identically zero function is a linear Hilbert space operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
⊢ 0hop ∈ LinOp | ||
Theorem | 0lnfn 29765 | The identically zero function is a linear Hilbert space functional. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
⊢ ( ℋ × {0}) ∈ LinFn | ||
Theorem | nmop0 29766 | The norm of the zero operator is zero. (Contributed by NM, 8-Feb-2006.) (New usage is discouraged.) |
⊢ (normop‘ 0hop ) = 0 | ||
Theorem | nmfn0 29767 | The norm of the identically zero functional is zero. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
⊢ (normfn‘( ℋ × {0})) = 0 | ||
Theorem | hmopbdoptHIL 29768 | 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 29769 | Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri 29560 does not require linearity.) (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
⊢ 𝑅 ∈ LinOp & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑅 ∘ (𝑆 −op 𝑇)) = ((𝑅 ∘ 𝑆) −op (𝑅 ∘ 𝑇)) | ||
Theorem | hoddi 29770 | Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri 29560 does not require linearity.) (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
⊢ ((𝑅 ∈ LinOp ∧ 𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑅 ∘ (𝑆 −op 𝑇)) = ((𝑅 ∘ 𝑆) −op (𝑅 ∘ 𝑇))) | ||
Theorem | nmop0h 29771 | The norm of any operator on the trivial Hilbert space is zero. (This is the reason we need ℋ ≠ 0ℋ in nmopun 29794.) (Contributed by NM, 24-Feb-2006.) (New usage is discouraged.) |
⊢ (( ℋ = 0ℋ ∧ 𝑇: ℋ⟶ ℋ) → (normop‘𝑇) = 0) | ||
Theorem | idlnop 29772 | 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 29773 | The identically zero operator is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
⊢ 0hop ∈ BndLinOp | ||
Theorem | adj0 29774 | Adjoint of the zero operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
⊢ (adjℎ‘ 0hop ) = 0hop | ||
Theorem | nmlnop0iALT 29775 | 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 29776 | 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 29777 | 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 29778 | 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 29779 | 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 29780 | 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 29781 | The sum of two linear operators is linear. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
⊢ 𝑆 ∈ LinOp & ⊢ 𝑇 ∈ LinOp ⇒ ⊢ (𝑆 +op 𝑇) ∈ LinOp | ||
Theorem | lnophdi 29782 | The difference of two linear operators is linear. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.) |
⊢ 𝑆 ∈ LinOp & ⊢ 𝑇 ∈ LinOp ⇒ ⊢ (𝑆 −op 𝑇) ∈ LinOp | ||
Theorem | lnopcoi 29783 | The composition of two linear operators is linear. (Contributed by NM, 8-Mar-2006.) (New usage is discouraged.) |
⊢ 𝑆 ∈ LinOp & ⊢ 𝑇 ∈ LinOp ⇒ ⊢ (𝑆 ∘ 𝑇) ∈ LinOp | ||
Theorem | lnopco0i 29784 | 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 29785 | Lemma for lnopeq0i 29787. Apply the generalized polarization identity polid2i 28937 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 29786 | Lemma for lnopeq0i 29787. (Contributed by NM, 26-Jul-2006.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝑇‘𝐴) ·ih 𝐵) = (((((𝑇‘(𝐴 +ℎ 𝐵)) ·ih (𝐴 +ℎ 𝐵)) − ((𝑇‘(𝐴 −ℎ 𝐵)) ·ih (𝐴 −ℎ 𝐵))) + (i · (((𝑇‘(𝐴 +ℎ (i ·ℎ 𝐵))) ·ih (𝐴 +ℎ (i ·ℎ 𝐵))) − ((𝑇‘(𝐴 −ℎ (i ·ℎ 𝐵))) ·ih (𝐴 −ℎ (i ·ℎ 𝐵)))))) / 4)) | ||
Theorem | lnopeq0i 29787* | A condition implying that a linear Hilbert space operator is identically zero. Unlike ho01i 29608 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 29788* | 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 29789* | 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 29790* | Lemma for lnopunii 29792. (Contributed by NM, 14-May-2005.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp & ⊢ ∀𝑥 ∈ ℋ (normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥) & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ (ℜ‘(𝐶 · ((𝑇‘𝐴) ·ih (𝑇‘𝐵)))) = (ℜ‘(𝐶 · (𝐴 ·ih 𝐵))) | ||
Theorem | lnopunilem2 29791* | Lemma for lnopunii 29792. (Contributed by NM, 12-May-2005.) (New usage is discouraged.) |
⊢ 𝑇 ∈ LinOp & ⊢ ∀𝑥 ∈ ℋ (normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥) & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ ((𝑇‘𝐴) ·ih (𝑇‘𝐵)) = (𝐴 ·ih 𝐵) | ||
Theorem | lnopunii 29792* | 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 29793* | 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 29794 | Norm of a unitary Hilbert space operator. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.) |
⊢ (( ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → (normop‘𝑇) = 1) | ||
Theorem | unopbd 29795 | A unitary operator is a bounded linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
⊢ (𝑇 ∈ UniOp → 𝑇 ∈ BndLinOp) | ||
Theorem | lnophmlem1 29796* | Lemma for lnophmi 29798. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝑇 ∈ LinOp & ⊢ ∀𝑥 ∈ ℋ (𝑥 ·ih (𝑇‘𝑥)) ∈ ℝ ⇒ ⊢ (𝐴 ·ih (𝑇‘𝐴)) ∈ ℝ | ||
Theorem | lnophmlem2 29797* | Lemma for lnophmi 29798. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝑇 ∈ LinOp & ⊢ ∀𝑥 ∈ ℋ (𝑥 ·ih (𝑇‘𝑥)) ∈ ℝ ⇒ ⊢ (𝐴 ·ih (𝑇‘𝐵)) = ((𝑇‘𝐴) ·ih 𝐵) | ||
Theorem | lnophmi 29798* | 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 29799* | 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 29800 | The sum of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 +op 𝑈) ∈ HrmOp) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |