Home | Metamath
Proof Explorer Theorem List (p. 273 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cel 27201 | Extend class notation with Hilbert space eigenvalue function. |
class eigval | ||
Syntax | cspc 27202 | Extend class notation with the spectrum of an operator. |
class Lambda | ||
Syntax | cst 27203 | Extend class notation with set of states on a Hilbert lattice. |
class States | ||
Syntax | chst 27204 | Extend class notation with set of Hilbert-space-valued states on a Hilbert lattice. |
class CHStates | ||
Syntax | ccv 27205 | Extend class notation with the covers relation on a Hilbert lattice. |
class ⋖ℋ | ||
Syntax | cat 27206 | Extend class notation with set of atoms on a Hilbert lattice. |
class HAtoms | ||
Syntax | cmd 27207 | Extend class notation with the modular pair relation on a Hilbert lattice. |
class 𝑀ℋ | ||
Syntax | cdmd 27208 | Extend class notation with the dual modular pair relation on a Hilbert lattice. |
class 𝑀ℋ* | ||
Definition | df-hnorm 27209 | Define the function for the norm of a vector of Hilbert space. See normval 27365 for its value and normcl 27366 for its closure. Theorems norm-i-i 27374, norm-ii-i 27378, and norm-iii-i 27380 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 27210 | Define base set of Hilbert space, for use if we want to develop Hilbert space independently from the axioms (see comments in ax-hilex 27240). 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 27408. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ ℋ = (BaseSet‘〈〈 +ℎ , ·ℎ 〉, normℎ〉) | ||
Definition | df-h0v 27211 | 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 27409. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 0ℎ = (0vec‘〈〈 +ℎ , ·ℎ 〉, normℎ〉) | ||
Definition | df-hvsub 27212* | Define vector subtraction. See hvsubvali 27261 for its value and hvsubcli 27262 for its closure. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.) |
⊢ −ℎ = (𝑥 ∈ ℋ, 𝑦 ∈ ℋ ↦ (𝑥 +ℎ (-1 ·ℎ 𝑦))) | ||
Definition | df-hlim 27213* | Define the limit relation for Hilbert space. See hlimi 27429 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 27214* | Define the set of Cauchy sequences on a Hilbert space. See hcau 27425 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 = {𝑓 ∈ ( ℋ ↑𝑚 ℕ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥} | ||
Theorem | h2hva 27215 | The group (addition) operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ NrmCVec ⇒ ⊢ +ℎ = ( +𝑣 ‘𝑈) | ||
Theorem | h2hsm 27216 | The scalar product operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ NrmCVec ⇒ ⊢ ·ℎ = ( ·𝑠OLD ‘𝑈) | ||
Theorem | h2hnm 27217 | The norm function of Hilbert space. (Contributed by NM, 5-Jun-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ NrmCVec ⇒ ⊢ normℎ = (normCV‘𝑈) | ||
Theorem | h2hvs 27218 | 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 27219 | 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 27220 | 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‘𝐷) ∩ ( ℋ ↑𝑚 ℕ)) | ||
Theorem | h2hlm 27221 | The limit 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‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ⇝𝑣 = ((⇝𝑡‘𝐽) ↾ ( ℋ ↑𝑚 ℕ)) | ||
Before introducing the 18 axioms for Hilbert space, we first prove them as the conclusions of theorems axhilex-zf 27222 through axhcompl-zf 27239, 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 27209 above. See also the comment in ax-hilex 27240. | ||
Theorem | axhilex-zf 27222 | Derive axiom ax-hilex 27240 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ℋ ∈ V | ||
Theorem | axhfvadd-zf 27223 | Derive axiom ax-hfvadd 27241 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ +ℎ :( ℋ × ℋ)⟶ ℋ | ||
Theorem | axhvcom-zf 27224 | Derive axiom ax-hvcom 27242 from Hilbert space under ZF set theory. (Contributed by NM, 27-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)) | ||
Theorem | axhvass-zf 27225 | Derive axiom ax-hvass 27243 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = (𝐴 +ℎ (𝐵 +ℎ 𝐶))) | ||
Theorem | axhv0cl-zf 27226 | Derive axiom ax-hv0cl 27244 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ 0ℎ ∈ ℋ | ||
Theorem | axhvaddid-zf 27227 | Derive axiom ax-hvaddid 27245 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴) | ||
Theorem | axhfvmul-zf 27228 | Derive axiom ax-hfvmul 27246 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ·ℎ :(ℂ × ℋ)⟶ ℋ | ||
Theorem | axhvmulid-zf 27229 | Derive axiom ax-hvmulid 27247 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴) | ||
Theorem | axhvmulass-zf 27230 | Derive axiom ax-hvmulass 27248 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))) | ||
Theorem | axhvdistr1-zf 27231 | Derive axiom ax-hvdistr1 27249 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 +ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) +ℎ (𝐴 ·ℎ 𝐶))) | ||
Theorem | axhvdistr2-zf 27232 | Derive axiom ax-hvdistr2 27250 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 + 𝐵) ·ℎ 𝐶) = ((𝐴 ·ℎ 𝐶) +ℎ (𝐵 ·ℎ 𝐶))) | ||
Theorem | axhvmul0-zf 27233 | Derive axiom ax-hvmul0 27251 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ (𝐴 ∈ ℋ → (0 ·ℎ 𝐴) = 0ℎ) | ||
Theorem | axhfi-zf 27234 | Derive axiom ax-hfi 27320 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 27235 | Derive axiom ax-his1 27323 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 27236 | Derive axiom ax-his2 27324 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 27237 | Derive axiom ax-his3 27325 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 27238 | Derive axiom ax-his4 27326 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 27239* | Derive axiom ax-hcompl 27443 from Hilbert space under ZF set theory. (Contributed by NM, 6-Jun-2008.) (Revised by Mario Carneiro, 13-May-2014.) (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 27240, ax-hfvadd 27241, ax-hvcom 27242, ax-hvass 27243, ax-hv0cl 27244, ax-hvaddid 27245, ax-hfvmul 27246, ax-hvmulid 27247, ax-hvmulass 27248, ax-hvdistr1 27249, ax-hvdistr2 27250, ax-hvmul0 27251, ax-hfi 27320, ax-his1 27323, ax-his2 27324, ax-his3 27325, ax-his4 27326, and ax-hcompl 27443. 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 27222, axhfvadd-zf 27223, axhvcom-zf 27224, axhvass-zf 27225, axhv0cl-zf 27226, axhvaddid-zf 27227, axhfvmul-zf 27228, axhvmulid-zf 27229, axhvmulass-zf 27230, axhvdistr1-zf 27231, axhvdistr2-zf 27232, axhvmul0-zf 27233, axhfi-zf 27234, axhis1-zf 27235, axhis2-zf 27236, axhis3-zf 27237, axhis4-zf 27238, and axhcompl-zf 27239 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 27222. | ||
Axiom | ax-hilex 27240 | 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 27241 | Vector addition is an operation on ℋ. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
⊢ +ℎ :( ℋ × ℋ)⟶ ℋ | ||
Axiom | ax-hvcom 27242 | Vector addition is commutative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)) | ||
Axiom | ax-hvass 27243 | Vector addition is associative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = (𝐴 +ℎ (𝐵 +ℎ 𝐶))) | ||
Axiom | ax-hv0cl 27244 | The zero vector is in the vector space. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
⊢ 0ℎ ∈ ℋ | ||
Axiom | ax-hvaddid 27245 | Addition with the zero vector. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴) | ||
Axiom | ax-hfvmul 27246 | Scalar multiplication is an operation on ℂ and ℋ. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
⊢ ·ℎ :(ℂ × ℋ)⟶ ℋ | ||
Axiom | ax-hvmulid 27247 | Scalar multiplication by one. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴) | ||
Axiom | ax-hvmulass 27248 | Scalar multiplication associative law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))) | ||
Axiom | ax-hvdistr1 27249 | Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 +ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) +ℎ (𝐴 ·ℎ 𝐶))) | ||
Axiom | ax-hvdistr2 27250 | Scalar multiplication distributive law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 + 𝐵) ·ℎ 𝐶) = ((𝐴 ·ℎ 𝐶) +ℎ (𝐵 ·ℎ 𝐶))) | ||
Axiom | ax-hvmul0 27251 | Scalar multiplication by zero. We can derive the existence of the negative of a vector from this axiom (see hvsubid 27267 and hvsubval 27257). (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (0 ·ℎ 𝐴) = 0ℎ) | ||
Theorem | hvmulex 27252 | The Hilbert space scalar product operation is a set. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.) |
⊢ ·ℎ ∈ V | ||
Theorem | hvaddcl 27253 | Closure of vector addition. (Contributed by NM, 18-Apr-2007.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) ∈ ℋ) | ||
Theorem | hvmulcl 27254 | Closure of scalar multiplication. (Contributed by NM, 19-Apr-2007.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ℎ 𝐵) ∈ ℋ) | ||
Theorem | hvmulcli 27255 | Closure inference for scalar multiplication. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 ·ℎ 𝐵) ∈ ℋ | ||
Theorem | hvsubf 27256 | Mapping domain and codomain of vector subtraction. (Contributed by NM, 6-Sep-2007.) (New usage is discouraged.) |
⊢ −ℎ :( ℋ × ℋ)⟶ ℋ | ||
Theorem | hvsubval 27257 | Value of vector subtraction. (Contributed by NM, 5-Sep-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 −ℎ 𝐵) = (𝐴 +ℎ (-1 ·ℎ 𝐵))) | ||
Theorem | hvsubcl 27258 | Closure of vector subtraction. (Contributed by NM, 17-Aug-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 −ℎ 𝐵) ∈ ℋ) | ||
Theorem | hvaddcli 27259 | Closure of vector addition. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 +ℎ 𝐵) ∈ ℋ | ||
Theorem | hvcomi 27260 | Commutation of vector addition. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴) | ||
Theorem | hvsubvali 27261 | Value of vector subtraction definition. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 −ℎ 𝐵) = (𝐴 +ℎ (-1 ·ℎ 𝐵)) | ||
Theorem | hvsubcli 27262 | Closure of vector subtraction. (Contributed by NM, 2-Aug-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 −ℎ 𝐵) ∈ ℋ | ||
Theorem | ifhvhv0 27263 | Prove if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ (common case). (Contributed by David A. Wheeler, 7-Dec-2018.) (New usage is discouraged.) |
⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ | ||
Theorem | hvaddid2 27264 | Addition with the zero vector. (Contributed by NM, 18-Oct-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (0ℎ +ℎ 𝐴) = 𝐴) | ||
Theorem | hvmul0 27265 | Scalar multiplication with the zero vector. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℂ → (𝐴 ·ℎ 0ℎ) = 0ℎ) | ||
Theorem | hvmul0or 27266 | If a scalar product is zero, one of its factors must be zero. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) = 0ℎ ↔ (𝐴 = 0 ∨ 𝐵 = 0ℎ))) | ||
Theorem | hvsubid 27267 | Subtraction of a vector from itself. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (𝐴 −ℎ 𝐴) = 0ℎ) | ||
Theorem | hvnegid 27268 | Addition of negative of a vector to itself. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ (-1 ·ℎ 𝐴)) = 0ℎ) | ||
Theorem | hv2neg 27269 | Two ways to express the negative of a vector. (Contributed by NM, 23-May-2005.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (0ℎ −ℎ 𝐴) = (-1 ·ℎ 𝐴)) | ||
Theorem | hvaddid2i 27270 | Addition with the zero vector. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ ⇒ ⊢ (0ℎ +ℎ 𝐴) = 𝐴 | ||
Theorem | hvnegidi 27271 | Addition of negative of a vector to itself. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ ⇒ ⊢ (𝐴 +ℎ (-1 ·ℎ 𝐴)) = 0ℎ | ||
Theorem | hv2negi 27272 | Two ways to express the negative of a vector. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ ⇒ ⊢ (0ℎ −ℎ 𝐴) = (-1 ·ℎ 𝐴) | ||
Theorem | hvm1neg 27273 | Convert minus one times a scalar product to the negative of the scalar. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (-1 ·ℎ (𝐴 ·ℎ 𝐵)) = (-𝐴 ·ℎ 𝐵)) | ||
Theorem | hvaddsubval 27274 | Value of vector addition in terms of vector subtraction. (Contributed by NM, 10-Jun-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐴 −ℎ (-1 ·ℎ 𝐵))) | ||
Theorem | hvadd32 27275 | Commutative/associative law. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = ((𝐴 +ℎ 𝐶) +ℎ 𝐵)) | ||
Theorem | hvadd12 27276 | Commutative/associative law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 +ℎ (𝐵 +ℎ 𝐶)) = (𝐵 +ℎ (𝐴 +ℎ 𝐶))) | ||
Theorem | hvadd4 27277 | Hilbert vector space addition law. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 +ℎ 𝐵) +ℎ (𝐶 +ℎ 𝐷)) = ((𝐴 +ℎ 𝐶) +ℎ (𝐵 +ℎ 𝐷))) | ||
Theorem | hvsub4 27278 | Hilbert vector space addition/subtraction law. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 +ℎ 𝐵) −ℎ (𝐶 +ℎ 𝐷)) = ((𝐴 −ℎ 𝐶) +ℎ (𝐵 −ℎ 𝐷))) | ||
Theorem | hvaddsub12 27279 | Commutative/associative law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 +ℎ (𝐵 −ℎ 𝐶)) = (𝐵 +ℎ (𝐴 −ℎ 𝐶))) | ||
Theorem | hvpncan 27280 | Addition/subtraction cancellation law for vectors in Hilbert space. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 +ℎ 𝐵) −ℎ 𝐵) = 𝐴) | ||
Theorem | hvpncan2 27281 | Addition/subtraction cancellation law for vectors in Hilbert space. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 +ℎ 𝐵) −ℎ 𝐴) = 𝐵) | ||
Theorem | hvaddsubass 27282 | Associativity of sum and difference of Hilbert space vectors. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) −ℎ 𝐶) = (𝐴 +ℎ (𝐵 −ℎ 𝐶))) | ||
Theorem | hvpncan3 27283 | Subtraction and addition of equal Hilbert space vectors. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ (𝐵 −ℎ 𝐴)) = 𝐵) | ||
Theorem | hvmulcom 27284 | Scalar multiplication commutative law. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) = (𝐵 ·ℎ (𝐴 ·ℎ 𝐶))) | ||
Theorem | hvsubass 27285 | Hilbert vector space associative law for subtraction. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 −ℎ 𝐵) −ℎ 𝐶) = (𝐴 −ℎ (𝐵 +ℎ 𝐶))) | ||
Theorem | hvsub32 27286 | Hilbert vector space commutative/associative law. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 −ℎ 𝐵) −ℎ 𝐶) = ((𝐴 −ℎ 𝐶) −ℎ 𝐵)) | ||
Theorem | hvmulassi 27287 | Scalar multiplication associative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) | ||
Theorem | hvmulcomi 27288 | Scalar multiplication commutative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) = (𝐵 ·ℎ (𝐴 ·ℎ 𝐶)) | ||
Theorem | hvmul2negi 27289 | Double negative in scalar multiplication. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ (-𝐴 ·ℎ (-𝐵 ·ℎ 𝐶)) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) | ||
Theorem | hvsubdistr1 27290 | Scalar multiplication distributive law for subtraction. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 −ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) −ℎ (𝐴 ·ℎ 𝐶))) | ||
Theorem | hvsubdistr2 27291 | Scalar multiplication distributive law for subtraction. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 − 𝐵) ·ℎ 𝐶) = ((𝐴 ·ℎ 𝐶) −ℎ (𝐵 ·ℎ 𝐶))) | ||
Theorem | hvdistr1i 27292 | Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ (𝐴 ·ℎ (𝐵 +ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) +ℎ (𝐴 ·ℎ 𝐶)) | ||
Theorem | hvsubdistr1i 27293 | Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ (𝐴 ·ℎ (𝐵 −ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) −ℎ (𝐴 ·ℎ 𝐶)) | ||
Theorem | hvassi 27294 | Hilbert vector space associative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = (𝐴 +ℎ (𝐵 +ℎ 𝐶)) | ||
Theorem | hvadd32i 27295 | Hilbert vector space commutative/associative law. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = ((𝐴 +ℎ 𝐶) +ℎ 𝐵) | ||
Theorem | hvsubassi 27296 | Hilbert vector space associative law for subtraction. (Contributed by NM, 7-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((𝐴 −ℎ 𝐵) −ℎ 𝐶) = (𝐴 −ℎ (𝐵 +ℎ 𝐶)) | ||
Theorem | hvsub32i 27297 | Hilbert vector space commutative/associative law. (Contributed by NM, 7-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((𝐴 −ℎ 𝐵) −ℎ 𝐶) = ((𝐴 −ℎ 𝐶) −ℎ 𝐵) | ||
Theorem | hvadd12i 27298 | Hilbert vector space commutative/associative law. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ (𝐴 +ℎ (𝐵 +ℎ 𝐶)) = (𝐵 +ℎ (𝐴 +ℎ 𝐶)) | ||
Theorem | hvadd4i 27299 | Hilbert vector space addition law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ & ⊢ 𝐷 ∈ ℋ ⇒ ⊢ ((𝐴 +ℎ 𝐵) +ℎ (𝐶 +ℎ 𝐷)) = ((𝐴 +ℎ 𝐶) +ℎ (𝐵 +ℎ 𝐷)) | ||
Theorem | hvsubsub4i 27300 | Hilbert vector space addition law. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ & ⊢ 𝐷 ∈ ℋ ⇒ ⊢ ((𝐴 −ℎ 𝐵) −ℎ (𝐶 −ℎ 𝐷)) = ((𝐴 −ℎ 𝐶) −ℎ (𝐵 −ℎ 𝐷)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |