HomeTheorem List (p. 319 of 489)
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. 319 of 489) | < 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-30950) |
Hilbert Space Explorer
(30951-32473) |
Users' Mathboxes
(32474-48899) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | hosubcli 31801 | Mapping of difference of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑆 −op 𝑇): ℋ⟶ ℋ | ||
| Theorem | hoaddfni 31802 | Functionality of sum of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑆 +op 𝑇) Fn ℋ | ||
| Theorem | hosubfni 31803 | Functionality of difference of Hilbert space operators. (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑆 −op 𝑇) Fn ℋ | ||
| Theorem | hoaddcomi 31804 | Commutativity of sum of Hilbert space operators. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑆 +op 𝑇) = (𝑇 +op 𝑆) | ||
| Theorem | hosubcl 31805 | Mapping of difference of Hilbert space operators. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑆 −op 𝑇): ℋ⟶ ℋ) | ||
| Theorem | hoaddcom 31806 | Commutativity of sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑆 +op 𝑇) = (𝑇 +op 𝑆)) | ||
| Theorem | hodsi 31807 | Relationship between Hilbert space operator difference and sum. (Contributed by NM, 17-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((𝑅 −op 𝑆) = 𝑇 ↔ (𝑆 +op 𝑇) = 𝑅) | ||
| Theorem | hoaddassi 31808 | Associativity of sum of Hilbert space operators. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((𝑅 +op 𝑆) +op 𝑇) = (𝑅 +op (𝑆 +op 𝑇)) | ||
| Theorem | hoadd12i 31809 | Commutative/associative law for Hilbert space operator sum that swaps the first two terms. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
| ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑅 +op (𝑆 +op 𝑇)) = (𝑆 +op (𝑅 +op 𝑇)) | ||
| Theorem | hoadd32i 31810 | Commutative/associative law for Hilbert space operator sum that swaps the second and third terms. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.) |
| ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((𝑅 +op 𝑆) +op 𝑇) = ((𝑅 +op 𝑇) +op 𝑆) | ||
| Theorem | hocadddiri 31811 | Distributive law for Hilbert space operator sum. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((𝑅 +op 𝑆) ∘ 𝑇) = ((𝑅 ∘ 𝑇) +op (𝑆 ∘ 𝑇)) | ||
| Theorem | hocsubdiri 31812 | Distributive law for Hilbert space operator difference. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((𝑅 −op 𝑆) ∘ 𝑇) = ((𝑅 ∘ 𝑇) −op (𝑆 ∘ 𝑇)) | ||
| Theorem | ho2coi 31813 | Double composition of Hilbert space operators. (Contributed by NM, 1-Dec-2000.) (New usage is discouraged.) |
| ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝐴 ∈ ℋ → (((𝑅 ∘ 𝑆) ∘ 𝑇)‘𝐴) = (𝑅‘(𝑆‘(𝑇‘𝐴)))) | ||
| Theorem | hoaddass 31814 | Associativity of sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑅: ℋ⟶ ℋ ∧ 𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → ((𝑅 +op 𝑆) +op 𝑇) = (𝑅 +op (𝑆 +op 𝑇))) | ||
| Theorem | hoadd32 31815 | Commutative/associative law for Hilbert space operator sum that swaps the second and third terms. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑅: ℋ⟶ ℋ ∧ 𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → ((𝑅 +op 𝑆) +op 𝑇) = ((𝑅 +op 𝑇) +op 𝑆)) | ||
| Theorem | hoadd4 31816 | Rearrangement of 4 terms in a sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ (((𝑅: ℋ⟶ ℋ ∧ 𝑆: ℋ⟶ ℋ) ∧ (𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ)) → ((𝑅 +op 𝑆) +op (𝑇 +op 𝑈)) = ((𝑅 +op 𝑇) +op (𝑆 +op 𝑈))) | ||
| Theorem | hocsubdir 31817 | Distributive law for Hilbert space operator difference. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑅: ℋ⟶ ℋ ∧ 𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → ((𝑅 −op 𝑆) ∘ 𝑇) = ((𝑅 ∘ 𝑇) −op (𝑆 ∘ 𝑇))) | ||
| Theorem | hoaddridi 31818 | Sum of a Hilbert space operator with the zero operator. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑇 +op 0hop ) = 𝑇 | ||
| Theorem | hodidi 31819 | Difference of a Hilbert space operator from itself. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑇 −op 𝑇) = 0hop | ||
| Theorem | ho0coi 31820 | Composition of the zero operator and a Hilbert space operator. (Contributed by NM, 9-Aug-2006.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ( 0hop ∘ 𝑇) = 0hop | ||
| Theorem | hoid1i 31821 | Composition of Hilbert space operator with unit identity. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑇 ∘ Iop ) = 𝑇 | ||
| Theorem | hoid1ri 31822 | Composition of Hilbert space operator with unit identity. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ( Iop ∘ 𝑇) = 𝑇 | ||
| Theorem | hoaddrid 31823 | Sum of a Hilbert space operator with the zero operator. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (𝑇 +op 0hop ) = 𝑇) | ||
| Theorem | hodid 31824 | Difference of a Hilbert space operator from itself. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (𝑇 −op 𝑇) = 0hop ) | ||
| Theorem | hon0 31825 | A Hilbert space operator is not empty. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → ¬ 𝑇 = ∅) | ||
| Theorem | hodseqi 31826 | Subtraction and addition of equal Hilbert space operators. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑆 +op (𝑇 −op 𝑆)) = 𝑇 | ||
| Theorem | ho0subi 31827 | Subtraction of Hilbert space operators expressed in terms of difference from zero. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑆 −op 𝑇) = (𝑆 +op ( 0hop −op 𝑇)) | ||
| Theorem | honegsubi 31828 | Relationship between Hilbert operator addition and subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑆 +op (-1 ·op 𝑇)) = (𝑆 −op 𝑇) | ||
| Theorem | ho0sub 31829 | Subtraction of Hilbert space operators expressed in terms of difference from zero. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑆 −op 𝑇) = (𝑆 +op ( 0hop −op 𝑇))) | ||
| Theorem | hosubid1 31830 | The zero operator subtracted from a Hilbert space operator. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (𝑇 −op 0hop ) = 𝑇) | ||
| Theorem | honegsub 31831 | Relationship between Hilbert space operator addition and subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑇 +op (-1 ·op 𝑈)) = (𝑇 −op 𝑈)) | ||
| Theorem | homullid 31832 | An operator equals its scalar product with one. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (1 ·op 𝑇) = 𝑇) | ||
| Theorem | homco1 31833 | Associative law for scalar product and composition of operators. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ((𝐴 ·op 𝑇) ∘ 𝑈) = (𝐴 ·op (𝑇 ∘ 𝑈))) | ||
| Theorem | homulass 31834 | Scalar product associative law for Hilbert space operators. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → ((𝐴 · 𝐵) ·op 𝑇) = (𝐴 ·op (𝐵 ·op 𝑇))) | ||
| Theorem | hoadddi 31835 | Scalar product distributive law for Hilbert space operators. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝐴 ·op (𝑇 +op 𝑈)) = ((𝐴 ·op 𝑇) +op (𝐴 ·op 𝑈))) | ||
| Theorem | hoadddir 31836 | Scalar product reverse distributive law for Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → ((𝐴 + 𝐵) ·op 𝑇) = ((𝐴 ·op 𝑇) +op (𝐵 ·op 𝑇))) | ||
| Theorem | homul12 31837 | Swap first and second factors in a nested operator scalar product. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → (𝐴 ·op (𝐵 ·op 𝑇)) = (𝐵 ·op (𝐴 ·op 𝑇))) | ||
| Theorem | honegneg 31838 | Double negative of a Hilbert space operator. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (-1 ·op (-1 ·op 𝑇)) = 𝑇) | ||
| Theorem | hosubneg 31839 | Relationship between operator subtraction and negative. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑇 −op (-1 ·op 𝑈)) = (𝑇 +op 𝑈)) | ||
| Theorem | hosubdi 31840 | Scalar product distributive law for operator difference. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝐴 ·op (𝑇 −op 𝑈)) = ((𝐴 ·op 𝑇) −op (𝐴 ·op 𝑈))) | ||
| Theorem | honegdi 31841 | Distribution of negative over addition. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (-1 ·op (𝑇 +op 𝑈)) = ((-1 ·op 𝑇) +op (-1 ·op 𝑈))) | ||
| Theorem | honegsubdi 31842 | Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (-1 ·op (𝑇 −op 𝑈)) = ((-1 ·op 𝑇) +op 𝑈)) | ||
| Theorem | honegsubdi2 31843 | Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (-1 ·op (𝑇 −op 𝑈)) = (𝑈 −op 𝑇)) | ||
| Theorem | hosubsub2 31844 | Law for double subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑆 −op (𝑇 −op 𝑈)) = (𝑆 +op (𝑈 −op 𝑇))) | ||
| Theorem | hosub4 31845 | Rearrangement of 4 terms in a mixed addition and subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ (((𝑅: ℋ⟶ ℋ ∧ 𝑆: ℋ⟶ ℋ) ∧ (𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ)) → ((𝑅 +op 𝑆) −op (𝑇 +op 𝑈)) = ((𝑅 −op 𝑇) +op (𝑆 −op 𝑈))) | ||
| Theorem | hosubadd4 31846 | Rearrangement of 4 terms in a mixed addition and subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ (((𝑅: ℋ⟶ ℋ ∧ 𝑆: ℋ⟶ ℋ) ∧ (𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ)) → ((𝑅 −op 𝑆) −op (𝑇 −op 𝑈)) = ((𝑅 +op 𝑈) −op (𝑆 +op 𝑇))) | ||
| Theorem | hoaddsubass 31847 | Associative-type law for addition and subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ((𝑆 +op 𝑇) −op 𝑈) = (𝑆 +op (𝑇 −op 𝑈))) | ||
| Theorem | hoaddsub 31848 | Law for operator addition and subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ((𝑆 +op 𝑇) −op 𝑈) = ((𝑆 −op 𝑈) +op 𝑇)) | ||
| Theorem | hosubsub 31849 | Law for double subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑆 −op (𝑇 −op 𝑈)) = ((𝑆 −op 𝑇) +op 𝑈)) | ||
| Theorem | hosubsub4 31850 | Law for double subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ((𝑆 −op 𝑇) −op 𝑈) = (𝑆 −op (𝑇 +op 𝑈))) | ||
| Theorem | ho2times 31851 | Two times a Hilbert space operator. (Contributed by NM, 26-Aug-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (2 ·op 𝑇) = (𝑇 +op 𝑇)) | ||
| Theorem | hoaddsubassi 31852 | Associativity of sum and difference of Hilbert space operators. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
| ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((𝑅 +op 𝑆) −op 𝑇) = (𝑅 +op (𝑆 −op 𝑇)) | ||
| Theorem | hoaddsubi 31853 | Law for sum and difference of Hilbert space operators. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
| ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((𝑅 +op 𝑆) −op 𝑇) = ((𝑅 −op 𝑇) +op 𝑆) | ||
| Theorem | hosd1i 31854 | Hilbert space operator sum expressed in terms of difference. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ & ⊢ 𝑈: ℋ⟶ ℋ ⇒ ⊢ (𝑇 +op 𝑈) = (𝑇 −op ( 0hop −op 𝑈)) | ||
| Theorem | hosd2i 31855 | Hilbert space operator sum expressed in terms of difference. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ & ⊢ 𝑈: ℋ⟶ ℋ ⇒ ⊢ (𝑇 +op 𝑈) = (𝑇 −op ((𝑈 −op 𝑈) −op 𝑈)) | ||
| Theorem | hopncani 31856 | Hilbert space operator cancellation law. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ & ⊢ 𝑈: ℋ⟶ ℋ ⇒ ⊢ ((𝑇 +op 𝑈) −op 𝑈) = 𝑇 | ||
| Theorem | honpcani 31857 | Hilbert space operator cancellation law. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ & ⊢ 𝑈: ℋ⟶ ℋ ⇒ ⊢ ((𝑇 −op 𝑈) +op 𝑈) = 𝑇 | ||
| Theorem | hosubeq0i 31858 | If the difference between two operators is zero, they are equal. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ & ⊢ 𝑈: ℋ⟶ ℋ ⇒ ⊢ ((𝑇 −op 𝑈) = 0hop ↔ 𝑇 = 𝑈) | ||
| Theorem | honpncani 31859 | Hilbert space operator cancellation law. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((𝑅 −op 𝑆) +op (𝑆 −op 𝑇)) = (𝑅 −op 𝑇) | ||
| Theorem | ho01i 31860* | A condition implying that a Hilbert space operator is identically zero. Lemma 3.2(S8) of [Beran] p. 95. (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑦) = 0 ↔ 𝑇 = 0hop ) | ||
| Theorem | ho02i 31861* | A condition implying that a Hilbert space operator is identically zero. Lemma 3.2(S10) of [Beran] p. 95. (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = 0 ↔ 𝑇 = 0hop ) | ||
| Theorem | hoeq1 31862* | A condition implying that two Hilbert space operators are equal. Lemma 3.2(S9) of [Beran] p. 95. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑆‘𝑥) ·ih 𝑦) = ((𝑇‘𝑥) ·ih 𝑦) ↔ 𝑆 = 𝑇)) | ||
| Theorem | hoeq2 31863* | A condition implying that two Hilbert space operators are equal. Lemma 3.2(S11) of [Beran] p. 95. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑆‘𝑦)) = (𝑥 ·ih (𝑇‘𝑦)) ↔ 𝑆 = 𝑇)) | ||
| Theorem | adjmo 31864* | Every Hilbert space operator has at most one adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
| ⊢ ∃*𝑢(𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦)) | ||
| Theorem | adjsym 31865* | Symmetry property of an adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦))) | ||
| Theorem | eigrei 31866 | A necessary and sufficient condition (that holds when 𝑇 is a Hermitian operator) for an eigenvalue 𝐵 to be real. Generalization of Equation 1.30 of [Hughes] p. 49. (Contributed by NM, 21-Jan-2005.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ) → ((𝐴 ·ih (𝑇‘𝐴)) = ((𝑇‘𝐴) ·ih 𝐴) ↔ 𝐵 ∈ ℝ)) | ||
| Theorem | eigre 31867 | A necessary and sufficient condition (that holds when 𝑇 is a Hermitian operator) for an eigenvalue 𝐵 to be real. Generalization of Equation 1.30 of [Hughes] p. 49. (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → ((𝐴 ·ih (𝑇‘𝐴)) = ((𝑇‘𝐴) ·ih 𝐴) ↔ 𝐵 ∈ ℝ)) | ||
| Theorem | eigposi 31868 | A sufficient condition (first conjunct pair, that holds when 𝑇 is a positive operator) for an eigenvalue 𝐵 (second conjunct pair) to be nonnegative. Remark (ii) in [Hughes] p. 137. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((((𝐴 ·ih (𝑇‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝐴 ·ih (𝑇‘𝐴))) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) | ||
| Theorem | eigorthi 31869 | A necessary and sufficient condition (that holds when 𝑇 is a Hermitian operator) for two eigenvectors 𝐴 and 𝐵 to be orthogonal. Generalization of Equation 1.31 of [Hughes] p. 49. (Contributed by NM, 23-Jan-2005.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈ ℂ ⇒ ⊢ ((((𝑇‘𝐴) = (𝐶 ·ℎ 𝐴) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)) ∧ 𝐶 ≠ (∗‘𝐷)) → ((𝐴 ·ih (𝑇‘𝐵)) = ((𝑇‘𝐴) ·ih 𝐵) ↔ (𝐴 ·ih 𝐵) = 0)) | ||
| Theorem | eigorth 31870 | A necessary and sufficient condition (that holds when 𝑇 is a Hermitian operator) for two eigenvectors 𝐴 and 𝐵 to be orthogonal. Generalization of Equation 1.31 of [Hughes] p. 49. (Contributed by NM, 23-Mar-2006.) (New usage is discouraged.) |
| ⊢ ((((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) ∧ (((𝑇‘𝐴) = (𝐶 ·ℎ 𝐴) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)) ∧ 𝐶 ≠ (∗‘𝐷))) → ((𝐴 ·ih (𝑇‘𝐵)) = ((𝑇‘𝐴) ·ih 𝐵) ↔ (𝐴 ·ih 𝐵) = 0)) | ||
| Definition | df-nmop 31871* | Define the norm of a Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
| ⊢ normop = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑡‘𝑧)))}, ℝ*, < )) | ||
| Definition | df-cnop 31872* | Define the set of continuous operators on Hilbert space. For every "epsilon" (𝑦) there is a "delta" (𝑧) such that... (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.) |
| ⊢ ContOp = {𝑡 ∈ ( ℋ ↑m ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥))) < 𝑦)} | ||
| Definition | df-lnop 31873* | Define the set of linear operators on Hilbert space. (See df-hosum 31762 for definition of operator.) (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
| ⊢ LinOp = {𝑡 ∈ ( ℋ ↑m ℋ) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑡‘𝑦)) +ℎ (𝑡‘𝑧))} | ||
| Definition | df-bdop 31874 | Define the set of bounded linear Hilbert space operators. (See df-hosum 31762 for definition of operator.) (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
| ⊢ BndLinOp = {𝑡 ∈ LinOp ∣ (normop‘𝑡) < +∞} | ||
| Definition | df-unop 31875* | Define the set of unitary operators on Hilbert space. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
| ⊢ UniOp = {𝑡 ∣ (𝑡: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡‘𝑥) ·ih (𝑡‘𝑦)) = (𝑥 ·ih 𝑦))} | ||
| Definition | df-hmop 31876* | Define the set of Hermitian operators on Hilbert space. Some books call these "symmetric operators" and others call them "self-adjoint operators", sometimes with slightly different technical meanings. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
| ⊢ HrmOp = {𝑡 ∈ ( ℋ ↑m ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦)} | ||
| Definition | df-nmfn 31877* | Define the norm of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
| ⊢ normfn = (𝑡 ∈ (ℂ ↑m ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (abs‘(𝑡‘𝑧)))}, ℝ*, < )) | ||
| Definition | df-nlfn 31878 | Define the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
| ⊢ null = (𝑡 ∈ (ℂ ↑m ℋ) ↦ (◡𝑡 “ {0})) | ||
| Definition | df-cnfn 31879* | Define the set of continuous functionals on Hilbert space. For every "epsilon" (𝑦) there is a "delta" (𝑧) such that... (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
| ⊢ ContFn = {𝑡 ∈ (ℂ ↑m ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (abs‘((𝑡‘𝑤) − (𝑡‘𝑥))) < 𝑦)} | ||
| Definition | df-lnfn 31880* | Define the set of linear functionals on Hilbert space. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
| ⊢ LinFn = {𝑡 ∈ (ℂ ↑m ℋ) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))} | ||
| Definition | df-adjh 31881* | Define the adjoint of a Hilbert space operator (if it exists). The domain of adjℎ is the set of all adjoint operators. Definition of adjoint in [Kalmbach2] p. 8. Unlike Kalmbach (and most authors), we do not demand that the operator be linear, but instead show (in adjbdln 32115) that the adjoint exists for a bounded linear operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
| ⊢ adjℎ = {⟨𝑡, 𝑢⟩ ∣ (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢‘𝑦)))} | ||
| Definition | df-bra 31882* |
Define the bra of a vector used by Dirac notation. Based on definition
of bra in [Prugovecki] p. 186 (p.
180 in 1971 edition). In Dirac
bra-ket notation, ⟨𝐴 ∣ 𝐵⟩ is a complex number equal to
the inner
product (𝐵 ·ih 𝐴). But physicists like
to talk about the
individual components ⟨𝐴 ∣ and ∣
𝐵⟩, called bra
and ket
respectively. In order for their properties to make sense formally, we
define the ket ∣ 𝐵⟩ as the vector 𝐵 itself,
and the bra
⟨𝐴 ∣ as a functional from ℋ to ℂ. We represent the
Dirac notation ⟨𝐴 ∣ 𝐵⟩ by ((bra‘𝐴)‘𝐵); see
braval 31976. The reversal of the inner product
arguments not only makes
the bra-ket behavior consistent with physics literature (see comments
under ax-his3 31116) but is also required in order for the
associative law
kbass2 32149 to work.
Our definition of bra and the associated outer product df-kb 31883 differs from, but is equivalent to, a common approach in the literature that makes use of mappings to a dual space. Our approach eliminates the need to have a parallel development of this dual space and instead keeps everything in Hilbert space. For an extensive discussion about how our notation maps to the bra-ket notation in physics textbooks, see mmnotes.txt 31883, under the 17-May-2006 entry. (Contributed by NM, 15-May-2006.) (New usage is discouraged.) |
| ⊢ bra = (𝑥 ∈ ℋ ↦ (𝑦 ∈ ℋ ↦ (𝑦 ·ih 𝑥))) | ||
| Definition | df-kb 31883* | Define a commuted bra and ket juxtaposition used by Dirac notation. In Dirac notation, ∣ 𝐴⟩⟨𝐵 ∣ is an operator known as the outer product of 𝐴 and 𝐵, which we represent by (𝐴 ketbra 𝐵). Based on Equation 8.1 of [Prugovecki] p. 376. This definition, combined with Definition df-bra 31882, allows any legal juxtaposition of bras and kets to make sense formally and also to obey the associative law when mapped back to Dirac notation. (Contributed by NM, 15-May-2006.) (New usage is discouraged.) |
| ⊢ ketbra = (𝑥 ∈ ℋ, 𝑦 ∈ ℋ ↦ (𝑧 ∈ ℋ ↦ ((𝑧 ·ih 𝑦) ·ℎ 𝑥))) | ||
| Definition | df-leop 31884* | Define positive operator ordering. Definition VI.1 of [Retherford] p. 49. Note that ( ℋ × 0ℋ) ≤op 𝑇 means that 𝑇 is a positive operator. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
| ⊢ ≤op = {⟨𝑡, 𝑢⟩ ∣ ((𝑢 −op 𝑡) ∈ HrmOp ∧ ∀𝑥 ∈ ℋ 0 ≤ (((𝑢 −op 𝑡)‘𝑥) ·ih 𝑥))} | ||
| Definition | df-eigvec 31885* | Define the eigenvector function. Theorem eleigveccl 31991 shows that eigvec‘𝑇, the set of eigenvectors of Hilbert space operator 𝑇, are Hilbert space vectors. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
| ⊢ eigvec = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ {𝑥 ∈ ( ℋ ∖ 0ℋ) ∣ ∃𝑧 ∈ ℂ (𝑡‘𝑥) = (𝑧 ·ℎ 𝑥)}) | ||
| Definition | df-eigval 31886* | Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 31993 shows that (eigval‘𝑇)‘𝐴, the eigenvalue associated with eigenvector 𝐴, is a complex number. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
| ⊢ eigval = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2)))) | ||
| Definition | df-spec 31887* | Define the spectrum of an operator. Definition of spectrum in [Halmos] p. 50. (Contributed by NM, 11-Apr-2006.) (New usage is discouraged.) |
| ⊢ Lambda = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ {𝑥 ∈ ℂ ∣ ¬ (𝑡 −op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ}) | ||
| Theorem | nmopval 31888* | Value of the norm of a Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (normop‘𝑇) = sup({𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}, ℝ*, < )) | ||
| Theorem | elcnop 31889* | Property defining a continuous Hilbert space operator. (Contributed by NM, 28-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ ContOp ↔ (𝑇: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (normℎ‘((𝑇‘𝑤) −ℎ (𝑇‘𝑥))) < 𝑦))) | ||
| Theorem | ellnop 31890* | Property defining a linear Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ LinOp ↔ (𝑇: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑇‘𝑦)) +ℎ (𝑇‘𝑧)))) | ||
| Theorem | lnopf 31891 | A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ LinOp → 𝑇: ℋ⟶ ℋ) | ||
| Theorem | elbdop 31892 | Property defining a bounded linear Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ BndLinOp ↔ (𝑇 ∈ LinOp ∧ (normop‘𝑇) < +∞)) | ||
| Theorem | bdopln 31893 | A bounded linear Hilbert space operator is a linear operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ BndLinOp → 𝑇 ∈ LinOp) | ||
| Theorem | bdopf 31894 | A bounded linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇 ∈ BndLinOp → 𝑇: ℋ⟶ ℋ) | ||
| Theorem | nmopsetretALT 31895* | The set in the supremum of the operator norm definition df-nmop 31871 is a set of reals. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ⊆ ℝ) | ||
| Theorem | nmopsetretHIL 31896* | The set in the supremum of the operator norm definition df-nmop 31871 is a set of reals. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ⊆ ℝ) | ||
| Theorem | nmopsetn0 31897* | The set in the supremum of the operator norm definition df-nmop 31871 is nonempty. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.) |
| ⊢ (normℎ‘(𝑇‘0ℎ)) ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} | ||
| Theorem | nmopxr 31898 | The norm of a Hilbert space operator is an extended real. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (normop‘𝑇) ∈ ℝ*) | ||
| Theorem | nmoprepnf 31899 | The norm of a Hilbert space operator is either real or plus infinity. (Contributed by NM, 5-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → ((normop‘𝑇) ∈ ℝ ↔ (normop‘𝑇) ≠ +∞)) | ||
| Theorem | nmopgtmnf 31900 | The norm of a Hilbert space operator is not minus infinity. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → -∞ < (normop‘𝑇)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |