![]() |
Metamath
Proof Explorer Theorem List (p. 288 of 454) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | htth 28701* | Hellinger-Toeplitz Theorem: any self-adjoint linear operator defined on all of Hilbert space is bounded. Theorem 10.1-1 of [Kreyszig] p. 525. Discovered by E. Hellinger and O. Toeplitz in 1910, "it aroused both admiration and puzzlement since the theorem establishes a relation between properties of two different kinds, namely, the properties of being defined everywhere and being bounded." (Contributed by NM, 11-Jan-2008.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝐿 = (𝑈 LnOp 𝑈) & ⊢ 𝐵 = (𝑈 BLnOp 𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ 𝑇 ∈ 𝐿 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑃(𝑇‘𝑦)) = ((𝑇‘𝑥)𝑃𝑦)) → 𝑇 ∈ 𝐵) | ||
This part contains the definitions and theorems used by the Hilbert Space Explorer (HSE), mmhil.html. Because it axiomatizes a single complex Hilbert space whose existence is assumed, its usefulness is limited. For example, it cannot work with real or quaternion Hilbert spaces and it cannot study relationships between two Hilbert spaces. More information can be found on the Hilbert Space Explorer page. Future development should instead work with general Hilbert spaces as defined by df-hil 20393; note that df-hil 20393 uses extensible structures. The intent is for this deprecated section to be deleted once all its theorems have been translated into extensible structure versions (or are not useful). Many of the theorems in this section have already been translated to extensible structure versions, but there is still a lot in this section that might be useful for future reference. It is much easier to translate these by hand from this section than to start from scratch from textbook proofs, since the HSE omits no details. | ||
Syntax | chba 28702 | Extend class notation with Hilbert vector space. |
class ℋ | ||
Syntax | cva 28703 | Extend class notation with vector addition in Hilbert space. In the literature, the subscript "h" is omitted, but we need it to avoid ambiguity with complex number addition + caddc 10529. |
class +ℎ | ||
Syntax | csm 28704 | Extend class notation with scalar multiplication in Hilbert space. In the literature scalar multiplication is usually indicated by juxtaposition, but we need an explicit symbol to prevent ambiguity. |
class ·ℎ | ||
Syntax | csp 28705 | Extend class notation with inner (scalar) product in Hilbert space. In the literature, the inner product of 𝐴 and 𝐵 is usually written 〈𝐴, 𝐵〉 but our operation notation allows us to use existing theorems about operations and also eliminates ambiguity with the definition of an ordered pair df-op 4532. |
class ·ih | ||
Syntax | cno 28706 | Extend class notation with the norm function in Hilbert space. In the literature, the norm of 𝐴 is usually written "|| 𝐴 ||", but we use function notation to take advantage of our existing theorems about functions. |
class normℎ | ||
Syntax | c0v 28707 | Extend class notation with zero vector in Hilbert space. |
class 0ℎ | ||
Syntax | cmv 28708 | Extend class notation with vector subtraction in Hilbert space. |
class −ℎ | ||
Syntax | ccauold 28709 | Extend class notation with set of Cauchy sequences in Hilbert space. |
class Cauchy | ||
Syntax | chli 28710 | Extend class notation with convergence relation in Hilbert space. |
class ⇝𝑣 | ||
Syntax | csh 28711 | Extend class notation with set of subspaces of a Hilbert space. |
class Sℋ | ||
Syntax | cch 28712 | Extend class notation with set of closed subspaces of a Hilbert space. |
class Cℋ | ||
Syntax | cort 28713 | Extend class notation with orthogonal complement in Cℋ. |
class ⊥ | ||
Syntax | cph 28714 | Extend class notation with subspace sum in Cℋ. |
class +ℋ | ||
Syntax | cspn 28715 | Extend class notation with subspace span in Cℋ. |
class span | ||
Syntax | chj 28716 | Extend class notation with join in Cℋ. |
class ∨ℋ | ||
Syntax | chsup 28717 | Extend class notation with supremum of a collection in Cℋ. |
class ∨ℋ | ||
Syntax | c0h 28718 | Extend class notation with zero of Cℋ. |
class 0ℋ | ||
Syntax | ccm 28719 | Extend class notation with the commutes relation on a Hilbert lattice. |
class 𝐶ℋ | ||
Syntax | cpjh 28720 | Extend class notation with set of projections on a Hilbert space. |
class projℎ | ||
Syntax | chos 28721 | Extend class notation with sum of Hilbert space operators. |
class +op | ||
Syntax | chot 28722 | Extend class notation with scalar product of a Hilbert space operator. |
class ·op | ||
Syntax | chod 28723 | Extend class notation with difference of Hilbert space operators. |
class −op | ||
Syntax | chfs 28724 | Extend class notation with sum of Hilbert space functionals. |
class +fn | ||
Syntax | chft 28725 | Extend class notation with scalar product of Hilbert space functional. |
class ·fn | ||
Syntax | ch0o 28726 | Extend class notation with the Hilbert space zero operator. |
class 0hop | ||
Syntax | chio 28727 | Extend class notation with Hilbert space identity operator. |
class Iop | ||
Syntax | cnop 28728 | Extend class notation with the operator norm function. |
class normop | ||
Syntax | ccop 28729 | Extend class notation with set of continuous Hilbert space operators. |
class ContOp | ||
Syntax | clo 28730 | Extend class notation with set of linear Hilbert space operators. |
class LinOp | ||
Syntax | cbo 28731 | Extend class notation with set of bounded linear operators. |
class BndLinOp | ||
Syntax | cuo 28732 | Extend class notation with set of unitary Hilbert space operators. |
class UniOp | ||
Syntax | cho 28733 | Extend class notation with set of Hermitian Hilbert space operators. |
class HrmOp | ||
Syntax | cnmf 28734 | Extend class notation with the functional norm function. |
class normfn | ||
Syntax | cnl 28735 | Extend class notation with the functional nullspace function. |
class null | ||
Syntax | ccnfn 28736 | Extend class notation with set of continuous Hilbert space functionals. |
class ContFn | ||
Syntax | clf 28737 | Extend class notation with set of linear Hilbert space functionals. |
class LinFn | ||
Syntax | cado 28738 | Extend class notation with Hilbert space adjoint function. |
class adjℎ | ||
Syntax | cbr 28739 | Extend class notation with the bra of a vector in Dirac bra-ket notation. |
class bra | ||
Syntax | ck 28740 | Extend class notation with the outer product of two vectors in Dirac bra-ket notation. |
class ketbra | ||
Syntax | cleo 28741 | Extend class notation with positive operator ordering. |
class ≤op | ||
Syntax | cei 28742 | Extend class notation with Hilbert space eigenvector function. |
class eigvec | ||
Syntax | cel 28743 | Extend class notation with Hilbert space eigenvalue function. |
class eigval | ||
Syntax | cspc 28744 | Extend class notation with the spectrum of an operator. |
class Lambda | ||
Syntax | cst 28745 | Extend class notation with set of states on a Hilbert lattice. |
class States | ||
Syntax | chst 28746 | Extend class notation with set of Hilbert-space-valued states on a Hilbert lattice. |
class CHStates | ||
Syntax | ccv 28747 | Extend class notation with the covers relation on a Hilbert lattice. |
class ⋖ℋ | ||
Syntax | cat 28748 | Extend class notation with set of atoms on a Hilbert lattice. |
class HAtoms | ||
Syntax | cmd 28749 | Extend class notation with the modular pair relation on a Hilbert lattice. |
class 𝑀ℋ | ||
Syntax | cdmd 28750 | Extend class notation with the dual modular pair relation on a Hilbert lattice. |
class 𝑀ℋ* | ||
Definition | df-hnorm 28751 | Define the function for the norm of a vector of Hilbert space. See normval 28907 for its value and normcl 28908 for its closure. Theorems norm-i-i 28916, norm-ii-i 28920, and norm-iii-i 28922 show it has the expected properties of a norm. In the literature, the norm of 𝐴 is usually written "|| 𝐴 ||", but we use function notation to take advantage of our existing theorems about functions. Definition of norm in [Beran] p. 96. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.) |
⊢ normℎ = (𝑥 ∈ dom dom ·ih ↦ (√‘(𝑥 ·ih 𝑥))) | ||
Definition | df-hba 28752 | Define base set of Hilbert space, for use if we want to develop Hilbert space independently from the axioms (see comments in ax-hilex 28782). Note that ℋ is considered a primitive in the Hilbert space axioms below, and we don't use this definition outside of this section. This definition can be proved independently from those axioms as theorem hhba 28950. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ ℋ = (BaseSet‘〈〈 +ℎ , ·ℎ 〉, normℎ〉) | ||
Definition | df-h0v 28753 | Define the zero vector of Hilbert space. Note that 0vec is considered a primitive in the Hilbert space axioms below, and we don't use this definition outside of this section. It is proved from the axioms as theorem hh0v 28951. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 0ℎ = (0vec‘〈〈 +ℎ , ·ℎ 〉, normℎ〉) | ||
Definition | df-hvsub 28754* | Define vector subtraction. See hvsubvali 28803 for its value and hvsubcli 28804 for its closure. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.) |
⊢ −ℎ = (𝑥 ∈ ℋ, 𝑦 ∈ ℋ ↦ (𝑥 +ℎ (-1 ·ℎ 𝑦))) | ||
Definition | df-hlim 28755* | Define the limit relation for Hilbert space. See hlimi 28971 for its relational expression. Note that 𝑓:ℕ⟶ ℋ is an infinite sequence of vectors, i.e. a mapping from integers to vectors. Definition of converge in [Beran] p. 96. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.) |
⊢ ⇝𝑣 = {〈𝑓, 𝑤〉 ∣ ((𝑓:ℕ⟶ ℋ ∧ 𝑤 ∈ ℋ) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑧) −ℎ 𝑤)) < 𝑥)} | ||
Definition | df-hcau 28756* | Define the set of Cauchy sequences on a Hilbert space. See hcau 28967 for its membership relation. Note that 𝑓:ℕ⟶ ℋ is an infinite sequence of vectors, i.e. a mapping from integers to vectors. Definition of Cauchy sequence in [Beran] p. 96. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.) |
⊢ Cauchy = {𝑓 ∈ ( ℋ ↑m ℕ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥} | ||
Theorem | h2hva 28757 | The group (addition) operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ NrmCVec ⇒ ⊢ +ℎ = ( +𝑣 ‘𝑈) | ||
Theorem | h2hsm 28758 | The scalar product operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ NrmCVec ⇒ ⊢ ·ℎ = ( ·𝑠OLD ‘𝑈) | ||
Theorem | h2hnm 28759 | The norm function of Hilbert space. (Contributed by NM, 5-Jun-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ NrmCVec ⇒ ⊢ normℎ = (normCV‘𝑈) | ||
Theorem | h2hvs 28760 | The vector subtraction operation of Hilbert space. (Contributed by NM, 6-Jun-2008.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ NrmCVec & ⊢ ℋ = (BaseSet‘𝑈) ⇒ ⊢ −ℎ = ( −𝑣 ‘𝑈) | ||
Theorem | h2hmetdval 28761 | Value of the distance function of the metric space of Hilbert space. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ NrmCVec & ⊢ ℋ = (BaseSet‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴𝐷𝐵) = (normℎ‘(𝐴 −ℎ 𝐵))) | ||
Theorem | h2hcau 28762 | The Cauchy sequences of Hilbert space. (Contributed by NM, 6-Jun-2008.) (Revised by Mario Carneiro, 13-May-2014.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ NrmCVec & ⊢ ℋ = (BaseSet‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ Cauchy = ((Cau‘𝐷) ∩ ( ℋ ↑m ℕ)) | ||
Theorem | h2hlm 28763 | The limit sequences of Hilbert space. (Contributed by NM, 6-Jun-2008.) (Revised by Mario Carneiro, 13-May-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ NrmCVec & ⊢ ℋ = (BaseSet‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ⇝𝑣 = ((⇝𝑡‘𝐽) ↾ ( ℋ ↑m ℕ)) | ||
Before introducing the 18 axioms for Hilbert space, we first prove them as the conclusions of theorems axhilex-zf 28764 through axhcompl-zf 28781, using ZFC set theory only. These show that if we are given a known, fixed Hilbert space 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 that satisfies their hypotheses, then we can derive the Hilbert space axioms as theorems of ZFC set theory. In practice, in order to use these theorems to convert the Hilbert Space explorer to a ZFC-only subtheory, we would also have to provide definitions for the 3 (otherwise primitive) class constants +ℎ, ·ℎ, and ·ih before df-hnorm 28751 above. See also the comment in ax-hilex 28782. | ||
Theorem | axhilex-zf 28764 | Derive axiom ax-hilex 28782 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ℋ ∈ V | ||
Theorem | axhfvadd-zf 28765 | Derive axiom ax-hfvadd 28783 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ +ℎ :( ℋ × ℋ)⟶ ℋ | ||
Theorem | axhvcom-zf 28766 | Derive axiom ax-hvcom 28784 from Hilbert space under ZF set theory. (Contributed by NM, 27-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)) | ||
Theorem | axhvass-zf 28767 | Derive axiom ax-hvass 28785 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = (𝐴 +ℎ (𝐵 +ℎ 𝐶))) | ||
Theorem | axhv0cl-zf 28768 | Derive axiom ax-hv0cl 28786 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ 0ℎ ∈ ℋ | ||
Theorem | axhvaddid-zf 28769 | Derive axiom ax-hvaddid 28787 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴) | ||
Theorem | axhfvmul-zf 28770 | Derive axiom ax-hfvmul 28788 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ·ℎ :(ℂ × ℋ)⟶ ℋ | ||
Theorem | axhvmulid-zf 28771 | Derive axiom ax-hvmulid 28789 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴) | ||
Theorem | axhvmulass-zf 28772 | Derive axiom ax-hvmulass 28790 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))) | ||
Theorem | axhvdistr1-zf 28773 | Derive axiom ax-hvdistr1 28791 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 +ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) +ℎ (𝐴 ·ℎ 𝐶))) | ||
Theorem | axhvdistr2-zf 28774 | Derive axiom ax-hvdistr2 28792 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 + 𝐵) ·ℎ 𝐶) = ((𝐴 ·ℎ 𝐶) +ℎ (𝐵 ·ℎ 𝐶))) | ||
Theorem | axhvmul0-zf 28775 | Derive axiom ax-hvmul0 28793 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ (𝐴 ∈ ℋ → (0 ·ℎ 𝐴) = 0ℎ) | ||
Theorem | axhfi-zf 28776 | Derive axiom ax-hfi 28862 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD & ⊢ ·ih = (·𝑖OLD‘𝑈) ⇒ ⊢ ·ih :( ℋ × ℋ)⟶ℂ | ||
Theorem | axhis1-zf 28777 | Derive axiom ax-his1 28865 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD & ⊢ ·ih = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih 𝐵) = (∗‘(𝐵 ·ih 𝐴))) | ||
Theorem | axhis2-zf 28778 | Derive axiom ax-his2 28866 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD & ⊢ ·ih = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) ·ih 𝐶) = ((𝐴 ·ih 𝐶) + (𝐵 ·ih 𝐶))) | ||
Theorem | axhis3-zf 28779 | Derive axiom ax-his3 28867 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD & ⊢ ·ih = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))) | ||
Theorem | axhis4-zf 28780 | Derive axiom ax-his4 28868 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD & ⊢ ·ih = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ) → 0 < (𝐴 ·ih 𝐴)) | ||
Theorem | axhcompl-zf 28781* | Derive axiom ax-hcompl 28985 from Hilbert space under ZF set theory. (Contributed by NM, 6-Jun-2008.) (Revised by Mario Carneiro, 13-May-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ (𝐹 ∈ Cauchy → ∃𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥) | ||
Here we introduce the axioms a complex Hilbert space, which is the foundation for quantum mechanics and quantum field theory. The 18 axioms for a complex Hilbert space consist of ax-hilex 28782, ax-hfvadd 28783, ax-hvcom 28784, ax-hvass 28785, ax-hv0cl 28786, ax-hvaddid 28787, ax-hfvmul 28788, ax-hvmulid 28789, ax-hvmulass 28790, ax-hvdistr1 28791, ax-hvdistr2 28792, ax-hvmul0 28793, ax-hfi 28862, ax-his1 28865, ax-his2 28866, ax-his3 28867, ax-his4 28868, and ax-hcompl 28985. The axioms specify the properties of 5 primitive symbols, ℋ, +ℎ, ·ℎ, 0ℎ, and ·ih. If we can prove in ZFC set theory that a class 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 is a complex Hilbert space, i.e. that 𝑈 ∈ CHilOLD, then these axioms can be proved as theorems axhilex-zf 28764, axhfvadd-zf 28765, axhvcom-zf 28766, axhvass-zf 28767, axhv0cl-zf 28768, axhvaddid-zf 28769, axhfvmul-zf 28770, axhvmulid-zf 28771, axhvmulass-zf 28772, axhvdistr1-zf 28773, axhvdistr2-zf 28774, axhvmul0-zf 28775, axhfi-zf 28776, axhis1-zf 28777, axhis2-zf 28778, axhis3-zf 28779, axhis4-zf 28780, and axhcompl-zf 28781 respectively. In that case, the theorems of the Hilbert Space Explorer will become theorems of ZFC set theory. See also the comments in axhilex-zf 28764. | ||
Axiom | ax-hilex 28782 | This is our first axiom for a complex Hilbert space, which is the foundation for quantum mechanics and quantum field theory. We assume that there exists a primitive class, ℋ, which contains objects called vectors. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
⊢ ℋ ∈ V | ||
Axiom | ax-hfvadd 28783 | Vector addition is an operation on ℋ. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
⊢ +ℎ :( ℋ × ℋ)⟶ ℋ | ||
Axiom | ax-hvcom 28784 | Vector addition is commutative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)) | ||
Axiom | ax-hvass 28785 | Vector addition is associative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = (𝐴 +ℎ (𝐵 +ℎ 𝐶))) | ||
Axiom | ax-hv0cl 28786 | The zero vector is in the vector space. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
⊢ 0ℎ ∈ ℋ | ||
Axiom | ax-hvaddid 28787 | Addition with the zero vector. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴) | ||
Axiom | ax-hfvmul 28788 | Scalar multiplication is an operation on ℂ and ℋ. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
⊢ ·ℎ :(ℂ × ℋ)⟶ ℋ | ||
Axiom | ax-hvmulid 28789 | Scalar multiplication by one. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴) | ||
Axiom | ax-hvmulass 28790 | Scalar multiplication associative law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))) | ||
Axiom | ax-hvdistr1 28791 | Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 +ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) +ℎ (𝐴 ·ℎ 𝐶))) | ||
Axiom | ax-hvdistr2 28792 | Scalar multiplication distributive law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 + 𝐵) ·ℎ 𝐶) = ((𝐴 ·ℎ 𝐶) +ℎ (𝐵 ·ℎ 𝐶))) | ||
Axiom | ax-hvmul0 28793 | Scalar multiplication by zero. We can derive the existence of the negative of a vector from this axiom (see hvsubid 28809 and hvsubval 28799). (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (0 ·ℎ 𝐴) = 0ℎ) | ||
Theorem | hvmulex 28794 | The Hilbert space scalar product operation is a set. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.) |
⊢ ·ℎ ∈ V | ||
Theorem | hvaddcl 28795 | Closure of vector addition. (Contributed by NM, 18-Apr-2007.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) ∈ ℋ) | ||
Theorem | hvmulcl 28796 | Closure of scalar multiplication. (Contributed by NM, 19-Apr-2007.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ℎ 𝐵) ∈ ℋ) | ||
Theorem | hvmulcli 28797 | Closure inference for scalar multiplication. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 ·ℎ 𝐵) ∈ ℋ | ||
Theorem | hvsubf 28798 | Mapping domain and codomain of vector subtraction. (Contributed by NM, 6-Sep-2007.) (New usage is discouraged.) |
⊢ −ℎ :( ℋ × ℋ)⟶ ℋ | ||
Theorem | hvsubval 28799 | Value of vector subtraction. (Contributed by NM, 5-Sep-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 −ℎ 𝐵) = (𝐴 +ℎ (-1 ·ℎ 𝐵))) | ||
Theorem | hvsubcl 28800 | Closure of vector subtraction. (Contributed by NM, 17-Aug-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 −ℎ 𝐵) ∈ ℋ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |