![]() |
Metamath
Proof Explorer Theorem List (p. 303 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cbo 30201 | Extend class notation with set of bounded linear operators. |
class BndLinOp | ||
Syntax | cuo 30202 | Extend class notation with set of unitary Hilbert space operators. |
class UniOp | ||
Syntax | cho 30203 | Extend class notation with set of Hermitian Hilbert space operators. |
class HrmOp | ||
Syntax | cnmf 30204 | Extend class notation with the functional norm function. |
class normfn | ||
Syntax | cnl 30205 | Extend class notation with the functional nullspace function. |
class null | ||
Syntax | ccnfn 30206 | Extend class notation with set of continuous Hilbert space functionals. |
class ContFn | ||
Syntax | clf 30207 | Extend class notation with set of linear Hilbert space functionals. |
class LinFn | ||
Syntax | cado 30208 | Extend class notation with Hilbert space adjoint function. |
class adjβ | ||
Syntax | cbr 30209 | Extend class notation with the bra of a vector in Dirac bra-ket notation. |
class bra | ||
Syntax | ck 30210 | Extend class notation with the outer product of two vectors in Dirac bra-ket notation. |
class ketbra | ||
Syntax | cleo 30211 | Extend class notation with positive operator ordering. |
class β€op | ||
Syntax | cei 30212 | Extend class notation with Hilbert space eigenvector function. |
class eigvec | ||
Syntax | cel 30213 | Extend class notation with Hilbert space eigenvalue function. |
class eigval | ||
Syntax | cspc 30214 | Extend class notation with the spectrum of an operator. |
class Lambda | ||
Syntax | cst 30215 | Extend class notation with set of states on a Hilbert lattice. |
class States | ||
Syntax | chst 30216 | Extend class notation with set of Hilbert-space-valued states on a Hilbert lattice. |
class CHStates | ||
Syntax | ccv 30217 | Extend class notation with the covers relation on a Hilbert lattice. |
class ββ | ||
Syntax | cat 30218 | Extend class notation with set of atoms on a Hilbert lattice. |
class HAtoms | ||
Syntax | cmd 30219 | Extend class notation with the modular pair relation on a Hilbert lattice. |
class πβ | ||
Syntax | cdmd 30220 | Extend class notation with the dual modular pair relation on a Hilbert lattice. |
class πβ* | ||
Definition | df-hnorm 30221 | Define the function for the norm of a vector of Hilbert space. See normval 30377 for its value and normcl 30378 for its closure. Theorems norm-i-i 30386, norm-ii-i 30390, and norm-iii-i 30392 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 30222 | Define base set of Hilbert space, for use if we want to develop Hilbert space independently from the axioms (see comments in ax-hilex 30252). 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 30420. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ β = (BaseSetββ¨β¨ +β , Β·β β©, normββ©) | ||
Definition | df-h0v 30223 | 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 30421. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ 0β = (0vecββ¨β¨ +β , Β·β β©, normββ©) | ||
Definition | df-hvsub 30224* | Define vector subtraction. See hvsubvali 30273 for its value and hvsubcli 30274 for its closure. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.) |
β’ ββ = (π₯ β β, π¦ β β β¦ (π₯ +β (-1 Β·β π¦))) | ||
Definition | df-hlim 30225* | Define the limit relation for Hilbert space. See hlimi 30441 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 30226* | Define the set of Cauchy sequences on a Hilbert space. See hcau 30437 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 30227 | The group (addition) operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β NrmCVec β β’ +β = ( +π£ βπ) | ||
Theorem | h2hsm 30228 | The scalar product operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β NrmCVec β β’ Β·β = ( Β·π OLD βπ) | ||
Theorem | h2hnm 30229 | The norm function of Hilbert space. (Contributed by NM, 5-Jun-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β NrmCVec β β’ normβ = (normCVβπ) | ||
Theorem | h2hvs 30230 | 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 30231 | 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 30232 | 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 30233 | 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 30234 through axhcompl-zf 30251, 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 30221 above. See also the comment in ax-hilex 30252. | ||
Theorem | axhilex-zf 30234 | Derive Axiom ax-hilex 30252 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ β β V | ||
Theorem | axhfvadd-zf 30235 | Derive Axiom ax-hfvadd 30253 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ +β :( β Γ β)βΆ β | ||
Theorem | axhvcom-zf 30236 | Derive Axiom ax-hvcom 30254 from Hilbert space under ZF set theory. (Contributed by NM, 27-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ ((π΄ β β β§ π΅ β β) β (π΄ +β π΅) = (π΅ +β π΄)) | ||
Theorem | axhvass-zf 30237 | Derive Axiom ax-hvass 30255 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ +β π΅) +β πΆ) = (π΄ +β (π΅ +β πΆ))) | ||
Theorem | axhv0cl-zf 30238 | Derive Axiom ax-hv0cl 30256 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ 0β β β | ||
Theorem | axhvaddid-zf 30239 | Derive Axiom ax-hvaddid 30257 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ (π΄ β β β (π΄ +β 0β) = π΄) | ||
Theorem | axhfvmul-zf 30240 | Derive Axiom ax-hfvmul 30258 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ Β·β :(β Γ β)βΆ β | ||
Theorem | axhvmulid-zf 30241 | Derive Axiom ax-hvmulid 30259 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ (π΄ β β β (1 Β·β π΄) = π΄) | ||
Theorem | axhvmulass-zf 30242 | Derive Axiom ax-hvmulass 30260 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ Β· π΅) Β·β πΆ) = (π΄ Β·β (π΅ Β·β πΆ))) | ||
Theorem | axhvdistr1-zf 30243 | Derive Axiom ax-hvdistr1 30261 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β·β (π΅ +β πΆ)) = ((π΄ Β·β π΅) +β (π΄ Β·β πΆ))) | ||
Theorem | axhvdistr2-zf 30244 | Derive Axiom ax-hvdistr2 30262 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + π΅) Β·β πΆ) = ((π΄ Β·β πΆ) +β (π΅ Β·β πΆ))) | ||
Theorem | axhvmul0-zf 30245 | Derive Axiom ax-hvmul0 30263 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ (π΄ β β β (0 Β·β π΄) = 0β) | ||
Theorem | axhfi-zf 30246 | Derive Axiom ax-hfi 30332 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 30247 | Derive Axiom ax-his1 30335 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 30248 | Derive Axiom ax-his2 30336 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 30249 | Derive Axiom ax-his3 30337 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 30250 | Derive Axiom ax-his4 30338 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 30251* | Derive Axiom ax-hcompl 30455 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 30252, ax-hfvadd 30253, ax-hvcom 30254, ax-hvass 30255, ax-hv0cl 30256, ax-hvaddid 30257, ax-hfvmul 30258, ax-hvmulid 30259, ax-hvmulass 30260, ax-hvdistr1 30261, ax-hvdistr2 30262, ax-hvmul0 30263, ax-hfi 30332, ax-his1 30335, ax-his2 30336, ax-his3 30337, ax-his4 30338, and ax-hcompl 30455. 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 30234, axhfvadd-zf 30235, axhvcom-zf 30236, axhvass-zf 30237, axhv0cl-zf 30238, axhvaddid-zf 30239, axhfvmul-zf 30240, axhvmulid-zf 30241, axhvmulass-zf 30242, axhvdistr1-zf 30243, axhvdistr2-zf 30244, axhvmul0-zf 30245, axhfi-zf 30246, axhis1-zf 30247, axhis2-zf 30248, axhis3-zf 30249, axhis4-zf 30250, and axhcompl-zf 30251 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 30234. | ||
Axiom | ax-hilex 30252 | 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 30253 | Vector addition is an operation on β. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
β’ +β :( β Γ β)βΆ β | ||
Axiom | ax-hvcom 30254 | Vector addition is commutative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ +β π΅) = (π΅ +β π΄)) | ||
Axiom | ax-hvass 30255 | Vector addition is associative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ +β π΅) +β πΆ) = (π΄ +β (π΅ +β πΆ))) | ||
Axiom | ax-hv0cl 30256 | The zero vector is in the vector space. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
β’ 0β β β | ||
Axiom | ax-hvaddid 30257 | Addition with the zero vector. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (π΄ +β 0β) = π΄) | ||
Axiom | ax-hfvmul 30258 | Scalar multiplication is an operation on β and β. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
β’ Β·β :(β Γ β)βΆ β | ||
Axiom | ax-hvmulid 30259 | Scalar multiplication by one. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (1 Β·β π΄) = π΄) | ||
Axiom | ax-hvmulass 30260 | Scalar multiplication associative law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ Β· π΅) Β·β πΆ) = (π΄ Β·β (π΅ Β·β πΆ))) | ||
Axiom | ax-hvdistr1 30261 | Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β·β (π΅ +β πΆ)) = ((π΄ Β·β π΅) +β (π΄ Β·β πΆ))) | ||
Axiom | ax-hvdistr2 30262 | Scalar multiplication distributive law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + π΅) Β·β πΆ) = ((π΄ Β·β πΆ) +β (π΅ Β·β πΆ))) | ||
Axiom | ax-hvmul0 30263 | Scalar multiplication by zero. We can derive the existence of the negative of a vector from this axiom (see hvsubid 30279 and hvsubval 30269). (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (0 Β·β π΄) = 0β) | ||
Theorem | hvmulex 30264 | The Hilbert space scalar product operation is a set. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.) |
β’ Β·β β V | ||
Theorem | hvaddcl 30265 | Closure of vector addition. (Contributed by NM, 18-Apr-2007.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ +β π΅) β β) | ||
Theorem | hvmulcl 30266 | Closure of scalar multiplication. (Contributed by NM, 19-Apr-2007.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ Β·β π΅) β β) | ||
Theorem | hvmulcli 30267 | Closure inference for scalar multiplication. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ Β·β π΅) β β | ||
Theorem | hvsubf 30268 | Mapping domain and codomain of vector subtraction. (Contributed by NM, 6-Sep-2007.) (New usage is discouraged.) |
β’ ββ :( β Γ β)βΆ β | ||
Theorem | hvsubval 30269 | Value of vector subtraction. (Contributed by NM, 5-Sep-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ ββ π΅) = (π΄ +β (-1 Β·β π΅))) | ||
Theorem | hvsubcl 30270 | Closure of vector subtraction. (Contributed by NM, 17-Aug-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ ββ π΅) β β) | ||
Theorem | hvaddcli 30271 | Closure of vector addition. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ +β π΅) β β | ||
Theorem | hvcomi 30272 | Commutation of vector addition. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ +β π΅) = (π΅ +β π΄) | ||
Theorem | hvsubvali 30273 | Value of vector subtraction definition. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ ββ π΅) = (π΄ +β (-1 Β·β π΅)) | ||
Theorem | hvsubcli 30274 | Closure of vector subtraction. (Contributed by NM, 2-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ ββ π΅) β β | ||
Theorem | ifhvhv0 30275 | Prove if(π΄ β β, π΄, 0β) β β. (Contributed by David A. Wheeler, 7-Dec-2018.) (New usage is discouraged.) |
β’ if(π΄ β β, π΄, 0β) β β | ||
Theorem | hvaddlid 30276 | Addition with the zero vector. (Contributed by NM, 18-Oct-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (0β +β π΄) = π΄) | ||
Theorem | hvmul0 30277 | Scalar multiplication with the zero vector. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (π΄ Β·β 0β) = 0β) | ||
Theorem | hvmul0or 30278 | 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 30279 | Subtraction of a vector from itself. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (π΄ ββ π΄) = 0β) | ||
Theorem | hvnegid 30280 | Addition of negative of a vector to itself. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.) |
β’ (π΄ β β β (π΄ +β (-1 Β·β π΄)) = 0β) | ||
Theorem | hv2neg 30281 | Two ways to express the negative of a vector. (Contributed by NM, 23-May-2005.) (New usage is discouraged.) |
β’ (π΄ β β β (0β ββ π΄) = (-1 Β·β π΄)) | ||
Theorem | hvaddlidi 30282 | Addition with the zero vector. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β β β’ (0β +β π΄) = π΄ | ||
Theorem | hvnegidi 30283 | Addition of negative of a vector to itself. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β β β’ (π΄ +β (-1 Β·β π΄)) = 0β | ||
Theorem | hv2negi 30284 | Two ways to express the negative of a vector. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β β β β’ (0β ββ π΄) = (-1 Β·β π΄) | ||
Theorem | hvm1neg 30285 | 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 30286 | Value of vector addition in terms of vector subtraction. (Contributed by NM, 10-Jun-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ +β π΅) = (π΄ ββ (-1 Β·β π΅))) | ||
Theorem | hvadd32 30287 | Commutative/associative law. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ +β π΅) +β πΆ) = ((π΄ +β πΆ) +β π΅)) | ||
Theorem | hvadd12 30288 | Commutative/associative law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ +β (π΅ +β πΆ)) = (π΅ +β (π΄ +β πΆ))) | ||
Theorem | hvadd4 30289 | Hilbert vector space addition law. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ +β π΅) +β (πΆ +β π·)) = ((π΄ +β πΆ) +β (π΅ +β π·))) | ||
Theorem | hvsub4 30290 | Hilbert vector space addition/subtraction law. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ +β π΅) ββ (πΆ +β π·)) = ((π΄ ββ πΆ) +β (π΅ ββ π·))) | ||
Theorem | hvaddsub12 30291 | Commutative/associative law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ +β (π΅ ββ πΆ)) = (π΅ +β (π΄ ββ πΆ))) | ||
Theorem | hvpncan 30292 | Addition/subtraction cancellation law for vectors in Hilbert space. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ +β π΅) ββ π΅) = π΄) | ||
Theorem | hvpncan2 30293 | Addition/subtraction cancellation law for vectors in Hilbert space. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ +β π΅) ββ π΄) = π΅) | ||
Theorem | hvaddsubass 30294 | Associativity of sum and difference of Hilbert space vectors. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ +β π΅) ββ πΆ) = (π΄ +β (π΅ ββ πΆ))) | ||
Theorem | hvpncan3 30295 | Subtraction and addition of equal Hilbert space vectors. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ +β (π΅ ββ π΄)) = π΅) | ||
Theorem | hvmulcom 30296 | Scalar multiplication commutative law. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β·β (π΅ Β·β πΆ)) = (π΅ Β·β (π΄ Β·β πΆ))) | ||
Theorem | hvsubass 30297 | Hilbert vector space associative law for subtraction. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) ββ πΆ) = (π΄ ββ (π΅ +β πΆ))) | ||
Theorem | hvsub32 30298 | Hilbert vector space commutative/associative law. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) ββ πΆ) = ((π΄ ββ πΆ) ββ π΅)) | ||
Theorem | hvmulassi 30299 | Scalar multiplication associative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ Β· π΅) Β·β πΆ) = (π΄ Β·β (π΅ Β·β πΆ)) | ||
Theorem | hvmulcomi 30300 | Scalar multiplication commutative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (π΄ Β·β (π΅ Β·β πΆ)) = (π΅ Β·β (π΄ Β·β πΆ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |