![]() |
Metamath
Proof Explorer Theorem List (p. 306 of 480) | < 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-30439) |
![]() (30440-31962) |
![]() (31963-47940) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | h2hlm 30501 | 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 30502 through axhcompl-zf 30519, 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 30489 above. See also the comment in ax-hilex 30520. | ||
Theorem | axhilex-zf 30502 | Derive Axiom ax-hilex 30520 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ β β V | ||
Theorem | axhfvadd-zf 30503 | Derive Axiom ax-hfvadd 30521 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ +β :( β Γ β)βΆ β | ||
Theorem | axhvcom-zf 30504 | Derive Axiom ax-hvcom 30522 from Hilbert space under ZF set theory. (Contributed by NM, 27-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ ((π΄ β β β§ π΅ β β) β (π΄ +β π΅) = (π΅ +β π΄)) | ||
Theorem | axhvass-zf 30505 | Derive Axiom ax-hvass 30523 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ +β π΅) +β πΆ) = (π΄ +β (π΅ +β πΆ))) | ||
Theorem | axhv0cl-zf 30506 | Derive Axiom ax-hv0cl 30524 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ 0β β β | ||
Theorem | axhvaddid-zf 30507 | Derive Axiom ax-hvaddid 30525 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ (π΄ β β β (π΄ +β 0β) = π΄) | ||
Theorem | axhfvmul-zf 30508 | Derive Axiom ax-hfvmul 30526 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ Β·β :(β Γ β)βΆ β | ||
Theorem | axhvmulid-zf 30509 | Derive Axiom ax-hvmulid 30527 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ (π΄ β β β (1 Β·β π΄) = π΄) | ||
Theorem | axhvmulass-zf 30510 | Derive Axiom ax-hvmulass 30528 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ Β· π΅) Β·β πΆ) = (π΄ Β·β (π΅ Β·β πΆ))) | ||
Theorem | axhvdistr1-zf 30511 | Derive Axiom ax-hvdistr1 30529 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β·β (π΅ +β πΆ)) = ((π΄ Β·β π΅) +β (π΄ Β·β πΆ))) | ||
Theorem | axhvdistr2-zf 30512 | Derive Axiom ax-hvdistr2 30530 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + π΅) Β·β πΆ) = ((π΄ Β·β πΆ) +β (π΅ Β·β πΆ))) | ||
Theorem | axhvmul0-zf 30513 | Derive Axiom ax-hvmul0 30531 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π β CHilOLD β β’ (π΄ β β β (0 Β·β π΄) = 0β) | ||
Theorem | axhfi-zf 30514 | Derive Axiom ax-hfi 30600 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 30515 | Derive Axiom ax-his1 30603 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 30516 | Derive Axiom ax-his2 30604 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 30517 | Derive Axiom ax-his3 30605 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 30518 | Derive Axiom ax-his4 30606 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 30519* | Derive Axiom ax-hcompl 30723 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 30520, ax-hfvadd 30521, ax-hvcom 30522, ax-hvass 30523, ax-hv0cl 30524, ax-hvaddid 30525, ax-hfvmul 30526, ax-hvmulid 30527, ax-hvmulass 30528, ax-hvdistr1 30529, ax-hvdistr2 30530, ax-hvmul0 30531, ax-hfi 30600, ax-his1 30603, ax-his2 30604, ax-his3 30605, ax-his4 30606, and ax-hcompl 30723. 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 30502, axhfvadd-zf 30503, axhvcom-zf 30504, axhvass-zf 30505, axhv0cl-zf 30506, axhvaddid-zf 30507, axhfvmul-zf 30508, axhvmulid-zf 30509, axhvmulass-zf 30510, axhvdistr1-zf 30511, axhvdistr2-zf 30512, axhvmul0-zf 30513, axhfi-zf 30514, axhis1-zf 30515, axhis2-zf 30516, axhis3-zf 30517, axhis4-zf 30518, and axhcompl-zf 30519 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 30502. | ||
Axiom | ax-hilex 30520 | 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 30521 | Vector addition is an operation on β. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
β’ +β :( β Γ β)βΆ β | ||
Axiom | ax-hvcom 30522 | Vector addition is commutative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ +β π΅) = (π΅ +β π΄)) | ||
Axiom | ax-hvass 30523 | Vector addition is associative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ +β π΅) +β πΆ) = (π΄ +β (π΅ +β πΆ))) | ||
Axiom | ax-hv0cl 30524 | The zero vector is in the vector space. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
β’ 0β β β | ||
Axiom | ax-hvaddid 30525 | Addition with the zero vector. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (π΄ +β 0β) = π΄) | ||
Axiom | ax-hfvmul 30526 | Scalar multiplication is an operation on β and β. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
β’ Β·β :(β Γ β)βΆ β | ||
Axiom | ax-hvmulid 30527 | Scalar multiplication by one. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (1 Β·β π΄) = π΄) | ||
Axiom | ax-hvmulass 30528 | Scalar multiplication associative law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ Β· π΅) Β·β πΆ) = (π΄ Β·β (π΅ Β·β πΆ))) | ||
Axiom | ax-hvdistr1 30529 | Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β·β (π΅ +β πΆ)) = ((π΄ Β·β π΅) +β (π΄ Β·β πΆ))) | ||
Axiom | ax-hvdistr2 30530 | Scalar multiplication distributive law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + π΅) Β·β πΆ) = ((π΄ Β·β πΆ) +β (π΅ Β·β πΆ))) | ||
Axiom | ax-hvmul0 30531 | Scalar multiplication by zero. We can derive the existence of the negative of a vector from this axiom (see hvsubid 30547 and hvsubval 30537). (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (0 Β·β π΄) = 0β) | ||
Theorem | hvmulex 30532 | The Hilbert space scalar product operation is a set. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.) |
β’ Β·β β V | ||
Theorem | hvaddcl 30533 | Closure of vector addition. (Contributed by NM, 18-Apr-2007.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ +β π΅) β β) | ||
Theorem | hvmulcl 30534 | Closure of scalar multiplication. (Contributed by NM, 19-Apr-2007.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ Β·β π΅) β β) | ||
Theorem | hvmulcli 30535 | Closure inference for scalar multiplication. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ Β·β π΅) β β | ||
Theorem | hvsubf 30536 | Mapping domain and codomain of vector subtraction. (Contributed by NM, 6-Sep-2007.) (New usage is discouraged.) |
β’ ββ :( β Γ β)βΆ β | ||
Theorem | hvsubval 30537 | Value of vector subtraction. (Contributed by NM, 5-Sep-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ ββ π΅) = (π΄ +β (-1 Β·β π΅))) | ||
Theorem | hvsubcl 30538 | Closure of vector subtraction. (Contributed by NM, 17-Aug-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ ββ π΅) β β) | ||
Theorem | hvaddcli 30539 | Closure of vector addition. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ +β π΅) β β | ||
Theorem | hvcomi 30540 | Commutation of vector addition. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ +β π΅) = (π΅ +β π΄) | ||
Theorem | hvsubvali 30541 | Value of vector subtraction definition. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ ββ π΅) = (π΄ +β (-1 Β·β π΅)) | ||
Theorem | hvsubcli 30542 | Closure of vector subtraction. (Contributed by NM, 2-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ ββ π΅) β β | ||
Theorem | ifhvhv0 30543 | Prove if(π΄ β β, π΄, 0β) β β. (Contributed by David A. Wheeler, 7-Dec-2018.) (New usage is discouraged.) |
β’ if(π΄ β β, π΄, 0β) β β | ||
Theorem | hvaddlid 30544 | Addition with the zero vector. (Contributed by NM, 18-Oct-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (0β +β π΄) = π΄) | ||
Theorem | hvmul0 30545 | Scalar multiplication with the zero vector. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (π΄ Β·β 0β) = 0β) | ||
Theorem | hvmul0or 30546 | 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 30547 | Subtraction of a vector from itself. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (π΄ ββ π΄) = 0β) | ||
Theorem | hvnegid 30548 | Addition of negative of a vector to itself. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.) |
β’ (π΄ β β β (π΄ +β (-1 Β·β π΄)) = 0β) | ||
Theorem | hv2neg 30549 | Two ways to express the negative of a vector. (Contributed by NM, 23-May-2005.) (New usage is discouraged.) |
β’ (π΄ β β β (0β ββ π΄) = (-1 Β·β π΄)) | ||
Theorem | hvaddlidi 30550 | Addition with the zero vector. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β β β’ (0β +β π΄) = π΄ | ||
Theorem | hvnegidi 30551 | Addition of negative of a vector to itself. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β β β’ (π΄ +β (-1 Β·β π΄)) = 0β | ||
Theorem | hv2negi 30552 | Two ways to express the negative of a vector. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β β β β’ (0β ββ π΄) = (-1 Β·β π΄) | ||
Theorem | hvm1neg 30553 | 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 30554 | Value of vector addition in terms of vector subtraction. (Contributed by NM, 10-Jun-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ +β π΅) = (π΄ ββ (-1 Β·β π΅))) | ||
Theorem | hvadd32 30555 | Commutative/associative law. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ +β π΅) +β πΆ) = ((π΄ +β πΆ) +β π΅)) | ||
Theorem | hvadd12 30556 | Commutative/associative law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ +β (π΅ +β πΆ)) = (π΅ +β (π΄ +β πΆ))) | ||
Theorem | hvadd4 30557 | Hilbert vector space addition law. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ +β π΅) +β (πΆ +β π·)) = ((π΄ +β πΆ) +β (π΅ +β π·))) | ||
Theorem | hvsub4 30558 | Hilbert vector space addition/subtraction law. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ +β π΅) ββ (πΆ +β π·)) = ((π΄ ββ πΆ) +β (π΅ ββ π·))) | ||
Theorem | hvaddsub12 30559 | Commutative/associative law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ +β (π΅ ββ πΆ)) = (π΅ +β (π΄ ββ πΆ))) | ||
Theorem | hvpncan 30560 | Addition/subtraction cancellation law for vectors in Hilbert space. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ +β π΅) ββ π΅) = π΄) | ||
Theorem | hvpncan2 30561 | Addition/subtraction cancellation law for vectors in Hilbert space. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ +β π΅) ββ π΄) = π΅) | ||
Theorem | hvaddsubass 30562 | Associativity of sum and difference of Hilbert space vectors. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ +β π΅) ββ πΆ) = (π΄ +β (π΅ ββ πΆ))) | ||
Theorem | hvpncan3 30563 | Subtraction and addition of equal Hilbert space vectors. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ +β (π΅ ββ π΄)) = π΅) | ||
Theorem | hvmulcom 30564 | Scalar multiplication commutative law. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β·β (π΅ Β·β πΆ)) = (π΅ Β·β (π΄ Β·β πΆ))) | ||
Theorem | hvsubass 30565 | Hilbert vector space associative law for subtraction. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) ββ πΆ) = (π΄ ββ (π΅ +β πΆ))) | ||
Theorem | hvsub32 30566 | Hilbert vector space commutative/associative law. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) ββ πΆ) = ((π΄ ββ πΆ) ββ π΅)) | ||
Theorem | hvmulassi 30567 | Scalar multiplication associative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ Β· π΅) Β·β πΆ) = (π΄ Β·β (π΅ Β·β πΆ)) | ||
Theorem | hvmulcomi 30568 | Scalar multiplication commutative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (π΄ Β·β (π΅ Β·β πΆ)) = (π΅ Β·β (π΄ Β·β πΆ)) | ||
Theorem | hvmul2negi 30569 | Double negative in scalar multiplication. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (-π΄ Β·β (-π΅ Β·β πΆ)) = (π΄ Β·β (π΅ Β·β πΆ)) | ||
Theorem | hvsubdistr1 30570 | Scalar multiplication distributive law for subtraction. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β·β (π΅ ββ πΆ)) = ((π΄ Β·β π΅) ββ (π΄ Β·β πΆ))) | ||
Theorem | hvsubdistr2 30571 | Scalar multiplication distributive law for subtraction. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ β π΅) Β·β πΆ) = ((π΄ Β·β πΆ) ββ (π΅ Β·β πΆ))) | ||
Theorem | hvdistr1i 30572 | Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (π΄ Β·β (π΅ +β πΆ)) = ((π΄ Β·β π΅) +β (π΄ Β·β πΆ)) | ||
Theorem | hvsubdistr1i 30573 | Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (π΄ Β·β (π΅ ββ πΆ)) = ((π΄ Β·β π΅) ββ (π΄ Β·β πΆ)) | ||
Theorem | hvassi 30574 | Hilbert vector space associative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ +β π΅) +β πΆ) = (π΄ +β (π΅ +β πΆ)) | ||
Theorem | hvadd32i 30575 | Hilbert vector space commutative/associative law. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ +β π΅) +β πΆ) = ((π΄ +β πΆ) +β π΅) | ||
Theorem | hvsubassi 30576 | 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 30577 | 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 30578 | Hilbert vector space commutative/associative law. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (π΄ +β (π΅ +β πΆ)) = (π΅ +β (π΄ +β πΆ)) | ||
Theorem | hvadd4i 30579 | Hilbert vector space addition law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β & β’ π· β β β β’ ((π΄ +β π΅) +β (πΆ +β π·)) = ((π΄ +β πΆ) +β (π΅ +β π·)) | ||
Theorem | hvsubsub4i 30580 | Hilbert vector space addition law. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β & β’ π· β β β β’ ((π΄ ββ π΅) ββ (πΆ ββ π·)) = ((π΄ ββ πΆ) ββ (π΅ ββ π·)) | ||
Theorem | hvsubsub4 30581 | Hilbert vector space addition/subtraction law. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ ββ π΅) ββ (πΆ ββ π·)) = ((π΄ ββ πΆ) ββ (π΅ ββ π·))) | ||
Theorem | hv2times 30582 | Two times a vector. (Contributed by NM, 22-Jun-2006.) (New usage is discouraged.) |
β’ (π΄ β β β (2 Β·β π΄) = (π΄ +β π΄)) | ||
Theorem | hvnegdii 30583 | Distribution of negative over subtraction. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (-1 Β·β (π΄ ββ π΅)) = (π΅ ββ π΄) | ||
Theorem | hvsubeq0i 30584 | If the difference between two vectors is zero, they are equal. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ ((π΄ ββ π΅) = 0β β π΄ = π΅) | ||
Theorem | hvsubcan2i 30585 | Vector cancellation law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ ((π΄ +β π΅) +β (π΄ ββ π΅)) = (2 Β·β π΄) | ||
Theorem | hvaddcani 30586 | Cancellation law for vector addition. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ +β π΅) = (π΄ +β πΆ) β π΅ = πΆ) | ||
Theorem | hvsubaddi 30587 | Relationship between vector subtraction and addition. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ ββ π΅) = πΆ β (π΅ +β πΆ) = π΄) | ||
Theorem | hvnegdi 30588 | Distribution of negative over subtraction. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (-1 Β·β (π΄ ββ π΅)) = (π΅ ββ π΄)) | ||
Theorem | hvsubeq0 30589 | If the difference between two vectors is zero, they are equal. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ ββ π΅) = 0β β π΄ = π΅)) | ||
Theorem | hvaddeq0 30590 | 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 30591 | Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ +β π΅) = (π΄ +β πΆ) β π΅ = πΆ)) | ||
Theorem | hvaddcan2 30592 | Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ +β πΆ) = (π΅ +β πΆ) β π΄ = π΅)) | ||
Theorem | hvmulcan 30593 | Cancellation law for scalar multiplication. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΄ β 0) β§ π΅ β β β§ πΆ β β) β ((π΄ Β·β π΅) = (π΄ Β·β πΆ) β π΅ = πΆ)) | ||
Theorem | hvmulcan2 30594 | Cancellation law for scalar multiplication. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ (πΆ β β β§ πΆ β 0β)) β ((π΄ Β·β πΆ) = (π΅ Β·β πΆ) β π΄ = π΅)) | ||
Theorem | hvsubcan 30595 | Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) = (π΄ ββ πΆ) β π΅ = πΆ)) | ||
Theorem | hvsubcan2 30596 | Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ πΆ) = (π΅ ββ πΆ) β π΄ = π΅)) | ||
Theorem | hvsub0 30597 | Subtraction of a zero vector. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.) |
β’ (π΄ β β β (π΄ ββ 0β) = π΄) | ||
Theorem | hvsubadd 30598 | Relationship between vector subtraction and addition. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) = πΆ β (π΅ +β πΆ) = π΄)) | ||
Theorem | hvaddsub4 30599 | Hilbert vector space addition/subtraction law. (Contributed by NM, 18-May-2005.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ +β π΅) = (πΆ +β π·) β (π΄ ββ πΆ) = (π· ββ π΅))) | ||
Axiom | ax-hfi 30600 | Inner product maps pairs from β to β. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
β’ Β·ih :( β Γ β)βΆβ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |