P. 324 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32301-32400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lnfnli 32301	Basic property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘((𝐴 ·ℎ 𝐵) +ℎ 𝐶)) = ((𝐴 · (𝑇‘𝐵)) + (𝑇‘𝐶)))
Theorem	lnfnfi 32302	A linear Hilbert space functional is a functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    ⇒   ⊢ 𝑇: ℋ⟶ℂ
Theorem	lnfn0i 32303	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 32304	Additive property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 +ℎ 𝐵)) = ((𝑇‘𝐴) + (𝑇‘𝐵)))
Theorem	lnfnmuli 32305	Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 ·ℎ 𝐵)) = (𝐴 · (𝑇‘𝐵)))
Theorem	lnfnaddmuli 32306	Sum/product property of a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘(𝐵 +ℎ (𝐴 ·ℎ 𝐶))) = ((𝑇‘𝐵) + (𝐴 · (𝑇‘𝐶))))
Theorem	lnfnsubi 32307	Subtraction property for a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinFn    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 −ℎ 𝐵)) = ((𝑇‘𝐴) − (𝑇‘𝐵)))
Theorem	lnfn0 32308	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 32309	Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ LinFn ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 ·ℎ 𝐵)) = (𝐴 · (𝑇‘𝐵)))
Theorem	nmbdfnlbi 32310	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 32311	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 32312	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 32313	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 32314	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 32315	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 32316*	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 32317*	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 32318	A linear functional is continuous iff it is bounded. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinFn → (𝑇 ∈ ContFn ↔ (normfn‘𝑇) ∈ ℝ))
Theorem	imaelshi 32319	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 32320	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 32321	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 32322	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 32323*	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 32324*	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 32325*	A continuous linear functional can be expressed as an inner product. Uniqueness part of Theorem 3.9 of [Beran] p. 104. See riesz2 32327 for the bounded linear functional version. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ (LinFn ∩ ContFn) → ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih 𝑤))
Theorem	riesz1 32326*	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 32327. For the continuous linear functional version, see riesz3i 32323 and riesz4 32325. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinFn → ((normfn‘𝑇) ∈ ℝ ↔ ∃𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑥 ·ih 𝑦)))
Theorem	riesz2 32327*	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 32326. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ LinFn ∧ (normfn‘𝑇) ∈ ℝ) → ∃!𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑥 ·ih 𝑦))
20.6.12  Adjoints (cont.)
Theorem	cnlnadjlem1 32328*	Lemma for cnlnadji 32337 (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 32329*	Lemma for cnlnadji 32337. 𝐺 is a continuous linear functional. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑇 ∈ ContOp    &   ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦))    ⇒   ⊢ (𝑦 ∈ ℋ → (𝐺 ∈ LinFn ∧ 𝐺 ∈ ContFn))
Theorem	cnlnadjlem3 32330*	Lemma for cnlnadji 32337. By riesz4 32325, 𝐵 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 32331*	Lemma for cnlnadji 32337. 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 32332*	Lemma for cnlnadji 32337. 𝐹 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 32333*	Lemma for cnlnadji 32337. 𝐹 is linear. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑇 ∈ ContOp    &   ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦))    &   ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))    &   ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵)    ⇒   ⊢ 𝐹 ∈ LinOp
Theorem	cnlnadjlem7 32334*	Lemma for cnlnadji 32337. 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 32335*	Lemma for cnlnadji 32337. 𝐹 is continuous. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑇 ∈ ContOp    &   ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦))    &   ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))    &   ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵)    ⇒   ⊢ 𝐹 ∈ ContOp
Theorem	cnlnadjlem9 32336*	Lemma for cnlnadji 32337. 𝐹 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 32337*	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 32338*	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 32339*	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 32340*	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 32341	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 32342	Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)
⊢ BndLinOp ⊆ dom adjℎ
Theorem	bdopadj 32343	Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ BndLinOp → 𝑇 ∈ dom adjℎ)
Theorem	adjbdln 32344	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 32345	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 32346	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 32347	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 32348	Every operator with an adjoint is linear. (Contributed by NM, 17-Jun-2006.) (New usage is discouraged.)
⊢ dom adjℎ ⊆ LinOp
Theorem	nmopadjlei 32349	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 32350	Lemma for nmopadji 32351. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ BndLinOp    ⇒   ⊢ (normop‘(adjℎ‘𝑇)) ≤ (normop‘𝑇)
Theorem	nmopadji 32351	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 32352	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 32353	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 32354	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 32355	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 32356	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 32357	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 32358	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 32359	The composition of two bounded linear operators is bounded. (Contributed by NM, 9-Mar-2006.) (New usage is discouraged.)
⊢ 𝑆 ∈ BndLinOp    &   ⊢ 𝑇 ∈ BndLinOp    ⇒   ⊢ (𝑆 ∘ 𝑇) ∈ BndLinOp
Theorem	nmoptri2i 32360	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 32361	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 32362	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 32363	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 32364	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 32365	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 32366	The norm of the bra function. (Contributed by NM, 24-May-2006.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (normfn‘(bra‘𝐴)) = (normℎ‘𝐴))
Theorem	brabn 32367	The bra of a vector is a bounded functional. (Contributed by NM, 26-May-2006.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (normfn‘(bra‘𝐴)) ∈ ℝ)
Theorem	rnbra 32368	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 32369	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 32370	A bra is a continuous linear functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (bra‘𝐴) ∈ (LinFn ∩ ContFn))
Theorem	cnvbraval 32371*	Value of the converse of the bra function. Based on the Riesz Lemma riesz4 32325, 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 32372	Closure of the converse of the bra function. (Contributed by NM, 26-May-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ (LinFn ∩ ContFn) → (◡bra‘𝑇) ∈ ℋ)
Theorem	cnvbrabra 32373	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 32374	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 32375*	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 32376	Multiplication property of the converse bra function. (Contributed by NM, 31-May-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑇 ∈ (LinFn ∩ ContFn)) → (◡bra‘(𝐴 ·fn 𝑇)) = ((∗‘𝐴) ·ℎ (◡bra‘𝑇)))
Theorem	kbass1 32377	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 32378	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 32379	Dirac bra-ket associative law ⟨𝐴 ∣ 𝐵⟩⟨𝐶 ∣ 𝐷⟩ = (⟨𝐴 ∣ 𝐵⟩⟨𝐶 ∣ ) ∣ 𝐷⟩. (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → (((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝐷)) = ((((bra‘𝐴)‘𝐵) ·fn (bra‘𝐶))‘𝐷))
Theorem	kbass4 32380	Dirac bra-ket associative law ⟨𝐴 ∣ 𝐵⟩⟨𝐶 ∣ 𝐷⟩ = ⟨𝐴 ∣ ( ∣ 𝐵⟩⟨𝐶 ∣ 𝐷⟩). (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → (((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝐷)) = ((bra‘𝐴)‘(((bra‘𝐶)‘𝐷) ·ℎ 𝐵)))
Theorem	kbass5 32381	Dirac bra-ket associative law ( ∣ 𝐴⟩⟨𝐵 ∣ )( ∣ 𝐶⟩⟨𝐷 ∣ ) = (( ∣ 𝐴⟩⟨𝐵 ∣ ) ∣ 𝐶⟩)⟨𝐷 ∣. (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 ketbra 𝐵) ∘ (𝐶 ketbra 𝐷)) = (((𝐴 ketbra 𝐵)‘𝐶) ketbra 𝐷))
Theorem	kbass6 32382	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 32383*	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 32384*	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 32385*	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 32386	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 32387*	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 32388	The ordering relation for operators is reflexive. (Contributed by NM, 24-Jul-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → 𝑇 ≤op 𝑇)
Theorem	leoprf 32389	The ordering relation for operators is reflexive. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ HrmOp → 𝑇 ≤op 𝑇)
Theorem	leopsq 32390	The square of a Hermitian operator is positive. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ HrmOp → 0hop ≤op (𝑇 ∘ 𝑇))
Theorem	0leop 32391	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 32392	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 32393	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 32394	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 32395	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 𝑇)))
Theorem	leopmul2i 32396	Scalar product applied to operator ordering. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)
⊢ (((𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (0 ≤ 𝐴 ∧ 𝑇 ≤op 𝑈)) → (𝐴 ·op 𝑇) ≤op (𝐴 ·op 𝑈))
Theorem	leoptri 32397	The positive operator ordering relation satisfies trichotomy. Exercise 1(iii) of [Retherford] p. 49. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → ((𝑇 ≤op 𝑈 ∧ 𝑈 ≤op 𝑇) ↔ 𝑇 = 𝑈))
Theorem	leoptr 32398	The positive operator ordering relation is transitive. Exercise 1(iv) of [Retherford] p. 49. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.)
⊢ (((𝑆 ∈ HrmOp ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑆 ≤op 𝑇 ∧ 𝑇 ≤op 𝑈)) → 𝑆 ≤op 𝑈)
Theorem	leopnmid 32399	A bounded Hermitian operator is less than or equal to its norm times the identity operator. (Contributed by NM, 11-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ HrmOp ∧ (normop‘𝑇) ∈ ℝ) → 𝑇 ≤op ((normop‘𝑇) ·op Iop ))
Theorem	nmopleid 32400	A nonzero, bounded Hermitian operator divided by its norm is less than or equal to the identity operator. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ HrmOp ∧ (normop‘𝑇) ∈ ℝ ∧ 𝑇 ≠ 0hop ) → ((1 / (normop‘𝑇)) ·op 𝑇) ≤op Iop )