P. 322 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32101-32200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lnopeq0i 32101*	A condition implying that a linear Hilbert space operator is identically zero. Unlike ho01i 31922 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 32102*	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 32103*	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 32104*	Lemma for lnopunii 32106. (Contributed by NM, 14-May-2005.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ ∀𝑥 ∈ ℋ (normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ (ℜ‘(𝐶 · ((𝑇‘𝐴) ·ih (𝑇‘𝐵)))) = (ℜ‘(𝐶 · (𝐴 ·ih 𝐵)))
Theorem	lnopunilem2 32105*	Lemma for lnopunii 32106. (Contributed by NM, 12-May-2005.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ ∀𝑥 ∈ ℋ (normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ ((𝑇‘𝐴) ·ih (𝑇‘𝐵)) = (𝐴 ·ih 𝐵)
Theorem	lnopunii 32106*	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 32107*	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 32108	Norm of a unitary Hilbert space operator. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.)
⊢ (( ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → (normop‘𝑇) = 1)
Theorem	unopbd 32109	A unitary operator is a bounded linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ UniOp → 𝑇 ∈ BndLinOp)
Theorem	lnophmlem1 32110*	Lemma for lnophmi 32112. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝑇 ∈ LinOp    &   ⊢ ∀𝑥 ∈ ℋ (𝑥 ·ih (𝑇‘𝑥)) ∈ ℝ    ⇒   ⊢ (𝐴 ·ih (𝑇‘𝐴)) ∈ ℝ
Theorem	lnophmlem2 32111*	Lemma for lnophmi 32112. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝑇 ∈ LinOp    &   ⊢ ∀𝑥 ∈ ℋ (𝑥 ·ih (𝑇‘𝑥)) ∈ ℝ    ⇒   ⊢ (𝐴 ·ih (𝑇‘𝐵)) = ((𝑇‘𝐴) ·ih 𝐵)
Theorem	lnophmi 32112*	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 32113*	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 32114	The sum of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 +op 𝑈) ∈ HrmOp)
Theorem	hmopm 32115	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 32116	The difference of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 −op 𝑈) ∈ HrmOp)
Theorem	hmopco 32117	The composition of two commuting Hermitian operators is Hermitian. (Contributed by NM, 22-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) → (𝑇 ∘ 𝑈) ∈ HrmOp)
Theorem	nmbdoplbi 32118	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 32119	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 32120*	Lemma for nmcopexi 32121 and nmcfnexi 32145. 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 32121	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 32122	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 32123	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 32124	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 32125	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 32126	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 32127*	Lemma for lnopconi 32128 and lnfnconi 32149. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ 𝐶 → 𝑆 ∈ ℝ)    &   ⊢ ((𝑇 ∈ 𝐶 ∧ 𝑦 ∈ ℋ) → (𝑁‘(𝑇‘𝑦)) ≤ (𝑆 · (normℎ‘𝑦)))    &   ⊢ (𝑇 ∈ 𝐶 ↔ ∀𝑥 ∈ ℋ ∀𝑧 ∈ ℝ+ ∃𝑦 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑦 → (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥))) < 𝑧))    &   ⊢ (𝑦 ∈ ℋ → (𝑁‘(𝑇‘𝑦)) ∈ ℝ)    &   ⊢ ((𝑤 ∈ ℋ ∧ 𝑥 ∈ ℋ) → (𝑇‘(𝑤 −ℎ 𝑥)) = ((𝑇‘𝑤)𝑀(𝑇‘𝑥)))    ⇒   ⊢ (𝑇 ∈ 𝐶 ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 · (normℎ‘𝑦)))
Theorem	lnopconi 32128*	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 32129*	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 32130	A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinOp → (𝑇 ∈ ContOp ↔ 𝑇 ∈ BndLinOp))
Theorem	lncnopbd 32131	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 32132	A continuous linear operator is a bounded linear operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
⊢ (LinOp ∩ ContOp) = BndLinOp
Theorem	lnopcnre 32133	A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinOp → (𝑇 ∈ ContOp ↔ (normop‘𝑇) ∈ ℝ))
Theorem	lnfnli 32134	Basic property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘((𝐴 ·ℎ 𝐵) +ℎ 𝐶)) = ((𝐴 · (𝑇‘𝐵)) + (𝑇‘𝐶)))
Theorem	lnfnfi 32135	A linear Hilbert space functional is a functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    ⇒   ⊢ 𝑇: ℋ⟶ℂ
Theorem	lnfn0i 32136	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 32137	Additive property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 +ℎ 𝐵)) = ((𝑇‘𝐴) + (𝑇‘𝐵)))
Theorem	lnfnmuli 32138	Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 ·ℎ 𝐵)) = (𝐴 · (𝑇‘𝐵)))
Theorem	lnfnaddmuli 32139	Sum/product property of a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘(𝐵 +ℎ (𝐴 ·ℎ 𝐶))) = ((𝑇‘𝐵) + (𝐴 · (𝑇‘𝐶))))
Theorem	lnfnsubi 32140	Subtraction property for a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 −ℎ 𝐵)) = ((𝑇‘𝐴) − (𝑇‘𝐵)))
Theorem	lnfn0 32141	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 32142	Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ LinFn ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 ·ℎ 𝐵)) = (𝐴 · (𝑇‘𝐵)))
Theorem	nmbdfnlbi 32143	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 32144	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 32145	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 32146	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 32147	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 32148	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 32149*	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 32150*	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 32151	A linear functional is continuous iff it is bounded. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinFn → (𝑇 ∈ ContFn ↔ (normfn‘𝑇) ∈ ℝ))
Theorem	imaelshi 32152	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 32153	The range of a linear operator is a subspace. (Contributed by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    ⇒   ⊢ ran 𝑇 ∈ Sℋ
Theorem	nlelshi 32154	The null space of a linear functional is a subspace. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    ⇒   ⊢ (null‘𝑇) ∈ Sℋ
Theorem	nlelchi 32155	The null space of a continuous linear functional is a closed subspace. Remark 3.8 of [Beran] p. 103. (Contributed by NM, 11-Feb-2006.) (Proof shortened by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    &   ⊢ 𝑇 ∈ ContFn    ⇒   ⊢ (null‘𝑇) ∈ Cℋ
20.6.11  Riesz lemma
Theorem	riesz3i 32156*	A continuous linear functional can be expressed as an inner product. Existence part of Theorem 3.9 of [Beran] p. 104. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    &   ⊢ 𝑇 ∈ ContFn    ⇒   ⊢ ∃𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih 𝑤)
Theorem	riesz4i 32157*	A continuous linear functional can be expressed as an inner product. Uniqueness part of Theorem 3.9 of [Beran] p. 104. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    &   ⊢ 𝑇 ∈ ContFn    ⇒   ⊢ ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih 𝑤)
Theorem	riesz4 32158*	A continuous linear functional can be expressed as an inner product. Uniqueness part of Theorem 3.9 of [Beran] p. 104. See riesz2 32160 for the bounded linear functional version. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ (LinFn ∩ ContFn) → ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih 𝑤))
Theorem	riesz1 32159*	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 riesz2 32160. For the continuous linear functional version, see riesz3i 32156 and riesz4 32158. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinFn → ((normfn‘𝑇) ∈ ℝ ↔ ∃𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑥 ·ih 𝑦)))
Theorem	riesz2 32160*	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 riesz1 32159. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ LinFn ∧ (normfn‘𝑇) ∈ ℝ) → ∃!𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑥 ·ih 𝑦))
20.6.12  Adjoints (cont.)
Theorem	cnlnadjlem1 32161*	Lemma for cnlnadji 32170 (Theorem 3.10 of [Beran] p. 104: every continuous linear operator has an adjoint). The value of the auxiliary functional 𝐺. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑇 ∈ ContOp    &   ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦))    ⇒   ⊢ (𝐴 ∈ ℋ → (𝐺‘𝐴) = ((𝑇‘𝐴) ·ih 𝑦))
Theorem	cnlnadjlem2 32162*	Lemma for cnlnadji 32170. 𝐺 is a continuous linear functional. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑇 ∈ ContOp    &   ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦))    ⇒   ⊢ (𝑦 ∈ ℋ → (𝐺 ∈ LinFn ∧ 𝐺 ∈ ContFn))
Theorem	cnlnadjlem3 32163*	Lemma for cnlnadji 32170. By riesz4 32158, 𝐵 is the unique vector such that (𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤) for all 𝑣. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑇 ∈ ContOp    &   ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦))    &   ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))    ⇒   ⊢ (𝑦 ∈ ℋ → 𝐵 ∈ ℋ)
Theorem	cnlnadjlem4 32164*	Lemma for cnlnadji 32170. The values of auxiliary function 𝐹 are vectors. (Contributed by NM, 17-Feb-2006.) (Proof shortened by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑇 ∈ ContOp    &   ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦))    &   ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))    &   ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵)    ⇒   ⊢ (𝐴 ∈ ℋ → (𝐹‘𝐴) ∈ ℋ)
Theorem	cnlnadjlem5 32165*	Lemma for cnlnadji 32170. 𝐹 is an adjoint of 𝑇 (later, we will show it is unique). (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑇 ∈ ContOp    &   ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦))    &   ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))    &   ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵)    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝑇‘𝐶) ·ih 𝐴) = (𝐶 ·ih (𝐹‘𝐴)))
Theorem	cnlnadjlem6 32166*	Lemma for cnlnadji 32170. 𝐹 is linear. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑇 ∈ ContOp    &   ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦))    &   ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))    &   ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵)    ⇒   ⊢ 𝐹 ∈ LinOp
Theorem	cnlnadjlem7 32167*	Lemma for cnlnadji 32170. Helper lemma to show that 𝐹 is continuous. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑇 ∈ ContOp    &   ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦))    &   ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))    &   ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵)    ⇒   ⊢ (𝐴 ∈ ℋ → (normℎ‘(𝐹‘𝐴)) ≤ ((normop‘𝑇) · (normℎ‘𝐴)))
Theorem	cnlnadjlem8 32168*	Lemma for cnlnadji 32170. 𝐹 is continuous. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑇 ∈ ContOp    &   ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦))    &   ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))    &   ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵)    ⇒   ⊢ 𝐹 ∈ ContOp
Theorem	cnlnadjlem9 32169*	Lemma for cnlnadji 32170. 𝐹 provides an example showing the existence of a continuous linear adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑇 ∈ ContOp    &   ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦))    &   ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))    &   ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵)    ⇒   ⊢ ∃𝑡 ∈ (LinOp ∩ ContOp)∀𝑥 ∈ ℋ ∀𝑧 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑧) = (𝑥 ·ih (𝑡‘𝑧))
Theorem	cnlnadji 32170*	Every continuous linear operator has an adjoint. Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑇 ∈ ContOp    ⇒   ⊢ ∃𝑡 ∈ (LinOp ∩ ContOp)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑡‘𝑦))
Theorem	cnlnadjeui 32171*	Every continuous linear operator has a unique adjoint. Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑇 ∈ ContOp    ⇒   ⊢ ∃!𝑡 ∈ (LinOp ∩ ContOp)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑡‘𝑦))
Theorem	cnlnadjeu 32172*	Every continuous linear operator has a unique adjoint. Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ (LinOp ∩ ContOp) → ∃!𝑡 ∈ (LinOp ∩ ContOp)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑡‘𝑦)))
Theorem	cnlnadj 32173*	Every continuous linear operator has an adjoint. Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ (LinOp ∩ ContOp) → ∃𝑡 ∈ (LinOp ∩ ContOp)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑡‘𝑦)))
Theorem	cnlnssadj 32174	Every continuous linear Hilbert space operator has an adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
⊢ (LinOp ∩ ContOp) ⊆ dom adjℎ
Theorem	bdopssadj 32175	Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)
⊢ BndLinOp ⊆ dom adjℎ
Theorem	bdopadj 32176	Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ BndLinOp → 𝑇 ∈ dom adjℎ)
Theorem	adjbdln 32177	The adjoint of a bounded linear operator is a bounded linear operator. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ BndLinOp → (adjℎ‘𝑇) ∈ BndLinOp)
Theorem	adjbdlnb 32178	An operator is bounded and linear iff its adjoint is. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ BndLinOp ↔ (adjℎ‘𝑇) ∈ BndLinOp)
Theorem	adjbd1o 32179	The mapping of adjoints of bounded linear operators is one-to-one onto. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)
⊢ (adjℎ ↾ BndLinOp):BndLinOp–1-1-onto→BndLinOp
Theorem	adjlnop 32180	The adjoint of an operator is linear. Proposition 1 of [AkhiezerGlazman] p. 80. (Contributed by NM, 17-Jun-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ dom adjℎ → (adjℎ‘𝑇) ∈ LinOp)
Theorem	adjsslnop 32181	Every operator with an adjoint is linear. (Contributed by NM, 17-Jun-2006.) (New usage is discouraged.)
⊢ dom adjℎ ⊆ LinOp
Theorem	nmopadjlei 32182	Property of the norm of an adjoint. Part of proof of Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ BndLinOp    ⇒   ⊢ (𝐴 ∈ ℋ → (normℎ‘((adjℎ‘𝑇)‘𝐴)) ≤ ((normop‘𝑇) · (normℎ‘𝐴)))
Theorem	nmopadjlem 32183	Lemma for nmopadji 32184. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ BndLinOp    ⇒   ⊢ (normop‘(adjℎ‘𝑇)) ≤ (normop‘𝑇)
Theorem	nmopadji 32184	Property of the norm of an adjoint. Theorem 3.11(v) of [Beran] p. 106. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ BndLinOp    ⇒   ⊢ (normop‘(adjℎ‘𝑇)) = (normop‘𝑇)
Theorem	adjeq0 32185	An operator is zero iff its adjoint is zero. Theorem 3.11(i) of [Beran] p. 106. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 = 0hop ↔ (adjℎ‘𝑇) = 0hop )
Theorem	adjmul 32186	The adjoint of the scalar product of an operator. Theorem 3.11(ii) of [Beran] p. 106. (Contributed by NM, 21-Feb-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑇 ∈ dom adjℎ) → (adjℎ‘(𝐴 ·op 𝑇)) = ((∗‘𝐴) ·op (adjℎ‘𝑇)))
Theorem	adjadd 32187	The adjoint of the sum of two operators. Theorem 3.11(iii) of [Beran] p. 106. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.)
⊢ ((𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ) → (adjℎ‘(𝑆 +op 𝑇)) = ((adjℎ‘𝑆) +op (adjℎ‘𝑇)))
Theorem	nmoptrii 32188	Triangle inequality for the norms of bounded linear operators. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
⊢ 𝑆 ∈ BndLinOp    &   ⊢ 𝑇 ∈ BndLinOp    ⇒   ⊢ (normop‘(𝑆 +op 𝑇)) ≤ ((normop‘𝑆) + (normop‘𝑇))
Theorem	nmopcoi 32189	Upper bound for the norm of the composition of two bounded linear operators. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
⊢ 𝑆 ∈ BndLinOp    &   ⊢ 𝑇 ∈ BndLinOp    ⇒   ⊢ (normop‘(𝑆 ∘ 𝑇)) ≤ ((normop‘𝑆) · (normop‘𝑇))
Theorem	bdophsi 32190	The sum of two bounded linear operators is a bounded linear operator. (Contributed by NM, 9-Mar-2006.) (New usage is discouraged.)
⊢ 𝑆 ∈ BndLinOp    &   ⊢ 𝑇 ∈ BndLinOp    ⇒   ⊢ (𝑆 +op 𝑇) ∈ BndLinOp
Theorem	bdophdi 32191	The difference between two bounded linear operators is bounded. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
⊢ 𝑆 ∈ BndLinOp    &   ⊢ 𝑇 ∈ BndLinOp    ⇒   ⊢ (𝑆 −op 𝑇) ∈ BndLinOp
Theorem	bdopcoi 32192	The composition of two bounded linear operators is bounded. (Contributed by NM, 9-Mar-2006.) (New usage is discouraged.)
⊢ 𝑆 ∈ BndLinOp    &   ⊢ 𝑇 ∈ BndLinOp    ⇒   ⊢ (𝑆 ∘ 𝑇) ∈ BndLinOp
Theorem	nmoptri2i 32193	Triangle-type inequality for the norms of bounded linear operators. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
⊢ 𝑆 ∈ BndLinOp    &   ⊢ 𝑇 ∈ BndLinOp    ⇒   ⊢ ((normop‘𝑆) − (normop‘𝑇)) ≤ (normop‘(𝑆 +op 𝑇))
Theorem	adjcoi 32194	The adjoint of a composition of bounded linear operators. Theorem 3.11(viii) of [Beran] p. 106. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
⊢ 𝑆 ∈ BndLinOp    &   ⊢ 𝑇 ∈ BndLinOp    ⇒   ⊢ (adjℎ‘(𝑆 ∘ 𝑇)) = ((adjℎ‘𝑇) ∘ (adjℎ‘𝑆))
Theorem	nmopcoadji 32195	The norm of an operator composed with its adjoint. Part of Theorem 3.11(vi) of [Beran] p. 106. (Contributed by NM, 8-Mar-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ BndLinOp    ⇒   ⊢ (normop‘((adjℎ‘𝑇) ∘ 𝑇)) = ((normop‘𝑇)↑2)
Theorem	nmopcoadj2i 32196	The norm of an operator composed with its adjoint. Part of Theorem 3.11(vi) of [Beran] p. 106. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ BndLinOp    ⇒   ⊢ (normop‘(𝑇 ∘ (adjℎ‘𝑇))) = ((normop‘𝑇)↑2)
Theorem	nmopcoadj0i 32197	An operator composed with its adjoint is zero iff the operator is zero. Theorem 3.11(vii) of [Beran] p. 106. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ BndLinOp    ⇒   ⊢ ((𝑇 ∘ (adjℎ‘𝑇)) = 0hop ↔ 𝑇 = 0hop )
20.6.13  Quantum computation error bound theorem
Theorem	unierri 32198	If we approximate a chain of unitary transformations (quantum computer gates) 𝐹, 𝐺 by other unitary transformations 𝑆, 𝑇, the error increases at most additively. Equation 4.73 of [NielsenChuang] p. 195. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
⊢ 𝐹 ∈ UniOp    &   ⊢ 𝐺 ∈ UniOp    &   ⊢ 𝑆 ∈ UniOp    &   ⊢ 𝑇 ∈ UniOp    ⇒   ⊢ (normop‘((𝐹 ∘ 𝐺) −op (𝑆 ∘ 𝑇))) ≤ ((normop‘(𝐹 −op 𝑆)) + (normop‘(𝐺 −op 𝑇)))
20.6.14  Dirac bra-ket notation (cont.)
Theorem	branmfn 32199	The norm of the bra function. (Contributed by NM, 24-May-2006.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (normfn‘(bra‘𝐴)) = (normℎ‘𝐴))
Theorem	brabn 32200	The bra of a vector is a bounded functional. (Contributed by NM, 26-May-2006.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (normfn‘(bra‘𝐴)) ∈ ℝ)