Home | Metamath
Proof Explorer Theorem List (p. 308 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29659) |
Hilbert Space Explorer
(29660-31182) |
Users' Mathboxes
(31183-46998) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | eigvalval 30701 | The eigenvalue of an eigenvector of a Hilbert space operator. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
β’ ((π: ββΆ β β§ π΄ β (eigvecβπ)) β ((eigvalβπ)βπ΄) = (((πβπ΄) Β·ih π΄) / ((normββπ΄)β2))) | ||
Theorem | eigvalcl 30702 | An eigenvalue is a complex number. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
β’ ((π: ββΆ β β§ π΄ β (eigvecβπ)) β ((eigvalβπ)βπ΄) β β) | ||
Theorem | eigvec1 30703 | Property of an eigenvector. (Contributed by NM, 12-Mar-2006.) (New usage is discouraged.) |
β’ ((π: ββΆ β β§ π΄ β (eigvecβπ)) β ((πβπ΄) = (((eigvalβπ)βπ΄) Β·β π΄) β§ π΄ β 0β)) | ||
Theorem | eighmre 30704 | The eigenvalues of a Hermitian operator are real. Equation 1.30 of [Hughes] p. 49. (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.) |
β’ ((π β HrmOp β§ π΄ β (eigvecβπ)) β ((eigvalβπ)βπ΄) β β) | ||
Theorem | eighmorth 30705 | Eigenvectors of a Hermitian operator with distinct eigenvalues are orthogonal. Equation 1.31 of [Hughes] p. 49. (Contributed by NM, 23-Mar-2006.) (New usage is discouraged.) |
β’ (((π β HrmOp β§ π΄ β (eigvecβπ)) β§ (π΅ β (eigvecβπ) β§ ((eigvalβπ)βπ΄) β ((eigvalβπ)βπ΅))) β (π΄ Β·ih π΅) = 0) | ||
Theorem | nmopnegi 30706 | Value of the norm of the negative of a Hilbert space operator. Unlike nmophmi 30772, the operator does not have to be bounded. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
β’ π: ββΆ β β β’ (normopβ(-1 Β·op π)) = (normopβπ) | ||
Theorem | lnop0 30707 | The value of a linear Hilbert space operator at zero is zero. Remark in [Beran] p. 99. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.) |
β’ (π β LinOp β (πβ0β) = 0β) | ||
Theorem | lnopmul 30708 | Multiplicative property of a linear Hilbert space operator. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.) |
β’ ((π β LinOp β§ π΄ β β β§ π΅ β β) β (πβ(π΄ Β·β π΅)) = (π΄ Β·β (πβπ΅))) | ||
Theorem | lnopli 30709 | Basic scalar product property of a linear Hilbert space operator. (Contributed by NM, 23-Jan-2006.) (New usage is discouraged.) |
β’ π β LinOp β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (πβ((π΄ Β·β π΅) +β πΆ)) = ((π΄ Β·β (πβπ΅)) +β (πβπΆ))) | ||
Theorem | lnopfi 30710 | A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 23-Jan-2006.) (New usage is discouraged.) |
β’ π β LinOp β β’ π: ββΆ β | ||
Theorem | lnop0i 30711 | The value of a linear Hilbert space operator at zero is zero. Remark in [Beran] p. 99. (Contributed by NM, 11-May-2005.) (New usage is discouraged.) |
β’ π β LinOp β β’ (πβ0β) = 0β | ||
Theorem | lnopaddi 30712 | Additive property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005.) (New usage is discouraged.) |
β’ π β LinOp β β’ ((π΄ β β β§ π΅ β β) β (πβ(π΄ +β π΅)) = ((πβπ΄) +β (πβπ΅))) | ||
Theorem | lnopmuli 30713 | Multiplicative property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005.) (New usage is discouraged.) |
β’ π β LinOp β β’ ((π΄ β β β§ π΅ β β) β (πβ(π΄ Β·β π΅)) = (π΄ Β·β (πβπ΅))) | ||
Theorem | lnopaddmuli 30714 | Sum/product property of a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.) |
β’ π β LinOp β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (πβ(π΅ +β (π΄ Β·β πΆ))) = ((πβπ΅) +β (π΄ Β·β (πβπΆ)))) | ||
Theorem | lnopsubi 30715 | Subtraction property for a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.) |
β’ π β LinOp β β’ ((π΄ β β β§ π΅ β β) β (πβ(π΄ ββ π΅)) = ((πβπ΄) ββ (πβπ΅))) | ||
Theorem | lnopsubmuli 30716 | Subtraction/product property of a linear Hilbert space operator. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.) |
β’ π β LinOp β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (πβ(π΅ ββ (π΄ Β·β πΆ))) = ((πβπ΅) ββ (π΄ Β·β (πβπΆ)))) | ||
Theorem | lnopmulsubi 30717 | Product/subtraction property of a linear Hilbert space operator. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.) |
β’ π β LinOp β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (πβ((π΄ Β·β π΅) ββ πΆ)) = ((π΄ Β·β (πβπ΅)) ββ (πβπΆ))) | ||
Theorem | homco2 30718 | Move a scalar product out of a composition of operators. The operator π must be linear, unlike homco1 30542 that works for any operators. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π β LinOp β§ π: ββΆ β) β (π β (π΄ Β·op π)) = (π΄ Β·op (π β π))) | ||
Theorem | idunop 30719 | The identity function (restricted to Hilbert space) is a unitary operator. (Contributed by NM, 21-Jan-2006.) (New usage is discouraged.) |
β’ ( I βΎ β) β UniOp | ||
Theorem | 0cnop 30720 | The identically zero function is a continuous Hilbert space operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
β’ 0hop β ContOp | ||
Theorem | 0cnfn 30721 | The identically zero function is a continuous Hilbert space functional. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
β’ ( β Γ {0}) β ContFn | ||
Theorem | idcnop 30722 | The identity function (restricted to Hilbert space) is a continuous operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
β’ ( I βΎ β) β ContOp | ||
Theorem | idhmop 30723 | The Hilbert space identity operator is a Hermitian operator. (Contributed by NM, 22-Apr-2006.) (New usage is discouraged.) |
β’ Iop β HrmOp | ||
Theorem | 0hmop 30724 | The identically zero function is a Hermitian operator. (Contributed by NM, 8-Aug-2006.) (New usage is discouraged.) |
β’ 0hop β HrmOp | ||
Theorem | 0lnop 30725 | The identically zero function is a linear Hilbert space operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
β’ 0hop β LinOp | ||
Theorem | 0lnfn 30726 | The identically zero function is a linear Hilbert space functional. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
β’ ( β Γ {0}) β LinFn | ||
Theorem | nmop0 30727 | The norm of the zero operator is zero. (Contributed by NM, 8-Feb-2006.) (New usage is discouraged.) |
β’ (normopβ 0hop ) = 0 | ||
Theorem | nmfn0 30728 | The norm of the identically zero functional is zero. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
β’ (normfnβ( β Γ {0})) = 0 | ||
Theorem | hmopbdoptHIL 30729 | A Hermitian operator is a bounded linear operator (Hellinger-Toeplitz Theorem). (Contributed by NM, 18-Jan-2008.) (New usage is discouraged.) |
β’ (π β HrmOp β π β BndLinOp) | ||
Theorem | hoddii 30730 | Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri 30521 does not require linearity.) (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π: ββΆ β & β’ π: ββΆ β β β’ (π β (π βop π)) = ((π β π) βop (π β π)) | ||
Theorem | hoddi 30731 | Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri 30521 does not require linearity.) (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
β’ ((π β LinOp β§ π: ββΆ β β§ π: ββΆ β) β (π β (π βop π)) = ((π β π) βop (π β π))) | ||
Theorem | nmop0h 30732 | The norm of any operator on the trivial Hilbert space is zero. (This is the reason we need β β 0β in nmopun 30755.) (Contributed by NM, 24-Feb-2006.) (New usage is discouraged.) |
β’ (( β = 0β β§ π: ββΆ β) β (normopβπ) = 0) | ||
Theorem | idlnop 30733 | The identity function (restricted to Hilbert space) is a linear operator. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.) |
β’ ( I βΎ β) β LinOp | ||
Theorem | 0bdop 30734 | The identically zero operator is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
β’ 0hop β BndLinOp | ||
Theorem | adj0 30735 | Adjoint of the zero operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
β’ (adjββ 0hop ) = 0hop | ||
Theorem | nmlnop0iALT 30736 | A linear operator with a zero norm is identically zero. (Contributed by NM, 8-Feb-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π β LinOp β β’ ((normopβπ) = 0 β π = 0hop ) | ||
Theorem | nmlnop0iHIL 30737 | A linear operator with a zero norm is identically zero. (Contributed by NM, 18-Jan-2008.) (New usage is discouraged.) |
β’ π β LinOp β β’ ((normopβπ) = 0 β π = 0hop ) | ||
Theorem | nmlnopgt0i 30738 | A linear Hilbert space operator that is not identically zero has a positive norm. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.) |
β’ π β LinOp β β’ (π β 0hop β 0 < (normopβπ)) | ||
Theorem | nmlnop0 30739 | A linear operator with a zero norm is identically zero. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
β’ (π β LinOp β ((normopβπ) = 0 β π = 0hop )) | ||
Theorem | nmlnopne0 30740 | A linear operator with a nonzero norm is nonzero. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
β’ (π β LinOp β ((normopβπ) β 0 β π β 0hop )) | ||
Theorem | lnopmi 30741 | The scalar product of a linear operator is a linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
β’ π β LinOp β β’ (π΄ β β β (π΄ Β·op π) β LinOp) | ||
Theorem | lnophsi 30742 | The sum of two linear operators is linear. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β LinOp β β’ (π +op π) β LinOp | ||
Theorem | lnophdi 30743 | The difference of two linear operators is linear. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β LinOp β β’ (π βop π) β LinOp | ||
Theorem | lnopcoi 30744 | The composition of two linear operators is linear. (Contributed by NM, 8-Mar-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β LinOp β β’ (π β π) β LinOp | ||
Theorem | lnopco0i 30745 | The composition of a linear operator with one whose norm is zero. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β LinOp β β’ ((normopβπ) = 0 β (normopβ(π β π)) = 0) | ||
Theorem | lnopeq0lem1 30746 | Lemma for lnopeq0i 30748. Apply the generalized polarization identity polid2i 29898 to the quadratic form ((πβπ₯), π₯). (Contributed by NM, 26-Jul-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π΄ β β & β’ π΅ β β β β’ ((πβπ΄) Β·ih π΅) = (((((πβ(π΄ +β π΅)) Β·ih (π΄ +β π΅)) β ((πβ(π΄ ββ π΅)) Β·ih (π΄ ββ π΅))) + (i Β· (((πβ(π΄ +β (i Β·β π΅))) Β·ih (π΄ +β (i Β·β π΅))) β ((πβ(π΄ ββ (i Β·β π΅))) Β·ih (π΄ ββ (i Β·β π΅)))))) / 4) | ||
Theorem | lnopeq0lem2 30747 | Lemma for lnopeq0i 30748. (Contributed by NM, 26-Jul-2006.) (New usage is discouraged.) |
β’ π β LinOp β β’ ((π΄ β β β§ π΅ β β) β ((πβπ΄) Β·ih π΅) = (((((πβ(π΄ +β π΅)) Β·ih (π΄ +β π΅)) β ((πβ(π΄ ββ π΅)) Β·ih (π΄ ββ π΅))) + (i Β· (((πβ(π΄ +β (i Β·β π΅))) Β·ih (π΄ +β (i Β·β π΅))) β ((πβ(π΄ ββ (i Β·β π΅))) Β·ih (π΄ ββ (i Β·β π΅)))))) / 4)) | ||
Theorem | lnopeq0i 30748* | A condition implying that a linear Hilbert space operator is identically zero. Unlike ho01i 30569 for arbitrary operators, when the operator is linear we need to consider only the values of the quadratic form (πβπ₯) Β·ih π₯). (Contributed by NM, 26-Jul-2006.) (New usage is discouraged.) |
β’ π β LinOp β β’ (βπ₯ β β ((πβπ₯) Β·ih π₯) = 0 β π = 0hop ) | ||
Theorem | lnopeqi 30749* | Two linear Hilbert space operators are equal iff their quadratic forms are equal. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β LinOp β β’ (βπ₯ β β ((πβπ₯) Β·ih π₯) = ((πβπ₯) Β·ih π₯) β π = π) | ||
Theorem | lnopeq 30750* | Two linear Hilbert space operators are equal iff their quadratic forms are equal. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.) |
β’ ((π β LinOp β§ π β LinOp) β (βπ₯ β β ((πβπ₯) Β·ih π₯) = ((πβπ₯) Β·ih π₯) β π = π)) | ||
Theorem | lnopunilem1 30751* | Lemma for lnopunii 30753. (Contributed by NM, 14-May-2005.) (New usage is discouraged.) |
β’ π β LinOp & β’ βπ₯ β β (normββ(πβπ₯)) = (normββπ₯) & β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (ββ(πΆ Β· ((πβπ΄) Β·ih (πβπ΅)))) = (ββ(πΆ Β· (π΄ Β·ih π΅))) | ||
Theorem | lnopunilem2 30752* | Lemma for lnopunii 30753. (Contributed by NM, 12-May-2005.) (New usage is discouraged.) |
β’ π β LinOp & β’ βπ₯ β β (normββ(πβπ₯)) = (normββπ₯) & β’ π΄ β β & β’ π΅ β β β β’ ((πβπ΄) Β·ih (πβπ΅)) = (π΄ Β·ih π΅) | ||
Theorem | lnopunii 30753* | If a linear operator (whose range is β) is idempotent in the norm, the operator is unitary. Similar to theorem in [AkhiezerGlazman] p. 73. (Contributed by NM, 23-Jan-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ π: ββontoβ β & β’ βπ₯ β β (normββ(πβπ₯)) = (normββπ₯) β β’ π β UniOp | ||
Theorem | elunop2 30754* | An operator is unitary iff it is linear, onto, and idempotent in the norm. Similar to theorem in [AkhiezerGlazman] p. 73, and its converse. (Contributed by NM, 24-Feb-2006.) (New usage is discouraged.) |
β’ (π β UniOp β (π β LinOp β§ π: ββontoβ β β§ βπ₯ β β (normββ(πβπ₯)) = (normββπ₯))) | ||
Theorem | nmopun 30755 | Norm of a unitary Hilbert space operator. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.) |
β’ (( β β 0β β§ π β UniOp) β (normopβπ) = 1) | ||
Theorem | unopbd 30756 | A unitary operator is a bounded linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
β’ (π β UniOp β π β BndLinOp) | ||
Theorem | lnophmlem1 30757* | Lemma for lnophmi 30759. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ π β LinOp & β’ βπ₯ β β (π₯ Β·ih (πβπ₯)) β β β β’ (π΄ Β·ih (πβπ΄)) β β | ||
Theorem | lnophmlem2 30758* | Lemma for lnophmi 30759. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ π β LinOp & β’ βπ₯ β β (π₯ Β·ih (πβπ₯)) β β β β’ (π΄ Β·ih (πβπ΅)) = ((πβπ΄) Β·ih π΅) | ||
Theorem | lnophmi 30759* | A linear operator is Hermitian if π₯ Β·ih (πβπ₯) takes only real values. Remark in [ReedSimon] p. 195. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.) |
β’ π β LinOp & β’ βπ₯ β β (π₯ Β·ih (πβπ₯)) β β β β’ π β HrmOp | ||
Theorem | lnophm 30760* | A linear operator is Hermitian if π₯ Β·ih (πβπ₯) takes only real values. Remark in [ReedSimon] p. 195. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.) |
β’ ((π β LinOp β§ βπ₯ β β (π₯ Β·ih (πβπ₯)) β β) β π β HrmOp) | ||
Theorem | hmops 30761 | The sum of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
β’ ((π β HrmOp β§ π β HrmOp) β (π +op π) β HrmOp) | ||
Theorem | hmopm 30762 | The scalar product of a Hermitian operator with a real is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π β HrmOp) β (π΄ Β·op π) β HrmOp) | ||
Theorem | hmopd 30763 | The difference of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
β’ ((π β HrmOp β§ π β HrmOp) β (π βop π) β HrmOp) | ||
Theorem | hmopco 30764 | The composition of two commuting Hermitian operators is Hermitian. (Contributed by NM, 22-Aug-2006.) (New usage is discouraged.) |
β’ ((π β HrmOp β§ π β HrmOp β§ (π β π) = (π β π)) β (π β π) β HrmOp) | ||
Theorem | nmbdoplbi 30765 | A lower bound for the norm of a bounded linear operator. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
β’ π β BndLinOp β β’ (π΄ β β β (normββ(πβπ΄)) β€ ((normopβπ) Β· (normββπ΄))) | ||
Theorem | nmbdoplb 30766 | A lower bound for the norm of a bounded linear Hilbert space operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
β’ ((π β BndLinOp β§ π΄ β β) β (normββ(πβπ΄)) β€ ((normopβπ) Β· (normββπ΄))) | ||
Theorem | nmcexi 30767* | Lemma for nmcopexi 30768 and nmcfnexi 30792. The norm of a continuous linear Hilbert space operator or functional exists. Theorem 3.5(i) of [Beran] p. 99. (Contributed by Mario Carneiro, 17-Nov-2013.) (Proof shortened by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ βπ¦ β β+ βπ§ β β ((normββπ§) < π¦ β (πβ(πβπ§)) < 1) & β’ (πβπ) = sup({π β£ βπ₯ β β ((normββπ₯) β€ 1 β§ π = (πβ(πβπ₯)))}, β*, < ) & β’ (π₯ β β β (πβ(πβπ₯)) β β) & β’ (πβ(πβ0β)) = 0 & β’ (((π¦ / 2) β β+ β§ π₯ β β) β ((π¦ / 2) Β· (πβ(πβπ₯))) = (πβ(πβ((π¦ / 2) Β·β π₯)))) β β’ (πβπ) β β | ||
Theorem | nmcopexi 30768 | The norm of a continuous linear Hilbert space operator exists. Theorem 3.5(i) of [Beran] p. 99. (Contributed by NM, 5-Feb-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β ContOp β β’ (normopβπ) β β | ||
Theorem | nmcoplbi 30769 | A lower bound for the norm of a continuous linear operator. Theorem 3.5(ii) of [Beran] p. 99. (Contributed by NM, 7-Feb-2006.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
β’ π β LinOp & β’ π β ContOp β β’ (π΄ β β β (normββ(πβπ΄)) β€ ((normopβπ) Β· (normββπ΄))) | ||
Theorem | nmcopex 30770 | The norm of a continuous linear Hilbert space operator exists. Theorem 3.5(i) of [Beran] p. 99. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
β’ ((π β LinOp β§ π β ContOp) β (normopβπ) β β) | ||
Theorem | nmcoplb 30771 | A lower bound for the norm of a continuous linear Hilbert space operator. Theorem 3.5(ii) of [Beran] p. 99. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
β’ ((π β LinOp β§ π β ContOp β§ π΄ β β) β (normββ(πβπ΄)) β€ ((normopβπ) Β· (normββπ΄))) | ||
Theorem | nmophmi 30772 | The norm of the scalar product of a bounded linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
β’ π β BndLinOp β β’ (π΄ β β β (normopβ(π΄ Β·op π)) = ((absβπ΄) Β· (normopβπ))) | ||
Theorem | bdophmi 30773 | The scalar product of a bounded linear operator is a bounded linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
β’ π β BndLinOp β β’ (π΄ β β β (π΄ Β·op π) β BndLinOp) | ||
Theorem | lnconi 30774* | Lemma for lnopconi 30775 and lnfnconi 30796. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
β’ (π β πΆ β π β β) & β’ ((π β πΆ β§ π¦ β β) β (πβ(πβπ¦)) β€ (π Β· (normββπ¦))) & β’ (π β πΆ β βπ₯ β β βπ§ β β+ βπ¦ β β+ βπ€ β β ((normββ(π€ ββ π₯)) < π¦ β (πβ((πβπ€)π(πβπ₯))) < π§)) & β’ (π¦ β β β (πβ(πβπ¦)) β β) & β’ ((π€ β β β§ π₯ β β) β (πβ(π€ ββ π₯)) = ((πβπ€)π(πβπ₯))) β β’ (π β πΆ β βπ₯ β β βπ¦ β β (πβ(πβπ¦)) β€ (π₯ Β· (normββπ¦))) | ||
Theorem | lnopconi 30775* | A condition equivalent to "π is continuous" when π is linear. Theorem 3.5(iii) of [Beran] p. 99. (Contributed by NM, 7-Feb-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
β’ π β LinOp β β’ (π β ContOp β βπ₯ β β βπ¦ β β (normββ(πβπ¦)) β€ (π₯ Β· (normββπ¦))) | ||
Theorem | lnopcon 30776* | A condition equivalent to "π is continuous" when π is linear. Theorem 3.5(iii) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
β’ (π β LinOp β (π β ContOp β βπ₯ β β βπ¦ β β (normββ(πβπ¦)) β€ (π₯ Β· (normββπ¦)))) | ||
Theorem | lnopcnbd 30777 | A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
β’ (π β LinOp β (π β ContOp β π β BndLinOp)) | ||
Theorem | lncnopbd 30778 | A continuous linear operator is a bounded linear operator. This theorem justifies our use of "bounded linear" as an interchangeable condition for "continuous linear" used in some textbook proofs. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
β’ (π β (LinOp β© ContOp) β π β BndLinOp) | ||
Theorem | lncnbd 30779 | A continuous linear operator is a bounded linear operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
β’ (LinOp β© ContOp) = BndLinOp | ||
Theorem | lnopcnre 30780 | A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
β’ (π β LinOp β (π β ContOp β (normopβπ) β β)) | ||
Theorem | lnfnli 30781 | Basic property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (πβ((π΄ Β·β π΅) +β πΆ)) = ((π΄ Β· (πβπ΅)) + (πβπΆ))) | ||
Theorem | lnfnfi 30782 | A linear Hilbert space functional is a functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn β β’ π: ββΆβ | ||
Theorem | lnfn0i 30783 | The value of a linear Hilbert space functional at zero is zero. Remark in [Beran] p. 99. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn β β’ (πβ0β) = 0 | ||
Theorem | lnfnaddi 30784 | Additive property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn β β’ ((π΄ β β β§ π΅ β β) β (πβ(π΄ +β π΅)) = ((πβπ΄) + (πβπ΅))) | ||
Theorem | lnfnmuli 30785 | Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn β β’ ((π΄ β β β§ π΅ β β) β (πβ(π΄ Β·β π΅)) = (π΄ Β· (πβπ΅))) | ||
Theorem | lnfnaddmuli 30786 | Sum/product property of a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (πβ(π΅ +β (π΄ Β·β πΆ))) = ((πβπ΅) + (π΄ Β· (πβπΆ)))) | ||
Theorem | lnfnsubi 30787 | Subtraction property for a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn β β’ ((π΄ β β β§ π΅ β β) β (πβ(π΄ ββ π΅)) = ((πβπ΄) β (πβπ΅))) | ||
Theorem | lnfn0 30788 | The value of a linear Hilbert space functional at zero is zero. Remark in [Beran] p. 99. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
β’ (π β LinFn β (πβ0β) = 0) | ||
Theorem | lnfnmul 30789 | Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
β’ ((π β LinFn β§ π΄ β β β§ π΅ β β) β (πβ(π΄ Β·β π΅)) = (π΄ Β· (πβπ΅))) | ||
Theorem | nmbdfnlbi 30790 | A lower bound for the norm of a bounded linear functional. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
β’ (π β LinFn β§ (normfnβπ) β β) β β’ (π΄ β β β (absβ(πβπ΄)) β€ ((normfnβπ) Β· (normββπ΄))) | ||
Theorem | nmbdfnlb 30791 | A lower bound for the norm of a bounded linear functional. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
β’ ((π β LinFn β§ (normfnβπ) β β β§ π΄ β β) β (absβ(πβπ΄)) β€ ((normfnβπ) Β· (normββπ΄))) | ||
Theorem | nmcfnexi 30792 | The norm of a continuous linear Hilbert space functional exists. Theorem 3.5(i) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
β’ π β LinFn & β’ π β ContFn β β’ (normfnβπ) β β | ||
Theorem | nmcfnlbi 30793 | A lower bound for the norm of a continuous linear functional. Theorem 3.5(ii) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
β’ π β LinFn & β’ π β ContFn β β’ (π΄ β β β (absβ(πβπ΄)) β€ ((normfnβπ) Β· (normββπ΄))) | ||
Theorem | nmcfnex 30794 | The norm of a continuous linear Hilbert space functional exists. Theorem 3.5(i) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
β’ ((π β LinFn β§ π β ContFn) β (normfnβπ) β β) | ||
Theorem | nmcfnlb 30795 | A lower bound of the norm of a continuous linear Hilbert space functional. Theorem 3.5(ii) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.) |
β’ ((π β LinFn β§ π β ContFn β§ π΄ β β) β (absβ(πβπ΄)) β€ ((normfnβπ) Β· (normββπ΄))) | ||
Theorem | lnfnconi 30796* | A condition equivalent to "π is continuous" when π is linear. Theorem 3.5(iii) of [Beran] p. 99. (Contributed by NM, 14-Feb-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
β’ π β LinFn β β’ (π β ContFn β βπ₯ β β βπ¦ β β (absβ(πβπ¦)) β€ (π₯ Β· (normββπ¦))) | ||
Theorem | lnfncon 30797* | A condition equivalent to "π is continuous" when π is linear. Theorem 3.5(iii) of [Beran] p. 99. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.) |
β’ (π β LinFn β (π β ContFn β βπ₯ β β βπ¦ β β (absβ(πβπ¦)) β€ (π₯ Β· (normββπ¦)))) | ||
Theorem | lnfncnbd 30798 | A linear functional is continuous iff it is bounded. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
β’ (π β LinFn β (π β ContFn β (normfnβπ) β β)) | ||
Theorem | imaelshi 30799 | The image of a subspace under a linear operator is a subspace. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
β’ π β LinOp & β’ π΄ β Sβ β β’ (π β π΄) β Sβ | ||
Theorem | rnelshi 30800 | The range of a linear operator is a subspace. (Contributed by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.) |
β’ π β LinOp β β’ ran π β Sβ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |