P. 321 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32001-32100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	riesz1 32001*	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 32002. For the continuous linear functional version, see riesz3i 31998 and riesz4 32000. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinFn → ((normfn‘𝑇) ∈ ℝ ↔ ∃𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑥 ·ih 𝑦)))
Theorem	riesz2 32002*	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 32001. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ LinFn ∧ (normfn‘𝑇) ∈ ℝ) → ∃!𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑥 ·ih 𝑦))
20.6.12  Adjoints (cont.)
Theorem	cnlnadjlem1 32003*	Lemma for cnlnadji 32012 (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 32004*	Lemma for cnlnadji 32012. 𝐺 is a continuous linear functional. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑇 ∈ ContOp    &   ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦))    ⇒   ⊢ (𝑦 ∈ ℋ → (𝐺 ∈ LinFn ∧ 𝐺 ∈ ContFn))
Theorem	cnlnadjlem3 32005*	Lemma for cnlnadji 32012. By riesz4 32000, 𝐵 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 32006*	Lemma for cnlnadji 32012. 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 32007*	Lemma for cnlnadji 32012. 𝐹 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 32008*	Lemma for cnlnadji 32012. 𝐹 is linear. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑇 ∈ ContOp    &   ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦))    &   ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))    &   ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵)    ⇒   ⊢ 𝐹 ∈ LinOp
Theorem	cnlnadjlem7 32009*	Lemma for cnlnadji 32012. 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 32010*	Lemma for cnlnadji 32012. 𝐹 is continuous. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑇 ∈ ContOp    &   ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦))    &   ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))    &   ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵)    ⇒   ⊢ 𝐹 ∈ ContOp
Theorem	cnlnadjlem9 32011*	Lemma for cnlnadji 32012. 𝐹 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 32012*	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 32013*	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 32014*	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 32015*	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 32016	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 32017	Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)
⊢ BndLinOp ⊆ dom adjℎ
Theorem	bdopadj 32018	Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ BndLinOp → 𝑇 ∈ dom adjℎ)
Theorem	adjbdln 32019	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 32020	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 32021	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 32022	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 32023	Every operator with an adjoint is linear. (Contributed by NM, 17-Jun-2006.) (New usage is discouraged.)
⊢ dom adjℎ ⊆ LinOp
Theorem	nmopadjlei 32024	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 32025	Lemma for nmopadji 32026. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ BndLinOp    ⇒   ⊢ (normop‘(adjℎ‘𝑇)) ≤ (normop‘𝑇)
Theorem	nmopadji 32026	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 32027	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 32028	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 32029	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 32030	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 32031	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 32032	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 32033	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 32034	The composition of two bounded linear operators is bounded. (Contributed by NM, 9-Mar-2006.) (New usage is discouraged.)
⊢ 𝑆 ∈ BndLinOp    &   ⊢ 𝑇 ∈ BndLinOp    ⇒   ⊢ (𝑆 ∘ 𝑇) ∈ BndLinOp
Theorem	nmoptri2i 32035	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 32036	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 32037	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 32038	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 32039	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 32040	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 32041	The norm of the bra function. (Contributed by NM, 24-May-2006.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (normfn‘(bra‘𝐴)) = (normℎ‘𝐴))
Theorem	brabn 32042	The bra of a vector is a bounded functional. (Contributed by NM, 26-May-2006.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (normfn‘(bra‘𝐴)) ∈ ℝ)
Theorem	rnbra 32043	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 32044	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 32045	A bra is a continuous linear functional. (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (bra‘𝐴) ∈ (LinFn ∩ ContFn))
Theorem	cnvbraval 32046*	Value of the converse of the bra function. Based on the Riesz Lemma riesz4 32000, 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 32047	Closure of the converse of the bra function. (Contributed by NM, 26-May-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ (LinFn ∩ ContFn) → (◡bra‘𝑇) ∈ ℋ)
Theorem	cnvbrabra 32048	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 32049	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 32050*	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 32051	Multiplication property of the converse bra function. (Contributed by NM, 31-May-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑇 ∈ (LinFn ∩ ContFn)) → (◡bra‘(𝐴 ·fn 𝑇)) = ((∗‘𝐴) ·ℎ (◡bra‘𝑇)))
Theorem	kbass1 32052	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 32053	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 32054	Dirac bra-ket associative law ⟨𝐴 ∣ 𝐵⟩⟨𝐶 ∣ 𝐷⟩ = (⟨𝐴 ∣ 𝐵⟩⟨𝐶 ∣ ) ∣ 𝐷⟩. (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → (((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝐷)) = ((((bra‘𝐴)‘𝐵) ·fn (bra‘𝐶))‘𝐷))
Theorem	kbass4 32055	Dirac bra-ket associative law ⟨𝐴 ∣ 𝐵⟩⟨𝐶 ∣ 𝐷⟩ = ⟨𝐴 ∣ ( ∣ 𝐵⟩⟨𝐶 ∣ 𝐷⟩). (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → (((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝐷)) = ((bra‘𝐴)‘(((bra‘𝐶)‘𝐷) ·ℎ 𝐵)))
Theorem	kbass5 32056	Dirac bra-ket associative law ( ∣ 𝐴⟩⟨𝐵 ∣ )( ∣ 𝐶⟩⟨𝐷 ∣ ) = (( ∣ 𝐴⟩⟨𝐵 ∣ ) ∣ 𝐶⟩)⟨𝐷 ∣. (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 ketbra 𝐵) ∘ (𝐶 ketbra 𝐷)) = (((𝐴 ketbra 𝐵)‘𝐶) ketbra 𝐷))
Theorem	kbass6 32057	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 32058*	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 32059*	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 32060*	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 32061	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 32062*	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 32063	The ordering relation for operators is reflexive. (Contributed by NM, 24-Jul-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → 𝑇 ≤op 𝑇)
Theorem	leoprf 32064	The ordering relation for operators is reflexive. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ HrmOp → 𝑇 ≤op 𝑇)
Theorem	leopsq 32065	The square of a Hermitian operator is positive. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ HrmOp → 0hop ≤op (𝑇 ∘ 𝑇))
Theorem	0leop 32066	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 32067	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 32068	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 32069	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 32070	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 32071	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 32072	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 32073	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 32074	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 32075	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 )
Theorem	opsqrlem1 32076*	Lemma for opsqri . (Contributed by NM, 9-Aug-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ HrmOp    &   ⊢ (normop‘𝑇) ∈ ℝ    &   ⊢ 0hop ≤op 𝑇    &   ⊢ 𝑅 = ((1 / (normop‘𝑇)) ·op 𝑇)    &   ⊢ (𝑇 ≠ 0hop → ∃𝑢 ∈ HrmOp ( 0hop ≤op 𝑢 ∧ (𝑢 ∘ 𝑢) = 𝑅))    ⇒   ⊢ (𝑇 ≠ 0hop → ∃𝑣 ∈ HrmOp ( 0hop ≤op 𝑣 ∧ (𝑣 ∘ 𝑣) = 𝑇))
Theorem	opsqrlem2 32077*	Lemma for opsqri . 𝐹‘𝑁 is the recursive function An (starting at n=1 instead of 0) of Theorem 9.4-2 of [Kreyszig] p. 476. (Contributed by NM, 17-Aug-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ HrmOp    &   ⊢ 𝑆 = (𝑥 ∈ HrmOp, 𝑦 ∈ HrmOp ↦ (𝑥 +op ((1 / 2) ·op (𝑇 −op (𝑥 ∘ 𝑥)))))    &   ⊢ 𝐹 = seq1(𝑆, (ℕ × { 0hop }))    ⇒   ⊢ (𝐹‘1) = 0hop
Theorem	opsqrlem3 32078*	Lemma for opsqri . (Contributed by NM, 22-Aug-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ HrmOp    &   ⊢ 𝑆 = (𝑥 ∈ HrmOp, 𝑦 ∈ HrmOp ↦ (𝑥 +op ((1 / 2) ·op (𝑇 −op (𝑥 ∘ 𝑥)))))    &   ⊢ 𝐹 = seq1(𝑆, (ℕ × { 0hop }))    ⇒   ⊢ ((𝐺 ∈ HrmOp ∧ 𝐻 ∈ HrmOp) → (𝐺𝑆𝐻) = (𝐺 +op ((1 / 2) ·op (𝑇 −op (𝐺 ∘ 𝐺)))))
Theorem	opsqrlem4 32079*	Lemma for opsqri . (Contributed by NM, 17-Aug-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ HrmOp    &   ⊢ 𝑆 = (𝑥 ∈ HrmOp, 𝑦 ∈ HrmOp ↦ (𝑥 +op ((1 / 2) ·op (𝑇 −op (𝑥 ∘ 𝑥)))))    &   ⊢ 𝐹 = seq1(𝑆, (ℕ × { 0hop }))    ⇒   ⊢ 𝐹:ℕ⟶HrmOp
Theorem	opsqrlem5 32080*	Lemma for opsqri . (Contributed by NM, 17-Aug-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ HrmOp    &   ⊢ 𝑆 = (𝑥 ∈ HrmOp, 𝑦 ∈ HrmOp ↦ (𝑥 +op ((1 / 2) ·op (𝑇 −op (𝑥 ∘ 𝑥)))))    &   ⊢ 𝐹 = seq1(𝑆, (ℕ × { 0hop }))    ⇒   ⊢ (𝑁 ∈ ℕ → (𝐹‘(𝑁 + 1)) = ((𝐹‘𝑁) +op ((1 / 2) ·op (𝑇 −op ((𝐹‘𝑁) ∘ (𝐹‘𝑁))))))
Theorem	opsqrlem6 32081*	Lemma for opsqri . (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ HrmOp    &   ⊢ 𝑆 = (𝑥 ∈ HrmOp, 𝑦 ∈ HrmOp ↦ (𝑥 +op ((1 / 2) ·op (𝑇 −op (𝑥 ∘ 𝑥)))))    &   ⊢ 𝐹 = seq1(𝑆, (ℕ × { 0hop }))    &   ⊢ 𝑇 ≤op Iop    ⇒   ⊢ (𝑁 ∈ ℕ → (𝐹‘𝑁) ≤op Iop )
20.6.16  Projectors as operators
Theorem	pjhmopi 32082	A projector is a Hermitian operator. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (projℎ‘𝐻) ∈ HrmOp
Theorem	pjlnopi 32083	A projector is a linear operator. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (projℎ‘𝐻) ∈ LinOp
Theorem	pjnmopi 32084	The operator norm of a projector on a nonzero closed subspace is one. Part of Theorem 26.1 of [Halmos] p. 43. (Contributed by NM, 9-Apr-2006.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐻 ≠ 0ℋ → (normop‘(projℎ‘𝐻)) = 1)
Theorem	pjbdlni 32085	A projector is a bounded linear operator. (Contributed by NM, 3-Jun-2006.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (projℎ‘𝐻) ∈ BndLinOp
Theorem	pjhmop 32086	A projection is a Hermitian operator. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
⊢ (𝐻 ∈ Cℋ → (projℎ‘𝐻) ∈ HrmOp)
Theorem	hmopidmchi 32087	An idempotent Hermitian operator generates a closed subspace. Part of proof of Theorem of [AkhiezerGlazman] p. 64. (Contributed by NM, 21-Apr-2006.) (Proof shortened by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ 𝑇 ∈ HrmOp    &   ⊢ (𝑇 ∘ 𝑇) = 𝑇    ⇒   ⊢ ran 𝑇 ∈ Cℋ
Theorem	hmopidmpji 32088	An idempotent Hermitian operator is a projection operator. Theorem 26.4 of [Halmos] p. 44. (Halmos seems to omit the proof that 𝐻 is a closed subspace, which is not trivial as hmopidmchi 32087 shows.) (Contributed by NM, 22-Apr-2006.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ 𝑇 ∈ HrmOp    &   ⊢ (𝑇 ∘ 𝑇) = 𝑇    ⇒   ⊢ 𝑇 = (projℎ‘ran 𝑇)
Theorem	hmopidmch 32089	An idempotent Hermitian operator generates a closed subspace. Part of proof of Theorem of [AkhiezerGlazman] p. 64. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ HrmOp ∧ (𝑇 ∘ 𝑇) = 𝑇) → ran 𝑇 ∈ Cℋ )
Theorem	hmopidmpj 32090	An idempotent Hermitian operator is a projection operator. Theorem 26.4 of [Halmos] p. 44. (Contributed by NM, 22-Apr-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ HrmOp ∧ (𝑇 ∘ 𝑇) = 𝑇) → 𝑇 = (projℎ‘ran 𝑇))
Theorem	pjsdii 32091	Distributive law for Hilbert space operator sum. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝑆: ℋ⟶ ℋ    &   ⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ ((projℎ‘𝐻) ∘ (𝑆 +op 𝑇)) = (((projℎ‘𝐻) ∘ 𝑆) +op ((projℎ‘𝐻) ∘ 𝑇))
Theorem	pjddii 32092	Distributive law for Hilbert space operator difference. (Contributed by NM, 24-Nov-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝑆: ℋ⟶ ℋ    &   ⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ ((projℎ‘𝐻) ∘ (𝑆 −op 𝑇)) = (((projℎ‘𝐻) ∘ 𝑆) −op ((projℎ‘𝐻) ∘ 𝑇))
Theorem	pjsdi2i 32093	Chained distributive law for Hilbert space operator difference. (Contributed by NM, 30-Nov-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝑅: ℋ⟶ ℋ    &   ⊢ 𝑆: ℋ⟶ ℋ    &   ⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ ((𝑅 ∘ (𝑆 +op 𝑇)) = ((𝑅 ∘ 𝑆) +op (𝑅 ∘ 𝑇)) → (((projℎ‘𝐻) ∘ 𝑅) ∘ (𝑆 +op 𝑇)) = ((((projℎ‘𝐻) ∘ 𝑅) ∘ 𝑆) +op (((projℎ‘𝐻) ∘ 𝑅) ∘ 𝑇)))
Theorem	pjcoi 32094	Composition of projections. (Contributed by NM, 16-Aug-2000.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ ℋ → (((projℎ‘𝐺) ∘ (projℎ‘𝐻))‘𝐴) = ((projℎ‘𝐺)‘((projℎ‘𝐻)‘𝐴)))
Theorem	pjcocli 32095	Closure of composition of projections. (Contributed by NM, 29-Nov-2000.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ ℋ → (((projℎ‘𝐺) ∘ (projℎ‘𝐻))‘𝐴) ∈ 𝐺)
Theorem	pjcohcli 32096	Closure of composition of projections. (Contributed by NM, 7-Oct-2000.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ ℋ → (((projℎ‘𝐺) ∘ (projℎ‘𝐻))‘𝐴) ∈ ℋ)
Theorem	pjadjcoi 32097	Adjoint of composition of projections. Special case of Theorem 3.11(viii) of [Beran] p. 106. (Contributed by NM, 6-Oct-2000.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((((projℎ‘𝐺) ∘ (projℎ‘𝐻))‘𝐴) ·ih 𝐵) = (𝐴 ·ih (((projℎ‘𝐻) ∘ (projℎ‘𝐺))‘𝐵)))
Theorem	pjcofni 32098	Functionality of composition of projections. (Contributed by NM, 1-Oct-2000.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((projℎ‘𝐺) ∘ (projℎ‘𝐻)) Fn ℋ
Theorem	pjss1coi 32099	Subset relationship for projections. Theorem 4.5(i)<->(iii) of [Beran] p. 112. (Contributed by NM, 1-Oct-2000.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐺 ⊆ 𝐻 ↔ ((projℎ‘𝐻) ∘ (projℎ‘𝐺)) = (projℎ‘𝐺))
Theorem	pjss2coi 32100	Subset relationship for projections. Theorem 4.5(i)<->(ii) of [Beran] p. 112. (Contributed by NM, 7-Oct-2000.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐺 ⊆ 𝐻 ↔ ((projℎ‘𝐺) ∘ (projℎ‘𝐻)) = (projℎ‘𝐺))