HomeTheorem List (p. 310 of 498)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 310 of 498) | < 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-30847) |
Hilbert Space Explorer
(30848-32370) |
Users' Mathboxes
(32371-49794) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Definition | df-hlim 30901* | Define the limit relation for Hilbert space. See hlimi 31117 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 30902* | Define the set of Cauchy sequences on a Hilbert space. See hcau 31113 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 30903 | The group (addition) operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝑈 ∈ NrmCVec ⇒ ⊢ +ℎ = ( +𝑣 ‘𝑈) | ||
| Theorem | h2hsm 30904 | The scalar product operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝑈 ∈ NrmCVec ⇒ ⊢ ·ℎ = ( ·𝑠OLD ‘𝑈) | ||
| Theorem | h2hnm 30905 | The norm function of Hilbert space. (Contributed by NM, 5-Jun-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝑈 ∈ NrmCVec ⇒ ⊢ normℎ = (normCV‘𝑈) | ||
| Theorem | h2hvs 30906 | 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 30907 | 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 30908 | 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 30909 | 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 30910 through axhcompl-zf 30927, 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 30897 above. See also the comment in ax-hilex 30928. | ||
| Theorem | axhilex-zf 30910 | Derive Axiom ax-hilex 30928 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ℋ ∈ V | ||
| Theorem | axhfvadd-zf 30911 | Derive Axiom ax-hfvadd 30929 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ +ℎ :( ℋ × ℋ)⟶ ℋ | ||
| Theorem | axhvcom-zf 30912 | Derive Axiom ax-hvcom 30930 from Hilbert space under ZF set theory. (Contributed by NM, 27-May-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)) | ||
| Theorem | axhvass-zf 30913 | Derive Axiom ax-hvass 30931 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = (𝐴 +ℎ (𝐵 +ℎ 𝐶))) | ||
| Theorem | axhv0cl-zf 30914 | Derive Axiom ax-hv0cl 30932 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ 0ℎ ∈ ℋ | ||
| Theorem | axhvaddid-zf 30915 | Derive Axiom ax-hvaddid 30933 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴) | ||
| Theorem | axhfvmul-zf 30916 | Derive Axiom ax-hfvmul 30934 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ·ℎ :(ℂ × ℋ)⟶ ℋ | ||
| Theorem | axhvmulid-zf 30917 | Derive Axiom ax-hvmulid 30935 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴) | ||
| Theorem | axhvmulass-zf 30918 | Derive Axiom ax-hvmulass 30936 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))) | ||
| Theorem | axhvdistr1-zf 30919 | Derive Axiom ax-hvdistr1 30937 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 +ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) +ℎ (𝐴 ·ℎ 𝐶))) | ||
| Theorem | axhvdistr2-zf 30920 | Derive Axiom ax-hvdistr2 30938 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 + 𝐵) ·ℎ 𝐶) = ((𝐴 ·ℎ 𝐶) +ℎ (𝐵 ·ℎ 𝐶))) | ||
| Theorem | axhvmul0-zf 30921 | Derive Axiom ax-hvmul0 30939 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ & ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ (𝐴 ∈ ℋ → (0 ·ℎ 𝐴) = 0ℎ) | ||
| Theorem | axhfi-zf 30922 | Derive Axiom ax-hfi 31008 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 30923 | Derive Axiom ax-his1 31011 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 30924 | Derive Axiom ax-his2 31012 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 30925 | Derive Axiom ax-his3 31013 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 30926 | Derive Axiom ax-his4 31014 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 30927* | Derive Axiom ax-hcompl 31131 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 30928, ax-hfvadd 30929, ax-hvcom 30930, ax-hvass 30931, ax-hv0cl 30932, ax-hvaddid 30933, ax-hfvmul 30934, ax-hvmulid 30935, ax-hvmulass 30936, ax-hvdistr1 30937, ax-hvdistr2 30938, ax-hvmul0 30939, ax-hfi 31008, ax-his1 31011, ax-his2 31012, ax-his3 31013, ax-his4 31014, and ax-hcompl 31131. 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 30910, axhfvadd-zf 30911, axhvcom-zf 30912, axhvass-zf 30913, axhv0cl-zf 30914, axhvaddid-zf 30915, axhfvmul-zf 30916, axhvmulid-zf 30917, axhvmulass-zf 30918, axhvdistr1-zf 30919, axhvdistr2-zf 30920, axhvmul0-zf 30921, axhfi-zf 30922, axhis1-zf 30923, axhis2-zf 30924, axhis3-zf 30925, axhis4-zf 30926, and axhcompl-zf 30927 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 30910. | ||
| Axiom | ax-hilex 30928 | 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 30929 | Vector addition is an operation on ℋ. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
| ⊢ +ℎ :( ℋ × ℋ)⟶ ℋ | ||
| Axiom | ax-hvcom 30930 | Vector addition is commutative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)) | ||
| Axiom | ax-hvass 30931 | Vector addition is associative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = (𝐴 +ℎ (𝐵 +ℎ 𝐶))) | ||
| Axiom | ax-hv0cl 30932 | The zero vector is in the vector space. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
| ⊢ 0ℎ ∈ ℋ | ||
| Axiom | ax-hvaddid 30933 | Addition with the zero vector. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴) | ||
| Axiom | ax-hfvmul 30934 | Scalar multiplication is an operation on ℂ and ℋ. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
| ⊢ ·ℎ :(ℂ × ℋ)⟶ ℋ | ||
| Axiom | ax-hvmulid 30935 | Scalar multiplication by one. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴) | ||
| Axiom | ax-hvmulass 30936 | Scalar multiplication associative law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))) | ||
| Axiom | ax-hvdistr1 30937 | Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 +ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) +ℎ (𝐴 ·ℎ 𝐶))) | ||
| Axiom | ax-hvdistr2 30938 | Scalar multiplication distributive law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 + 𝐵) ·ℎ 𝐶) = ((𝐴 ·ℎ 𝐶) +ℎ (𝐵 ·ℎ 𝐶))) | ||
| Axiom | ax-hvmul0 30939 | Scalar multiplication by zero. We can derive the existence of the negative of a vector from this axiom (see hvsubid 30955 and hvsubval 30945). (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (0 ·ℎ 𝐴) = 0ℎ) | ||
| Theorem | hvmulex 30940 | The Hilbert space scalar product operation is a set. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.) |
| ⊢ ·ℎ ∈ V | ||
| Theorem | hvaddcl 30941 | Closure of vector addition. (Contributed by NM, 18-Apr-2007.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) ∈ ℋ) | ||
| Theorem | hvmulcl 30942 | Closure of scalar multiplication. (Contributed by NM, 19-Apr-2007.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ℎ 𝐵) ∈ ℋ) | ||
| Theorem | hvmulcli 30943 | Closure inference for scalar multiplication. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 ·ℎ 𝐵) ∈ ℋ | ||
| Theorem | hvsubf 30944 | Mapping domain and codomain of vector subtraction. (Contributed by NM, 6-Sep-2007.) (New usage is discouraged.) |
| ⊢ −ℎ :( ℋ × ℋ)⟶ ℋ | ||
| Theorem | hvsubval 30945 | Value of vector subtraction. (Contributed by NM, 5-Sep-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 −ℎ 𝐵) = (𝐴 +ℎ (-1 ·ℎ 𝐵))) | ||
| Theorem | hvsubcl 30946 | Closure of vector subtraction. (Contributed by NM, 17-Aug-1999.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 −ℎ 𝐵) ∈ ℋ) | ||
| Theorem | hvaddcli 30947 | Closure of vector addition. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 +ℎ 𝐵) ∈ ℋ | ||
| Theorem | hvcomi 30948 | Commutation of vector addition. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴) | ||
| Theorem | hvsubvali 30949 | Value of vector subtraction definition. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 −ℎ 𝐵) = (𝐴 +ℎ (-1 ·ℎ 𝐵)) | ||
| Theorem | hvsubcli 30950 | Closure of vector subtraction. (Contributed by NM, 2-Aug-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 −ℎ 𝐵) ∈ ℋ | ||
| Theorem | ifhvhv0 30951 | Prove if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ. (Contributed by David A. Wheeler, 7-Dec-2018.) (New usage is discouraged.) |
| ⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ | ||
| Theorem | hvaddlid 30952 | Addition with the zero vector. (Contributed by NM, 18-Oct-1999.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (0ℎ +ℎ 𝐴) = 𝐴) | ||
| Theorem | hvmul0 30953 | Scalar multiplication with the zero vector. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℂ → (𝐴 ·ℎ 0ℎ) = 0ℎ) | ||
| Theorem | hvmul0or 30954 | 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 30955 | Subtraction of a vector from itself. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (𝐴 −ℎ 𝐴) = 0ℎ) | ||
| Theorem | hvnegid 30956 | Addition of negative of a vector to itself. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ (-1 ·ℎ 𝐴)) = 0ℎ) | ||
| Theorem | hv2neg 30957 | Two ways to express the negative of a vector. (Contributed by NM, 23-May-2005.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (0ℎ −ℎ 𝐴) = (-1 ·ℎ 𝐴)) | ||
| Theorem | hvaddlidi 30958 | Addition with the zero vector. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ ⇒ ⊢ (0ℎ +ℎ 𝐴) = 𝐴 | ||
| Theorem | hvnegidi 30959 | Addition of negative of a vector to itself. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ ⇒ ⊢ (𝐴 +ℎ (-1 ·ℎ 𝐴)) = 0ℎ | ||
| Theorem | hv2negi 30960 | Two ways to express the negative of a vector. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ ⇒ ⊢ (0ℎ −ℎ 𝐴) = (-1 ·ℎ 𝐴) | ||
| Theorem | hvm1neg 30961 | 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 30962 | Value of vector addition in terms of vector subtraction. (Contributed by NM, 10-Jun-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐴 −ℎ (-1 ·ℎ 𝐵))) | ||
| Theorem | hvadd32 30963 | Commutative/associative law. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = ((𝐴 +ℎ 𝐶) +ℎ 𝐵)) | ||
| Theorem | hvadd12 30964 | Commutative/associative law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 +ℎ (𝐵 +ℎ 𝐶)) = (𝐵 +ℎ (𝐴 +ℎ 𝐶))) | ||
| Theorem | hvadd4 30965 | Hilbert vector space addition law. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 +ℎ 𝐵) +ℎ (𝐶 +ℎ 𝐷)) = ((𝐴 +ℎ 𝐶) +ℎ (𝐵 +ℎ 𝐷))) | ||
| Theorem | hvsub4 30966 | Hilbert vector space addition/subtraction law. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 +ℎ 𝐵) −ℎ (𝐶 +ℎ 𝐷)) = ((𝐴 −ℎ 𝐶) +ℎ (𝐵 −ℎ 𝐷))) | ||
| Theorem | hvaddsub12 30967 | Commutative/associative law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 +ℎ (𝐵 −ℎ 𝐶)) = (𝐵 +ℎ (𝐴 −ℎ 𝐶))) | ||
| Theorem | hvpncan 30968 | Addition/subtraction cancellation law for vectors in Hilbert space. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 +ℎ 𝐵) −ℎ 𝐵) = 𝐴) | ||
| Theorem | hvpncan2 30969 | Addition/subtraction cancellation law for vectors in Hilbert space. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 +ℎ 𝐵) −ℎ 𝐴) = 𝐵) | ||
| Theorem | hvaddsubass 30970 | Associativity of sum and difference of Hilbert space vectors. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) −ℎ 𝐶) = (𝐴 +ℎ (𝐵 −ℎ 𝐶))) | ||
| Theorem | hvpncan3 30971 | Subtraction and addition of equal Hilbert space vectors. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ (𝐵 −ℎ 𝐴)) = 𝐵) | ||
| Theorem | hvmulcom 30972 | Scalar multiplication commutative law. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) = (𝐵 ·ℎ (𝐴 ·ℎ 𝐶))) | ||
| Theorem | hvsubass 30973 | Hilbert vector space associative law for subtraction. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 −ℎ 𝐵) −ℎ 𝐶) = (𝐴 −ℎ (𝐵 +ℎ 𝐶))) | ||
| Theorem | hvsub32 30974 | Hilbert vector space commutative/associative law. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 −ℎ 𝐵) −ℎ 𝐶) = ((𝐴 −ℎ 𝐶) −ℎ 𝐵)) | ||
| Theorem | hvmulassi 30975 | Scalar multiplication associative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) | ||
| Theorem | hvmulcomi 30976 | Scalar multiplication commutative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) = (𝐵 ·ℎ (𝐴 ·ℎ 𝐶)) | ||
| Theorem | hvmul2negi 30977 | Double negative in scalar multiplication. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ (-𝐴 ·ℎ (-𝐵 ·ℎ 𝐶)) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) | ||
| Theorem | hvsubdistr1 30978 | Scalar multiplication distributive law for subtraction. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 −ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) −ℎ (𝐴 ·ℎ 𝐶))) | ||
| Theorem | hvsubdistr2 30979 | Scalar multiplication distributive law for subtraction. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 − 𝐵) ·ℎ 𝐶) = ((𝐴 ·ℎ 𝐶) −ℎ (𝐵 ·ℎ 𝐶))) | ||
| Theorem | hvdistr1i 30980 | Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ (𝐴 ·ℎ (𝐵 +ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) +ℎ (𝐴 ·ℎ 𝐶)) | ||
| Theorem | hvsubdistr1i 30981 | Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ (𝐴 ·ℎ (𝐵 −ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) −ℎ (𝐴 ·ℎ 𝐶)) | ||
| Theorem | hvassi 30982 | Hilbert vector space associative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = (𝐴 +ℎ (𝐵 +ℎ 𝐶)) | ||
| Theorem | hvadd32i 30983 | Hilbert vector space commutative/associative law. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = ((𝐴 +ℎ 𝐶) +ℎ 𝐵) | ||
| Theorem | hvsubassi 30984 | 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 30985 | 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 30986 | Hilbert vector space commutative/associative law. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ (𝐴 +ℎ (𝐵 +ℎ 𝐶)) = (𝐵 +ℎ (𝐴 +ℎ 𝐶)) | ||
| Theorem | hvadd4i 30987 | Hilbert vector space addition law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ & ⊢ 𝐷 ∈ ℋ ⇒ ⊢ ((𝐴 +ℎ 𝐵) +ℎ (𝐶 +ℎ 𝐷)) = ((𝐴 +ℎ 𝐶) +ℎ (𝐵 +ℎ 𝐷)) | ||
| Theorem | hvsubsub4i 30988 | Hilbert vector space addition law. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ & ⊢ 𝐷 ∈ ℋ ⇒ ⊢ ((𝐴 −ℎ 𝐵) −ℎ (𝐶 −ℎ 𝐷)) = ((𝐴 −ℎ 𝐶) −ℎ (𝐵 −ℎ 𝐷)) | ||
| Theorem | hvsubsub4 30989 | Hilbert vector space addition/subtraction law. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 −ℎ 𝐵) −ℎ (𝐶 −ℎ 𝐷)) = ((𝐴 −ℎ 𝐶) −ℎ (𝐵 −ℎ 𝐷))) | ||
| Theorem | hv2times 30990 | Two times a vector. (Contributed by NM, 22-Jun-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (2 ·ℎ 𝐴) = (𝐴 +ℎ 𝐴)) | ||
| Theorem | hvnegdii 30991 | Distribution of negative over subtraction. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (-1 ·ℎ (𝐴 −ℎ 𝐵)) = (𝐵 −ℎ 𝐴) | ||
| Theorem | hvsubeq0i 30992 | If the difference between two vectors is zero, they are equal. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ ((𝐴 −ℎ 𝐵) = 0ℎ ↔ 𝐴 = 𝐵) | ||
| Theorem | hvsubcan2i 30993 | Vector cancellation law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ ((𝐴 +ℎ 𝐵) +ℎ (𝐴 −ℎ 𝐵)) = (2 ·ℎ 𝐴) | ||
| Theorem | hvaddcani 30994 | Cancellation law for vector addition. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((𝐴 +ℎ 𝐵) = (𝐴 +ℎ 𝐶) ↔ 𝐵 = 𝐶) | ||
| Theorem | hvsubaddi 30995 | Relationship between vector subtraction and addition. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((𝐴 −ℎ 𝐵) = 𝐶 ↔ (𝐵 +ℎ 𝐶) = 𝐴) | ||
| Theorem | hvnegdi 30996 | Distribution of negative over subtraction. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (-1 ·ℎ (𝐴 −ℎ 𝐵)) = (𝐵 −ℎ 𝐴)) | ||
| Theorem | hvsubeq0 30997 | If the difference between two vectors is zero, they are equal. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 −ℎ 𝐵) = 0ℎ ↔ 𝐴 = 𝐵)) | ||
| Theorem | hvaddeq0 30998 | 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 30999 | Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) = (𝐴 +ℎ 𝐶) ↔ 𝐵 = 𝐶)) | ||
| Theorem | hvaddcan2 31000 | Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐶) = (𝐵 +ℎ 𝐶) ↔ 𝐴 = 𝐵)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |