Home | Metamath
Proof Explorer Theorem List (p. 287 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hlpar2 28601 | The parallelogram law satisfied by Hilbert space vectors. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝑁‘(𝐴𝐺𝐵))↑2) + ((𝑁‘(𝐴𝑀𝐵))↑2)) = (2 · (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2)))) | ||
Theorem | hlpar 28602 | The parallelogram law satisfied by Hilbert space vectors. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝑁‘(𝐴𝐺𝐵))↑2) + ((𝑁‘(𝐴𝐺(-1𝑆𝐵)))↑2)) = (2 · (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2)))) | ||
Theorem | hlex 28603 | The base set of a Hilbert space is a set. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) ⇒ ⊢ 𝑋 ∈ V | ||
Theorem | hladdf 28604 | Mapping for Hilbert space vector addition. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) ⇒ ⊢ (𝑈 ∈ CHilOLD → 𝐺:(𝑋 × 𝑋)⟶𝑋) | ||
Theorem | hlcom 28605 | Hilbert space vector addition is commutative. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) = (𝐵𝐺𝐴)) | ||
Theorem | hlass 28606 | Hilbert space vector addition is associative. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = (𝐴𝐺(𝐵𝐺𝐶))) | ||
Theorem | hl0cl 28607 | The Hilbert space zero vector. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) ⇒ ⊢ (𝑈 ∈ CHilOLD → 𝑍 ∈ 𝑋) | ||
Theorem | hladdid 28608 | Hilbert space addition with the zero vector. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺𝑍) = 𝐴) | ||
Theorem | hlmulf 28609 | Mapping for Hilbert space scalar multiplication. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) ⇒ ⊢ (𝑈 ∈ CHilOLD → 𝑆:(ℂ × 𝑋)⟶𝑋) | ||
Theorem | hlmulid 28610 | Hilbert space scalar multiplication by one. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋) → (1𝑆𝐴) = 𝐴) | ||
Theorem | hlmulass 28611 | Hilbert space scalar multiplication associative law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → ((𝐴 · 𝐵)𝑆𝐶) = (𝐴𝑆(𝐵𝑆𝐶))) | ||
Theorem | hldi 28612 | Hilbert space scalar multiplication distributive law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑆(𝐵𝐺𝐶)) = ((𝐴𝑆𝐵)𝐺(𝐴𝑆𝐶))) | ||
Theorem | hldir 28613 | Hilbert space scalar multiplication distributive law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → ((𝐴 + 𝐵)𝑆𝐶) = ((𝐴𝑆𝐶)𝐺(𝐵𝑆𝐶))) | ||
Theorem | hlmul0 28614 | Hilbert space scalar multiplication by zero. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋) → (0𝑆𝐴) = 𝑍) | ||
Theorem | hlipf 28615 | Mapping for Hilbert space inner product. (Contributed by NM, 19-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ (𝑈 ∈ CHilOLD → 𝑃:(𝑋 × 𝑋)⟶ℂ) | ||
Theorem | hlipcj 28616 | Conjugate law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑃𝐵) = (∗‘(𝐵𝑃𝐴))) | ||
Theorem | hlipdir 28617 | Distributive law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝑃𝐶) = ((𝐴𝑃𝐶) + (𝐵𝑃𝐶))) | ||
Theorem | hlipass 28618 | Associative law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑆𝐵)𝑃𝐶) = (𝐴 · (𝐵𝑃𝐶))) | ||
Theorem | hlipgt0 28619 | The inner product of a Hilbert space vector by itself is positive. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 𝑍) → 0 < (𝐴𝑃𝐴)) | ||
Theorem | hlcompl 28620 | Completeness of a Hilbert space. (Contributed by NM, 8-Sep-2007.) (Revised by Mario Carneiro, 9-May-2014.) (New usage is discouraged.) |
⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐹 ∈ (Cau‘𝐷)) → 𝐹 ∈ dom (⇝𝑡‘𝐽)) | ||
Theorem | cnchl 28621 | The set of complex numbers is a complex Hilbert space. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 + , · 〉, abs〉 ⇒ ⊢ 𝑈 ∈ CHilOLD | ||
Theorem | htthlem 28622* | Lemma for htth 28623. The collection 𝐾, which consists of functions 𝐹(𝑧)(𝑤) = 〈𝑤 ∣ 𝑇(𝑧)〉 = 〈𝑇(𝑤) ∣ 𝑧〉 for each 𝑧 in the unit ball, is a collection of bounded linear functions by ipblnfi 28560, so by the Uniform Boundedness theorem ubth 28578, there is a uniform bound 𝑦 on ∥ 𝐹(𝑥) ∥ for all 𝑥 in the unit ball. Then ∣ 𝑇(𝑥) ∣ ↑2 = 〈𝑇(𝑥) ∣ 𝑇(𝑥)〉 = 𝐹(𝑥)( 𝑇(𝑥)) ≤ 𝑦 ∣ 𝑇(𝑥) ∣, so ∣ 𝑇(𝑥) ∣ ≤ 𝑦 and 𝑇 is bounded. (Contributed by NM, 11-Jan-2008.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝐿 = (𝑈 LnOp 𝑈) & ⊢ 𝐵 = (𝑈 BLnOp 𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑈 ∈ CHilOLD & ⊢ 𝑊 = 〈〈 + , · 〉, abs〉 & ⊢ (𝜑 → 𝑇 ∈ 𝐿) & ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑃(𝑇‘𝑦)) = ((𝑇‘𝑥)𝑃𝑦)) & ⊢ 𝐹 = (𝑧 ∈ 𝑋 ↦ (𝑤 ∈ 𝑋 ↦ (𝑤𝑃(𝑇‘𝑧)))) & ⊢ 𝐾 = (𝐹 “ {𝑧 ∈ 𝑋 ∣ (𝑁‘𝑧) ≤ 1}) ⇒ ⊢ (𝜑 → 𝑇 ∈ 𝐵) | ||
Theorem | htth 28623* | 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 20778; note that df-hil 20778 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 28624 | Extend class notation with Hilbert vector space. |
class ℋ | ||
Syntax | cva 28625 | 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 28626 | 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 28627 | 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 4566. |
class ·ih | ||
Syntax | cno 28628 | 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 28629 | Extend class notation with zero vector in Hilbert space. |
class 0ℎ | ||
Syntax | cmv 28630 | Extend class notation with vector subtraction in Hilbert space. |
class −ℎ | ||
Syntax | ccauold 28631 | Extend class notation with set of Cauchy sequences in Hilbert space. |
class Cauchy | ||
Syntax | chli 28632 | Extend class notation with convergence relation in Hilbert space. |
class ⇝𝑣 | ||
Syntax | csh 28633 | Extend class notation with set of subspaces of a Hilbert space. |
class Sℋ | ||
Syntax | cch 28634 | Extend class notation with set of closed subspaces of a Hilbert space. |
class Cℋ | ||
Syntax | cort 28635 | Extend class notation with orthogonal complement in Cℋ. |
class ⊥ | ||
Syntax | cph 28636 | Extend class notation with subspace sum in Cℋ. |
class +ℋ | ||
Syntax | cspn 28637 | Extend class notation with subspace span in Cℋ. |
class span | ||
Syntax | chj 28638 | Extend class notation with join in Cℋ. |
class ∨ℋ | ||
Syntax | chsup 28639 | Extend class notation with supremum of a collection in Cℋ. |
class ∨ℋ | ||
Syntax | c0h 28640 | Extend class notation with zero of Cℋ. |
class 0ℋ | ||
Syntax | ccm 28641 | Extend class notation with the commutes relation on a Hilbert lattice. |
class 𝐶ℋ | ||
Syntax | cpjh 28642 | Extend class notation with set of projections on a Hilbert space. |
class projℎ | ||
Syntax | chos 28643 | Extend class notation with sum of Hilbert space operators. |
class +op | ||
Syntax | chot 28644 | Extend class notation with scalar product of a Hilbert space operator. |
class ·op | ||
Syntax | chod 28645 | Extend class notation with difference of Hilbert space operators. |
class −op | ||
Syntax | chfs 28646 | Extend class notation with sum of Hilbert space functionals. |
class +fn | ||
Syntax | chft 28647 | Extend class notation with scalar product of Hilbert space functional. |
class ·fn | ||
Syntax | ch0o 28648 | Extend class notation with the Hilbert space zero operator. |
class 0hop | ||
Syntax | chio 28649 | Extend class notation with Hilbert space identity operator. |
class Iop | ||
Syntax | cnop 28650 | Extend class notation with the operator norm function. |
class normop | ||
Syntax | ccop 28651 | Extend class notation with set of continuous Hilbert space operators. |
class ContOp | ||
Syntax | clo 28652 | Extend class notation with set of linear Hilbert space operators. |
class LinOp | ||
Syntax | cbo 28653 | Extend class notation with set of bounded linear operators. |
class BndLinOp | ||
Syntax | cuo 28654 | Extend class notation with set of unitary Hilbert space operators. |
class UniOp | ||
Syntax | cho 28655 | Extend class notation with set of Hermitian Hilbert space operators. |
class HrmOp | ||
Syntax | cnmf 28656 | Extend class notation with the functional norm function. |
class normfn | ||
Syntax | cnl 28657 | Extend class notation with the functional nullspace function. |
class null | ||
Syntax | ccnfn 28658 | Extend class notation with set of continuous Hilbert space functionals. |
class ContFn | ||
Syntax | clf 28659 | Extend class notation with set of linear Hilbert space functionals. |
class LinFn | ||
Syntax | cado 28660 | Extend class notation with Hilbert space adjoint function. |
class adjℎ | ||
Syntax | cbr 28661 | Extend class notation with the bra of a vector in Dirac bra-ket notation. |
class bra | ||
Syntax | ck 28662 | Extend class notation with the outer product of two vectors in Dirac bra-ket notation. |
class ketbra | ||
Syntax | cleo 28663 | Extend class notation with positive operator ordering. |
class ≤op | ||
Syntax | cei 28664 | Extend class notation with Hilbert space eigenvector function. |
class eigvec | ||
Syntax | cel 28665 | Extend class notation with Hilbert space eigenvalue function. |
class eigval | ||
Syntax | cspc 28666 | Extend class notation with the spectrum of an operator. |
class Lambda | ||
Syntax | cst 28667 | Extend class notation with set of states on a Hilbert lattice. |
class States | ||
Syntax | chst 28668 | Extend class notation with set of Hilbert-space-valued states on a Hilbert lattice. |
class CHStates | ||
Syntax | ccv 28669 | Extend class notation with the covers relation on a Hilbert lattice. |
class ⋖ℋ | ||
Syntax | cat 28670 | Extend class notation with set of atoms on a Hilbert lattice. |
class HAtoms | ||
Syntax | cmd 28671 | Extend class notation with the modular pair relation on a Hilbert lattice. |
class 𝑀ℋ | ||
Syntax | cdmd 28672 | Extend class notation with the dual modular pair relation on a Hilbert lattice. |
class 𝑀ℋ* | ||
Definition | df-hnorm 28673 | Define the function for the norm of a vector of Hilbert space. See normval 28829 for its value and normcl 28830 for its closure. Theorems norm-i-i 28838, norm-ii-i 28842, and norm-iii-i 28844 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 28674 | Define base set of Hilbert space, for use if we want to develop Hilbert space independently from the axioms (see comments in ax-hilex 28704). 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 28872. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ ℋ = (BaseSet‘〈〈 +ℎ , ·ℎ 〉, normℎ〉) | ||
Definition | df-h0v 28675 | 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 28873. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 0ℎ = (0vec‘〈〈 +ℎ , ·ℎ 〉, normℎ〉) | ||
Definition | df-hvsub 28676* | Define vector subtraction. See hvsubvali 28725 for its value and hvsubcli 28726 for its closure. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.) |
⊢ −ℎ = (𝑥 ∈ ℋ, 𝑦 ∈ ℋ ↦ (𝑥 +ℎ (-1 ·ℎ 𝑦))) | ||
Definition | df-hlim 28677* | Define the limit relation for Hilbert space. See hlimi 28893 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 28678* | Define the set of Cauchy sequences on a Hilbert space. See hcau 28889 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 28679 | The group (addition) operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ NrmCVec ⇒ ⊢ +ℎ = ( +𝑣 ‘𝑈) | ||
Theorem | h2hsm 28680 | The scalar product operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ NrmCVec ⇒ ⊢ ·ℎ = ( ·𝑠OLD ‘𝑈) | ||
Theorem | h2hnm 28681 | The norm function of Hilbert space. (Contributed by NM, 5-Jun-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ NrmCVec ⇒ ⊢ normℎ = (normCV‘𝑈) | ||
Theorem | h2hvs 28682 | 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 28683 | 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 28684 | 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 28685 | 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 28686 through axhcompl-zf 28703, 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 28673 above. See also the comment in ax-hilex 28704. | ||
Theorem | axhilex-zf 28686 | Derive axiom ax-hilex 28704 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ℋ ∈ V | ||
Theorem | axhfvadd-zf 28687 | Derive axiom ax-hfvadd 28705 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ +ℎ :( ℋ × ℋ)⟶ ℋ | ||
Theorem | axhvcom-zf 28688 | Derive axiom ax-hvcom 28706 from Hilbert space under ZF set theory. (Contributed by NM, 27-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)) | ||
Theorem | axhvass-zf 28689 | Derive axiom ax-hvass 28707 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = (𝐴 +ℎ (𝐵 +ℎ 𝐶))) | ||
Theorem | axhv0cl-zf 28690 | Derive axiom ax-hv0cl 28708 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ 0ℎ ∈ ℋ | ||
Theorem | axhvaddid-zf 28691 | Derive axiom ax-hvaddid 28709 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴) | ||
Theorem | axhfvmul-zf 28692 | Derive axiom ax-hfvmul 28710 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ·ℎ :(ℂ × ℋ)⟶ ℋ | ||
Theorem | axhvmulid-zf 28693 | Derive axiom ax-hvmulid 28711 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴) | ||
Theorem | axhvmulass-zf 28694 | Derive axiom ax-hvmulass 28712 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))) | ||
Theorem | axhvdistr1-zf 28695 | Derive axiom ax-hvdistr1 28713 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 +ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) +ℎ (𝐴 ·ℎ 𝐶))) | ||
Theorem | axhvdistr2-zf 28696 | Derive axiom ax-hvdistr2 28714 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 + 𝐵) ·ℎ 𝐶) = ((𝐴 ·ℎ 𝐶) +ℎ (𝐵 ·ℎ 𝐶))) | ||
Theorem | axhvmul0-zf 28697 | Derive axiom ax-hvmul0 28715 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ (𝐴 ∈ ℋ → (0 ·ℎ 𝐴) = 0ℎ) | ||
Theorem | axhfi-zf 28698 | Derive axiom ax-hfi 28784 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 28699 | Derive axiom ax-his1 28787 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 28700 | Derive axiom ax-his2 28788 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD & ⊢ ·ih = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) ·ih 𝐶) = ((𝐴 ·ih 𝐶) + (𝐵 ·ih 𝐶))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |