![]() |
Metamath
Proof Explorer Theorem List (p. 299 of 472) | < 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-29746) |
![]() (29747-31269) |
![]() (31270-47184) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-hcau 29801* | Define the set of Cauchy sequences on a Hilbert space. See hcau 30012 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 29802 | The group (addition) operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ NrmCVec ⇒ ⊢ +ℎ = ( +𝑣 ‘𝑈) | ||
Theorem | h2hsm 29803 | The scalar product operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ NrmCVec ⇒ ⊢ ·ℎ = ( ·𝑠OLD ‘𝑈) | ||
Theorem | h2hnm 29804 | The norm function of Hilbert space. (Contributed by NM, 5-Jun-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ NrmCVec ⇒ ⊢ normℎ = (normCV‘𝑈) | ||
Theorem | h2hvs 29805 | 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 29806 | 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 29807 | 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 29808 | 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 29809 through axhcompl-zf 29826, 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 29796 above. See also the comment in ax-hilex 29827. | ||
Theorem | axhilex-zf 29809 | Derive Axiom ax-hilex 29827 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ℋ ∈ V | ||
Theorem | axhfvadd-zf 29810 | Derive Axiom ax-hfvadd 29828 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ +ℎ :( ℋ × ℋ)⟶ ℋ | ||
Theorem | axhvcom-zf 29811 | Derive Axiom ax-hvcom 29829 from Hilbert space under ZF set theory. (Contributed by NM, 27-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)) | ||
Theorem | axhvass-zf 29812 | Derive Axiom ax-hvass 29830 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = (𝐴 +ℎ (𝐵 +ℎ 𝐶))) | ||
Theorem | axhv0cl-zf 29813 | Derive Axiom ax-hv0cl 29831 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ 0ℎ ∈ ℋ | ||
Theorem | axhvaddid-zf 29814 | Derive Axiom ax-hvaddid 29832 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴) | ||
Theorem | axhfvmul-zf 29815 | Derive Axiom ax-hfvmul 29833 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ·ℎ :(ℂ × ℋ)⟶ ℋ | ||
Theorem | axhvmulid-zf 29816 | Derive Axiom ax-hvmulid 29834 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴) | ||
Theorem | axhvmulass-zf 29817 | Derive Axiom ax-hvmulass 29835 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))) | ||
Theorem | axhvdistr1-zf 29818 | Derive Axiom ax-hvdistr1 29836 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 +ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) +ℎ (𝐴 ·ℎ 𝐶))) | ||
Theorem | axhvdistr2-zf 29819 | Derive Axiom ax-hvdistr2 29837 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 + 𝐵) ·ℎ 𝐶) = ((𝐴 ·ℎ 𝐶) +ℎ (𝐵 ·ℎ 𝐶))) | ||
Theorem | axhvmul0-zf 29820 | Derive Axiom ax-hvmul0 29838 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ (𝐴 ∈ ℋ → (0 ·ℎ 𝐴) = 0ℎ) | ||
Theorem | axhfi-zf 29821 | Derive Axiom ax-hfi 29907 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 29822 | Derive Axiom ax-his1 29910 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 29823 | Derive Axiom ax-his2 29911 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 29824 | Derive Axiom ax-his3 29912 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 29825 | Derive Axiom ax-his4 29913 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 29826* | Derive Axiom ax-hcompl 30030 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 29827, ax-hfvadd 29828, ax-hvcom 29829, ax-hvass 29830, ax-hv0cl 29831, ax-hvaddid 29832, ax-hfvmul 29833, ax-hvmulid 29834, ax-hvmulass 29835, ax-hvdistr1 29836, ax-hvdistr2 29837, ax-hvmul0 29838, ax-hfi 29907, ax-his1 29910, ax-his2 29911, ax-his3 29912, ax-his4 29913, and ax-hcompl 30030. 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 29809, axhfvadd-zf 29810, axhvcom-zf 29811, axhvass-zf 29812, axhv0cl-zf 29813, axhvaddid-zf 29814, axhfvmul-zf 29815, axhvmulid-zf 29816, axhvmulass-zf 29817, axhvdistr1-zf 29818, axhvdistr2-zf 29819, axhvmul0-zf 29820, axhfi-zf 29821, axhis1-zf 29822, axhis2-zf 29823, axhis3-zf 29824, axhis4-zf 29825, and axhcompl-zf 29826 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 29809. | ||
Axiom | ax-hilex 29827 | 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 29828 | Vector addition is an operation on ℋ. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
⊢ +ℎ :( ℋ × ℋ)⟶ ℋ | ||
Axiom | ax-hvcom 29829 | Vector addition is commutative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)) | ||
Axiom | ax-hvass 29830 | Vector addition is associative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = (𝐴 +ℎ (𝐵 +ℎ 𝐶))) | ||
Axiom | ax-hv0cl 29831 | The zero vector is in the vector space. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
⊢ 0ℎ ∈ ℋ | ||
Axiom | ax-hvaddid 29832 | Addition with the zero vector. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴) | ||
Axiom | ax-hfvmul 29833 | Scalar multiplication is an operation on ℂ and ℋ. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
⊢ ·ℎ :(ℂ × ℋ)⟶ ℋ | ||
Axiom | ax-hvmulid 29834 | Scalar multiplication by one. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴) | ||
Axiom | ax-hvmulass 29835 | Scalar multiplication associative law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))) | ||
Axiom | ax-hvdistr1 29836 | Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 +ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) +ℎ (𝐴 ·ℎ 𝐶))) | ||
Axiom | ax-hvdistr2 29837 | Scalar multiplication distributive law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 + 𝐵) ·ℎ 𝐶) = ((𝐴 ·ℎ 𝐶) +ℎ (𝐵 ·ℎ 𝐶))) | ||
Axiom | ax-hvmul0 29838 | Scalar multiplication by zero. We can derive the existence of the negative of a vector from this axiom (see hvsubid 29854 and hvsubval 29844). (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (0 ·ℎ 𝐴) = 0ℎ) | ||
Theorem | hvmulex 29839 | The Hilbert space scalar product operation is a set. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.) |
⊢ ·ℎ ∈ V | ||
Theorem | hvaddcl 29840 | Closure of vector addition. (Contributed by NM, 18-Apr-2007.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) ∈ ℋ) | ||
Theorem | hvmulcl 29841 | Closure of scalar multiplication. (Contributed by NM, 19-Apr-2007.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ℎ 𝐵) ∈ ℋ) | ||
Theorem | hvmulcli 29842 | Closure inference for scalar multiplication. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 ·ℎ 𝐵) ∈ ℋ | ||
Theorem | hvsubf 29843 | Mapping domain and codomain of vector subtraction. (Contributed by NM, 6-Sep-2007.) (New usage is discouraged.) |
⊢ −ℎ :( ℋ × ℋ)⟶ ℋ | ||
Theorem | hvsubval 29844 | Value of vector subtraction. (Contributed by NM, 5-Sep-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 −ℎ 𝐵) = (𝐴 +ℎ (-1 ·ℎ 𝐵))) | ||
Theorem | hvsubcl 29845 | Closure of vector subtraction. (Contributed by NM, 17-Aug-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 −ℎ 𝐵) ∈ ℋ) | ||
Theorem | hvaddcli 29846 | Closure of vector addition. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 +ℎ 𝐵) ∈ ℋ | ||
Theorem | hvcomi 29847 | Commutation of vector addition. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴) | ||
Theorem | hvsubvali 29848 | Value of vector subtraction definition. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 −ℎ 𝐵) = (𝐴 +ℎ (-1 ·ℎ 𝐵)) | ||
Theorem | hvsubcli 29849 | Closure of vector subtraction. (Contributed by NM, 2-Aug-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 −ℎ 𝐵) ∈ ℋ | ||
Theorem | ifhvhv0 29850 | Prove if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ. (Contributed by David A. Wheeler, 7-Dec-2018.) (New usage is discouraged.) |
⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ | ||
Theorem | hvaddid2 29851 | Addition with the zero vector. (Contributed by NM, 18-Oct-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (0ℎ +ℎ 𝐴) = 𝐴) | ||
Theorem | hvmul0 29852 | Scalar multiplication with the zero vector. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℂ → (𝐴 ·ℎ 0ℎ) = 0ℎ) | ||
Theorem | hvmul0or 29853 | 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 29854 | Subtraction of a vector from itself. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (𝐴 −ℎ 𝐴) = 0ℎ) | ||
Theorem | hvnegid 29855 | Addition of negative of a vector to itself. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ (-1 ·ℎ 𝐴)) = 0ℎ) | ||
Theorem | hv2neg 29856 | Two ways to express the negative of a vector. (Contributed by NM, 23-May-2005.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (0ℎ −ℎ 𝐴) = (-1 ·ℎ 𝐴)) | ||
Theorem | hvaddid2i 29857 | Addition with the zero vector. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ ⇒ ⊢ (0ℎ +ℎ 𝐴) = 𝐴 | ||
Theorem | hvnegidi 29858 | Addition of negative of a vector to itself. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ ⇒ ⊢ (𝐴 +ℎ (-1 ·ℎ 𝐴)) = 0ℎ | ||
Theorem | hv2negi 29859 | Two ways to express the negative of a vector. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ ⇒ ⊢ (0ℎ −ℎ 𝐴) = (-1 ·ℎ 𝐴) | ||
Theorem | hvm1neg 29860 | 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 29861 | Value of vector addition in terms of vector subtraction. (Contributed by NM, 10-Jun-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐴 −ℎ (-1 ·ℎ 𝐵))) | ||
Theorem | hvadd32 29862 | Commutative/associative law. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = ((𝐴 +ℎ 𝐶) +ℎ 𝐵)) | ||
Theorem | hvadd12 29863 | Commutative/associative law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 +ℎ (𝐵 +ℎ 𝐶)) = (𝐵 +ℎ (𝐴 +ℎ 𝐶))) | ||
Theorem | hvadd4 29864 | Hilbert vector space addition law. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 +ℎ 𝐵) +ℎ (𝐶 +ℎ 𝐷)) = ((𝐴 +ℎ 𝐶) +ℎ (𝐵 +ℎ 𝐷))) | ||
Theorem | hvsub4 29865 | Hilbert vector space addition/subtraction law. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 +ℎ 𝐵) −ℎ (𝐶 +ℎ 𝐷)) = ((𝐴 −ℎ 𝐶) +ℎ (𝐵 −ℎ 𝐷))) | ||
Theorem | hvaddsub12 29866 | Commutative/associative law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 +ℎ (𝐵 −ℎ 𝐶)) = (𝐵 +ℎ (𝐴 −ℎ 𝐶))) | ||
Theorem | hvpncan 29867 | Addition/subtraction cancellation law for vectors in Hilbert space. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 +ℎ 𝐵) −ℎ 𝐵) = 𝐴) | ||
Theorem | hvpncan2 29868 | Addition/subtraction cancellation law for vectors in Hilbert space. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 +ℎ 𝐵) −ℎ 𝐴) = 𝐵) | ||
Theorem | hvaddsubass 29869 | Associativity of sum and difference of Hilbert space vectors. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) −ℎ 𝐶) = (𝐴 +ℎ (𝐵 −ℎ 𝐶))) | ||
Theorem | hvpncan3 29870 | Subtraction and addition of equal Hilbert space vectors. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ (𝐵 −ℎ 𝐴)) = 𝐵) | ||
Theorem | hvmulcom 29871 | Scalar multiplication commutative law. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) = (𝐵 ·ℎ (𝐴 ·ℎ 𝐶))) | ||
Theorem | hvsubass 29872 | Hilbert vector space associative law for subtraction. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 −ℎ 𝐵) −ℎ 𝐶) = (𝐴 −ℎ (𝐵 +ℎ 𝐶))) | ||
Theorem | hvsub32 29873 | Hilbert vector space commutative/associative law. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 −ℎ 𝐵) −ℎ 𝐶) = ((𝐴 −ℎ 𝐶) −ℎ 𝐵)) | ||
Theorem | hvmulassi 29874 | Scalar multiplication associative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) | ||
Theorem | hvmulcomi 29875 | Scalar multiplication commutative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) = (𝐵 ·ℎ (𝐴 ·ℎ 𝐶)) | ||
Theorem | hvmul2negi 29876 | Double negative in scalar multiplication. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ (-𝐴 ·ℎ (-𝐵 ·ℎ 𝐶)) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) | ||
Theorem | hvsubdistr1 29877 | Scalar multiplication distributive law for subtraction. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 −ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) −ℎ (𝐴 ·ℎ 𝐶))) | ||
Theorem | hvsubdistr2 29878 | Scalar multiplication distributive law for subtraction. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 − 𝐵) ·ℎ 𝐶) = ((𝐴 ·ℎ 𝐶) −ℎ (𝐵 ·ℎ 𝐶))) | ||
Theorem | hvdistr1i 29879 | Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ (𝐴 ·ℎ (𝐵 +ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) +ℎ (𝐴 ·ℎ 𝐶)) | ||
Theorem | hvsubdistr1i 29880 | Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ (𝐴 ·ℎ (𝐵 −ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) −ℎ (𝐴 ·ℎ 𝐶)) | ||
Theorem | hvassi 29881 | Hilbert vector space associative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = (𝐴 +ℎ (𝐵 +ℎ 𝐶)) | ||
Theorem | hvadd32i 29882 | Hilbert vector space commutative/associative law. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = ((𝐴 +ℎ 𝐶) +ℎ 𝐵) | ||
Theorem | hvsubassi 29883 | 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 29884 | 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 29885 | Hilbert vector space commutative/associative law. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ (𝐴 +ℎ (𝐵 +ℎ 𝐶)) = (𝐵 +ℎ (𝐴 +ℎ 𝐶)) | ||
Theorem | hvadd4i 29886 | Hilbert vector space addition law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ & ⊢ 𝐷 ∈ ℋ ⇒ ⊢ ((𝐴 +ℎ 𝐵) +ℎ (𝐶 +ℎ 𝐷)) = ((𝐴 +ℎ 𝐶) +ℎ (𝐵 +ℎ 𝐷)) | ||
Theorem | hvsubsub4i 29887 | Hilbert vector space addition law. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ & ⊢ 𝐷 ∈ ℋ ⇒ ⊢ ((𝐴 −ℎ 𝐵) −ℎ (𝐶 −ℎ 𝐷)) = ((𝐴 −ℎ 𝐶) −ℎ (𝐵 −ℎ 𝐷)) | ||
Theorem | hvsubsub4 29888 | Hilbert vector space addition/subtraction law. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 −ℎ 𝐵) −ℎ (𝐶 −ℎ 𝐷)) = ((𝐴 −ℎ 𝐶) −ℎ (𝐵 −ℎ 𝐷))) | ||
Theorem | hv2times 29889 | Two times a vector. (Contributed by NM, 22-Jun-2006.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (2 ·ℎ 𝐴) = (𝐴 +ℎ 𝐴)) | ||
Theorem | hvnegdii 29890 | Distribution of negative over subtraction. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (-1 ·ℎ (𝐴 −ℎ 𝐵)) = (𝐵 −ℎ 𝐴) | ||
Theorem | hvsubeq0i 29891 | If the difference between two vectors is zero, they are equal. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ ((𝐴 −ℎ 𝐵) = 0ℎ ↔ 𝐴 = 𝐵) | ||
Theorem | hvsubcan2i 29892 | Vector cancellation law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ ((𝐴 +ℎ 𝐵) +ℎ (𝐴 −ℎ 𝐵)) = (2 ·ℎ 𝐴) | ||
Theorem | hvaddcani 29893 | Cancellation law for vector addition. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((𝐴 +ℎ 𝐵) = (𝐴 +ℎ 𝐶) ↔ 𝐵 = 𝐶) | ||
Theorem | hvsubaddi 29894 | Relationship between vector subtraction and addition. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((𝐴 −ℎ 𝐵) = 𝐶 ↔ (𝐵 +ℎ 𝐶) = 𝐴) | ||
Theorem | hvnegdi 29895 | Distribution of negative over subtraction. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (-1 ·ℎ (𝐴 −ℎ 𝐵)) = (𝐵 −ℎ 𝐴)) | ||
Theorem | hvsubeq0 29896 | If the difference between two vectors is zero, they are equal. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 −ℎ 𝐵) = 0ℎ ↔ 𝐴 = 𝐵)) | ||
Theorem | hvaddeq0 29897 | If the sum of two vectors is zero, one is the negative of the other. (Contributed by NM, 10-Jun-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 +ℎ 𝐵) = 0ℎ ↔ 𝐴 = (-1 ·ℎ 𝐵))) | ||
Theorem | hvaddcan 29898 | Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) = (𝐴 +ℎ 𝐶) ↔ 𝐵 = 𝐶)) | ||
Theorem | hvaddcan2 29899 | Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐶) = (𝐵 +ℎ 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | hvmulcan 29900 | Cancellation law for scalar multiplication. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) = (𝐴 ·ℎ 𝐶) ↔ 𝐵 = 𝐶)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |