![]() |
Metamath
Proof Explorer Theorem List (p. 309 of 484) | < 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-30772) |
![]() (30773-32295) |
![]() (32296-48350) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | clo 30801 | Extend class notation with set of linear Hilbert space operators. |
class LinOp | ||
Syntax | cbo 30802 | Extend class notation with set of bounded linear operators. |
class BndLinOp | ||
Syntax | cuo 30803 | Extend class notation with set of unitary Hilbert space operators. |
class UniOp | ||
Syntax | cho 30804 | Extend class notation with set of Hermitian Hilbert space operators. |
class HrmOp | ||
Syntax | cnmf 30805 | Extend class notation with the functional norm function. |
class normfn | ||
Syntax | cnl 30806 | Extend class notation with the functional nullspace function. |
class null | ||
Syntax | ccnfn 30807 | Extend class notation with set of continuous Hilbert space functionals. |
class ContFn | ||
Syntax | clf 30808 | Extend class notation with set of linear Hilbert space functionals. |
class LinFn | ||
Syntax | cado 30809 | Extend class notation with Hilbert space adjoint function. |
class adjβ | ||
Syntax | cbr 30810 | Extend class notation with the bra of a vector in Dirac bra-ket notation. |
class bra | ||
Syntax | ck 30811 | Extend class notation with the outer product of two vectors in Dirac bra-ket notation. |
class ketbra | ||
Syntax | cleo 30812 | Extend class notation with positive operator ordering. |
class β€op | ||
Syntax | cei 30813 | Extend class notation with Hilbert space eigenvector function. |
class eigvec | ||
Syntax | cel 30814 | Extend class notation with Hilbert space eigenvalue function. |
class eigval | ||
Syntax | cspc 30815 | Extend class notation with the spectrum of an operator. |
class Lambda | ||
Syntax | cst 30816 | Extend class notation with set of states on a Hilbert lattice. |
class States | ||
Syntax | chst 30817 | Extend class notation with set of Hilbert-space-valued states on a Hilbert lattice. |
class CHStates | ||
Syntax | ccv 30818 | Extend class notation with the covers relation on a Hilbert lattice. |
class ββ | ||
Syntax | cat 30819 | Extend class notation with set of atoms on a Hilbert lattice. |
class HAtoms | ||
Syntax | cmd 30820 | Extend class notation with the modular pair relation on a Hilbert lattice. |
class πβ | ||
Syntax | cdmd 30821 | Extend class notation with the dual modular pair relation on a Hilbert lattice. |
class πβ* | ||
Definition | df-hnorm 30822 | Define the function for the norm of a vector of Hilbert space. See normval 30978 for its value and normcl 30979 for its closure. Theorems norm-i-i 30987, norm-ii-i 30991, and norm-iii-i 30993 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 30823 | Define base set of Hilbert space, for use if we want to develop Hilbert space independently from the axioms (see comments in ax-hilex 30853). 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 31021. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ β = (BaseSetββ¨β¨ +β , Β·β β©, normββ©) | ||
Definition | df-h0v 30824 | 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 31022. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ 0β = (0vecββ¨β¨ +β , Β·β β©, normββ©) | ||
Definition | df-hvsub 30825* | Define vector subtraction. See hvsubvali 30874 for its value and hvsubcli 30875 for its closure. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.) |
β’ ββ = (π₯ β β, π¦ β β β¦ (π₯ +β (-1 Β·β π¦))) | ||
Definition | df-hlim 30826* | Define the limit relation for Hilbert space. See hlimi 31042 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 30827* | Define the set of Cauchy sequences on a Hilbert space. See hcau 31038 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 30828 | The group (addition) operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β NrmCVec β β’ +β = ( +π£ βπ) | ||
Theorem | h2hsm 30829 | The scalar product operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β NrmCVec β β’ Β·β = ( Β·π OLD βπ) | ||
Theorem | h2hnm 30830 | The norm function of Hilbert space. (Contributed by NM, 5-Jun-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β NrmCVec β β’ normβ = (normCVβπ) | ||
Theorem | h2hvs 30831 | 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 30832 | 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 30833 | 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 30834 | 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 30835 through axhcompl-zf 30852, 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 30822 above. See also the comment in ax-hilex 30853. | ||
Theorem | axhilex-zf 30835 | Derive Axiom ax-hilex 30853 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ β β V | ||
Theorem | axhfvadd-zf 30836 | Derive Axiom ax-hfvadd 30854 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ +β :( β Γ β)βΆ β | ||
Theorem | axhvcom-zf 30837 | Derive Axiom ax-hvcom 30855 from Hilbert space under ZF set theory. (Contributed by NM, 27-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ ((π΄ β β β§ π΅ β β) β (π΄ +β π΅) = (π΅ +β π΄)) | ||
Theorem | axhvass-zf 30838 | Derive Axiom ax-hvass 30856 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ +β π΅) +β πΆ) = (π΄ +β (π΅ +β πΆ))) | ||
Theorem | axhv0cl-zf 30839 | Derive Axiom ax-hv0cl 30857 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ 0β β β | ||
Theorem | axhvaddid-zf 30840 | Derive Axiom ax-hvaddid 30858 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ (π΄ β β β (π΄ +β 0β) = π΄) | ||
Theorem | axhfvmul-zf 30841 | Derive Axiom ax-hfvmul 30859 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ Β·β :(β Γ β)βΆ β | ||
Theorem | axhvmulid-zf 30842 | Derive Axiom ax-hvmulid 30860 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ (π΄ β β β (1 Β·β π΄) = π΄) | ||
Theorem | axhvmulass-zf 30843 | Derive Axiom ax-hvmulass 30861 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ Β· π΅) Β·β πΆ) = (π΄ Β·β (π΅ Β·β πΆ))) | ||
Theorem | axhvdistr1-zf 30844 | Derive Axiom ax-hvdistr1 30862 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β·β (π΅ +β πΆ)) = ((π΄ Β·β π΅) +β (π΄ Β·β πΆ))) | ||
Theorem | axhvdistr2-zf 30845 | Derive Axiom ax-hvdistr2 30863 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + π΅) Β·β πΆ) = ((π΄ Β·β πΆ) +β (π΅ Β·β πΆ))) | ||
Theorem | axhvmul0-zf 30846 | Derive Axiom ax-hvmul0 30864 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ (π΄ β β β (0 Β·β π΄) = 0β) | ||
Theorem | axhfi-zf 30847 | Derive Axiom ax-hfi 30933 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 30848 | Derive Axiom ax-his1 30936 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 30849 | Derive Axiom ax-his2 30937 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 30850 | Derive Axiom ax-his3 30938 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 30851 | Derive Axiom ax-his4 30939 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 30852* | Derive Axiom ax-hcompl 31056 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 30853, ax-hfvadd 30854, ax-hvcom 30855, ax-hvass 30856, ax-hv0cl 30857, ax-hvaddid 30858, ax-hfvmul 30859, ax-hvmulid 30860, ax-hvmulass 30861, ax-hvdistr1 30862, ax-hvdistr2 30863, ax-hvmul0 30864, ax-hfi 30933, ax-his1 30936, ax-his2 30937, ax-his3 30938, ax-his4 30939, and ax-hcompl 31056. 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 30835, axhfvadd-zf 30836, axhvcom-zf 30837, axhvass-zf 30838, axhv0cl-zf 30839, axhvaddid-zf 30840, axhfvmul-zf 30841, axhvmulid-zf 30842, axhvmulass-zf 30843, axhvdistr1-zf 30844, axhvdistr2-zf 30845, axhvmul0-zf 30846, axhfi-zf 30847, axhis1-zf 30848, axhis2-zf 30849, axhis3-zf 30850, axhis4-zf 30851, and axhcompl-zf 30852 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 30835. | ||
Axiom | ax-hilex 30853 | 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 30854 | Vector addition is an operation on β. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
β’ +β :( β Γ β)βΆ β | ||
Axiom | ax-hvcom 30855 | Vector addition is commutative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ +β π΅) = (π΅ +β π΄)) | ||
Axiom | ax-hvass 30856 | Vector addition is associative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ +β π΅) +β πΆ) = (π΄ +β (π΅ +β πΆ))) | ||
Axiom | ax-hv0cl 30857 | The zero vector is in the vector space. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
β’ 0β β β | ||
Axiom | ax-hvaddid 30858 | Addition with the zero vector. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (π΄ +β 0β) = π΄) | ||
Axiom | ax-hfvmul 30859 | Scalar multiplication is an operation on β and β. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
β’ Β·β :(β Γ β)βΆ β | ||
Axiom | ax-hvmulid 30860 | Scalar multiplication by one. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (1 Β·β π΄) = π΄) | ||
Axiom | ax-hvmulass 30861 | Scalar multiplication associative law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ Β· π΅) Β·β πΆ) = (π΄ Β·β (π΅ Β·β πΆ))) | ||
Axiom | ax-hvdistr1 30862 | Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β·β (π΅ +β πΆ)) = ((π΄ Β·β π΅) +β (π΄ Β·β πΆ))) | ||
Axiom | ax-hvdistr2 30863 | Scalar multiplication distributive law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + π΅) Β·β πΆ) = ((π΄ Β·β πΆ) +β (π΅ Β·β πΆ))) | ||
Axiom | ax-hvmul0 30864 | Scalar multiplication by zero. We can derive the existence of the negative of a vector from this axiom (see hvsubid 30880 and hvsubval 30870). (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (0 Β·β π΄) = 0β) | ||
Theorem | hvmulex 30865 | The Hilbert space scalar product operation is a set. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.) |
β’ Β·β β V | ||
Theorem | hvaddcl 30866 | Closure of vector addition. (Contributed by NM, 18-Apr-2007.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ +β π΅) β β) | ||
Theorem | hvmulcl 30867 | Closure of scalar multiplication. (Contributed by NM, 19-Apr-2007.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ Β·β π΅) β β) | ||
Theorem | hvmulcli 30868 | Closure inference for scalar multiplication. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ Β·β π΅) β β | ||
Theorem | hvsubf 30869 | Mapping domain and codomain of vector subtraction. (Contributed by NM, 6-Sep-2007.) (New usage is discouraged.) |
β’ ββ :( β Γ β)βΆ β | ||
Theorem | hvsubval 30870 | Value of vector subtraction. (Contributed by NM, 5-Sep-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ ββ π΅) = (π΄ +β (-1 Β·β π΅))) | ||
Theorem | hvsubcl 30871 | Closure of vector subtraction. (Contributed by NM, 17-Aug-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ ββ π΅) β β) | ||
Theorem | hvaddcli 30872 | Closure of vector addition. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ +β π΅) β β | ||
Theorem | hvcomi 30873 | Commutation of vector addition. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ +β π΅) = (π΅ +β π΄) | ||
Theorem | hvsubvali 30874 | Value of vector subtraction definition. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ ββ π΅) = (π΄ +β (-1 Β·β π΅)) | ||
Theorem | hvsubcli 30875 | Closure of vector subtraction. (Contributed by NM, 2-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ ββ π΅) β β | ||
Theorem | ifhvhv0 30876 | Prove if(π΄ β β, π΄, 0β) β β. (Contributed by David A. Wheeler, 7-Dec-2018.) (New usage is discouraged.) |
β’ if(π΄ β β, π΄, 0β) β β | ||
Theorem | hvaddlid 30877 | Addition with the zero vector. (Contributed by NM, 18-Oct-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (0β +β π΄) = π΄) | ||
Theorem | hvmul0 30878 | Scalar multiplication with the zero vector. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (π΄ Β·β 0β) = 0β) | ||
Theorem | hvmul0or 30879 | 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 30880 | Subtraction of a vector from itself. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (π΄ ββ π΄) = 0β) | ||
Theorem | hvnegid 30881 | Addition of negative of a vector to itself. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.) |
β’ (π΄ β β β (π΄ +β (-1 Β·β π΄)) = 0β) | ||
Theorem | hv2neg 30882 | Two ways to express the negative of a vector. (Contributed by NM, 23-May-2005.) (New usage is discouraged.) |
β’ (π΄ β β β (0β ββ π΄) = (-1 Β·β π΄)) | ||
Theorem | hvaddlidi 30883 | Addition with the zero vector. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β β β’ (0β +β π΄) = π΄ | ||
Theorem | hvnegidi 30884 | Addition of negative of a vector to itself. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β β β’ (π΄ +β (-1 Β·β π΄)) = 0β | ||
Theorem | hv2negi 30885 | Two ways to express the negative of a vector. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β β β β’ (0β ββ π΄) = (-1 Β·β π΄) | ||
Theorem | hvm1neg 30886 | 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 30887 | Value of vector addition in terms of vector subtraction. (Contributed by NM, 10-Jun-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ +β π΅) = (π΄ ββ (-1 Β·β π΅))) | ||
Theorem | hvadd32 30888 | Commutative/associative law. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ +β π΅) +β πΆ) = ((π΄ +β πΆ) +β π΅)) | ||
Theorem | hvadd12 30889 | Commutative/associative law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ +β (π΅ +β πΆ)) = (π΅ +β (π΄ +β πΆ))) | ||
Theorem | hvadd4 30890 | Hilbert vector space addition law. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ +β π΅) +β (πΆ +β π·)) = ((π΄ +β πΆ) +β (π΅ +β π·))) | ||
Theorem | hvsub4 30891 | Hilbert vector space addition/subtraction law. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ +β π΅) ββ (πΆ +β π·)) = ((π΄ ββ πΆ) +β (π΅ ββ π·))) | ||
Theorem | hvaddsub12 30892 | Commutative/associative law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ +β (π΅ ββ πΆ)) = (π΅ +β (π΄ ββ πΆ))) | ||
Theorem | hvpncan 30893 | Addition/subtraction cancellation law for vectors in Hilbert space. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ +β π΅) ββ π΅) = π΄) | ||
Theorem | hvpncan2 30894 | Addition/subtraction cancellation law for vectors in Hilbert space. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ +β π΅) ββ π΄) = π΅) | ||
Theorem | hvaddsubass 30895 | Associativity of sum and difference of Hilbert space vectors. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ +β π΅) ββ πΆ) = (π΄ +β (π΅ ββ πΆ))) | ||
Theorem | hvpncan3 30896 | Subtraction and addition of equal Hilbert space vectors. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ +β (π΅ ββ π΄)) = π΅) | ||
Theorem | hvmulcom 30897 | Scalar multiplication commutative law. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β·β (π΅ Β·β πΆ)) = (π΅ Β·β (π΄ Β·β πΆ))) | ||
Theorem | hvsubass 30898 | Hilbert vector space associative law for subtraction. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) ββ πΆ) = (π΄ ββ (π΅ +β πΆ))) | ||
Theorem | hvsub32 30899 | Hilbert vector space commutative/associative law. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) ββ πΆ) = ((π΄ ββ πΆ) ββ π΅)) | ||
Theorem | hvmulassi 30900 | Scalar multiplication associative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ Β· π΅) Β·β πΆ) = (π΄ Β·β (π΅ Β·β πΆ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |