![]() |
Metamath
Proof Explorer Theorem List (p. 307 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hicli 30601 | Closure inference for inner product. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ด ยทih ๐ต) โ โ | ||
Axiom | ax-his1 30602 | Conjugate law for inner product. Postulate (S1) of [Beran] p. 95. Note that โโ๐ฅ is the complex conjugate cjval 15053 of ๐ฅ. In the literature, the inner product of ๐ด and ๐ต is usually written โจ๐ด, ๐ตโฉ, but our operation notation co 7411 allows to use existing theorems about operations and also avoids a clash with the definition of an ordered pair df-op 4634. Physicists use โจ๐ต โฃ ๐ดโฉ, called Dirac bra-ket notation, to represent this operation; see comments in df-bra 31370. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยทih ๐ต) = (โโ(๐ต ยทih ๐ด))) | ||
Axiom | ax-his2 30603 | 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 30604 | 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 31370 for why the physics definition is swapped. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด ยทโ ๐ต) ยทih ๐ถ) = (๐ด ยท (๐ต ยทih ๐ถ))) | ||
Axiom | ax-his4 30605 | 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 30606 | 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 30607 | Associative law for inner product. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ต ยทih ((โโ๐ด) ยทโ ๐ถ)) = (๐ด ยท (๐ต ยทih ๐ถ))) | ||
Theorem | his35 30608 | Move scalar multiplication to outside of inner product. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด ยทโ ๐ถ) ยทih (๐ต ยทโ ๐ท)) = ((๐ด ยท (โโ๐ต)) ยท (๐ถ ยทih ๐ท))) | ||
Theorem | his35i 30609 | 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 30610 | 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 30611 | 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 30612 | Distributive law for inner product of vector subtraction. (Contributed by NM, 16-Nov-1999.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด โโ ๐ต) ยทih ๐ถ) = ((๐ด ยทih ๐ถ) โ (๐ต ยทih ๐ถ))) | ||
Theorem | his2sub2 30613 | Distributive law for inner product of vector subtraction. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด ยทih (๐ต โโ ๐ถ)) = ((๐ด ยทih ๐ต) โ (๐ด ยทih ๐ถ))) | ||
Theorem | hire 30614 | 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 30615 | Real closure of inner product with self. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
โข (๐ด โ โ โ (๐ด ยทih ๐ด) โ โ) | ||
Theorem | hi01 30616 | Inner product with the 0 vector. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
โข (๐ด โ โ โ (0โ ยทih ๐ด) = 0) | ||
Theorem | hi02 30617 | Inner product with the 0 vector. (Contributed by NM, 13-Oct-1999.) (New usage is discouraged.) |
โข (๐ด โ โ โ (๐ด ยทih 0โ) = 0) | ||
Theorem | hiidge0 30618 | Inner product with self is not negative. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
โข (๐ด โ โ โ 0 โค (๐ด ยทih ๐ด)) | ||
Theorem | his6 30619 | 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 30620 | 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 30621 | Commuted inner products have the same absolute values. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (absโ(๐ด ยทih ๐ต)) = (absโ(๐ต ยทih ๐ด))) | ||
Theorem | hial0 30622* | 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 30623* | 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 30624 | Two vector subtractions simultaneously commute in an inner product. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ & โข ๐ท โ โ โ โข ((๐ด โโ ๐ต) ยทih (๐ถ โโ ๐ท)) = ((๐ต โโ ๐ด) ยทih (๐ท โโ ๐ถ)) | ||
Theorem | hi2eq 30625 | Lemma used to prove equality of vectors. (Contributed by NM, 16-Nov-1999.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด ยทih (๐ด โโ ๐ต)) = (๐ต ยทih (๐ด โโ ๐ต)) โ ๐ด = ๐ต)) | ||
Theorem | hial2eq 30626* | Two vectors whose inner product is always equal are equal. (Contributed by NM, 16-Nov-1999.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (โ๐ฅ โ โ (๐ด ยทih ๐ฅ) = (๐ต ยทih ๐ฅ) โ ๐ด = ๐ต)) | ||
Theorem | hial2eq2 30627* | Two vectors whose inner product is always equal are equal. (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (โ๐ฅ โ โ (๐ฅ ยทih ๐ด) = (๐ฅ ยทih ๐ต) โ ๐ด = ๐ต)) | ||
Theorem | orthcom 30628 | Orthogonality commutes. (Contributed by NM, 10-Oct-1999.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด ยทih ๐ต) = 0 โ (๐ต ยทih ๐ด) = 0)) | ||
Theorem | normlem0 30629 | 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 30630 | 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 30631 | 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 30632 | 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 30633 | 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 30634 | 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 30635 | 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 30636 | 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 30637 | Lemma used to derive properties of norm. (Contributed by NM, 30-Jun-2005.) (New usage is discouraged.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ & โข ๐ท โ โ โ โข ((๐ด +โ ๐ต) ยทih (๐ถ +โ ๐ท)) = (((๐ด ยทih ๐ถ) + (๐ต ยทih ๐ท)) + ((๐ด ยทih ๐ท) + (๐ต ยทih ๐ถ))) | ||
Theorem | normlem9 30638 | Lemma used to derive properties of norm. (Contributed by NM, 30-Jun-2005.) (New usage is discouraged.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ & โข ๐ท โ โ โ โข ((๐ด โโ ๐ต) ยทih (๐ถ โโ ๐ท)) = (((๐ด ยทih ๐ถ) + (๐ต ยทih ๐ท)) โ ((๐ด ยทih ๐ท) + (๐ต ยทih ๐ถ))) | ||
Theorem | normlem7tALT 30639 | 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 30640 | Equality case of Bunjakovaskij-Cauchy-Schwarz inequality. Specifically, in the equality case the two vectors are collinear. Compare bcsiHIL 30700. (Contributed by NM, 16-Jul-2001.) (New usage is discouraged.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (((๐ด ยทih ๐ต) ยท (๐ต ยทih ๐ด)) = ((๐ด ยทih ๐ด) ยท (๐ต ยทih ๐ต)) โ ((๐ต ยทih ๐ต) ยทโ ๐ด) = ((๐ด ยทih ๐ต) ยทโ ๐ต)) | ||
Theorem | normlem9at 30641 | 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 30642 | 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 30643 | 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 30644 | 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 30645 | Real closure of the norm of a vector. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
โข (๐ด โ โ โ (normโโ๐ด) โ โ) | ||
Theorem | normge0 30646 | The norm of a vector is nonnegative. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
โข (๐ด โ โ โ 0 โค (normโโ๐ด)) | ||
Theorem | normgt0 30647 | The norm of nonzero vector is positive. (Contributed by NM, 10-Apr-2006.) (New usage is discouraged.) |
โข (๐ด โ โ โ (๐ด โ 0โ โ 0 < (normโโ๐ด))) | ||
Theorem | norm0 30648 | The norm of a zero vector. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
โข (normโโ0โ) = 0 | ||
Theorem | norm-i 30649 | Theorem 3.3(i) of [Beran] p. 97. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.) |
โข (๐ด โ โ โ ((normโโ๐ด) = 0 โ ๐ด = 0โ)) | ||
Theorem | normne0 30650 | 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 30651 | Real closure of the norm of a vector. (Contributed by NM, 30-Sep-1999.) (New usage is discouraged.) |
โข ๐ด โ โ โ โข (normโโ๐ด) โ โ | ||
Theorem | normsqi 30652 | The square of a norm. (Contributed by NM, 21-Aug-1999.) (New usage is discouraged.) |
โข ๐ด โ โ โ โข ((normโโ๐ด)โ2) = (๐ด ยทih ๐ด) | ||
Theorem | norm-i-i 30653 | Theorem 3.3(i) of [Beran] p. 97. (Contributed by NM, 5-Sep-1999.) (New usage is discouraged.) |
โข ๐ด โ โ โ โข ((normโโ๐ด) = 0 โ ๐ด = 0โ) | ||
Theorem | normsq 30654 | The square of a norm. (Contributed by NM, 12-May-2005.) (New usage is discouraged.) |
โข (๐ด โ โ โ ((normโโ๐ด)โ2) = (๐ด ยทih ๐ด)) | ||
Theorem | normsub0i 30655 | 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 30656 | 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 30657 | 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 30658 | 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โโ๐ต))) | ||
Theorem | norm-iii-i 30659 | Theorem 3.3(iii) of [Beran] p. 97. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (normโโ(๐ด ยทโ ๐ต)) = ((absโ๐ด) ยท (normโโ๐ต)) | ||
Theorem | norm-iii 30660 | Theorem 3.3(iii) of [Beran] p. 97. (Contributed by NM, 25-Oct-1999.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (normโโ(๐ด ยทโ ๐ต)) = ((absโ๐ด) ยท (normโโ๐ต))) | ||
Theorem | normsubi 30661 | Negative doesn't change the norm of a Hilbert space vector. (Contributed by NM, 11-Aug-1999.) (New usage is discouraged.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (normโโ(๐ด โโ ๐ต)) = (normโโ(๐ต โโ ๐ด)) | ||
Theorem | normpythi 30662 | Analogy to Pythagorean theorem for orthogonal vectors. Remark 3.4(C) of [Beran] p. 98. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((๐ด ยทih ๐ต) = 0 โ ((normโโ(๐ด +โ ๐ต))โ2) = (((normโโ๐ด)โ2) + ((normโโ๐ต)โ2))) | ||
Theorem | normsub 30663 | Swapping order of subtraction doesn't change the norm of a vector. (Contributed by NM, 14-Aug-1999.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (normโโ(๐ด โโ ๐ต)) = (normโโ(๐ต โโ ๐ด))) | ||
Theorem | normneg 30664 | The norm of a vector equals the norm of its negative. (Contributed by NM, 23-May-2005.) (New usage is discouraged.) |
โข (๐ด โ โ โ (normโโ(-1 ยทโ ๐ด)) = (normโโ๐ด)) | ||
Theorem | normpyth 30665 | Analogy to Pythagorean theorem for orthogonal vectors. Remark 3.4(C) of [Beran] p. 98. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด ยทih ๐ต) = 0 โ ((normโโ(๐ด +โ ๐ต))โ2) = (((normโโ๐ด)โ2) + ((normโโ๐ต)โ2)))) | ||
Theorem | normpyc 30666 | Corollary to Pythagorean theorem for orthogonal vectors. Remark 3.4(C) of [Beran] p. 98. (Contributed by NM, 26-Oct-1999.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด ยทih ๐ต) = 0 โ (normโโ๐ด) โค (normโโ(๐ด +โ ๐ต)))) | ||
Theorem | norm3difi 30667 | Norm of differences around common element. Part of Lemma 3.6 of [Beran] p. 101. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข (normโโ(๐ด โโ ๐ต)) โค ((normโโ(๐ด โโ ๐ถ)) + (normโโ(๐ถ โโ ๐ต))) | ||
Theorem | norm3adifii 30668 | Norm of differences around common element. Part of Lemma 3.6 of [Beran] p. 101. (Contributed by NM, 30-Sep-1999.) (New usage is discouraged.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข (absโ((normโโ(๐ด โโ ๐ถ)) โ (normโโ(๐ต โโ ๐ถ)))) โค (normโโ(๐ด โโ ๐ต)) | ||
Theorem | norm3lem 30669 | Lemma involving norm of differences in Hilbert space. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ & โข ๐ท โ โ โ โข (((normโโ(๐ด โโ ๐ถ)) < (๐ท / 2) โง (normโโ(๐ถ โโ ๐ต)) < (๐ท / 2)) โ (normโโ(๐ด โโ ๐ต)) < ๐ท) | ||
Theorem | norm3dif 30670 | Norm of differences around common element. Part of Lemma 3.6 of [Beran] p. 101. (Contributed by NM, 20-Apr-2006.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (normโโ(๐ด โโ ๐ต)) โค ((normโโ(๐ด โโ ๐ถ)) + (normโโ(๐ถ โโ ๐ต)))) | ||
Theorem | norm3dif2 30671 | Norm of differences around common element. (Contributed by NM, 18-Apr-2007.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (normโโ(๐ด โโ ๐ต)) โค ((normโโ(๐ถ โโ ๐ด)) + (normโโ(๐ถ โโ ๐ต)))) | ||
Theorem | norm3lemt 30672 | Lemma involving norm of differences in Hilbert space. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ (((normโโ(๐ด โโ ๐ถ)) < (๐ท / 2) โง (normโโ(๐ถ โโ ๐ต)) < (๐ท / 2)) โ (normโโ(๐ด โโ ๐ต)) < ๐ท)) | ||
Theorem | norm3adifi 30673 | Norm of differences around common element. Part of Lemma 3.6 of [Beran] p. 101. (Contributed by NM, 3-Oct-1999.) (New usage is discouraged.) |
โข ๐ถ โ โ โ โข ((๐ด โ โ โง ๐ต โ โ) โ (absโ((normโโ(๐ด โโ ๐ถ)) โ (normโโ(๐ต โโ ๐ถ)))) โค (normโโ(๐ด โโ ๐ต))) | ||
Theorem | normpari 30674 | Parallelogram law for norms. Remark 3.4(B) of [Beran] p. 98. (Contributed by NM, 21-Aug-1999.) (New usage is discouraged.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (((normโโ(๐ด โโ ๐ต))โ2) + ((normโโ(๐ด +โ ๐ต))โ2)) = ((2 ยท ((normโโ๐ด)โ2)) + (2 ยท ((normโโ๐ต)โ2))) | ||
Theorem | normpar 30675 | Parallelogram law for norms. Remark 3.4(B) of [Beran] p. 98. (Contributed by NM, 15-Apr-2007.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (((normโโ(๐ด โโ ๐ต))โ2) + ((normโโ(๐ด +โ ๐ต))โ2)) = ((2 ยท ((normโโ๐ด)โ2)) + (2 ยท ((normโโ๐ต)โ2)))) | ||
Theorem | normpar2i 30676 | Corollary of parallelogram law for norms. Part of Lemma 3.6 of [Beran] p. 100. (Contributed by NM, 5-Oct-1999.) (New usage is discouraged.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข ((normโโ(๐ด โโ ๐ต))โ2) = (((2 ยท ((normโโ(๐ด โโ ๐ถ))โ2)) + (2 ยท ((normโโ(๐ต โโ ๐ถ))โ2))) โ ((normโโ((๐ด +โ ๐ต) โโ (2 ยทโ ๐ถ)))โ2)) | ||
Theorem | polid2i 30677 | Generalized polarization identity. Generalization of Exercise 4(a) of [ReedSimon] p. 63. (Contributed by NM, 30-Jun-2005.) (New usage is discouraged.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ & โข ๐ท โ โ โ โข (๐ด ยทih ๐ต) = (((((๐ด +โ ๐ถ) ยทih (๐ท +โ ๐ต)) โ ((๐ด โโ ๐ถ) ยทih (๐ท โโ ๐ต))) + (i ยท (((๐ด +โ (i ยทโ ๐ถ)) ยทih (๐ท +โ (i ยทโ ๐ต))) โ ((๐ด โโ (i ยทโ ๐ถ)) ยทih (๐ท โโ (i ยทโ ๐ต)))))) / 4) | ||
Theorem | polidi 30678 | Polarization identity. Recovers inner product from norm. Exercise 4(a) of [ReedSimon] p. 63. The outermost operation is + instead of - due to our mathematicians' (rather than physicists') version of Axiom ax-his3 30604. (Contributed by NM, 30-Jun-2005.) (New usage is discouraged.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ด ยทih ๐ต) = (((((normโโ(๐ด +โ ๐ต))โ2) โ ((normโโ(๐ด โโ ๐ต))โ2)) + (i ยท (((normโโ(๐ด +โ (i ยทโ ๐ต)))โ2) โ ((normโโ(๐ด โโ (i ยทโ ๐ต)))โ2)))) / 4) | ||
Theorem | polid 30679 | Polarization identity. Recovers inner product from norm. Exercise 4(a) of [ReedSimon] p. 63. The outermost operation is + instead of - due to our mathematicians' (rather than physicists') version of Axiom ax-his3 30604. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยทih ๐ต) = (((((normโโ(๐ด +โ ๐ต))โ2) โ ((normโโ(๐ด โโ ๐ต))โ2)) + (i ยท (((normโโ(๐ด +โ (i ยทโ ๐ต)))โ2) โ ((normโโ(๐ด โโ (i ยทโ ๐ต)))โ2)))) / 4)) | ||
Theorem | hilablo 30680 | Hilbert space vector addition is an Abelian group operation. (Contributed by NM, 15-Apr-2007.) (New usage is discouraged.) |
โข +โ โ AbelOp | ||
Theorem | hilid 30681 | The group identity element of Hilbert space vector addition is the zero vector. (Contributed by NM, 16-Apr-2007.) (New usage is discouraged.) |
โข (GIdโ +โ ) = 0โ | ||
Theorem | hilvc 30682 | Hilbert space is a complex vector space. Vector addition is +โ, and scalar product is ยทโ. (Contributed by NM, 15-Apr-2007.) (New usage is discouraged.) |
โข โจ +โ , ยทโ โฉ โ CVecOLD | ||
Theorem | hilnormi 30683 | Hilbert space norm in terms of vector space norm. (Contributed by NM, 11-Sep-2007.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
โข โ = (BaseSetโ๐) & โข ยทih = (ยท๐OLDโ๐) & โข ๐ โ NrmCVec โ โข normโ = (normCVโ๐) | ||
Theorem | hilhhi 30684 | Deduce the structure of Hilbert space from its components. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
โข โ = (BaseSetโ๐) & โข +โ = ( +๐ฃ โ๐) & โข ยทโ = ( ยท๐ OLD โ๐) & โข ยทih = (ยท๐OLDโ๐) & โข ๐ โ NrmCVec โ โข ๐ = โจโจ +โ , ยทโ โฉ, normโโฉ | ||
Theorem | hhnv 30685 | Hilbert space is a normed complex vector space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
โข ๐ = โจโจ +โ , ยทโ โฉ, normโโฉ โ โข ๐ โ NrmCVec | ||
Theorem | hhva 30686 | The group (addition) operation of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
โข ๐ = โจโจ +โ , ยทโ โฉ, normโโฉ โ โข +โ = ( +๐ฃ โ๐) | ||
Theorem | hhba 30687 | The base set of Hilbert space. This theorem provides an independent proof of df-hba 30489 (see comments in that definition). (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
โข ๐ = โจโจ +โ , ยทโ โฉ, normโโฉ โ โข โ = (BaseSetโ๐) | ||
Theorem | hh0v 30688 | The zero vector of Hilbert space. (Contributed by NM, 17-Nov-2007.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
โข ๐ = โจโจ +โ , ยทโ โฉ, normโโฉ โ โข 0โ = (0vecโ๐) | ||
Theorem | hhsm 30689 | The scalar product operation of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
โข ๐ = โจโจ +โ , ยทโ โฉ, normโโฉ โ โข ยทโ = ( ยท๐ OLD โ๐) | ||
Theorem | hhvs 30690 | The vector subtraction operation of Hilbert space. (Contributed by NM, 13-Dec-2007.) (New usage is discouraged.) |
โข ๐ = โจโจ +โ , ยทโ โฉ, normโโฉ โ โข โโ = ( โ๐ฃ โ๐) | ||
Theorem | hhnm 30691 | The norm function of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
โข ๐ = โจโจ +โ , ยทโ โฉ, normโโฉ โ โข normโ = (normCVโ๐) | ||
Theorem | hhims 30692 | The induced metric of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
โข ๐ = โจโจ +โ , ยทโ โฉ, normโโฉ & โข ๐ท = (normโ โ โโ ) โ โข ๐ท = (IndMetโ๐) | ||
Theorem | hhims2 30693 | Hilbert space distance metric. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
โข ๐ = โจโจ +โ , ยทโ โฉ, normโโฉ & โข ๐ท = (IndMetโ๐) โ โข ๐ท = (normโ โ โโ ) | ||
Theorem | hhmet 30694 | The induced metric of Hilbert space. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
โข ๐ = โจโจ +โ , ยทโ โฉ, normโโฉ & โข ๐ท = (IndMetโ๐) โ โข ๐ท โ (Metโ โ) | ||
Theorem | hhxmet 30695 | The induced metric of Hilbert space. (Contributed by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
โข ๐ = โจโจ +โ , ยทโ โฉ, normโโฉ & โข ๐ท = (IndMetโ๐) โ โข ๐ท โ (โMetโ โ) | ||
Theorem | hhmetdval 30696 | Value of the distance function of the metric space of Hilbert space. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
โข ๐ = โจโจ +โ , ยทโ โฉ, normโโฉ & โข ๐ท = (IndMetโ๐) โ โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด๐ท๐ต) = (normโโ(๐ด โโ ๐ต))) | ||
Theorem | hhip 30697 | The inner product operation of Hilbert space. (Contributed by NM, 17-Nov-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
โข ๐ = โจโจ +โ , ยทโ โฉ, normโโฉ โ โข ยทih = (ยท๐OLDโ๐) | ||
Theorem | hhph 30698 | The Hilbert space of the Hilbert Space Explorer is an inner product space. (Contributed by NM, 24-Nov-2007.) (New usage is discouraged.) |
โข ๐ = โจโจ +โ , ยทโ โฉ, normโโฉ โ โข ๐ โ CPreHilOLD | ||
Theorem | bcsiALT 30699 | Bunjakovaskij-Cauchy-Schwarz inequality. Remark 3.4 of [Beran] p. 98. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.) (Proof modification is discouraged.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (absโ(๐ด ยทih ๐ต)) โค ((normโโ๐ด) ยท (normโโ๐ต)) | ||
Theorem | bcsiHIL 30700 | Bunjakovaskij-Cauchy-Schwarz inequality. Remark 3.4 of [Beran] p. 98. (Proved from ZFC version.) (Contributed by NM, 24-Nov-2007.) (New usage is discouraged.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (absโ(๐ด ยทih ๐ต)) โค ((normโโ๐ด) ยท (normโโ๐ต)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |