Home | Metamath
Proof Explorer Theorem List (p. 288 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 | axhis3-zf 28701 | Derive axiom ax-his3 28789 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 28702 | Derive axiom ax-his4 28790 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 28703* | Derive axiom ax-hcompl 28907 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 28704, ax-hfvadd 28705, ax-hvcom 28706, ax-hvass 28707, ax-hv0cl 28708, ax-hvaddid 28709, ax-hfvmul 28710, ax-hvmulid 28711, ax-hvmulass 28712, ax-hvdistr1 28713, ax-hvdistr2 28714, ax-hvmul0 28715, ax-hfi 28784, ax-his1 28787, ax-his2 28788, ax-his3 28789, ax-his4 28790, and ax-hcompl 28907. 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 28686, axhfvadd-zf 28687, axhvcom-zf 28688, axhvass-zf 28689, axhv0cl-zf 28690, axhvaddid-zf 28691, axhfvmul-zf 28692, axhvmulid-zf 28693, axhvmulass-zf 28694, axhvdistr1-zf 28695, axhvdistr2-zf 28696, axhvmul0-zf 28697, axhfi-zf 28698, axhis1-zf 28699, axhis2-zf 28700, axhis3-zf 28701, axhis4-zf 28702, and axhcompl-zf 28703 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 28686. | ||
Axiom | ax-hilex 28704 | 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 28705 | Vector addition is an operation on ℋ. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
⊢ +ℎ :( ℋ × ℋ)⟶ ℋ | ||
Axiom | ax-hvcom 28706 | Vector addition is commutative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)) | ||
Axiom | ax-hvass 28707 | Vector addition is associative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = (𝐴 +ℎ (𝐵 +ℎ 𝐶))) | ||
Axiom | ax-hv0cl 28708 | The zero vector is in the vector space. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
⊢ 0ℎ ∈ ℋ | ||
Axiom | ax-hvaddid 28709 | Addition with the zero vector. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴) | ||
Axiom | ax-hfvmul 28710 | Scalar multiplication is an operation on ℂ and ℋ. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
⊢ ·ℎ :(ℂ × ℋ)⟶ ℋ | ||
Axiom | ax-hvmulid 28711 | Scalar multiplication by one. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴) | ||
Axiom | ax-hvmulass 28712 | Scalar multiplication associative law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))) | ||
Axiom | ax-hvdistr1 28713 | Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 +ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) +ℎ (𝐴 ·ℎ 𝐶))) | ||
Axiom | ax-hvdistr2 28714 | Scalar multiplication distributive law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 + 𝐵) ·ℎ 𝐶) = ((𝐴 ·ℎ 𝐶) +ℎ (𝐵 ·ℎ 𝐶))) | ||
Axiom | ax-hvmul0 28715 | Scalar multiplication by zero. We can derive the existence of the negative of a vector from this axiom (see hvsubid 28731 and hvsubval 28721). (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (0 ·ℎ 𝐴) = 0ℎ) | ||
Theorem | hvmulex 28716 | The Hilbert space scalar product operation is a set. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.) |
⊢ ·ℎ ∈ V | ||
Theorem | hvaddcl 28717 | Closure of vector addition. (Contributed by NM, 18-Apr-2007.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) ∈ ℋ) | ||
Theorem | hvmulcl 28718 | Closure of scalar multiplication. (Contributed by NM, 19-Apr-2007.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ℎ 𝐵) ∈ ℋ) | ||
Theorem | hvmulcli 28719 | Closure inference for scalar multiplication. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 ·ℎ 𝐵) ∈ ℋ | ||
Theorem | hvsubf 28720 | Mapping domain and codomain of vector subtraction. (Contributed by NM, 6-Sep-2007.) (New usage is discouraged.) |
⊢ −ℎ :( ℋ × ℋ)⟶ ℋ | ||
Theorem | hvsubval 28721 | Value of vector subtraction. (Contributed by NM, 5-Sep-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 −ℎ 𝐵) = (𝐴 +ℎ (-1 ·ℎ 𝐵))) | ||
Theorem | hvsubcl 28722 | Closure of vector subtraction. (Contributed by NM, 17-Aug-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 −ℎ 𝐵) ∈ ℋ) | ||
Theorem | hvaddcli 28723 | Closure of vector addition. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 +ℎ 𝐵) ∈ ℋ | ||
Theorem | hvcomi 28724 | Commutation of vector addition. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴) | ||
Theorem | hvsubvali 28725 | Value of vector subtraction definition. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 −ℎ 𝐵) = (𝐴 +ℎ (-1 ·ℎ 𝐵)) | ||
Theorem | hvsubcli 28726 | Closure of vector subtraction. (Contributed by NM, 2-Aug-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 −ℎ 𝐵) ∈ ℋ | ||
Theorem | ifhvhv0 28727 | Prove if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ. (Contributed by David A. Wheeler, 7-Dec-2018.) (New usage is discouraged.) |
⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ | ||
Theorem | hvaddid2 28728 | Addition with the zero vector. (Contributed by NM, 18-Oct-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (0ℎ +ℎ 𝐴) = 𝐴) | ||
Theorem | hvmul0 28729 | Scalar multiplication with the zero vector. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℂ → (𝐴 ·ℎ 0ℎ) = 0ℎ) | ||
Theorem | hvmul0or 28730 | 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 28731 | Subtraction of a vector from itself. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (𝐴 −ℎ 𝐴) = 0ℎ) | ||
Theorem | hvnegid 28732 | Addition of negative of a vector to itself. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ (-1 ·ℎ 𝐴)) = 0ℎ) | ||
Theorem | hv2neg 28733 | Two ways to express the negative of a vector. (Contributed by NM, 23-May-2005.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (0ℎ −ℎ 𝐴) = (-1 ·ℎ 𝐴)) | ||
Theorem | hvaddid2i 28734 | Addition with the zero vector. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ ⇒ ⊢ (0ℎ +ℎ 𝐴) = 𝐴 | ||
Theorem | hvnegidi 28735 | Addition of negative of a vector to itself. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ ⇒ ⊢ (𝐴 +ℎ (-1 ·ℎ 𝐴)) = 0ℎ | ||
Theorem | hv2negi 28736 | Two ways to express the negative of a vector. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ ⇒ ⊢ (0ℎ −ℎ 𝐴) = (-1 ·ℎ 𝐴) | ||
Theorem | hvm1neg 28737 | 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 28738 | Value of vector addition in terms of vector subtraction. (Contributed by NM, 10-Jun-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐴 −ℎ (-1 ·ℎ 𝐵))) | ||
Theorem | hvadd32 28739 | Commutative/associative law. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = ((𝐴 +ℎ 𝐶) +ℎ 𝐵)) | ||
Theorem | hvadd12 28740 | Commutative/associative law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 +ℎ (𝐵 +ℎ 𝐶)) = (𝐵 +ℎ (𝐴 +ℎ 𝐶))) | ||
Theorem | hvadd4 28741 | Hilbert vector space addition law. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 +ℎ 𝐵) +ℎ (𝐶 +ℎ 𝐷)) = ((𝐴 +ℎ 𝐶) +ℎ (𝐵 +ℎ 𝐷))) | ||
Theorem | hvsub4 28742 | Hilbert vector space addition/subtraction law. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 +ℎ 𝐵) −ℎ (𝐶 +ℎ 𝐷)) = ((𝐴 −ℎ 𝐶) +ℎ (𝐵 −ℎ 𝐷))) | ||
Theorem | hvaddsub12 28743 | Commutative/associative law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 +ℎ (𝐵 −ℎ 𝐶)) = (𝐵 +ℎ (𝐴 −ℎ 𝐶))) | ||
Theorem | hvpncan 28744 | Addition/subtraction cancellation law for vectors in Hilbert space. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 +ℎ 𝐵) −ℎ 𝐵) = 𝐴) | ||
Theorem | hvpncan2 28745 | Addition/subtraction cancellation law for vectors in Hilbert space. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 +ℎ 𝐵) −ℎ 𝐴) = 𝐵) | ||
Theorem | hvaddsubass 28746 | Associativity of sum and difference of Hilbert space vectors. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) −ℎ 𝐶) = (𝐴 +ℎ (𝐵 −ℎ 𝐶))) | ||
Theorem | hvpncan3 28747 | Subtraction and addition of equal Hilbert space vectors. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ (𝐵 −ℎ 𝐴)) = 𝐵) | ||
Theorem | hvmulcom 28748 | Scalar multiplication commutative law. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) = (𝐵 ·ℎ (𝐴 ·ℎ 𝐶))) | ||
Theorem | hvsubass 28749 | Hilbert vector space associative law for subtraction. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 −ℎ 𝐵) −ℎ 𝐶) = (𝐴 −ℎ (𝐵 +ℎ 𝐶))) | ||
Theorem | hvsub32 28750 | Hilbert vector space commutative/associative law. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 −ℎ 𝐵) −ℎ 𝐶) = ((𝐴 −ℎ 𝐶) −ℎ 𝐵)) | ||
Theorem | hvmulassi 28751 | Scalar multiplication associative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) | ||
Theorem | hvmulcomi 28752 | Scalar multiplication commutative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) = (𝐵 ·ℎ (𝐴 ·ℎ 𝐶)) | ||
Theorem | hvmul2negi 28753 | Double negative in scalar multiplication. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ (-𝐴 ·ℎ (-𝐵 ·ℎ 𝐶)) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) | ||
Theorem | hvsubdistr1 28754 | Scalar multiplication distributive law for subtraction. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 −ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) −ℎ (𝐴 ·ℎ 𝐶))) | ||
Theorem | hvsubdistr2 28755 | Scalar multiplication distributive law for subtraction. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 − 𝐵) ·ℎ 𝐶) = ((𝐴 ·ℎ 𝐶) −ℎ (𝐵 ·ℎ 𝐶))) | ||
Theorem | hvdistr1i 28756 | Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ (𝐴 ·ℎ (𝐵 +ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) +ℎ (𝐴 ·ℎ 𝐶)) | ||
Theorem | hvsubdistr1i 28757 | Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ (𝐴 ·ℎ (𝐵 −ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) −ℎ (𝐴 ·ℎ 𝐶)) | ||
Theorem | hvassi 28758 | Hilbert vector space associative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = (𝐴 +ℎ (𝐵 +ℎ 𝐶)) | ||
Theorem | hvadd32i 28759 | Hilbert vector space commutative/associative law. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = ((𝐴 +ℎ 𝐶) +ℎ 𝐵) | ||
Theorem | hvsubassi 28760 | 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 28761 | 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 28762 | Hilbert vector space commutative/associative law. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ (𝐴 +ℎ (𝐵 +ℎ 𝐶)) = (𝐵 +ℎ (𝐴 +ℎ 𝐶)) | ||
Theorem | hvadd4i 28763 | Hilbert vector space addition law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ & ⊢ 𝐷 ∈ ℋ ⇒ ⊢ ((𝐴 +ℎ 𝐵) +ℎ (𝐶 +ℎ 𝐷)) = ((𝐴 +ℎ 𝐶) +ℎ (𝐵 +ℎ 𝐷)) | ||
Theorem | hvsubsub4i 28764 | Hilbert vector space addition law. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ & ⊢ 𝐷 ∈ ℋ ⇒ ⊢ ((𝐴 −ℎ 𝐵) −ℎ (𝐶 −ℎ 𝐷)) = ((𝐴 −ℎ 𝐶) −ℎ (𝐵 −ℎ 𝐷)) | ||
Theorem | hvsubsub4 28765 | Hilbert vector space addition/subtraction law. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 −ℎ 𝐵) −ℎ (𝐶 −ℎ 𝐷)) = ((𝐴 −ℎ 𝐶) −ℎ (𝐵 −ℎ 𝐷))) | ||
Theorem | hv2times 28766 | Two times a vector. (Contributed by NM, 22-Jun-2006.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (2 ·ℎ 𝐴) = (𝐴 +ℎ 𝐴)) | ||
Theorem | hvnegdii 28767 | Distribution of negative over subtraction. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (-1 ·ℎ (𝐴 −ℎ 𝐵)) = (𝐵 −ℎ 𝐴) | ||
Theorem | hvsubeq0i 28768 | If the difference between two vectors is zero, they are equal. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ ((𝐴 −ℎ 𝐵) = 0ℎ ↔ 𝐴 = 𝐵) | ||
Theorem | hvsubcan2i 28769 | Vector cancellation law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ ((𝐴 +ℎ 𝐵) +ℎ (𝐴 −ℎ 𝐵)) = (2 ·ℎ 𝐴) | ||
Theorem | hvaddcani 28770 | Cancellation law for vector addition. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((𝐴 +ℎ 𝐵) = (𝐴 +ℎ 𝐶) ↔ 𝐵 = 𝐶) | ||
Theorem | hvsubaddi 28771 | Relationship between vector subtraction and addition. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((𝐴 −ℎ 𝐵) = 𝐶 ↔ (𝐵 +ℎ 𝐶) = 𝐴) | ||
Theorem | hvnegdi 28772 | Distribution of negative over subtraction. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (-1 ·ℎ (𝐴 −ℎ 𝐵)) = (𝐵 −ℎ 𝐴)) | ||
Theorem | hvsubeq0 28773 | If the difference between two vectors is zero, they are equal. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 −ℎ 𝐵) = 0ℎ ↔ 𝐴 = 𝐵)) | ||
Theorem | hvaddeq0 28774 | 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 28775 | Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) = (𝐴 +ℎ 𝐶) ↔ 𝐵 = 𝐶)) | ||
Theorem | hvaddcan2 28776 | Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐶) = (𝐵 +ℎ 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | hvmulcan 28777 | Cancellation law for scalar multiplication. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) = (𝐴 ·ℎ 𝐶) ↔ 𝐵 = 𝐶)) | ||
Theorem | hvmulcan2 28778 | Cancellation law for scalar multiplication. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℋ ∧ 𝐶 ≠ 0ℎ)) → ((𝐴 ·ℎ 𝐶) = (𝐵 ·ℎ 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | hvsubcan 28779 | Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 −ℎ 𝐵) = (𝐴 −ℎ 𝐶) ↔ 𝐵 = 𝐶)) | ||
Theorem | hvsubcan2 28780 | Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 −ℎ 𝐶) = (𝐵 −ℎ 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | hvsub0 28781 | Subtraction of a zero vector. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (𝐴 −ℎ 0ℎ) = 𝐴) | ||
Theorem | hvsubadd 28782 | Relationship between vector subtraction and addition. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 −ℎ 𝐵) = 𝐶 ↔ (𝐵 +ℎ 𝐶) = 𝐴)) | ||
Theorem | hvaddsub4 28783 | Hilbert vector space addition/subtraction law. (Contributed by NM, 18-May-2005.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 +ℎ 𝐵) = (𝐶 +ℎ 𝐷) ↔ (𝐴 −ℎ 𝐶) = (𝐷 −ℎ 𝐵))) | ||
Axiom | ax-hfi 28784 | Inner product maps pairs from ℋ to ℂ. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
⊢ ·ih :( ℋ × ℋ)⟶ℂ | ||
Theorem | hicl 28785 | Closure of inner product. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih 𝐵) ∈ ℂ) | ||
Theorem | hicli 28786 | Closure inference for inner product. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 ·ih 𝐵) ∈ ℂ | ||
Axiom | ax-his1 28787 | Conjugate law for inner product. Postulate (S1) of [Beran] p. 95. Note that ∗‘𝑥 is the complex conjugate cjval 14451 of 𝑥. In the literature, the inner product of 𝐴 and 𝐵 is usually written 〈𝐴, 𝐵〉, but our operation notation co 7145 allows us to use existing theorems about operations and also avoids a clash with the definition of an ordered pair df-op 4566. Physicists use 〈𝐵 ∣ 𝐴〉, called Dirac bra-ket notation, to represent this operation; see comments in df-bra 29555. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih 𝐵) = (∗‘(𝐵 ·ih 𝐴))) | ||
Axiom | ax-his2 28788 | Distributive law for inner product. Postulate (S2) of [Beran] p. 95. (Contributed by NM, 31-Jul-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) ·ih 𝐶) = ((𝐴 ·ih 𝐶) + (𝐵 ·ih 𝐶))) | ||
Axiom | ax-his3 28789 | Associative law for inner product. Postulate (S3) of [Beran] p. 95. Warning: Mathematics textbooks usually use our version of the axiom. Physics textbooks, on the other hand, usually replace the left-hand side with (𝐵 ·ih (𝐴 ·ℎ 𝐶)) (e.g., Equation 1.21b of [Hughes] p. 44; Definition (iii) of [ReedSimon] p. 36). See the comments in df-bra 29555 for why the physics definition is swapped. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))) | ||
Axiom | ax-his4 28790 | Identity law for inner product. Postulate (S4) of [Beran] p. 95. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ) → 0 < (𝐴 ·ih 𝐴)) | ||
Theorem | his5 28791 | Associative law for inner product. Lemma 3.1(S5) of [Beran] p. 95. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐵 ·ih (𝐴 ·ℎ 𝐶)) = ((∗‘𝐴) · (𝐵 ·ih 𝐶))) | ||
Theorem | his52 28792 | Associative law for inner product. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐵 ·ih ((∗‘𝐴) ·ℎ 𝐶)) = (𝐴 · (𝐵 ·ih 𝐶))) | ||
Theorem | his35 28793 | Move scalar multiplication to outside of inner product. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 ·ℎ 𝐶) ·ih (𝐵 ·ℎ 𝐷)) = ((𝐴 · (∗‘𝐵)) · (𝐶 ·ih 𝐷))) | ||
Theorem | his35i 28794 | Move scalar multiplication to outside of inner product. (Contributed by NM, 1-Jul-2005.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℋ & ⊢ 𝐷 ∈ ℋ ⇒ ⊢ ((𝐴 ·ℎ 𝐶) ·ih (𝐵 ·ℎ 𝐷)) = ((𝐴 · (∗‘𝐵)) · (𝐶 ·ih 𝐷)) | ||
Theorem | his7 28795 | Distributive law for inner product. Lemma 3.1(S7) of [Beran] p. 95. (Contributed by NM, 31-Jul-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ih (𝐵 +ℎ 𝐶)) = ((𝐴 ·ih 𝐵) + (𝐴 ·ih 𝐶))) | ||
Theorem | hiassdi 28796 | Distributive/associative law for inner product, useful for linearity proofs. (Contributed by NM, 10-May-2005.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → (((𝐴 ·ℎ 𝐵) +ℎ 𝐶) ·ih 𝐷) = ((𝐴 · (𝐵 ·ih 𝐷)) + (𝐶 ·ih 𝐷))) | ||
Theorem | his2sub 28797 | Distributive law for inner product of vector subtraction. (Contributed by NM, 16-Nov-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 −ℎ 𝐵) ·ih 𝐶) = ((𝐴 ·ih 𝐶) − (𝐵 ·ih 𝐶))) | ||
Theorem | his2sub2 28798 | Distributive law for inner product of vector subtraction. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ih (𝐵 −ℎ 𝐶)) = ((𝐴 ·ih 𝐵) − (𝐴 ·ih 𝐶))) | ||
Theorem | hire 28799 | A necessary and sufficient condition for an inner product to be real. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 ·ih 𝐵) ∈ ℝ ↔ (𝐴 ·ih 𝐵) = (𝐵 ·ih 𝐴))) | ||
Theorem | hiidrcl 28800 | Real closure of inner product with self. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (𝐴 ·ih 𝐴) ∈ ℝ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |