P. 320 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 31901-32000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lnopcon 31901*	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 31902	A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinOp → (𝑇 ∈ ContOp ↔ 𝑇 ∈ BndLinOp))
Theorem	lncnopbd 31903	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 31904	A continuous linear operator is a bounded linear operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
⊢ (LinOp ∩ ContOp) = BndLinOp
Theorem	lnopcnre 31905	A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinOp → (𝑇 ∈ ContOp ↔ (normop‘𝑇) ∈ ℝ))
Theorem	lnfnli 31906	Basic property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘((𝐴 ·ℎ 𝐵) +ℎ 𝐶)) = ((𝐴 · (𝑇‘𝐵)) + (𝑇‘𝐶)))
Theorem	lnfnfi 31907	A linear Hilbert space functional is a functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    ⇒   ⊢ 𝑇: ℋ⟶ℂ
Theorem	lnfn0i 31908	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 31909	Additive property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 +ℎ 𝐵)) = ((𝑇‘𝐴) + (𝑇‘𝐵)))
Theorem	lnfnmuli 31910	Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 ·ℎ 𝐵)) = (𝐴 · (𝑇‘𝐵)))
Theorem	lnfnaddmuli 31911	Sum/product property of a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘(𝐵 +ℎ (𝐴 ·ℎ 𝐶))) = ((𝑇‘𝐵) + (𝐴 · (𝑇‘𝐶))))
Theorem	lnfnsubi 31912	Subtraction property for a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 −ℎ 𝐵)) = ((𝑇‘𝐴) − (𝑇‘𝐵)))
Theorem	lnfn0 31913	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 31914	Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ LinFn ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 ·ℎ 𝐵)) = (𝐴 · (𝑇‘𝐵)))
Theorem	nmbdfnlbi 31915	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 31916	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 31917	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 31918	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 31919	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 31920	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 31921*	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 31922*	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 31923	A linear functional is continuous iff it is bounded. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinFn → (𝑇 ∈ ContFn ↔ (normfn‘𝑇) ∈ ℝ))
Theorem	imaelshi 31924	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 31925	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 31926	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 31927	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 31928*	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 31929*	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 31930*	A continuous linear functional can be expressed as an inner product. Uniqueness part of Theorem 3.9 of [Beran] p. 104. See riesz2 31932 for the bounded linear functional version. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ (LinFn ∩ ContFn) → ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih 𝑤))
Theorem	riesz1 31931*	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 31932. For the continuous linear functional version, see riesz3i 31928 and riesz4 31930. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinFn → ((normfn‘𝑇) ∈ ℝ ↔ ∃𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑥 ·ih 𝑦)))
Theorem	riesz2 31932*	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 31931. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ LinFn ∧ (normfn‘𝑇) ∈ ℝ) → ∃!𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑥 ·ih 𝑦))
20.6.12  Adjoints (cont.)
Theorem	cnlnadjlem1 31933*	Lemma for cnlnadji 31942 (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 31934*	Lemma for cnlnadji 31942. 𝐺 is a continuous linear functional. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑇 ∈ ContOp    &   ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦))    ⇒   ⊢ (𝑦 ∈ ℋ → (𝐺 ∈ LinFn ∧ 𝐺 ∈ ContFn))
Theorem	cnlnadjlem3 31935*	Lemma for cnlnadji 31942. By riesz4 31930, 𝐵 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 31936*	Lemma for cnlnadji 31942. 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 31937*	Lemma for cnlnadji 31942. 𝐹 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 31938*	Lemma for cnlnadji 31942. 𝐹 is linear. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑇 ∈ ContOp    &   ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦))    &   ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))    &   ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵)    ⇒   ⊢ 𝐹 ∈ LinOp
Theorem	cnlnadjlem7 31939*	Lemma for cnlnadji 31942. 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 31940*	Lemma for cnlnadji 31942. 𝐹 is continuous. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑇 ∈ ContOp    &   ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦))    &   ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))    &   ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵)    ⇒   ⊢ 𝐹 ∈ ContOp
Theorem	cnlnadjlem9 31941*	Lemma for cnlnadji 31942. 𝐹 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 31942*	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 31943*	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 31944*	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 31945*	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 31946	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 31947	Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)
⊢ BndLinOp ⊆ dom adjℎ
Theorem	bdopadj 31948	Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ BndLinOp → 𝑇 ∈ dom adjℎ)
Theorem	adjbdln 31949	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 31950	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 31951	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 31952	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 31953	Every operator with an adjoint is linear. (Contributed by NM, 17-Jun-2006.) (New usage is discouraged.)
⊢ dom adjℎ ⊆ LinOp
Theorem	nmopadjlei 31954	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 31955	Lemma for nmopadji 31956. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ BndLinOp    ⇒   ⊢ (normop‘(adjℎ‘𝑇)) ≤ (normop‘𝑇)
Theorem	nmopadji 31956	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 31957	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 31958	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 31959	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 31960	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 31961	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 31962	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 31963	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 31964	The composition of two bounded linear operators is bounded. (Contributed by NM, 9-Mar-2006.) (New usage is discouraged.)
⊢ 𝑆 ∈ BndLinOp    &   ⊢ 𝑇 ∈ BndLinOp    ⇒   ⊢ (𝑆 ∘ 𝑇) ∈ BndLinOp
Theorem	nmoptri2i 31965	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 31966	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 31967	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 31968	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 31969	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 31970	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 31971	The norm of the bra function. (Contributed by NM, 24-May-2006.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (normfn‘(bra‘𝐴)) = (normℎ‘𝐴))
Theorem	brabn 31972	The bra of a vector is a bounded functional. (Contributed by NM, 26-May-2006.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (normfn‘(bra‘𝐴)) ∈ ℝ)
Theorem	rnbra 31973	The set of bras equals the set of continuous linear functionals. (Contributed by NM, 26-May-2006.) (New usage is discouraged.)
⊢ ran bra = (LinFn ∩ ContFn)
Theorem	bra11 31974	The bra function maps vectors one-to-one onto the set of continuous linear functionals. (Contributed by NM, 26-May-2006.) (Proof shortened by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ bra: ℋ–1-1-onto→(LinFn ∩ ContFn)
Theorem	bracnln 31975	A bra is a continuous linear functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (bra‘𝐴) ∈ (LinFn ∩ ContFn))
Theorem	cnvbraval 31976*	Value of the converse of the bra function. Based on the Riesz Lemma riesz4 31930, this very important theorem not only justifies the Dirac bra-ket notation, but allows to extract a unique vector from any continuous linear functional from which the functional can be recovered; i.e. a single vector can "store" all of the information contained in any entire continuous linear functional (mapping from ℋ to ℂ). (Contributed by NM, 26-May-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ (LinFn ∩ ContFn) → (◡bra‘𝑇) = (℩𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑥 ·ih 𝑦)))
Theorem	cnvbracl 31977	Closure of the converse of the bra function. (Contributed by NM, 26-May-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ (LinFn ∩ ContFn) → (◡bra‘𝑇) ∈ ℋ)
Theorem	cnvbrabra 31978	The converse bra of the bra of a vector is the vector itself. (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (◡bra‘(bra‘𝐴)) = 𝐴)
Theorem	bracnvbra 31979	The bra of the converse bra of a continuous linear functional. (Contributed by NM, 31-May-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ (LinFn ∩ ContFn) → (bra‘(◡bra‘𝑇)) = 𝑇)
Theorem	bracnlnval 31980*	The vector that a continuous linear functional is the bra of. (Contributed by NM, 26-May-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ (LinFn ∩ ContFn) → 𝑇 = (bra‘(℩𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑥 ·ih 𝑦))))
Theorem	cnvbramul 31981	Multiplication property of the converse bra function. (Contributed by NM, 31-May-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑇 ∈ (LinFn ∩ ContFn)) → (◡bra‘(𝐴 ·fn 𝑇)) = ((∗‘𝐴) ·ℎ (◡bra‘𝑇)))
Theorem	kbass1 31982	Dirac bra-ket associative law ( ∣ 𝐴⟩⟨𝐵 ∣ ) ∣ 𝐶⟩ = ∣ 𝐴⟩(⟨𝐵 ∣ 𝐶⟩), i.e., the juxtaposition of an outer product with a ket equals a bra juxtaposed with an inner product. Since ⟨𝐵 ∣ 𝐶⟩ is a complex number, it is the first argument in the inner product ·ℎ that it is mapped to, although in Dirac notation it is placed after the ket. (Contributed by NM, 15-May-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ketbra 𝐵)‘𝐶) = (((bra‘𝐵)‘𝐶) ·ℎ 𝐴))
Theorem	kbass2 31983	Dirac bra-ket associative law (⟨𝐴 ∣ 𝐵⟩)⟨𝐶 ∣ = ⟨𝐴 ∣ ( ∣ 𝐵⟩⟨𝐶 ∣ ), i.e., the juxtaposition of an inner product with a bra equals a ket juxtaposed with an outer product. (Contributed by NM, 23-May-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (((bra‘𝐴)‘𝐵) ·fn (bra‘𝐶)) = ((bra‘𝐴) ∘ (𝐵 ketbra 𝐶)))
Theorem	kbass3 31984	Dirac bra-ket associative law ⟨𝐴 ∣ 𝐵⟩⟨𝐶 ∣ 𝐷⟩ = (⟨𝐴 ∣ 𝐵⟩⟨𝐶 ∣ ) ∣ 𝐷⟩. (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → (((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝐷)) = ((((bra‘𝐴)‘𝐵) ·fn (bra‘𝐶))‘𝐷))
Theorem	kbass4 31985	Dirac bra-ket associative law ⟨𝐴 ∣ 𝐵⟩⟨𝐶 ∣ 𝐷⟩ = ⟨𝐴 ∣ ( ∣ 𝐵⟩⟨𝐶 ∣ 𝐷⟩). (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → (((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝐷)) = ((bra‘𝐴)‘(((bra‘𝐶)‘𝐷) ·ℎ 𝐵)))
Theorem	kbass5 31986	Dirac bra-ket associative law ( ∣ 𝐴⟩⟨𝐵 ∣ )( ∣ 𝐶⟩⟨𝐷 ∣ ) = (( ∣ 𝐴⟩⟨𝐵 ∣ ) ∣ 𝐶⟩)⟨𝐷 ∣. (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 ketbra 𝐵) ∘ (𝐶 ketbra 𝐷)) = (((𝐴 ketbra 𝐵)‘𝐶) ketbra 𝐷))
Theorem	kbass6 31987	Dirac bra-ket associative law ( ∣ 𝐴⟩⟨𝐵 ∣ )( ∣ 𝐶⟩⟨𝐷 ∣ ) = ∣ 𝐴⟩(⟨𝐵 ∣ ( ∣ 𝐶⟩⟨𝐷 ∣ )). (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 ketbra 𝐵) ∘ (𝐶 ketbra 𝐷)) = (𝐴 ketbra (◡bra‘((bra‘𝐵) ∘ (𝐶 ketbra 𝐷)))))
20.6.15  Positive operators (cont.)
Theorem	leopg 31988*	Ordering relation for positive operators. Definition of positive operator ordering in [Kreyszig] p. 470. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐵) → (𝑇 ≤op 𝑈 ↔ ((𝑈 −op 𝑇) ∈ HrmOp ∧ ∀𝑥 ∈ ℋ 0 ≤ (((𝑈 −op 𝑇)‘𝑥) ·ih 𝑥))))
Theorem	leop 31989*	Ordering relation for operators. Definition of positive operator ordering in [Kreyszig] p. 470. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 ≤op 𝑈 ↔ ∀𝑥 ∈ ℋ 0 ≤ (((𝑈 −op 𝑇)‘𝑥) ·ih 𝑥)))
Theorem	leop2 31990*	Ordering relation for operators. Definition of operator ordering in [Young] p. 141. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 ≤op 𝑈 ↔ ∀𝑥 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑥) ≤ ((𝑈‘𝑥) ·ih 𝑥)))
Theorem	leop3 31991	Operator ordering in terms of a positive operator. Definition of operator ordering in [Retherford] p. 49. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 ≤op 𝑈 ↔ 0hop ≤op (𝑈 −op 𝑇)))
Theorem	leoppos 31992*	Binary relation defining a positive operator. Definition VI.1 of [Retherford] p. 49. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ HrmOp → ( 0hop ≤op 𝑇 ↔ ∀𝑥 ∈ ℋ 0 ≤ ((𝑇‘𝑥) ·ih 𝑥)))
Theorem	leoprf2 31993	The ordering relation for operators is reflexive. (Contributed by NM, 24-Jul-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → 𝑇 ≤op 𝑇)
Theorem	leoprf 31994	The ordering relation for operators is reflexive. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ HrmOp → 𝑇 ≤op 𝑇)
Theorem	leopsq 31995	The square of a Hermitian operator is positive. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ HrmOp → 0hop ≤op (𝑇 ∘ 𝑇))
Theorem	0leop 31996	The zero operator is a positive operator. (The literature calls it "positive", even though in some sense it is really "nonnegative".) Part of Example 12.2(i) in [Young] p. 142. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
⊢ 0hop ≤op 0hop
Theorem	idleop 31997	The identity operator is a positive operator. Part of Example 12.2(i) in [Young] p. 142. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
⊢ 0hop ≤op Iop
Theorem	leopadd 31998	The sum of two positive operators is positive. Exercise 1(i) of [Retherford] p. 49. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.)
⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ ( 0hop ≤op 𝑇 ∧ 0hop ≤op 𝑈)) → 0hop ≤op (𝑇 +op 𝑈))
Theorem	leopmuli 31999	The scalar product of a nonnegative real and a positive operator is a positive operator. Exercise 1(ii) of [Retherford] p. 49. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.)
⊢ (((𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp) ∧ (0 ≤ 𝐴 ∧ 0hop ≤op 𝑇)) → 0hop ≤op (𝐴 ·op 𝑇))
Theorem	leopmul 32000	The scalar product of a positive real and a positive operator is a positive operator. Exercise 1(ii) of [Retherford] p. 49. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 0 < 𝐴) → ( 0hop ≤op 𝑇 ↔ 0hop ≤op (𝐴 ·op 𝑇)))