Home | Metamath
Proof Explorer Theorem List (p. 298 of 470) | < 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-29659) |
Hilbert Space Explorer
(29660-31182) |
Users' Mathboxes
(31183-46998) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cel 29701 | Extend class notation with Hilbert space eigenvalue function. |
class eigval | ||
Syntax | cspc 29702 | Extend class notation with the spectrum of an operator. |
class Lambda | ||
Syntax | cst 29703 | Extend class notation with set of states on a Hilbert lattice. |
class States | ||
Syntax | chst 29704 | Extend class notation with set of Hilbert-space-valued states on a Hilbert lattice. |
class CHStates | ||
Syntax | ccv 29705 | Extend class notation with the covers relation on a Hilbert lattice. |
class ββ | ||
Syntax | cat 29706 | Extend class notation with set of atoms on a Hilbert lattice. |
class HAtoms | ||
Syntax | cmd 29707 | Extend class notation with the modular pair relation on a Hilbert lattice. |
class πβ | ||
Syntax | cdmd 29708 | Extend class notation with the dual modular pair relation on a Hilbert lattice. |
class πβ* | ||
Definition | df-hnorm 29709 | Define the function for the norm of a vector of Hilbert space. See normval 29865 for its value and normcl 29866 for its closure. Theorems norm-i-i 29874, norm-ii-i 29878, and norm-iii-i 29880 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 29710 | Define base set of Hilbert space, for use if we want to develop Hilbert space independently from the axioms (see comments in ax-hilex 29740). 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 29908. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ β = (BaseSetββ¨β¨ +β , Β·β β©, normββ©) | ||
Definition | df-h0v 29711 | 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 29909. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ 0β = (0vecββ¨β¨ +β , Β·β β©, normββ©) | ||
Definition | df-hvsub 29712* | Define vector subtraction. See hvsubvali 29761 for its value and hvsubcli 29762 for its closure. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.) |
β’ ββ = (π₯ β β, π¦ β β β¦ (π₯ +β (-1 Β·β π¦))) | ||
Definition | df-hlim 29713* | Define the limit relation for Hilbert space. See hlimi 29929 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 29714* | Define the set of Cauchy sequences on a Hilbert space. See hcau 29925 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 29715 | The group (addition) operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β NrmCVec β β’ +β = ( +π£ βπ) | ||
Theorem | h2hsm 29716 | The scalar product operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β NrmCVec β β’ Β·β = ( Β·π OLD βπ) | ||
Theorem | h2hnm 29717 | The norm function of Hilbert space. (Contributed by NM, 5-Jun-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β NrmCVec β β’ normβ = (normCVβπ) | ||
Theorem | h2hvs 29718 | 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 29719 | 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 29720 | 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 29721 | 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 29722 through axhcompl-zf 29739, 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 29709 above. See also the comment in ax-hilex 29740. | ||
Theorem | axhilex-zf 29722 | Derive Axiom ax-hilex 29740 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ β β V | ||
Theorem | axhfvadd-zf 29723 | Derive Axiom ax-hfvadd 29741 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ +β :( β Γ β)βΆ β | ||
Theorem | axhvcom-zf 29724 | Derive Axiom ax-hvcom 29742 from Hilbert space under ZF set theory. (Contributed by NM, 27-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ ((π΄ β β β§ π΅ β β) β (π΄ +β π΅) = (π΅ +β π΄)) | ||
Theorem | axhvass-zf 29725 | Derive Axiom ax-hvass 29743 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ +β π΅) +β πΆ) = (π΄ +β (π΅ +β πΆ))) | ||
Theorem | axhv0cl-zf 29726 | Derive Axiom ax-hv0cl 29744 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ 0β β β | ||
Theorem | axhvaddid-zf 29727 | Derive Axiom ax-hvaddid 29745 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ (π΄ β β β (π΄ +β 0β) = π΄) | ||
Theorem | axhfvmul-zf 29728 | Derive Axiom ax-hfvmul 29746 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ Β·β :(β Γ β)βΆ β | ||
Theorem | axhvmulid-zf 29729 | Derive Axiom ax-hvmulid 29747 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ (π΄ β β β (1 Β·β π΄) = π΄) | ||
Theorem | axhvmulass-zf 29730 | Derive Axiom ax-hvmulass 29748 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ Β· π΅) Β·β πΆ) = (π΄ Β·β (π΅ Β·β πΆ))) | ||
Theorem | axhvdistr1-zf 29731 | Derive Axiom ax-hvdistr1 29749 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β·β (π΅ +β πΆ)) = ((π΄ Β·β π΅) +β (π΄ Β·β πΆ))) | ||
Theorem | axhvdistr2-zf 29732 | Derive Axiom ax-hvdistr2 29750 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + π΅) Β·β πΆ) = ((π΄ Β·β πΆ) +β (π΅ Β·β πΆ))) | ||
Theorem | axhvmul0-zf 29733 | Derive Axiom ax-hvmul0 29751 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ (π΄ β β β (0 Β·β π΄) = 0β) | ||
Theorem | axhfi-zf 29734 | Derive Axiom ax-hfi 29820 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 29735 | Derive Axiom ax-his1 29823 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 29736 | Derive Axiom ax-his2 29824 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 29737 | Derive Axiom ax-his3 29825 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 29738 | Derive Axiom ax-his4 29826 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 29739* | Derive Axiom ax-hcompl 29943 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 29740, ax-hfvadd 29741, ax-hvcom 29742, ax-hvass 29743, ax-hv0cl 29744, ax-hvaddid 29745, ax-hfvmul 29746, ax-hvmulid 29747, ax-hvmulass 29748, ax-hvdistr1 29749, ax-hvdistr2 29750, ax-hvmul0 29751, ax-hfi 29820, ax-his1 29823, ax-his2 29824, ax-his3 29825, ax-his4 29826, and ax-hcompl 29943. 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 29722, axhfvadd-zf 29723, axhvcom-zf 29724, axhvass-zf 29725, axhv0cl-zf 29726, axhvaddid-zf 29727, axhfvmul-zf 29728, axhvmulid-zf 29729, axhvmulass-zf 29730, axhvdistr1-zf 29731, axhvdistr2-zf 29732, axhvmul0-zf 29733, axhfi-zf 29734, axhis1-zf 29735, axhis2-zf 29736, axhis3-zf 29737, axhis4-zf 29738, and axhcompl-zf 29739 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 29722. | ||
Axiom | ax-hilex 29740 | 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 29741 | Vector addition is an operation on β. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
β’ +β :( β Γ β)βΆ β | ||
Axiom | ax-hvcom 29742 | Vector addition is commutative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ +β π΅) = (π΅ +β π΄)) | ||
Axiom | ax-hvass 29743 | Vector addition is associative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ +β π΅) +β πΆ) = (π΄ +β (π΅ +β πΆ))) | ||
Axiom | ax-hv0cl 29744 | The zero vector is in the vector space. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
β’ 0β β β | ||
Axiom | ax-hvaddid 29745 | Addition with the zero vector. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (π΄ +β 0β) = π΄) | ||
Axiom | ax-hfvmul 29746 | Scalar multiplication is an operation on β and β. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
β’ Β·β :(β Γ β)βΆ β | ||
Axiom | ax-hvmulid 29747 | Scalar multiplication by one. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (1 Β·β π΄) = π΄) | ||
Axiom | ax-hvmulass 29748 | Scalar multiplication associative law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ Β· π΅) Β·β πΆ) = (π΄ Β·β (π΅ Β·β πΆ))) | ||
Axiom | ax-hvdistr1 29749 | Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β·β (π΅ +β πΆ)) = ((π΄ Β·β π΅) +β (π΄ Β·β πΆ))) | ||
Axiom | ax-hvdistr2 29750 | Scalar multiplication distributive law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + π΅) Β·β πΆ) = ((π΄ Β·β πΆ) +β (π΅ Β·β πΆ))) | ||
Axiom | ax-hvmul0 29751 | Scalar multiplication by zero. We can derive the existence of the negative of a vector from this axiom (see hvsubid 29767 and hvsubval 29757). (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (0 Β·β π΄) = 0β) | ||
Theorem | hvmulex 29752 | The Hilbert space scalar product operation is a set. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.) |
β’ Β·β β V | ||
Theorem | hvaddcl 29753 | Closure of vector addition. (Contributed by NM, 18-Apr-2007.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ +β π΅) β β) | ||
Theorem | hvmulcl 29754 | Closure of scalar multiplication. (Contributed by NM, 19-Apr-2007.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ Β·β π΅) β β) | ||
Theorem | hvmulcli 29755 | Closure inference for scalar multiplication. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ Β·β π΅) β β | ||
Theorem | hvsubf 29756 | Mapping domain and codomain of vector subtraction. (Contributed by NM, 6-Sep-2007.) (New usage is discouraged.) |
β’ ββ :( β Γ β)βΆ β | ||
Theorem | hvsubval 29757 | Value of vector subtraction. (Contributed by NM, 5-Sep-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ ββ π΅) = (π΄ +β (-1 Β·β π΅))) | ||
Theorem | hvsubcl 29758 | Closure of vector subtraction. (Contributed by NM, 17-Aug-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ ββ π΅) β β) | ||
Theorem | hvaddcli 29759 | Closure of vector addition. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ +β π΅) β β | ||
Theorem | hvcomi 29760 | Commutation of vector addition. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ +β π΅) = (π΅ +β π΄) | ||
Theorem | hvsubvali 29761 | Value of vector subtraction definition. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ ββ π΅) = (π΄ +β (-1 Β·β π΅)) | ||
Theorem | hvsubcli 29762 | Closure of vector subtraction. (Contributed by NM, 2-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ ββ π΅) β β | ||
Theorem | ifhvhv0 29763 | Prove if(π΄ β β, π΄, 0β) β β. (Contributed by David A. Wheeler, 7-Dec-2018.) (New usage is discouraged.) |
β’ if(π΄ β β, π΄, 0β) β β | ||
Theorem | hvaddid2 29764 | Addition with the zero vector. (Contributed by NM, 18-Oct-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (0β +β π΄) = π΄) | ||
Theorem | hvmul0 29765 | Scalar multiplication with the zero vector. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (π΄ Β·β 0β) = 0β) | ||
Theorem | hvmul0or 29766 | 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 29767 | Subtraction of a vector from itself. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (π΄ ββ π΄) = 0β) | ||
Theorem | hvnegid 29768 | Addition of negative of a vector to itself. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.) |
β’ (π΄ β β β (π΄ +β (-1 Β·β π΄)) = 0β) | ||
Theorem | hv2neg 29769 | Two ways to express the negative of a vector. (Contributed by NM, 23-May-2005.) (New usage is discouraged.) |
β’ (π΄ β β β (0β ββ π΄) = (-1 Β·β π΄)) | ||
Theorem | hvaddid2i 29770 | Addition with the zero vector. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β β β’ (0β +β π΄) = π΄ | ||
Theorem | hvnegidi 29771 | Addition of negative of a vector to itself. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β β β’ (π΄ +β (-1 Β·β π΄)) = 0β | ||
Theorem | hv2negi 29772 | Two ways to express the negative of a vector. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β β β β’ (0β ββ π΄) = (-1 Β·β π΄) | ||
Theorem | hvm1neg 29773 | 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 29774 | Value of vector addition in terms of vector subtraction. (Contributed by NM, 10-Jun-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ +β π΅) = (π΄ ββ (-1 Β·β π΅))) | ||
Theorem | hvadd32 29775 | Commutative/associative law. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ +β π΅) +β πΆ) = ((π΄ +β πΆ) +β π΅)) | ||
Theorem | hvadd12 29776 | Commutative/associative law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ +β (π΅ +β πΆ)) = (π΅ +β (π΄ +β πΆ))) | ||
Theorem | hvadd4 29777 | Hilbert vector space addition law. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ +β π΅) +β (πΆ +β π·)) = ((π΄ +β πΆ) +β (π΅ +β π·))) | ||
Theorem | hvsub4 29778 | Hilbert vector space addition/subtraction law. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ +β π΅) ββ (πΆ +β π·)) = ((π΄ ββ πΆ) +β (π΅ ββ π·))) | ||
Theorem | hvaddsub12 29779 | Commutative/associative law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ +β (π΅ ββ πΆ)) = (π΅ +β (π΄ ββ πΆ))) | ||
Theorem | hvpncan 29780 | Addition/subtraction cancellation law for vectors in Hilbert space. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ +β π΅) ββ π΅) = π΄) | ||
Theorem | hvpncan2 29781 | Addition/subtraction cancellation law for vectors in Hilbert space. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ +β π΅) ββ π΄) = π΅) | ||
Theorem | hvaddsubass 29782 | Associativity of sum and difference of Hilbert space vectors. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ +β π΅) ββ πΆ) = (π΄ +β (π΅ ββ πΆ))) | ||
Theorem | hvpncan3 29783 | Subtraction and addition of equal Hilbert space vectors. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ +β (π΅ ββ π΄)) = π΅) | ||
Theorem | hvmulcom 29784 | Scalar multiplication commutative law. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β·β (π΅ Β·β πΆ)) = (π΅ Β·β (π΄ Β·β πΆ))) | ||
Theorem | hvsubass 29785 | Hilbert vector space associative law for subtraction. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) ββ πΆ) = (π΄ ββ (π΅ +β πΆ))) | ||
Theorem | hvsub32 29786 | Hilbert vector space commutative/associative law. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) ββ πΆ) = ((π΄ ββ πΆ) ββ π΅)) | ||
Theorem | hvmulassi 29787 | Scalar multiplication associative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ Β· π΅) Β·β πΆ) = (π΄ Β·β (π΅ Β·β πΆ)) | ||
Theorem | hvmulcomi 29788 | Scalar multiplication commutative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (π΄ Β·β (π΅ Β·β πΆ)) = (π΅ Β·β (π΄ Β·β πΆ)) | ||
Theorem | hvmul2negi 29789 | Double negative in scalar multiplication. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (-π΄ Β·β (-π΅ Β·β πΆ)) = (π΄ Β·β (π΅ Β·β πΆ)) | ||
Theorem | hvsubdistr1 29790 | Scalar multiplication distributive law for subtraction. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β·β (π΅ ββ πΆ)) = ((π΄ Β·β π΅) ββ (π΄ Β·β πΆ))) | ||
Theorem | hvsubdistr2 29791 | Scalar multiplication distributive law for subtraction. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ β π΅) Β·β πΆ) = ((π΄ Β·β πΆ) ββ (π΅ Β·β πΆ))) | ||
Theorem | hvdistr1i 29792 | Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (π΄ Β·β (π΅ +β πΆ)) = ((π΄ Β·β π΅) +β (π΄ Β·β πΆ)) | ||
Theorem | hvsubdistr1i 29793 | Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (π΄ Β·β (π΅ ββ πΆ)) = ((π΄ Β·β π΅) ββ (π΄ Β·β πΆ)) | ||
Theorem | hvassi 29794 | Hilbert vector space associative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ +β π΅) +β πΆ) = (π΄ +β (π΅ +β πΆ)) | ||
Theorem | hvadd32i 29795 | Hilbert vector space commutative/associative law. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ +β π΅) +β πΆ) = ((π΄ +β πΆ) +β π΅) | ||
Theorem | hvsubassi 29796 | 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 29797 | 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 29798 | Hilbert vector space commutative/associative law. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (π΄ +β (π΅ +β πΆ)) = (π΅ +β (π΄ +β πΆ)) | ||
Theorem | hvadd4i 29799 | Hilbert vector space addition law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β & β’ π· β β β β’ ((π΄ +β π΅) +β (πΆ +β π·)) = ((π΄ +β πΆ) +β (π΅ +β π·)) | ||
Theorem | hvsubsub4i 29800 | Hilbert vector space addition law. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β & β’ π· β β β β’ ((π΄ ββ π΅) ββ (πΆ ββ π·)) = ((π΄ ββ πΆ) ββ (π΅ ββ π·)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |