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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-hcau 29701* | Define the set of Cauchy sequences on a Hilbert space. See hcau 29912 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 29702 | The group (addition) operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β NrmCVec β β’ +β = ( +π£ βπ) | ||
Theorem | h2hsm 29703 | The scalar product operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β NrmCVec β β’ Β·β = ( Β·π OLD βπ) | ||
Theorem | h2hnm 29704 | The norm function of Hilbert space. (Contributed by NM, 5-Jun-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β NrmCVec β β’ normβ = (normCVβπ) | ||
Theorem | h2hvs 29705 | 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 29706 | 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 29707 | 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 29708 | 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 29709 through axhcompl-zf 29726, 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 29696 above. See also the comment in ax-hilex 29727. | ||
Theorem | axhilex-zf 29709 | Derive Axiom ax-hilex 29727 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ β β V | ||
Theorem | axhfvadd-zf 29710 | Derive Axiom ax-hfvadd 29728 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ +β :( β Γ β)βΆ β | ||
Theorem | axhvcom-zf 29711 | Derive Axiom ax-hvcom 29729 from Hilbert space under ZF set theory. (Contributed by NM, 27-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ ((π΄ β β β§ π΅ β β) β (π΄ +β π΅) = (π΅ +β π΄)) | ||
Theorem | axhvass-zf 29712 | Derive Axiom ax-hvass 29730 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ +β π΅) +β πΆ) = (π΄ +β (π΅ +β πΆ))) | ||
Theorem | axhv0cl-zf 29713 | Derive Axiom ax-hv0cl 29731 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ 0β β β | ||
Theorem | axhvaddid-zf 29714 | Derive Axiom ax-hvaddid 29732 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ (π΄ β β β (π΄ +β 0β) = π΄) | ||
Theorem | axhfvmul-zf 29715 | Derive Axiom ax-hfvmul 29733 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ Β·β :(β Γ β)βΆ β | ||
Theorem | axhvmulid-zf 29716 | Derive Axiom ax-hvmulid 29734 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ (π΄ β β β (1 Β·β π΄) = π΄) | ||
Theorem | axhvmulass-zf 29717 | Derive Axiom ax-hvmulass 29735 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ Β· π΅) Β·β πΆ) = (π΄ Β·β (π΅ Β·β πΆ))) | ||
Theorem | axhvdistr1-zf 29718 | Derive Axiom ax-hvdistr1 29736 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β·β (π΅ +β πΆ)) = ((π΄ Β·β π΅) +β (π΄ Β·β πΆ))) | ||
Theorem | axhvdistr2-zf 29719 | Derive Axiom ax-hvdistr2 29737 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + π΅) Β·β πΆ) = ((π΄ Β·β πΆ) +β (π΅ Β·β πΆ))) | ||
Theorem | axhvmul0-zf 29720 | Derive Axiom ax-hvmul0 29738 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ (π΄ β β β (0 Β·β π΄) = 0β) | ||
Theorem | axhfi-zf 29721 | Derive Axiom ax-hfi 29807 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 29722 | Derive Axiom ax-his1 29810 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 29723 | Derive Axiom ax-his2 29811 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 29724 | Derive Axiom ax-his3 29812 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 29725 | Derive Axiom ax-his4 29813 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 29726* | Derive Axiom ax-hcompl 29930 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 29727, ax-hfvadd 29728, ax-hvcom 29729, ax-hvass 29730, ax-hv0cl 29731, ax-hvaddid 29732, ax-hfvmul 29733, ax-hvmulid 29734, ax-hvmulass 29735, ax-hvdistr1 29736, ax-hvdistr2 29737, ax-hvmul0 29738, ax-hfi 29807, ax-his1 29810, ax-his2 29811, ax-his3 29812, ax-his4 29813, and ax-hcompl 29930. 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 29709, axhfvadd-zf 29710, axhvcom-zf 29711, axhvass-zf 29712, axhv0cl-zf 29713, axhvaddid-zf 29714, axhfvmul-zf 29715, axhvmulid-zf 29716, axhvmulass-zf 29717, axhvdistr1-zf 29718, axhvdistr2-zf 29719, axhvmul0-zf 29720, axhfi-zf 29721, axhis1-zf 29722, axhis2-zf 29723, axhis3-zf 29724, axhis4-zf 29725, and axhcompl-zf 29726 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 29709. | ||
Axiom | ax-hilex 29727 | 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 29728 | Vector addition is an operation on β. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
β’ +β :( β Γ β)βΆ β | ||
Axiom | ax-hvcom 29729 | Vector addition is commutative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ +β π΅) = (π΅ +β π΄)) | ||
Axiom | ax-hvass 29730 | Vector addition is associative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ +β π΅) +β πΆ) = (π΄ +β (π΅ +β πΆ))) | ||
Axiom | ax-hv0cl 29731 | The zero vector is in the vector space. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
β’ 0β β β | ||
Axiom | ax-hvaddid 29732 | Addition with the zero vector. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (π΄ +β 0β) = π΄) | ||
Axiom | ax-hfvmul 29733 | Scalar multiplication is an operation on β and β. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
β’ Β·β :(β Γ β)βΆ β | ||
Axiom | ax-hvmulid 29734 | Scalar multiplication by one. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (1 Β·β π΄) = π΄) | ||
Axiom | ax-hvmulass 29735 | Scalar multiplication associative law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ Β· π΅) Β·β πΆ) = (π΄ Β·β (π΅ Β·β πΆ))) | ||
Axiom | ax-hvdistr1 29736 | Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β·β (π΅ +β πΆ)) = ((π΄ Β·β π΅) +β (π΄ Β·β πΆ))) | ||
Axiom | ax-hvdistr2 29737 | Scalar multiplication distributive law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + π΅) Β·β πΆ) = ((π΄ Β·β πΆ) +β (π΅ Β·β πΆ))) | ||
Axiom | ax-hvmul0 29738 | Scalar multiplication by zero. We can derive the existence of the negative of a vector from this axiom (see hvsubid 29754 and hvsubval 29744). (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (0 Β·β π΄) = 0β) | ||
Theorem | hvmulex 29739 | The Hilbert space scalar product operation is a set. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.) |
β’ Β·β β V | ||
Theorem | hvaddcl 29740 | Closure of vector addition. (Contributed by NM, 18-Apr-2007.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ +β π΅) β β) | ||
Theorem | hvmulcl 29741 | Closure of scalar multiplication. (Contributed by NM, 19-Apr-2007.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ Β·β π΅) β β) | ||
Theorem | hvmulcli 29742 | Closure inference for scalar multiplication. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ Β·β π΅) β β | ||
Theorem | hvsubf 29743 | Mapping domain and codomain of vector subtraction. (Contributed by NM, 6-Sep-2007.) (New usage is discouraged.) |
β’ ββ :( β Γ β)βΆ β | ||
Theorem | hvsubval 29744 | Value of vector subtraction. (Contributed by NM, 5-Sep-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ ββ π΅) = (π΄ +β (-1 Β·β π΅))) | ||
Theorem | hvsubcl 29745 | Closure of vector subtraction. (Contributed by NM, 17-Aug-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ ββ π΅) β β) | ||
Theorem | hvaddcli 29746 | Closure of vector addition. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ +β π΅) β β | ||
Theorem | hvcomi 29747 | Commutation of vector addition. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ +β π΅) = (π΅ +β π΄) | ||
Theorem | hvsubvali 29748 | Value of vector subtraction definition. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ ββ π΅) = (π΄ +β (-1 Β·β π΅)) | ||
Theorem | hvsubcli 29749 | Closure of vector subtraction. (Contributed by NM, 2-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ ββ π΅) β β | ||
Theorem | ifhvhv0 29750 | Prove if(π΄ β β, π΄, 0β) β β. (Contributed by David A. Wheeler, 7-Dec-2018.) (New usage is discouraged.) |
β’ if(π΄ β β, π΄, 0β) β β | ||
Theorem | hvaddid2 29751 | Addition with the zero vector. (Contributed by NM, 18-Oct-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (0β +β π΄) = π΄) | ||
Theorem | hvmul0 29752 | Scalar multiplication with the zero vector. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (π΄ Β·β 0β) = 0β) | ||
Theorem | hvmul0or 29753 | 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 29754 | Subtraction of a vector from itself. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (π΄ ββ π΄) = 0β) | ||
Theorem | hvnegid 29755 | Addition of negative of a vector to itself. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.) |
β’ (π΄ β β β (π΄ +β (-1 Β·β π΄)) = 0β) | ||
Theorem | hv2neg 29756 | Two ways to express the negative of a vector. (Contributed by NM, 23-May-2005.) (New usage is discouraged.) |
β’ (π΄ β β β (0β ββ π΄) = (-1 Β·β π΄)) | ||
Theorem | hvaddid2i 29757 | Addition with the zero vector. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β β β’ (0β +β π΄) = π΄ | ||
Theorem | hvnegidi 29758 | Addition of negative of a vector to itself. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β β β’ (π΄ +β (-1 Β·β π΄)) = 0β | ||
Theorem | hv2negi 29759 | Two ways to express the negative of a vector. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β β β β’ (0β ββ π΄) = (-1 Β·β π΄) | ||
Theorem | hvm1neg 29760 | 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 29761 | Value of vector addition in terms of vector subtraction. (Contributed by NM, 10-Jun-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ +β π΅) = (π΄ ββ (-1 Β·β π΅))) | ||
Theorem | hvadd32 29762 | Commutative/associative law. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ +β π΅) +β πΆ) = ((π΄ +β πΆ) +β π΅)) | ||
Theorem | hvadd12 29763 | Commutative/associative law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ +β (π΅ +β πΆ)) = (π΅ +β (π΄ +β πΆ))) | ||
Theorem | hvadd4 29764 | Hilbert vector space addition law. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ +β π΅) +β (πΆ +β π·)) = ((π΄ +β πΆ) +β (π΅ +β π·))) | ||
Theorem | hvsub4 29765 | Hilbert vector space addition/subtraction law. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ +β π΅) ββ (πΆ +β π·)) = ((π΄ ββ πΆ) +β (π΅ ββ π·))) | ||
Theorem | hvaddsub12 29766 | Commutative/associative law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ +β (π΅ ββ πΆ)) = (π΅ +β (π΄ ββ πΆ))) | ||
Theorem | hvpncan 29767 | Addition/subtraction cancellation law for vectors in Hilbert space. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ +β π΅) ββ π΅) = π΄) | ||
Theorem | hvpncan2 29768 | Addition/subtraction cancellation law for vectors in Hilbert space. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ +β π΅) ββ π΄) = π΅) | ||
Theorem | hvaddsubass 29769 | Associativity of sum and difference of Hilbert space vectors. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ +β π΅) ββ πΆ) = (π΄ +β (π΅ ββ πΆ))) | ||
Theorem | hvpncan3 29770 | Subtraction and addition of equal Hilbert space vectors. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ +β (π΅ ββ π΄)) = π΅) | ||
Theorem | hvmulcom 29771 | Scalar multiplication commutative law. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β·β (π΅ Β·β πΆ)) = (π΅ Β·β (π΄ Β·β πΆ))) | ||
Theorem | hvsubass 29772 | Hilbert vector space associative law for subtraction. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) ββ πΆ) = (π΄ ββ (π΅ +β πΆ))) | ||
Theorem | hvsub32 29773 | Hilbert vector space commutative/associative law. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) ββ πΆ) = ((π΄ ββ πΆ) ββ π΅)) | ||
Theorem | hvmulassi 29774 | Scalar multiplication associative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ Β· π΅) Β·β πΆ) = (π΄ Β·β (π΅ Β·β πΆ)) | ||
Theorem | hvmulcomi 29775 | Scalar multiplication commutative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (π΄ Β·β (π΅ Β·β πΆ)) = (π΅ Β·β (π΄ Β·β πΆ)) | ||
Theorem | hvmul2negi 29776 | Double negative in scalar multiplication. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (-π΄ Β·β (-π΅ Β·β πΆ)) = (π΄ Β·β (π΅ Β·β πΆ)) | ||
Theorem | hvsubdistr1 29777 | Scalar multiplication distributive law for subtraction. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β·β (π΅ ββ πΆ)) = ((π΄ Β·β π΅) ββ (π΄ Β·β πΆ))) | ||
Theorem | hvsubdistr2 29778 | Scalar multiplication distributive law for subtraction. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ β π΅) Β·β πΆ) = ((π΄ Β·β πΆ) ββ (π΅ Β·β πΆ))) | ||
Theorem | hvdistr1i 29779 | Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (π΄ Β·β (π΅ +β πΆ)) = ((π΄ Β·β π΅) +β (π΄ Β·β πΆ)) | ||
Theorem | hvsubdistr1i 29780 | Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (π΄ Β·β (π΅ ββ πΆ)) = ((π΄ Β·β π΅) ββ (π΄ Β·β πΆ)) | ||
Theorem | hvassi 29781 | Hilbert vector space associative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ +β π΅) +β πΆ) = (π΄ +β (π΅ +β πΆ)) | ||
Theorem | hvadd32i 29782 | Hilbert vector space commutative/associative law. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ +β π΅) +β πΆ) = ((π΄ +β πΆ) +β π΅) | ||
Theorem | hvsubassi 29783 | 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 29784 | 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 29785 | Hilbert vector space commutative/associative law. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (π΄ +β (π΅ +β πΆ)) = (π΅ +β (π΄ +β πΆ)) | ||
Theorem | hvadd4i 29786 | Hilbert vector space addition law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β & β’ π· β β β β’ ((π΄ +β π΅) +β (πΆ +β π·)) = ((π΄ +β πΆ) +β (π΅ +β π·)) | ||
Theorem | hvsubsub4i 29787 | Hilbert vector space addition law. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β & β’ π· β β β β’ ((π΄ ββ π΅) ββ (πΆ ββ π·)) = ((π΄ ββ πΆ) ββ (π΅ ββ π·)) | ||
Theorem | hvsubsub4 29788 | Hilbert vector space addition/subtraction law. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ ββ π΅) ββ (πΆ ββ π·)) = ((π΄ ββ πΆ) ββ (π΅ ββ π·))) | ||
Theorem | hv2times 29789 | Two times a vector. (Contributed by NM, 22-Jun-2006.) (New usage is discouraged.) |
β’ (π΄ β β β (2 Β·β π΄) = (π΄ +β π΄)) | ||
Theorem | hvnegdii 29790 | Distribution of negative over subtraction. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (-1 Β·β (π΄ ββ π΅)) = (π΅ ββ π΄) | ||
Theorem | hvsubeq0i 29791 | If the difference between two vectors is zero, they are equal. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ ((π΄ ββ π΅) = 0β β π΄ = π΅) | ||
Theorem | hvsubcan2i 29792 | Vector cancellation law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ ((π΄ +β π΅) +β (π΄ ββ π΅)) = (2 Β·β π΄) | ||
Theorem | hvaddcani 29793 | Cancellation law for vector addition. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ +β π΅) = (π΄ +β πΆ) β π΅ = πΆ) | ||
Theorem | hvsubaddi 29794 | Relationship between vector subtraction and addition. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ ββ π΅) = πΆ β (π΅ +β πΆ) = π΄) | ||
Theorem | hvnegdi 29795 | Distribution of negative over subtraction. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (-1 Β·β (π΄ ββ π΅)) = (π΅ ββ π΄)) | ||
Theorem | hvsubeq0 29796 | If the difference between two vectors is zero, they are equal. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ ββ π΅) = 0β β π΄ = π΅)) | ||
Theorem | hvaddeq0 29797 | 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 29798 | Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ +β π΅) = (π΄ +β πΆ) β π΅ = πΆ)) | ||
Theorem | hvaddcan2 29799 | Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ +β πΆ) = (π΅ +β πΆ) β π΄ = π΅)) | ||
Theorem | hvmulcan 29800 | Cancellation law for scalar multiplication. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΄ β 0) β§ π΅ β β β§ πΆ β β) β ((π΄ Β·β π΅) = (π΄ Β·β πΆ) β π΅ = πΆ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |