![]() |
Metamath
Proof Explorer Theorem List (p. 309 of 482) | < 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-30680) |
![]() (30681-32203) |
![]() (32204-48126) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hvpncan 30801 | Addition/subtraction cancellation law for vectors in Hilbert space. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ +β π΅) ββ π΅) = π΄) | ||
Theorem | hvpncan2 30802 | Addition/subtraction cancellation law for vectors in Hilbert space. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ +β π΅) ββ π΄) = π΅) | ||
Theorem | hvaddsubass 30803 | Associativity of sum and difference of Hilbert space vectors. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ +β π΅) ββ πΆ) = (π΄ +β (π΅ ββ πΆ))) | ||
Theorem | hvpncan3 30804 | Subtraction and addition of equal Hilbert space vectors. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ +β (π΅ ββ π΄)) = π΅) | ||
Theorem | hvmulcom 30805 | Scalar multiplication commutative law. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β·β (π΅ Β·β πΆ)) = (π΅ Β·β (π΄ Β·β πΆ))) | ||
Theorem | hvsubass 30806 | Hilbert vector space associative law for subtraction. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) ββ πΆ) = (π΄ ββ (π΅ +β πΆ))) | ||
Theorem | hvsub32 30807 | Hilbert vector space commutative/associative law. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) ββ πΆ) = ((π΄ ββ πΆ) ββ π΅)) | ||
Theorem | hvmulassi 30808 | Scalar multiplication associative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ Β· π΅) Β·β πΆ) = (π΄ Β·β (π΅ Β·β πΆ)) | ||
Theorem | hvmulcomi 30809 | Scalar multiplication commutative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (π΄ Β·β (π΅ Β·β πΆ)) = (π΅ Β·β (π΄ Β·β πΆ)) | ||
Theorem | hvmul2negi 30810 | Double negative in scalar multiplication. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (-π΄ Β·β (-π΅ Β·β πΆ)) = (π΄ Β·β (π΅ Β·β πΆ)) | ||
Theorem | hvsubdistr1 30811 | Scalar multiplication distributive law for subtraction. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β·β (π΅ ββ πΆ)) = ((π΄ Β·β π΅) ββ (π΄ Β·β πΆ))) | ||
Theorem | hvsubdistr2 30812 | Scalar multiplication distributive law for subtraction. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ β π΅) Β·β πΆ) = ((π΄ Β·β πΆ) ββ (π΅ Β·β πΆ))) | ||
Theorem | hvdistr1i 30813 | Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (π΄ Β·β (π΅ +β πΆ)) = ((π΄ Β·β π΅) +β (π΄ Β·β πΆ)) | ||
Theorem | hvsubdistr1i 30814 | Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (π΄ Β·β (π΅ ββ πΆ)) = ((π΄ Β·β π΅) ββ (π΄ Β·β πΆ)) | ||
Theorem | hvassi 30815 | Hilbert vector space associative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ +β π΅) +β πΆ) = (π΄ +β (π΅ +β πΆ)) | ||
Theorem | hvadd32i 30816 | Hilbert vector space commutative/associative law. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ +β π΅) +β πΆ) = ((π΄ +β πΆ) +β π΅) | ||
Theorem | hvsubassi 30817 | 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 30818 | 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 30819 | Hilbert vector space commutative/associative law. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (π΄ +β (π΅ +β πΆ)) = (π΅ +β (π΄ +β πΆ)) | ||
Theorem | hvadd4i 30820 | Hilbert vector space addition law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β & β’ π· β β β β’ ((π΄ +β π΅) +β (πΆ +β π·)) = ((π΄ +β πΆ) +β (π΅ +β π·)) | ||
Theorem | hvsubsub4i 30821 | Hilbert vector space addition law. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β & β’ π· β β β β’ ((π΄ ββ π΅) ββ (πΆ ββ π·)) = ((π΄ ββ πΆ) ββ (π΅ ββ π·)) | ||
Theorem | hvsubsub4 30822 | Hilbert vector space addition/subtraction law. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ ββ π΅) ββ (πΆ ββ π·)) = ((π΄ ββ πΆ) ββ (π΅ ββ π·))) | ||
Theorem | hv2times 30823 | Two times a vector. (Contributed by NM, 22-Jun-2006.) (New usage is discouraged.) |
β’ (π΄ β β β (2 Β·β π΄) = (π΄ +β π΄)) | ||
Theorem | hvnegdii 30824 | Distribution of negative over subtraction. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (-1 Β·β (π΄ ββ π΅)) = (π΅ ββ π΄) | ||
Theorem | hvsubeq0i 30825 | If the difference between two vectors is zero, they are equal. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ ((π΄ ββ π΅) = 0β β π΄ = π΅) | ||
Theorem | hvsubcan2i 30826 | Vector cancellation law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ ((π΄ +β π΅) +β (π΄ ββ π΅)) = (2 Β·β π΄) | ||
Theorem | hvaddcani 30827 | Cancellation law for vector addition. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ +β π΅) = (π΄ +β πΆ) β π΅ = πΆ) | ||
Theorem | hvsubaddi 30828 | Relationship between vector subtraction and addition. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((π΄ ββ π΅) = πΆ β (π΅ +β πΆ) = π΄) | ||
Theorem | hvnegdi 30829 | Distribution of negative over subtraction. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (-1 Β·β (π΄ ββ π΅)) = (π΅ ββ π΄)) | ||
Theorem | hvsubeq0 30830 | If the difference between two vectors is zero, they are equal. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ ββ π΅) = 0β β π΄ = π΅)) | ||
Theorem | hvaddeq0 30831 | 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 30832 | Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ +β π΅) = (π΄ +β πΆ) β π΅ = πΆ)) | ||
Theorem | hvaddcan2 30833 | Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ +β πΆ) = (π΅ +β πΆ) β π΄ = π΅)) | ||
Theorem | hvmulcan 30834 | Cancellation law for scalar multiplication. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΄ β 0) β§ π΅ β β β§ πΆ β β) β ((π΄ Β·β π΅) = (π΄ Β·β πΆ) β π΅ = πΆ)) | ||
Theorem | hvmulcan2 30835 | Cancellation law for scalar multiplication. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ (πΆ β β β§ πΆ β 0β)) β ((π΄ Β·β πΆ) = (π΅ Β·β πΆ) β π΄ = π΅)) | ||
Theorem | hvsubcan 30836 | Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) = (π΄ ββ πΆ) β π΅ = πΆ)) | ||
Theorem | hvsubcan2 30837 | Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ πΆ) = (π΅ ββ πΆ) β π΄ = π΅)) | ||
Theorem | hvsub0 30838 | Subtraction of a zero vector. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.) |
β’ (π΄ β β β (π΄ ββ 0β) = π΄) | ||
Theorem | hvsubadd 30839 | Relationship between vector subtraction and addition. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) = πΆ β (π΅ +β πΆ) = π΄)) | ||
Theorem | hvaddsub4 30840 | Hilbert vector space addition/subtraction law. (Contributed by NM, 18-May-2005.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ +β π΅) = (πΆ +β π·) β (π΄ ββ πΆ) = (π· ββ π΅))) | ||
Axiom | ax-hfi 30841 | Inner product maps pairs from β to β. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
β’ Β·ih :( β Γ β)βΆβ | ||
Theorem | hicl 30842 | Closure of inner product. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ Β·ih π΅) β β) | ||
Theorem | hicli 30843 | Closure inference for inner product. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ Β·ih π΅) β β | ||
Axiom | ax-his1 30844 | Conjugate law for inner product. Postulate (S1) of [Beran] p. 95. Note that ββπ₯ is the complex conjugate cjval 15055 of π₯. In the literature, the inner product of π΄ and π΅ is usually written β¨π΄, π΅β©, but our operation notation co 7405 allows to use existing theorems about operations and also avoids a clash with the definition of an ordered pair df-op 4630. Physicists use β¨π΅ β£ π΄β©, called Dirac bra-ket notation, to represent this operation; see comments in df-bra 31612. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ Β·ih π΅) = (ββ(π΅ Β·ih π΄))) | ||
Axiom | ax-his2 30845 | Distributive law for inner product. Postulate (S2) of [Beran] p. 95. (Contributed by NM, 31-Jul-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ +β π΅) Β·ih πΆ) = ((π΄ Β·ih πΆ) + (π΅ Β·ih πΆ))) | ||
Axiom | ax-his3 30846 | Associative law for inner product. Postulate (S3) of [Beran] p. 95. Warning: Mathematics textbooks usually use our version of the axiom. Physics textbooks, on the other hand, usually replace the left-hand side with (π΅ Β·ih (π΄ Β·β πΆ)) (e.g., Equation 1.21b of [Hughes] p. 44; Definition (iii) of [ReedSimon] p. 36). See the comments in df-bra 31612 for why the physics definition is swapped. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ Β·β π΅) Β·ih πΆ) = (π΄ Β· (π΅ Β·ih πΆ))) | ||
Axiom | ax-his4 30847 | Identity law for inner product. Postulate (S4) of [Beran] p. 95. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΄ β 0β) β 0 < (π΄ Β·ih π΄)) | ||
Theorem | his5 30848 | Associative law for inner product. Lemma 3.1(S5) of [Beran] p. 95. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΅ Β·ih (π΄ Β·β πΆ)) = ((ββπ΄) Β· (π΅ Β·ih πΆ))) | ||
Theorem | his52 30849 | Associative law for inner product. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΅ Β·ih ((ββπ΄) Β·β πΆ)) = (π΄ Β· (π΅ Β·ih πΆ))) | ||
Theorem | his35 30850 | Move scalar multiplication to outside of inner product. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ Β·β πΆ) Β·ih (π΅ Β·β π·)) = ((π΄ Β· (ββπ΅)) Β· (πΆ Β·ih π·))) | ||
Theorem | his35i 30851 | Move scalar multiplication to outside of inner product. (Contributed by NM, 1-Jul-2005.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β & β’ π· β β β β’ ((π΄ Β·β πΆ) Β·ih (π΅ Β·β π·)) = ((π΄ Β· (ββπ΅)) Β· (πΆ Β·ih π·)) | ||
Theorem | his7 30852 | Distributive law for inner product. Lemma 3.1(S7) of [Beran] p. 95. (Contributed by NM, 31-Jul-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β·ih (π΅ +β πΆ)) = ((π΄ Β·ih π΅) + (π΄ Β·ih πΆ))) | ||
Theorem | hiassdi 30853 | Distributive/associative law for inner product, useful for linearity proofs. (Contributed by NM, 10-May-2005.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β (((π΄ Β·β π΅) +β πΆ) Β·ih π·) = ((π΄ Β· (π΅ Β·ih π·)) + (πΆ Β·ih π·))) | ||
Theorem | his2sub 30854 | Distributive law for inner product of vector subtraction. (Contributed by NM, 16-Nov-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) Β·ih πΆ) = ((π΄ Β·ih πΆ) β (π΅ Β·ih πΆ))) | ||
Theorem | his2sub2 30855 | Distributive law for inner product of vector subtraction. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β·ih (π΅ ββ πΆ)) = ((π΄ Β·ih π΅) β (π΄ Β·ih πΆ))) | ||
Theorem | hire 30856 | A necessary and sufficient condition for an inner product to be real. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ Β·ih π΅) β β β (π΄ Β·ih π΅) = (π΅ Β·ih π΄))) | ||
Theorem | hiidrcl 30857 | Real closure of inner product with self. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (π΄ Β·ih π΄) β β) | ||
Theorem | hi01 30858 | Inner product with the 0 vector. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (0β Β·ih π΄) = 0) | ||
Theorem | hi02 30859 | Inner product with the 0 vector. (Contributed by NM, 13-Oct-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (π΄ Β·ih 0β) = 0) | ||
Theorem | hiidge0 30860 | Inner product with self is not negative. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
β’ (π΄ β β β 0 β€ (π΄ Β·ih π΄)) | ||
Theorem | his6 30861 | Zero inner product with self means vector is zero. Lemma 3.1(S6) of [Beran] p. 95. (Contributed by NM, 27-Jul-1999.) (New usage is discouraged.) |
β’ (π΄ β β β ((π΄ Β·ih π΄) = 0 β π΄ = 0β)) | ||
Theorem | his1i 30862 | Conjugate law for inner product. Postulate (S1) of [Beran] p. 95. (Contributed by NM, 15-May-2005.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ Β·ih π΅) = (ββ(π΅ Β·ih π΄)) | ||
Theorem | abshicom 30863 | Commuted inner products have the same absolute values. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (absβ(π΄ Β·ih π΅)) = (absβ(π΅ Β·ih π΄))) | ||
Theorem | hial0 30864* | A vector whose inner product is always zero is zero. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (βπ₯ β β (π΄ Β·ih π₯) = 0 β π΄ = 0β)) | ||
Theorem | hial02 30865* | A vector whose inner product is always zero is zero. (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.) |
β’ (π΄ β β β (βπ₯ β β (π₯ Β·ih π΄) = 0 β π΄ = 0β)) | ||
Theorem | hisubcomi 30866 | Two vector subtractions simultaneously commute in an inner product. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β & β’ π· β β β β’ ((π΄ ββ π΅) Β·ih (πΆ ββ π·)) = ((π΅ ββ π΄) Β·ih (π· ββ πΆ)) | ||
Theorem | hi2eq 30867 | Lemma used to prove equality of vectors. (Contributed by NM, 16-Nov-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ Β·ih (π΄ ββ π΅)) = (π΅ Β·ih (π΄ ββ π΅)) β π΄ = π΅)) | ||
Theorem | hial2eq 30868* | Two vectors whose inner product is always equal are equal. (Contributed by NM, 16-Nov-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (βπ₯ β β (π΄ Β·ih π₯) = (π΅ Β·ih π₯) β π΄ = π΅)) | ||
Theorem | hial2eq2 30869* | Two vectors whose inner product is always equal are equal. (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (βπ₯ β β (π₯ Β·ih π΄) = (π₯ Β·ih π΅) β π΄ = π΅)) | ||
Theorem | orthcom 30870 | Orthogonality commutes. (Contributed by NM, 10-Oct-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ Β·ih π΅) = 0 β (π΅ Β·ih π΄) = 0)) | ||
Theorem | normlem0 30871 | Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 7-Oct-1999.) (New usage is discouraged.) |
β’ π β β & β’ πΉ β β & β’ πΊ β β β β’ ((πΉ ββ (π Β·β πΊ)) Β·ih (πΉ ββ (π Β·β πΊ))) = (((πΉ Β·ih πΉ) + (-(ββπ) Β· (πΉ Β·ih πΊ))) + ((-π Β· (πΊ Β·ih πΉ)) + ((π Β· (ββπ)) Β· (πΊ Β·ih πΊ)))) | ||
Theorem | normlem1 30872 | Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 22-Aug-1999.) (New usage is discouraged.) |
β’ π β β & β’ πΉ β β & β’ πΊ β β & β’ π β β & β’ (absβπ) = 1 β β’ ((πΉ ββ ((π Β· π ) Β·β πΊ)) Β·ih (πΉ ββ ((π Β· π ) Β·β πΊ))) = (((πΉ Β·ih πΉ) + (((ββπ) Β· -π ) Β· (πΉ Β·ih πΊ))) + (((π Β· -π ) Β· (πΊ Β·ih πΉ)) + ((π β2) Β· (πΊ Β·ih πΊ)))) | ||
Theorem | normlem2 30873 | Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 27-Jul-1999.) (New usage is discouraged.) |
β’ π β β & β’ πΉ β β & β’ πΊ β β & β’ π΅ = -(((ββπ) Β· (πΉ Β·ih πΊ)) + (π Β· (πΊ Β·ih πΉ))) β β’ π΅ β β | ||
Theorem | normlem3 30874 | Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 21-Aug-1999.) (New usage is discouraged.) |
β’ π β β & β’ πΉ β β & β’ πΊ β β & β’ π΅ = -(((ββπ) Β· (πΉ Β·ih πΊ)) + (π Β· (πΊ Β·ih πΉ))) & β’ π΄ = (πΊ Β·ih πΊ) & β’ πΆ = (πΉ Β·ih πΉ) & β’ π β β β β’ (((π΄ Β· (π β2)) + (π΅ Β· π )) + πΆ) = (((πΉ Β·ih πΉ) + (((ββπ) Β· -π ) Β· (πΉ Β·ih πΊ))) + (((π Β· -π ) Β· (πΊ Β·ih πΉ)) + ((π β2) Β· (πΊ Β·ih πΊ)))) | ||
Theorem | normlem4 30875 | Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.) |
β’ π β β & β’ πΉ β β & β’ πΊ β β & β’ π΅ = -(((ββπ) Β· (πΉ Β·ih πΊ)) + (π Β· (πΊ Β·ih πΉ))) & β’ π΄ = (πΊ Β·ih πΊ) & β’ πΆ = (πΉ Β·ih πΉ) & β’ π β β & β’ (absβπ) = 1 β β’ ((πΉ ββ ((π Β· π ) Β·β πΊ)) Β·ih (πΉ ββ ((π Β· π ) Β·β πΊ))) = (((π΄ Β· (π β2)) + (π΅ Β· π )) + πΆ) | ||
Theorem | normlem5 30876 | Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 10-Aug-1999.) (New usage is discouraged.) |
β’ π β β & β’ πΉ β β & β’ πΊ β β & β’ π΅ = -(((ββπ) Β· (πΉ Β·ih πΊ)) + (π Β· (πΊ Β·ih πΉ))) & β’ π΄ = (πΊ Β·ih πΊ) & β’ πΆ = (πΉ Β·ih πΉ) & β’ π β β & β’ (absβπ) = 1 β β’ 0 β€ (((π΄ Β· (π β2)) + (π΅ Β· π )) + πΆ) | ||
Theorem | normlem6 30877 | Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 2-Aug-1999.) (Revised by Mario Carneiro, 4-Jun-2014.) (New usage is discouraged.) |
β’ π β β & β’ πΉ β β & β’ πΊ β β & β’ π΅ = -(((ββπ) Β· (πΉ Β·ih πΊ)) + (π Β· (πΊ Β·ih πΉ))) & β’ π΄ = (πΊ Β·ih πΊ) & β’ πΆ = (πΉ Β·ih πΉ) & β’ (absβπ) = 1 β β’ (absβπ΅) β€ (2 Β· ((ββπ΄) Β· (ββπΆ))) | ||
Theorem | normlem7 30878 | Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 11-Aug-1999.) (New usage is discouraged.) |
β’ π β β & β’ πΉ β β & β’ πΊ β β & β’ (absβπ) = 1 β β’ (((ββπ) Β· (πΉ Β·ih πΊ)) + (π Β· (πΊ Β·ih πΉ))) β€ (2 Β· ((ββ(πΊ Β·ih πΊ)) Β· (ββ(πΉ Β·ih πΉ)))) | ||
Theorem | normlem8 30879 | Lemma used to derive properties of norm. (Contributed by NM, 30-Jun-2005.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β & β’ π· β β β β’ ((π΄ +β π΅) Β·ih (πΆ +β π·)) = (((π΄ Β·ih πΆ) + (π΅ Β·ih π·)) + ((π΄ Β·ih π·) + (π΅ Β·ih πΆ))) | ||
Theorem | normlem9 30880 | Lemma used to derive properties of norm. (Contributed by NM, 30-Jun-2005.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β & β’ π· β β β β’ ((π΄ ββ π΅) Β·ih (πΆ ββ π·)) = (((π΄ Β·ih πΆ) + (π΅ Β·ih π·)) β ((π΄ Β·ih π·) + (π΅ Β·ih πΆ))) | ||
Theorem | normlem7tALT 30881 | Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ ((π β β β§ (absβπ) = 1) β (((ββπ) Β· (π΄ Β·ih π΅)) + (π Β· (π΅ Β·ih π΄))) β€ (2 Β· ((ββ(π΅ Β·ih π΅)) Β· (ββ(π΄ Β·ih π΄))))) | ||
Theorem | bcseqi 30882 | Equality case of Bunjakovaskij-Cauchy-Schwarz inequality. Specifically, in the equality case the two vectors are collinear. Compare bcsiHIL 30942. (Contributed by NM, 16-Jul-2001.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (((π΄ Β·ih π΅) Β· (π΅ Β·ih π΄)) = ((π΄ Β·ih π΄) Β· (π΅ Β·ih π΅)) β ((π΅ Β·ih π΅) Β·β π΄) = ((π΄ Β·ih π΅) Β·β π΅)) | ||
Theorem | normlem9at 30883 | Lemma used to derive properties of norm. Part of Remark 3.4(B) of [Beran] p. 98. (Contributed by NM, 10-May-2005.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ ββ π΅) Β·ih (π΄ ββ π΅)) = (((π΄ Β·ih π΄) + (π΅ Β·ih π΅)) β ((π΄ Β·ih π΅) + (π΅ Β·ih π΄)))) | ||
Theorem | dfhnorm2 30884 | Alternate definition of the norm of a vector of Hilbert space. Definition of norm in [Beran] p. 96. (Contributed by NM, 6-Jun-2008.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
β’ normβ = (π₯ β β β¦ (ββ(π₯ Β·ih π₯))) | ||
Theorem | normf 30885 | The norm function maps from Hilbert space to reals. (Contributed by NM, 6-Sep-2007.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
β’ normβ: ββΆβ | ||
Theorem | normval 30886 | The value of the norm of a vector in Hilbert space. Definition of norm in [Beran] p. 96. In the literature, the norm of π΄ is usually written as "|| π΄ ||", but we use function value notation to take advantage of our existing theorems about functions. (Contributed by NM, 29-May-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ (π΄ β β β (normββπ΄) = (ββ(π΄ Β·ih π΄))) | ||
Theorem | normcl 30887 | Real closure of the norm of a vector. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
β’ (π΄ β β β (normββπ΄) β β) | ||
Theorem | normge0 30888 | The norm of a vector is nonnegative. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
β’ (π΄ β β β 0 β€ (normββπ΄)) | ||
Theorem | normgt0 30889 | The norm of nonzero vector is positive. (Contributed by NM, 10-Apr-2006.) (New usage is discouraged.) |
β’ (π΄ β β β (π΄ β 0β β 0 < (normββπ΄))) | ||
Theorem | norm0 30890 | The norm of a zero vector. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
β’ (normββ0β) = 0 | ||
Theorem | norm-i 30891 | Theorem 3.3(i) of [Beran] p. 97. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.) |
β’ (π΄ β β β ((normββπ΄) = 0 β π΄ = 0β)) | ||
Theorem | normne0 30892 | A norm is nonzero iff its argument is a nonzero vector. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
β’ (π΄ β β β ((normββπ΄) β 0 β π΄ β 0β)) | ||
Theorem | normcli 30893 | Real closure of the norm of a vector. (Contributed by NM, 30-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β β β’ (normββπ΄) β β | ||
Theorem | normsqi 30894 | The square of a norm. (Contributed by NM, 21-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β β β’ ((normββπ΄)β2) = (π΄ Β·ih π΄) | ||
Theorem | norm-i-i 30895 | Theorem 3.3(i) of [Beran] p. 97. (Contributed by NM, 5-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β β β β’ ((normββπ΄) = 0 β π΄ = 0β) | ||
Theorem | normsq 30896 | The square of a norm. (Contributed by NM, 12-May-2005.) (New usage is discouraged.) |
β’ (π΄ β β β ((normββπ΄)β2) = (π΄ Β·ih π΄)) | ||
Theorem | normsub0i 30897 | Two vectors are equal iff the norm of their difference is zero. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ ((normββ(π΄ ββ π΅)) = 0 β π΄ = π΅) | ||
Theorem | normsub0 30898 | Two vectors are equal iff the norm of their difference is zero. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β ((normββ(π΄ ββ π΅)) = 0 β π΄ = π΅)) | ||
Theorem | norm-ii-i 30899 | Triangle inequality for norms. Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 11-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (normββ(π΄ +β π΅)) β€ ((normββπ΄) + (normββπ΅)) | ||
Theorem | norm-ii 30900 | Triangle inequality for norms. Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (normββ(π΄ +β π΅)) β€ ((normββπ΄) + (normββπ΅))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |