HomeTheorem List (p. 277 of 426)
Unicode version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 277 of 426) | < Previous Next > |
| Browser slow? Try the
Unicode version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Definition | df-blo 27601* | Define the class of bounded linear operators between two normed complex vector spaces. (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.) |
  
                  | ||
| Definition | df-0o 27602* | Define the zero operator between two normed complex vector spaces. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.) |
   | ||
| Syntax | caj 27603 | Adjoint of an operator. |
  | ||
| Syntax | chmo 27604 | Set of Hermitional (self-adjoint) operators. |
 | ||
| Definition | df-aj 27605* |
Define the adjoint of an operator (if it exists). The domain of
  is the set of all operators from to that have an
adjoint. Definition 3.9-1 of [Kreyszig] p. 196, although we don't
require that
and be Hilbert spaces
nor that the operators be
linear. Although we define it for any normed vector space for
convenience, the definition is meaningful only for inner product spaces.
(Contributed by NM, 25-Jan-2008.) (New usage is discouraged.)
|
    
![/\](wedge.gif "/\"){kind=small}     | ||
| Definition | df-hmo 27606* | Define the set of Hermitian (self-adjoint) operators on a normed complex vector space (normally a Hilbert space). Although we define it for any normed vector space for convenience, the definition is meaningful only for inner product spaces. (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.) |
| ||
| Theorem | lnoval 27607* | The set of linear operators between two normed complex vector spaces. (Contributed by NM, 6-Nov-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
           
  | ||
| Theorem | islno 27608* | The predicate "is a linear operator." (Contributed by NM, 4-Dec-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ||
| Theorem | lnolin 27609 | Basic linearity property of a linear operator. (Contributed by NM, 4-Dec-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
  
| ||
| Theorem | lnof 27610 | A linear operator is a mapping. (Contributed by NM, 4-Dec-2007.) (Revised by Mario Carneiro, 18-Nov-2013.) (New usage is discouraged.) |
| | ||
| Theorem | lno0 27611 | The value of a linear operator at zero is zero. (Contributed by NM, 4-Dec-2007.) (Revised by Mario Carneiro, 18-Nov-2013.) (New usage is discouraged.) |
  | ||
| Theorem | lnocoi 27612 | The composition of two linear operators is linear. (Contributed by NM, 12-Jan-2008.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.) |
| ||
| Theorem | lnoadd 27613 | Addition property of a linear operator. (Contributed by NM, 7-Dec-2007.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | lnosub 27614 | Subtraction property of a linear operator. (Contributed by NM, 7-Dec-2007.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.) |
| ||
| Theorem | lnomul 27615 | Scalar multiplication property of a linear operator. (Contributed by NM, 5-Dec-2007.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | nvo00 27616 | Two ways to express a zero operator. (Contributed by NM, 27-Nov-2007.) (New usage is discouraged.) |
 | ||
| Theorem | nmoofval 27617* | The operator norm function. (Contributed by NM, 6-Nov-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
 CV CV
 
 
 | ||
| Theorem | nmooval 27618* | The operator norm function. (Contributed by NM, 27-Nov-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| CV CV
| ||
| Theorem | nmosetre 27619* | The set in the supremum of the operator norm definition df-nmoo 27600 is a set of reals. (Contributed by NM, 13-Nov-2007.) (New usage is discouraged.) |
CV
  | ||
| Theorem | nmosetn0 27620* | The set in the supremum of the operator norm definition df-nmoo 27600 is nonempty. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
| CV
| ||
| Theorem | nmoxr 27621 | The norm of an operator is an extended real. (Contributed by NM, 27-Nov-2007.) (New usage is discouraged.) |
| | ||
| Theorem | nmooge0 27622 | The norm of an operator is nonnegative. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
| ||
| Theorem | nmorepnf 27623 | The norm of an operator is either real or plus infinity. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
 | ||
| Theorem | nmoreltpnf 27624 | The norm of any operator is real iff it is less than plus infinity. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
|
| ||
| Theorem | nmogtmnf 27625 | The norm of an operator is greater than minus infinity. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
 | ||
| Theorem | nmoolb 27626 | A lower bound for an operator norm. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
| CV CV
| ||
| Theorem | nmoubi 27627* | An upper bound for an operator norm. (Contributed by NM, 11-Dec-2007.) (New usage is discouraged.) |
| CV CV
| ||
| Theorem | nmoub3i 27628* | An upper bound for an operator norm. (Contributed by NM, 12-Dec-2007.) (New usage is discouraged.) |
CV CV
  | ||
| Theorem | nmoub2i 27629* | An upper bound for an operator norm. (Contributed by NM, 11-Dec-2007.) (New usage is discouraged.) |
| CV CV
| ||
| Theorem | nmobndi 27630* | Two ways to express that an operator is bounded. (Contributed by NM, 11-Jan-2008.) (New usage is discouraged.) |
CV CV 
| ||
| Theorem | nmounbi 27631* | Two ways two express that an operator is unbounded. (Contributed by NM, 11-Jan-2008.) (New usage is discouraged.) |
| CV CV
| ||
| Theorem | nmounbseqi 27632* | An unbounded operator determines an unbounded sequence. (Contributed by NM, 11-Jan-2008.) (Revised by Mario Carneiro, 7-Apr-2013.) (New usage is discouraged.) |
CV CV
  
| ||
| Theorem | nmounbseqiALT 27633* | Alternate shorter proof of nmounbseqi 27632 based on axioms ax-reg 8497 and ax-ac2 9285 instead of ax-cc 9257. (Contributed by NM, 11-Jan-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
| CV CV
| ||
| Theorem | nmobndseqi 27634* | A bounded sequence determines a bounded operator. (Contributed by NM, 18-Jan-2008.) (Revised by Mario Carneiro, 7-Apr-2013.) (New usage is discouraged.) |
| CV CV
| ||
| Theorem | nmobndseqiALT 27635* | Alternate shorter proof of nmobndseqi 27634 based on axioms ax-reg 8497 and ax-ac2 9285 instead of ax-cc 9257. (Contributed by NM, 18-Jan-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
| CV CV
| ||
| Theorem | bloval 27636* | The class of bounded linear operators between two normed complex vector spaces. (Contributed by NM, 6-Nov-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | isblo 27637 | The predicate "is a bounded linear operator." (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.) |
|
| ||
| Theorem | isblo2 27638 | The predicate "is a bounded linear operator." (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
|
| ||
| Theorem | bloln 27639 | A bounded operator is a linear operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
|
| ||
| Theorem | blof 27640 | A bounded operator is an operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
| | ||
| Theorem | nmblore 27641 | The norm of a bounded operator is a real number. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
| | ||
| Theorem | 0ofval 27642 | The zero operator between two normed complex vector spaces. (Contributed by NM, 28-Nov-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ||
| Theorem | 0oval 27643 | Value of the zero operator. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.) |
| | ||
| Theorem | 0oo 27644 | The zero operator is an operator. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.) |
| | ||
| Theorem | 0lno 27645 | The zero operator is linear. (Contributed by NM, 28-Nov-2007.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | nmoo0 27646 | The operator norm of the zero operator. (Contributed by NM, 27-Nov-2007.) (New usage is discouraged.) |
| | ||
| Theorem | 0blo 27647 | The zero operator is a bounded linear operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
|
| ||
| Theorem | nmlno0lem 27648 | Lemma for nmlno0i 27649. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.) |
  CV CV
| ||
| Theorem | nmlno0i 27649 | The norm of a linear operator is zero iff the operator is zero. (Contributed by NM, 6-Dec-2007.) (New usage is discouraged.) |
|
| ||
| Theorem | nmlno0 27650 | The norm of a linear operator is zero iff the operator is zero. (Contributed by NM, 24-Nov-2007.) (New usage is discouraged.) |
|
| ||
| Theorem | nmlnoubi 27651* | An upper bound for the operator norm of a linear operator, using only the properties of nonzero arguments. (Contributed by NM, 1-Jan-2008.) (New usage is discouraged.) |
| CV CV
| ||
| Theorem | nmlnogt0 27652 | The norm of a nonzero linear operator is positive. (Contributed by NM, 10-Dec-2007.) (New usage is discouraged.) |
| | ||
| Theorem | lnon0 27653* | The domain of a nonzero linear operator contains a nonzero vector. (Contributed by NM, 15-Dec-2007.) (New usage is discouraged.) |
|
| ||
| Theorem | nmblolbii 27654 | A lower bound for the norm of a bounded linear operator. (Contributed by NM, 7-Dec-2007.) (New usage is discouraged.) |
| CV CV
| ||
| Theorem | nmblolbi 27655 | A lower bound for the norm of a bounded linear operator. (Contributed by NM, 10-Dec-2007.) (New usage is discouraged.) |
| CV CV
| ||
| Theorem | isblo3i 27656* | The predicate "is a bounded linear operator." Definition 2.7-1 of [Kreyszig] p. 91. (Contributed by NM, 11-Dec-2007.) (New usage is discouraged.) |
| CV CV
| ||
| Theorem | blo3i 27657* | Properties that determine a bounded linear operator. (Contributed by NM, 13-Jan-2008.) (New usage is discouraged.) |
| CV CV
| ||
| Theorem | blometi 27658 | Upper bound for the distance between the values of a bounded linear operator. (Contributed by NM, 11-Dec-2007.) (New usage is discouraged.) |
 
| ||
| Theorem | blocnilem 27659 | Lemma for blocni 27660 and lnocni 27661. If a linear operator is continuous at any point, it is bounded. (Contributed by NM, 17-Dec-2007.) (Revised by Mario Carneiro, 10-Jan-2014.) (New usage is discouraged.) |
 
| ||
| Theorem | blocni 27660 | A linear operator is continuous iff it is bounded. Theorem 2.7-9(a) of [Kreyszig] p. 97. (Contributed by NM, 18-Dec-2007.) (Revised by Mario Carneiro, 10-Jan-2014.) (New usage is discouraged.) |
| ||
| Theorem | lnocni 27661 | If a linear operator is continuous at any point, it is continuous everywhere. Theorem 2.7-9(b) of [Kreyszig] p. 97. (Contributed by NM, 18-Dec-2007.) (New usage is discouraged.) |
|
| ||
| Theorem | blocn 27662 | A linear operator is continuous iff it is bounded. Theorem 2.7-9(a) of [Kreyszig] p. 97. (Contributed by NM, 25-Dec-2007.) (New usage is discouraged.) |
|
| ||
| Theorem | blocn2 27663 | A bounded linear operator is continuous. (Contributed by NM, 25-Dec-2007.) (New usage is discouraged.) |
|
| ||
| Theorem | ajfval 27664* | The adjoint function. (Contributed by NM, 25-Jan-2008.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | hmoval 27665* | The set of Hermitian (self-adjoint) operators on a normed complex vector space. (Contributed by NM, 26-Jan-2008.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | ishmo 27666 | The predicate "is a hermitian operator." (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.) |
|
| ||
| Syntax | ccphlo 27667 | Extend class notation with the class of all complex inner product spaces (also called pre-Hilbert spaces). |
 | ||
| Definition | df-ph 27668* |
Define the class of all complex inner product spaces. An inner product
space is a normed vector space whose norm satisfies the parallelogram
law (a property that induces an inner product). Based on Exercise 4(b)
of [ReedSimon] p. 63. The vector
operation is  , the
scalar
product is , and
the norm is  . An inner
product space is
also called a pre-Hilbert space. (Contributed by NM, 2-Apr-2007.)
(New usage is discouraged.)
|
    | ||
| Theorem | phnv 27669 | Every complex inner product space is a normed complex vector space. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.) |
| | ||
| Theorem | phrel 27670 | The class of all complex inner product spaces is a relation. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.) |
 | ||
| Theorem | phnvi 27671 | Every complex inner product space is a normed complex vector space. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
| | ||
| Theorem | isphg 27672* |
The predicate "is a complex inner product space." An inner product
space is a normed vector space whose norm satisfies the parallelogram
law. The vector (group) addition operation is , the scalar
product is ,
and the norm is . An
inner product space is
also called a pre-Hilbert space. (Contributed by NM, 2-Apr-2007.)
(New usage is discouraged.)
|
|
| ||
| Theorem | phop 27673 | A complex inner product space in terms of ordered pair components. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.) |
| CV | ||
| Theorem | cncph 27674 | The set of complex numbers is an inner product (pre-Hilbert) space. (Contributed by Steve Rodriguez, 28-Apr-2007.) (Revised by Mario Carneiro, 7-Nov-2013.) (New usage is discouraged.) |
| | ||
| Theorem | elimph 27675 | Hypothesis elimination lemma for complex inner product spaces to assist weak deduction theorem. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.) |
| ||
| Theorem | elimphu 27676 | Hypothesis elimination lemma for complex inner product spaces to assist weak deduction theorem. (Contributed by NM, 6-May-2007.) (New usage is discouraged.) |
|
| ||
| Theorem | isph 27677* | The predicate "is an inner product space." (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.) |
|
CV
| ||
| Theorem | phpar2 27678 | The parallelogram law for an inner product space. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.) |
|
CV
| ||
| Theorem | phpar 27679 | The parallelogram law for an inner product space. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.) |
|
CV
| ||
| Theorem | ip0i 27680 |
A slight variant of Equation 6.46 of [Ponnusamy] p. 362, where
is either 1 or -1 to represent +-1. (Contributed by NM,
23-Apr-2007.) (New usage is discouraged.)
|
CV  | ||
| Theorem | ip1ilem 27681 | Lemma for ip1i 27682. (Contributed by NM, 21-Apr-2007.) (New usage is discouraged.) |
|
CV
| ||
| Theorem | ip1i 27682 | Equation 6.47 of [Ponnusamy] p. 362. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.) |
|
| ||
| Theorem | ip2i 27683 | Equation 6.48 of [Ponnusamy] p. 362. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.) |
|
| ||
| Theorem | ipdirilem 27684 | Lemma for ipdiri 27685. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.) |
|
| ||
| Theorem | ipdiri 27685 | Distributive law for inner product. Equation I3 of [Ponnusamy] p. 362. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.) |
|
| ||
| Theorem | ipasslem1 27686 | Lemma for ipassi 27696. Show the inner product associative law for nonnegative integers. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.) |
| ||
| Theorem | ipasslem2 27687 | Lemma for ipassi 27696. Show the inner product associative law for nonpositive integers. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.) |
|
| ||
| Theorem | ipasslem3 27688 | Lemma for ipassi 27696. Show the inner product associative law for all integers. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.) |
 | ||
| Theorem | ipasslem4 27689 | Lemma for ipassi 27696. Show the inner product associative law for positive integer reciprocals. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.) |
| ||
| Theorem | ipasslem5 27690 | Lemma for ipassi 27696. Show the inner product associative law for rational numbers. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.) |
 | ||
| Theorem | ipasslem7 27691* |
Lemma for ipassi 27696. Show that
is continuous on .
(Contributed by NM, 23-Aug-2007.) (Revised by Mario Carneiro,
6-May-2014.) (New usage is discouraged.)
|
    ℂfld | ||
| Theorem | ipasslem8 27692* |
Lemma for ipassi 27696. By ipasslem5 27690, is 0 for all ;
since it is continuous and is dense in by qdensere2 22600,
we conclude
is 0 for all .
(Contributed by NM,
24-Aug-2007.) (Revised by Mario Carneiro, 6-May-2014.)
(New usage is discouraged.)
|
|
| ||
| Theorem | ipasslem9 27693 | Lemma for ipassi 27696. Conclude from ipasslem8 27692 the inner product associative law for real numbers. (Contributed by NM, 24-Aug-2007.) (New usage is discouraged.) |
|
| ||
| Theorem | ipasslem10 27694 |
Lemma for ipassi 27696. Show the inner product associative law for
the
imaginary number  . (Contributed by NM, 24-Aug-2007.)
(New usage is discouraged.)
|
|
CV
| ||
| Theorem | ipasslem11 27695 | Lemma for ipassi 27696. Show the inner product associative law for all complex numbers. (Contributed by NM, 25-Aug-2007.) (New usage is discouraged.) |
|
| ||
| Theorem | ipassi 27696 | Associative law for inner product. Equation I2 of [Ponnusamy] p. 363. (Contributed by NM, 25-Aug-2007.) (New usage is discouraged.) |
|
| ||
| Theorem | dipdir 27697 | Distributive law for inner product. Equation I3 of [Ponnusamy] p. 362. (Contributed by NM, 25-Aug-2007.) (New usage is discouraged.) |
|
| ||
| Theorem | dipdi 27698 | Distributive law for inner product. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
|
| ||
| Theorem | ip2dii 27699 | Inner product of two sums. (Contributed by NM, 17-Apr-2008.) (New usage is discouraged.) |
|
| ||
| Theorem | dipass 27700 | Associative law for inner product. Equation I2 of [Ponnusamy] p. 363. (Contributed by NM, 25-Aug-2007.) (New usage is discouraged.) |
|
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |