mmtheorems100 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10752

Statement List for Metamath Proof Explorer - 9901-10000 - Page 100 of 108

Type	Label	Description
Statement
Theorem	idhmop 9901	The Hilbert space identity operator is a Hermitian operator.
⊢ Iop ∈ HrmOp
Theorem	0hmop 9902	The identically zero function is a Hermitian operator.
⊢ 0hop ∈ HrmOp
Theorem	0lnop 9903	The identically zero function is a linear Hilbert space operator.
⊢ 0hop ∈ LinOp
Theorem	0lnfn 9904	The identically zero function is a linear Hilbert space functional.
⊢ ( ℋ × {0}) ∈ LinFn
Theorem	nmop0 9905	The norm of the zero operator is zero.
⊢ (normop ‘ 0hop ) = 0
Theorem	nmfn0 9906	The norm of the identically zero functional is zero.
⊢ (normfn ‘( ℋ × {0})) = 0
Theorem	hmopbdopHIL 9907	A Hermitian operator is a bounded linear operator (Hellinger-Toeplitz Theorem).
⊢ T ∈ HrmOp    ⇒   ⊢ T ∈ BndLinOp
Theorem	hmopbdoptHIL 9908	A Hermitian operator is a bounded linear operator (Hellinger-Toeplitz Theorem).
⊢ (T ∈ HrmOp → T ∈ BndLinOp)
Theorem	hoddi 9909	Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdir 9701 does not require linearity.)
⊢ R ∈ LinOp    &   ⊢ S: ℋ –→ ℋ    &   ⊢ T: ℋ –→ ℋ    ⇒   ⊢ (R ∘ (S −op T)) = ((R ∘ S) −op (R ∘ T))
Theorem	hoddit 9910	Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdir 9701 does not require linearity.)
⊢ ((R ∈ LinOp ⋀ S: ℋ –→ ℋ ⋀ T: ℋ –→ ℋ ) → (R ∘ (S −op T)) = ((R ∘ S) −op (R ∘ T)))
Theorem	nmop0h 9911	The norm of any operator on the trivial Hilbert space is zero. (This is the reason we need ℋ ≠ 0ℋ in nmopunt 9934.)
⊢ (( ℋ = 0ℋ ⋀ T: ℋ –→ ℋ ) → (normop ‘T) = 0)
Theorem	idlnop 9912	The identity function (restricted to Hilbert space) is a linear operator.
⊢ (I ↾ ℋ ) ∈ LinOp
Theorem	0bdop 9913	The identically zero operator is bounded.
⊢ 0hop ∈ BndLinOp
Theorem	adj0 9914	Adjoint of the zero operator.
⊢ (adjh ‘ 0hop ) = 0hop
Theorem	nmlnop0ALT 9915	A linear operator with a zero norm is identically zero.
⊢ T ∈ LinOp    ⇒   ⊢ ((normop ‘T) = 0 ↔ T = 0hop )
Theorem	nmlnop0HIL 9916	A linear operator with a zero norm is identically zero.
⊢ T ∈ LinOp    ⇒   ⊢ ((normop ‘T) = 0 ↔ T = 0hop )
Theorem	nmlnopgt0 9917	A linear Hilbert space operator that is not identically zero has a positive norm.
⊢ T ∈ LinOp    ⇒   ⊢ (T ≠ 0hop ↔ 0 < (normop ‘T))
Theorem	nmlnop0t 9918	A linear operator with a zero norm is identically zero.
⊢ (T ∈ LinOp → ((normop ‘T) = 0 ↔ T = 0hop ))
Theorem	nmlnopne0t 9919	A linear operator with a nonzero norm is nonzero.
⊢ (T ∈ LinOp → ((normop ‘T) ≠ 0 ↔ T ≠ 0hop ))
Theorem	lnopm 9920	The scalar product of a linear operator is a linear operator.
⊢ T ∈ LinOp    ⇒   ⊢ (A ∈ ℂ → (A ·op T) ∈ LinOp)
Theorem	lnophs 9921	The sum of two linear operators is linear.
⊢ S ∈ LinOp    &   ⊢ T ∈ LinOp    ⇒   ⊢ (S +op T) ∈ LinOp
Theorem	lnophd 9922	The difference of two linear operators is linear.
⊢ S ∈ LinOp    &   ⊢ T ∈ LinOp    ⇒   ⊢ (S −op T) ∈ LinOp
Theorem	lnopco 9923	The composition of two linear operators is linear.
⊢ S ∈ LinOp    &   ⊢ T ∈ LinOp    ⇒   ⊢ (S ∘ T) ∈ LinOp
Theorem	lnopco0 9924	The composition of a linear operator with one whose norm is zero.
⊢ S ∈ LinOp    &   ⊢ T ∈ LinOp    ⇒   ⊢ ((normop ‘T) = 0 → (normop ‘(S ∘ T)) = 0)
Theorem	lnopeq0lem1 9925	Lemma for lnopeq0 9927. Apply the generalized polarization identity polid2 9019 to the quadratic form ((T ‘x), x).
Theorem	lnopeq0lem2 9926	Lemma for lnopeq0 9927.
Theorem	lnopeq0 9927	A condition implying that a linear Hilbert space operator is identically zero. Unlike ho01 9749 for arbitrary operators, when the operator is linear we need to consider only the values of the quadratic form (T ‘x) ·ih x).
⊢ T ∈ LinOp    ⇒   ⊢ (∀x ∈ ℋ ((T ‘x) ·ih x) = 0 ↔ T = 0hop )
Theorem	lnopeq 9928	Two linear Hilbert space operators are equal iff their quadratic forms are equal.
⊢ T ∈ LinOp    &   ⊢ U ∈ LinOp    ⇒   ⊢ (∀x ∈ ℋ ((T ‘x) ·ih x) = ((U ‘x) ·ih x) ↔ T = U)
Theorem	lnopeqt 9929	Two linear Hilbert space operators are equal iff their quadratic forms are equal.
⊢ ((T ∈ LinOp ⋀ U ∈ LinOp) → (∀x ∈ ℋ ((T ‘x) ·ih x) = ((U ‘x) ·ih x) ↔ T = U))
Theorem	lnopunilem1 9930	Lemma for lnopuni 9932.
Theorem	lnopunilem2 9931	Lemma for lnopuni 9932.
Theorem	lnopuni 9932	If a linear operator (whose range is ℋ) is idempotent in the norm, the operator is unitary. Similar to theorem in [AkhiezerGlazman] p. 73.
⊢ T ∈ LinOp    &   ⊢ T: ℋ –onto→ ℋ    &   ⊢ ∀x ∈ ℋ (normh ‘(T ‘x)) = (normh ‘x)    ⇒   ⊢ T ∈ UniOp
Theorem	elunop2t 9933	An operator is unitary iff it is linear, onto, and idempotent in the norm. Similar to theorem in [AkhiezerGlazman] p. 73, and its converse.
⊢ (T ∈ UniOp ↔ (T ∈ LinOp ⋀ T: ℋ –onto→ ℋ ⋀ ∀x ∈ ℋ (normh ‘(T ‘x)) = (normh ‘x)))
Theorem	nmopunt 9934	Norm of a unitary Hilbert space operator.
⊢ (( ℋ ≠ 0ℋ ⋀ T ∈ UniOp) → (normop ‘T) = 1)
Theorem	unopbdt 9935	A unitary operator is a bounded linear operator.
⊢ (T ∈ UniOp → T ∈ BndLinOp)
Theorem	lnophmlem1 9936	Lemma for lnophm 9938.
Theorem	lnophmlem2 9937	Lemma for lnophm 9938. Warning: The HTML proof page is 1/2 megabyte in size.
Theorem	lnophm 9938	A linear operator is Hermitian if x ·ih (T ‘x) takes only real values. Remark in [ReedSimon] p. 195.
⊢ T ∈ LinOp    &   ⊢ ∀x ∈ ℋ (x ·ih (T ‘x)) ∈ ℝ    ⇒   ⊢ T ∈ HrmOp
Theorem	lnophmt 9939	A linear operator is Hermitian if x ·ih (T ‘x) takes only real values. Remark in [ReedSimon] p. 195.
⊢ ((T ∈ LinOp ⋀ ∀x ∈ ℋ (x ·ih (T ‘x)) ∈ ℝ) → T ∈ HrmOp)
Theorem	hmopst 9940	The sum of two Hermitian operators is Hermitian.
⊢ ((T ∈ HrmOp ⋀ U ∈ HrmOp) → (T +op U) ∈ HrmOp)
Theorem	hmopmt 9941	The scalar product of a Hermitian operator with a real is Hermitian.
⊢ ((A ∈ ℝ ⋀ T ∈ HrmOp) → (A ·op T) ∈ HrmOp)
Theorem	hmopdt 9942	The difference of two Hermitian operators is Hermitian.
⊢ ((T ∈ HrmOp ⋀ U ∈ HrmOp) → (T −op U) ∈ HrmOp)
Theorem	hmopcot 9943	The composition of two commuting Hermitian operators is Hermitian.
⊢ ((T ∈ HrmOp ⋀ U ∈ HrmOp ⋀ (T ∘ U) = (U ∘ T)) → (T ∘ U) ∈ HrmOp)
Theorem	nmbdoplb 9944	A lower bound for the norm of a bounded linear operator.
⊢ T ∈ BndLinOp    ⇒   ⊢ (A ∈ ℋ → (normh ‘(T ‘A)) ≤ ((normop ‘T) · (normh ‘A)))
Theorem	nmbdoplbt 9945	A lower bound for the norm of a bounded linear Hilbert space operator.
⊢ ((T ∈ BndLinOp ⋀ A ∈ ℋ ) → (normh ‘(T ‘A)) ≤ ((normop ‘T) · (normh ‘A)))
Theorem	nmcopexlem1 9946	Lemma for nmcopex 9952 (Theorem 3.5(i) of [Beran] p. 99). A sufficient condition for the norm of an operator to be real, based on its definition and the properties of supremum. Compared to Beran, we use a direct proof instead of a proof by contradiction.
Theorem	nmcopexlem2 9947	Lemma for nmcopex 9952. Apply definition of continuity. Note that we use 1 instead of 0.5 that Beran uses for epsilon (e = 0.5 in his proof).
Theorem	nmcopexlem3 9948	Lemma for nmcopex 9952. Move 1 / n out of the norm, using linearity.
Theorem	nmcopexlem4 9949	Lemma for nmcopex 9952. Properties of the infimum of a collection of integers whose reciprocals are less than a real number y (which will later become the "epsilon" of the epsilon/delta continuity definition df-cnop 9761). Note that ◡ < in the fourth hypothesis signifies infimum. (This lemma involves only real numbers and is independent of Hilbert space. The first two hypotheses aren't used.)
Theorem	nmcopexlem5 9950	Lemma for nmcopex 9952.
Theorem	nmcopexlem6 9951	Lemma for nmcopex 9952. Combine lemmas to obtain the result (with hypotheses to be eliminated).
Theorem	nmcopex 9952	The norm of a continuous linear Hilbert space operator exists. Theorem 3.5(i) of [Beran] p. 99.
⊢ T ∈ LinOp    &   ⊢ T ∈ ConOp    ⇒   ⊢ (normop ‘T) ∈ ℝ
Theorem	nmcoplb 9953	A lower bound for the norm of a continuous linear operator. Theorem 3.5(ii) of [Beran] p. 99.
⊢ T ∈ LinOp    &   ⊢ T ∈ ConOp    ⇒   ⊢ (A ∈ ℋ → (normh ‘(T ‘A)) ≤ ((normop ‘T) · (normh ‘A)))
Theorem	nmcopext 9954	The norm of a continuous linear Hilbert space operator exists. Theorem 3.5(i) of [Beran] p. 99.
⊢ ((T ∈ LinOp ⋀ T ∈ ConOp) → (normop ‘T) ∈ ℝ)
Theorem	nmcoplbt 9955	A lower bound for the norm of a continuous linear Hilbert space operator. Theorem 3.5(ii) of [Beran] p. 99.
⊢ ((T ∈ LinOp ⋀ T ∈ ConOp ⋀ A ∈ ℋ ) → (normh ‘(T ‘A)) ≤ ((normop ‘T) · (normh ‘A)))
Theorem	nmophm 9956	The norm of the scalar product of a bounded linear operator.
⊢ T ∈ BndLinOp    ⇒   ⊢ (A ∈ ℂ → (normop ‘(A ·op T)) = ((abs ‘A) · (normop ‘T)))
Theorem	bdophm 9957	The scalar product of a bounded linear operator is a bounded linear operator.
⊢ T ∈ BndLinOp    ⇒   ⊢ (A ∈ ℂ → (A ·op T) ∈ BndLinOp)
Theorem	lnopcon 9958	A condition equivalent to "T is continuous" when T is linear. Theorem 3.5(iii) of [Beran] p. 99.
⊢ T ∈ LinOp    ⇒   ⊢ (T ∈ ConOp ↔ ∃x ∈ ℝ ∀y ∈ ℋ (normh ‘(T ‘y)) ≤ (x · (normh ‘y)))
Theorem	lnopcont 9959	A condition equivalent to "T is continuous" when T is linear. Theorem 3.5(iii) of [Beran] p. 99.
⊢ (T ∈ LinOp → (T ∈ ConOp ↔ ∃x ∈ ℝ ∀y ∈ ℋ (normh ‘(T ‘y)) ≤ (x · (normh ‘y))))
Theorem	lnopcnbdt 9960	A linear operator is continuous iff it is bounded.
⊢ (T ∈ LinOp → (T ∈ ConOp ↔ T ∈ BndLinOp))
Theorem	lncnopbd 9961	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.
⊢ (T ∈ (LinOp ∩ ConOp) ↔ T ∈ BndLinOp)
Theorem	lncnbd 9962	A continuous linear operator is a bounded linear operator.
⊢ (LinOp ∩ ConOp) = BndLinOp
Theorem	lnopcnret 9963	A linear operator is continuous iff it is bounded.
⊢ (T ∈ LinOp → (T ∈ ConOp ↔ (normop ‘T) ∈ ℝ))
Theorem	lnfnl 9964	Basic property of a linear Hilbert space functional.
⊢ T ∈ LinFn    ⇒   ⊢ ((A ∈ ℂ ⋀ B ∈ ℋ ⋀ C ∈ ℋ ) → (T ‘((A ·h B) +h C)) = ((A · (T ‘B)) + (T ‘C)))
Theorem	lnfnf 9965	A linear Hilbert space functional is a functional.
⊢ T ∈ LinFn    ⇒   ⊢ T: ℋ –→ℂ
Theorem	lnfn0 9966	The value of a linear Hilbert space functional at zero is zero. Remark in [Beran] p. 99.
⊢ T ∈ LinFn    ⇒   ⊢ (T ‘0h) = 0
Theorem	lnfnadd 9967	Additive property of a linear Hilbert space functional.
⊢ T ∈ LinFn    ⇒   ⊢ ((A ∈ ℋ ⋀ B ∈ ℋ ) → (T ‘(A +h B)) = ((T ‘A) + (T ‘B)))
Theorem	lnfnmul 9968	Multiplicative property of a linear Hilbert space functional.
⊢ T ∈ LinFn    ⇒   ⊢ ((A ∈ ℂ ⋀ B ∈ ℋ ) → (T ‘(A ·h B)) = (A · (T ‘B)))
Theorem	lnfnaddmul 9969	Sum/product property of a linear Hilbert space functional.
⊢ T ∈ LinFn    ⇒   ⊢ ((A ∈ ℂ ⋀ B ∈ ℋ ⋀ C ∈ ℋ ) → (T ‘(B +h (A ·h C))) = ((T ‘B) + (A · (T ‘C))))
Theorem	lnfnsub 9970	Subtraction property for a linear Hilbert space functional.
⊢ T ∈ LinFn    ⇒   ⊢ ((A ∈ ℋ ⋀ B ∈ ℋ ) → (T ‘(A −h B)) = ((T ‘A) − (T ‘B)))
Theorem	lnfn0t 9971	The value of a linear Hilbert space functional at zero is zero. Remark in [Beran] p. 99.
⊢ (T ∈ LinFn → (T ‘0h) = 0)
Theorem	lnfnmult 9972	Multiplicative property of a linear Hilbert space functional.
⊢ ((T ∈ LinFn ⋀ A ∈ ℂ ⋀ B ∈ ℋ ) → (T ‘(A ·h B)) = (A · (T ‘B)))
Theorem	nmbdfnlb 9973	A lower bound for the norm of a bounded linear functional.
⊢ (T ∈ LinFn ⋀ (normfn ‘T) ∈ ℝ)    ⇒   ⊢ (A ∈ ℋ → (abs ‘(T ‘A)) ≤ ((normfn ‘T) · (normh ‘A)))
Theorem	nmbdfnlbt 9974	A lower bound for the norm of a bounded linear functional.
⊢ ((T ∈ LinFn ⋀ (normfn ‘T) ∈ ℝ ⋀ A ∈ ℋ ) → (abs ‘(T ‘A)) ≤ ((normfn ‘T) · (normh ‘A)))
Theorem	nmcfnexlem1 9975	Lemma for nmcfnex 9981. Show a condition for the norm of a functional to exist, based on its definition and the properties of supremum. Compared to Beran, we use a direct proof instead of a proof by contradiction.
Theorem	nmcfnexlem2 9976	Lemma for nmcfnex 9981. Apply definition of continuity. Note that we use 1 instead of 0.5 that Beran uses for epsilon (e = 0.5 in his proof).
Theorem	nmcfnexlem3 9977	Lemma for nmcfnex 9981. Move 1 / n out of the norm, using linearity.
Theorem	nmcfnexlem4 9978	Lemma for nmcfnex 9981. Properties of the infimum of the collection of integers whose reciprocals are less than the delta of the continuity definition.
Theorem	nmcfnexlem5 9979	Lemma for nmcfnex 9981.
Theorem	nmcfnexlem6 9980	Lemma for nmcfnex 9981. Combine lemmas to obtain the result (with hypotheses to be eliminated).
Theorem	nmcfnex 9981	The norm of a continuous linear Hilbert space functional exists. Theorem 3.5(i) of [Beran] p. 99.
⊢ T ∈ LinFn    &   ⊢ T ∈ ConFn    ⇒   ⊢ (normfn ‘T) ∈ ℝ
Theorem	nmcfnlb 9982	A lower bound for the norm of a continuous linear functional. Theorem 3.5(ii) of [Beran] p. 99.
⊢ T ∈ LinFn    &   ⊢ T ∈ ConFn    ⇒   ⊢ (A ∈ ℋ → (abs ‘(T ‘A)) ≤ ((normfn ‘T) · (normh ‘A)))
Theorem	nmcfnext 9983	The norm of a continuous linear Hilbert space functional exists. Theorem 3.5(i) of [Beran] p. 99.
⊢ ((T ∈ LinFn ⋀ T ∈ ConFn) → (normfn ‘T) ∈ ℝ)
Theorem	nmcfnlbt 9984	A lower bound of the norm of a continuous linear Hilbert space functional. Theorem 3.5(ii) of [Beran] p. 99.
⊢ ((T ∈ LinFn ⋀ T ∈ ConFn ⋀ A ∈ ℋ ) → (abs ‘(T ‘A)) ≤ ((normfn ‘T) · (normh ‘A)))
Theorem	lnfncon 9985	A condition equivalent to "T is continuous" when T is linear. Theorem 3.5(iii) of [Beran] p. 99.
⊢ T ∈ LinFn    ⇒   ⊢ (T ∈ ConFn ↔ ∃x ∈ ℝ ∀y ∈ ℋ (abs ‘(T ‘y)) ≤ (x · (normh ‘y)))
Theorem	lnfncont 9986	A condition equivalent to "T is continuous" when T is linear. Theorem 3.5(iii) of [Beran] p. 99.
⊢ (T ∈ LinFn → (T ∈ ConFn ↔ ∃x ∈ ℝ ∀y ∈ ℋ (abs ‘(T ‘y)) ≤ (x · (normh ‘y))))
Theorem	lnfncnbdt 9987	A linear functional is continuous iff it is bounded.
⊢ (T ∈ LinFn → (T ∈ ConFn ↔ (normfn ‘T) ∈ ℝ))
Theorem	nlelsh 9988	The null space of a linear functional is a subspace.
⊢ T ∈ LinFn    ⇒   ⊢ (null ‘T) ∈ Sℋ
Theorem	nlelch 9989	The null space of a continuous linear functional is a closed subspace. Remark 3.8 of [Beran] p. 103.
⊢ T ∈ LinFn    &   ⊢ T ∈ ConFn    ⇒   ⊢ (null ‘T) ∈ Cℋ
Riesz lemma
Theorem	riesz3 9990	A continuous linear functional can be expressed as an inner product. Existence part of Theorem 3.9 of [Beran] p. 104.
⊢ T ∈ LinFn    &   ⊢ T ∈ ConFn    ⇒   ⊢ ∃w ∈ ℋ ∀v ∈ ℋ (T ‘v) = (v ·ih w)
Theorem	riesz4 9991	A continuous linear functional can be expressed as an inner product. Uniqueness part of Theorem 3.9 of [Beran] p. 104.
⊢ T ∈ LinFn    &   ⊢ T ∈ ConFn    ⇒   ⊢ ∃!w ∈ ℋ ∀v ∈ ℋ (T ‘v) = (v ·ih w)
Theorem	riesz4t 9992	A continuous linear functional can be expressed as an inner product. Uniqueness part of Theorem 3.9 of [Beran] p. 104. See riesz2t 9994 for the bounded linear functional version.
⊢ (T ∈ (LinFn ∩ ConFn) → ∃!w ∈ ℋ ∀v ∈ ℋ (T ‘v) = (v ·ih w))
Theorem	riesz1t 9993	Part 1 of the Riesz representation theorem for bounded linear functionals. A linear functional is bounded iff its value can be expressed as an inner product. Part of Theorem 17.3 of [Halmos] p. 31. For part 2, see riesz2t 9994. For the continuous linear functional version, see riesz3 9990 and riesz4t 9992.
⊢ (T ∈ LinFn → ((normfn ‘T) ∈ ℝ ↔ ∃y ∈ ℋ ∀x ∈ ℋ (T ‘x) = (x ·ih y)))
Theorem	riesz2t 9994	Part 2 of the Riesz representation theorem for bounded linear functionals. The value of a bounded linear functional corresponds to a unique inner product. Part of Theorem 17.3 of [Halmos] p. 31. For part 1, see riesz1t 9993.
⊢ ((T ∈ LinFn ⋀ (normfn ‘T) ∈ ℝ) → ∃!y ∈ ℋ ∀x ∈ ℋ (T ‘x) = (x ·ih y))
Adjoints (cont.)
Theorem	cnlnadjlem1 9995	Lemma for cnlnadj 10004 (Theorem 3.10 of [Beran] p. 104: every continuous linear operator has an adjoint). The value of the auxiliary functional G.
Theorem	cnlnadjlem2 9996	Lemma for cnlnadj 10004. G is a continuous linear functional.
Theorem	cnlnadjlem3 9997	Lemma for cnlnadj 10004. By riesz4t 9992, B is the unique vector such that (T ‘v) ·ih y) = (v ·ih w) for all v.
Theorem	cnlnadjlem4 9998	Lemma for cnlnadj 10004. The values of auxiliary function F are vectors.
Theorem	cnlnadjlem5 9999	Lemma for cnlnadj 10004. F is an adjoint of T (later, we will show it is unique).
Theorem	cnlnadjlem6 10000	Lemma for cnlnadj 10004. F is linear.