P. 319 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 31801-31900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hmopf 31801	A Hermitian operator is a Hilbert space operator (mapping). (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ HrmOp → 𝑇: ℋ⟶ ℋ)
Theorem	hmopex 31802	The class of Hermitian operators is a set. (Contributed by NM, 17-Aug-2006.) (New usage is discouraged.)
⊢ HrmOp ∈ V
Theorem	nmfnval 31803*	Value of the norm of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ℂ → (normfn‘𝑇) = sup({𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘(𝑇‘𝑦)))}, ℝ*, < ))
Theorem	nmfnsetre 31804*	The set in the supremum of the functional norm definition df-nmfn 31772 is a set of reals. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ℂ → {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘(𝑇‘𝑦)))} ⊆ ℝ)
Theorem	nmfnsetn0 31805*	The set in the supremum of the functional norm definition df-nmfn 31772 is nonempty. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
⊢ (abs‘(𝑇‘0ℎ)) ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘(𝑇‘𝑦)))}
Theorem	nmfnxr 31806	The norm of any Hilbert space functional is an extended real. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ℂ → (normfn‘𝑇) ∈ ℝ*)
Theorem	nmfnrepnf 31807	The norm of a Hilbert space functional is either real or plus infinity. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ℂ → ((normfn‘𝑇) ∈ ℝ ↔ (normfn‘𝑇) ≠ +∞))
Theorem	nlfnval 31808	Value of the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ℂ → (null‘𝑇) = (◡𝑇 “ {0}))
Theorem	elcnfn 31809*	Property defining a continuous functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ (𝑇 ∈ ContFn ↔ (𝑇: ℋ⟶ℂ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (abs‘((𝑇‘𝑤) − (𝑇‘𝑥))) < 𝑦)))
Theorem	ellnfn 31810*	Property defining a linear functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinFn ↔ (𝑇: ℋ⟶ℂ ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑇‘𝑦)) + (𝑇‘𝑧))))
Theorem	lnfnf 31811	A linear Hilbert space functional is a functional. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinFn → 𝑇: ℋ⟶ℂ)
Theorem	dfadj2 31812*	Alternate definition of the adjoint of a Hilbert space operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.)
⊢ adjℎ = {⟨𝑡, 𝑢⟩ ∣ (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦))}
Theorem	funadj 31813	Functionality of the adjoint function. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
⊢ Fun adjℎ
Theorem	dmadjss 31814	The domain of the adjoint function is a subset of the maps from ℋ to ℋ. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
⊢ dom adjℎ ⊆ ( ℋ ↑m ℋ)
Theorem	dmadjop 31815	A member of the domain of the adjoint function is a Hilbert space operator. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ dom adjℎ → 𝑇: ℋ⟶ ℋ)
Theorem	adjeu 31816*	Elementhood in the domain of the adjoint function. (Contributed by Mario Carneiro, 11-Sep-2015.) (Revised by Mario Carneiro, 24-Dec-2016.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → (𝑇 ∈ dom adjℎ ↔ ∃!𝑢 ∈ ( ℋ ↑m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦)))
Theorem	adjval 31817*	Value of the adjoint function for 𝑇 in the domain of adjℎ. (Contributed by NM, 19-Feb-2006.) (Revised by Mario Carneiro, 24-Dec-2016.) (New usage is discouraged.)
⊢ (𝑇 ∈ dom adjℎ → (adjℎ‘𝑇) = (℩𝑢 ∈ ( ℋ ↑m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦)))
Theorem	adjval2 31818*	Value of the adjoint function. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ dom adjℎ → (adjℎ‘𝑇) = (℩𝑢 ∈ ( ℋ ↑m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢‘𝑦))))
Theorem	cnvadj 31819	The adjoint function equals its converse. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
⊢ ◡adjℎ = adjℎ
Theorem	funcnvadj 31820	The converse of the adjoint function is a function. (Contributed by NM, 25-Jan-2006.) (New usage is discouraged.)
⊢ Fun ◡adjℎ
Theorem	adj1o 31821	The adjoint function maps one-to-one onto its domain. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
⊢ adjℎ:dom adjℎ–1-1-onto→dom adjℎ
Theorem	dmadjrn 31822	The adjoint of an operator belongs to the adjoint function's domain. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ dom adjℎ → (adjℎ‘𝑇) ∈ dom adjℎ)
Theorem	eigvecval 31823*	The set of eigenvectors of a Hilbert space operator. (Contributed by NM, 11-Mar-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → (eigvec‘𝑇) = {𝑥 ∈ ( ℋ ∖ 0ℋ) ∣ ∃𝑦 ∈ ℂ (𝑇‘𝑥) = (𝑦 ·ℎ 𝑥)})
Theorem	eigvalfval 31824*	The eigenvalues of eigenvectors of a Hilbert space operator. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → (eigval‘𝑇) = (𝑥 ∈ (eigvec‘𝑇) ↦ (((𝑇‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))
Theorem	specval 31825*	The value of the spectrum of an operator. (Contributed by NM, 11-Apr-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → (Lambda‘𝑇) = {𝑥 ∈ ℂ ∣ ¬ (𝑇 −op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ})
Theorem	speccl 31826	The spectrum of an operator is a set of complex numbers. (Contributed by NM, 11-Apr-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → (Lambda‘𝑇) ⊆ ℂ)
Theorem	hhlnoi 31827	The linear operators of Hilbert space. (Contributed by NM, 19-Nov-2007.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝐿 = (𝑈 LnOp 𝑈)    ⇒   ⊢ LinOp = 𝐿
Theorem	hhnmoi 31828	The norm of an operator in Hilbert space. (Contributed by NM, 19-Nov-2007.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑁 = (𝑈 normOpOLD 𝑈)    ⇒   ⊢ normop = 𝑁
Theorem	hhbloi 31829	A bounded linear operator in Hilbert space. (Contributed by NM, 19-Nov-2007.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑈)    ⇒   ⊢ BndLinOp = 𝐵
Theorem	hh0oi 31830	The zero operator in Hilbert space. (Contributed by NM, 7-Dec-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑍 = (𝑈 0op 𝑈)    ⇒   ⊢ 0hop = 𝑍
Theorem	hhcno 31831	The continuous operators of Hilbert space. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ 𝐷 = (normℎ ∘ −ℎ )    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ContOp = (𝐽 Cn 𝐽)
Theorem	hhcnf 31832	The continuous functionals of Hilbert space. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ 𝐷 = (normℎ ∘ −ℎ )    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ ContFn = (𝐽 Cn 𝐾)
Theorem	dmadjrnb 31833	The adjoint of an operator belongs to the adjoint function's domain. (Note: the converse is dependent on our definition of function value, since it uses ndmfv 6910.) (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ dom adjℎ ↔ (adjℎ‘𝑇) ∈ dom adjℎ)
Theorem	nmoplb 31834	A lower bound for an operator norm. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ ℋ ∧ (normℎ‘𝐴) ≤ 1) → (normℎ‘(𝑇‘𝐴)) ≤ (normop‘𝑇))
Theorem	nmopub 31835*	An upper bound for an operator norm. (Contributed by NM, 7-Mar-2006.) (New usage is discouraged.)
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ ℝ*) → ((normop‘𝑇) ≤ 𝐴 ↔ ∀𝑥 ∈ ℋ ((normℎ‘𝑥) ≤ 1 → (normℎ‘(𝑇‘𝑥)) ≤ 𝐴)))
Theorem	nmopub2tALT 31836*	An upper bound for an operator norm. (Contributed by NM, 12-Apr-2006.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝑇: ℋ⟶ ℋ ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ ∀𝑥 ∈ ℋ (normℎ‘(𝑇‘𝑥)) ≤ (𝐴 · (normℎ‘𝑥))) → (normop‘𝑇) ≤ 𝐴)
Theorem	nmopub2tHIL 31837*	An upper bound for an operator norm. (Contributed by NM, 13-Dec-2007.) (New usage is discouraged.)
⊢ ((𝑇: ℋ⟶ ℋ ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ ∀𝑥 ∈ ℋ (normℎ‘(𝑇‘𝑥)) ≤ (𝐴 · (normℎ‘𝑥))) → (normop‘𝑇) ≤ 𝐴)
Theorem	nmopge0 31838	The norm of any Hilbert space operator is nonnegative. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → 0 ≤ (normop‘𝑇))
Theorem	nmopgt0 31839	A linear Hilbert space operator that is not identically zero has a positive norm. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → ((normop‘𝑇) ≠ 0 ↔ 0 < (normop‘𝑇)))
Theorem	cnopc 31840*	Basic continuity property of a continuous Hilbert space operator. (Contributed by NM, 2-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ ((𝑇 ∈ ContOp ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℝ+) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ ℋ ((normℎ‘(𝑦 −ℎ 𝐴)) < 𝑥 → (normℎ‘((𝑇‘𝑦) −ℎ (𝑇‘𝐴))) < 𝐵))
Theorem	lnopl 31841	Basic linearity property of a linear Hilbert space operator. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.)
⊢ (((𝑇 ∈ LinOp ∧ 𝐴 ∈ ℂ) ∧ (𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)) → (𝑇‘((𝐴 ·ℎ 𝐵) +ℎ 𝐶)) = ((𝐴 ·ℎ (𝑇‘𝐵)) +ℎ (𝑇‘𝐶)))
Theorem	unop 31842	Basic inner product property of a unitary operator. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ UniOp ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝑇‘𝐴) ·ih (𝑇‘𝐵)) = (𝐴 ·ih 𝐵))
Theorem	unopf1o 31843	A unitary operator in Hilbert space is one-to-one and onto. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ UniOp → 𝑇: ℋ–1-1-onto→ ℋ)
Theorem	unopnorm 31844	A unitary operator is idempotent in the norm. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ UniOp ∧ 𝐴 ∈ ℋ) → (normℎ‘(𝑇‘𝐴)) = (normℎ‘𝐴))
Theorem	cnvunop 31845	The inverse (converse) of a unitary operator in Hilbert space is unitary. Theorem in [AkhiezerGlazman] p. 72. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ UniOp → ◡𝑇 ∈ UniOp)
Theorem	unopadj 31846	The inverse (converse) of a unitary operator is its adjoint. Equation 2 of [AkhiezerGlazman] p. 72. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ UniOp ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝑇‘𝐴) ·ih 𝐵) = (𝐴 ·ih (◡𝑇‘𝐵)))
Theorem	unoplin 31847	A unitary operator is linear. Theorem in [AkhiezerGlazman] p. 72. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ UniOp → 𝑇 ∈ LinOp)
Theorem	counop 31848	The composition of two unitary operators is unitary. (Contributed by NM, 22-Jan-2006.) (New usage is discouraged.)
⊢ ((𝑆 ∈ UniOp ∧ 𝑇 ∈ UniOp) → (𝑆 ∘ 𝑇) ∈ UniOp)
Theorem	hmop 31849	Basic inner product property of a Hermitian operator. (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ HrmOp ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih (𝑇‘𝐵)) = ((𝑇‘𝐴) ·ih 𝐵))
Theorem	hmopre 31850	The inner product of the value and argument of a Hermitian operator is real. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ HrmOp ∧ 𝐴 ∈ ℋ) → ((𝑇‘𝐴) ·ih 𝐴) ∈ ℝ)
Theorem	nmfnlb 31851	A lower bound for a functional norm. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
⊢ ((𝑇: ℋ⟶ℂ ∧ 𝐴 ∈ ℋ ∧ (normℎ‘𝐴) ≤ 1) → (abs‘(𝑇‘𝐴)) ≤ (normfn‘𝑇))
Theorem	nmfnleub 31852*	An upper bound for the norm of a functional. (Contributed by NM, 24-May-2006.) (Revised by Mario Carneiro, 7-Sep-2014.) (New usage is discouraged.)
⊢ ((𝑇: ℋ⟶ℂ ∧ 𝐴 ∈ ℝ*) → ((normfn‘𝑇) ≤ 𝐴 ↔ ∀𝑥 ∈ ℋ ((normℎ‘𝑥) ≤ 1 → (abs‘(𝑇‘𝑥)) ≤ 𝐴)))
Theorem	nmfnleub2 31853*	An upper bound for the norm of a functional. (Contributed by NM, 24-May-2006.) (New usage is discouraged.)
⊢ ((𝑇: ℋ⟶ℂ ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ ∀𝑥 ∈ ℋ (abs‘(𝑇‘𝑥)) ≤ (𝐴 · (normℎ‘𝑥))) → (normfn‘𝑇) ≤ 𝐴)
Theorem	nmfnge0 31854	The norm of any Hilbert space functional is nonnegative. (Contributed by NM, 24-May-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ℂ → 0 ≤ (normfn‘𝑇))
Theorem	elnlfn 31855	Membership in the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ℂ → (𝐴 ∈ (null‘𝑇) ↔ (𝐴 ∈ ℋ ∧ (𝑇‘𝐴) = 0)))
Theorem	elnlfn2 31856	Membership in the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
⊢ ((𝑇: ℋ⟶ℂ ∧ 𝐴 ∈ (null‘𝑇)) → (𝑇‘𝐴) = 0)
Theorem	cnfnc 31857*	Basic continuity property of a continuous functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ ((𝑇 ∈ ContFn ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℝ+) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ ℋ ((normℎ‘(𝑦 −ℎ 𝐴)) < 𝑥 → (abs‘((𝑇‘𝑦) − (𝑇‘𝐴))) < 𝐵))
Theorem	lnfnl 31858	Basic linearity property of a linear functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
⊢ (((𝑇 ∈ LinFn ∧ 𝐴 ∈ ℂ) ∧ (𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)) → (𝑇‘((𝐴 ·ℎ 𝐵) +ℎ 𝐶)) = ((𝐴 · (𝑇‘𝐵)) + (𝑇‘𝐶)))
Theorem	adjcl 31859	Closure of the adjoint of a Hilbert space operator. (Contributed by NM, 17-Jun-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ) → ((adjℎ‘𝑇)‘𝐴) ∈ ℋ)
Theorem	adj1 31860	Property of an adjoint Hilbert space operator. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih (𝑇‘𝐵)) = (((adjℎ‘𝑇)‘𝐴) ·ih 𝐵))
Theorem	adj2 31861	Property of an adjoint Hilbert space operator. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝑇‘𝐴) ·ih 𝐵) = (𝐴 ·ih ((adjℎ‘𝑇)‘𝐵)))
Theorem	adjeq 31862*	A property that determines the adjoint of a Hilbert space operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.)
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑆: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑆‘𝑦))) → (adjℎ‘𝑇) = 𝑆)
Theorem	adjadj 31863	Double adjoint. Theorem 3.11(iv) of [Beran] p. 106. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ dom adjℎ → (adjℎ‘(adjℎ‘𝑇)) = 𝑇)
Theorem	adjvalval 31864*	Value of the value of the adjoint function. (Contributed by NM, 22-Feb-2006.) (Proof shortened by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
⊢ ((𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ) → ((adjℎ‘𝑇)‘𝐴) = (℩𝑤 ∈ ℋ ∀𝑥 ∈ ℋ ((𝑇‘𝑥) ·ih 𝐴) = (𝑥 ·ih 𝑤)))
Theorem	unopadj2 31865	The adjoint of a unitary operator is its inverse (converse). Equation 2 of [AkhiezerGlazman] p. 72. (Contributed by NM, 23-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ UniOp → (adjℎ‘𝑇) = ◡𝑇)
Theorem	hmopadj 31866	A Hermitian operator is self-adjoint. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ HrmOp → (adjℎ‘𝑇) = 𝑇)
Theorem	hmdmadj 31867	Every Hermitian operator has an adjoint. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ HrmOp → 𝑇 ∈ dom adjℎ)
Theorem	hmopadj2 31868	An operator is Hermitian iff it is self-adjoint. Definition of Hermitian in [Halmos] p. 41. (Contributed by NM, 9-Apr-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ dom adjℎ → (𝑇 ∈ HrmOp ↔ (adjℎ‘𝑇) = 𝑇))
Theorem	hmoplin 31869	A Hermitian operator is linear. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ HrmOp → 𝑇 ∈ LinOp)
Theorem	brafval 31870*	The bra of a vector, expressed as ⟨𝐴 ∣ in Dirac notation. See df-bra 31777. (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (bra‘𝐴) = (𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐴)))
Theorem	braval 31871	A bra-ket juxtaposition, expressed as ⟨𝐴 ∣ 𝐵⟩ in Dirac notation, equals the inner product of the vectors. Based on definition of bra in [Prugovecki] p. 186. (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 17-Nov-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((bra‘𝐴)‘𝐵) = (𝐵 ·ih 𝐴))
Theorem	braadd 31872	Linearity property of bra for addition. (Contributed by NM, 23-May-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((bra‘𝐴)‘(𝐵 +ℎ 𝐶)) = (((bra‘𝐴)‘𝐵) + ((bra‘𝐴)‘𝐶)))
Theorem	bramul 31873	Linearity property of bra for multiplication. (Contributed by NM, 23-May-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((bra‘𝐴)‘(𝐵 ·ℎ 𝐶)) = (𝐵 · ((bra‘𝐴)‘𝐶)))
Theorem	brafn 31874	The bra function is a functional. (Contributed by NM, 23-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (bra‘𝐴): ℋ⟶ℂ)
Theorem	bralnfn 31875	The Dirac bra function is a linear functional. (Contributed by NM, 23-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (bra‘𝐴) ∈ LinFn)
Theorem	bracl 31876	Closure of the bra function. (Contributed by NM, 23-May-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((bra‘𝐴)‘𝐵) ∈ ℂ)
Theorem	bra0 31877	The Dirac bra of the zero vector. (Contributed by NM, 25-May-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.)
⊢ (bra‘0ℎ) = ( ℋ × {0})
Theorem	brafnmul 31878	Anti-linearity property of bra functional for multiplication. (Contributed by NM, 31-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (bra‘(𝐴 ·ℎ 𝐵)) = ((∗‘𝐴) ·fn (bra‘𝐵)))
Theorem	kbfval 31879*	The outer product of two vectors, expressed as ∣ 𝐴⟩⟨𝐵 ∣ in Dirac notation. See df-kb 31778. (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ketbra 𝐵) = (𝑥 ∈ ℋ ↦ ((𝑥 ·ih 𝐵) ·ℎ 𝐴)))
Theorem	kbop 31880	The outer product of two vectors, expressed as ∣ 𝐴⟩⟨𝐵 ∣ in Dirac notation, is an operator. (Contributed by NM, 30-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ketbra 𝐵): ℋ⟶ ℋ)
Theorem	kbval 31881	The value of the operator resulting from the outer product ∣ 𝐴⟩ ⟨𝐵 ∣ of two vectors. Equation 8.1 of [Prugovecki] p. 376. (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ketbra 𝐵)‘𝐶) = ((𝐶 ·ih 𝐵) ·ℎ 𝐴))
Theorem	kbmul 31882	Multiplication property of outer product. (Contributed by NM, 31-May-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ketbra 𝐶) = (𝐵 ketbra ((∗‘𝐴) ·ℎ 𝐶)))
Theorem	kbpj 31883	If a vector 𝐴 has norm 1, the outer product ∣ 𝐴⟩⟨𝐴 ∣ is the projector onto the subspace spanned by 𝐴. http://en.wikipedia.org/wiki/Bra-ket#Linear%5Foperators. (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ (normℎ‘𝐴) = 1) → (𝐴 ketbra 𝐴) = (projℎ‘(span‘{𝐴})))
Theorem	eleigvec 31884*	Membership in the set of eigenvectors of a Hilbert space operator. (Contributed by NM, 11-Mar-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → (𝐴 ∈ (eigvec‘𝑇) ↔ (𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ∧ ∃𝑥 ∈ ℂ (𝑇‘𝐴) = (𝑥 ·ℎ 𝐴))))
Theorem	eleigvec2 31885	Membership in the set of eigenvectors of a Hilbert space operator. (Contributed by NM, 18-Mar-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → (𝐴 ∈ (eigvec‘𝑇) ↔ (𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ∧ (𝑇‘𝐴) ∈ (span‘{𝐴}))))
Theorem	eleigveccl 31886	Closure of an eigenvector of a Hilbert space operator. (Contributed by NM, 23-Mar-2006.) (New usage is discouraged.)
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ (eigvec‘𝑇)) → 𝐴 ∈ ℋ)
Theorem	eigvalval 31887	The eigenvalue of an eigenvector of a Hilbert space operator. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ (eigvec‘𝑇)) → ((eigval‘𝑇)‘𝐴) = (((𝑇‘𝐴) ·ih 𝐴) / ((normℎ‘𝐴)↑2)))
Theorem	eigvalcl 31888	An eigenvalue is a complex number. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ (eigvec‘𝑇)) → ((eigval‘𝑇)‘𝐴) ∈ ℂ)
Theorem	eigvec1 31889	Property of an eigenvector. (Contributed by NM, 12-Mar-2006.) (New usage is discouraged.)
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ (eigvec‘𝑇)) → ((𝑇‘𝐴) = (((eigval‘𝑇)‘𝐴) ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ))
Theorem	eighmre 31890	The eigenvalues of a Hermitian operator are real. Equation 1.30 of [Hughes] p. 49. (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ HrmOp ∧ 𝐴 ∈ (eigvec‘𝑇)) → ((eigval‘𝑇)‘𝐴) ∈ ℝ)
Theorem	eighmorth 31891	Eigenvectors of a Hermitian operator with distinct eigenvalues are orthogonal. Equation 1.31 of [Hughes] p. 49. (Contributed by NM, 23-Mar-2006.) (New usage is discouraged.)
⊢ (((𝑇 ∈ HrmOp ∧ 𝐴 ∈ (eigvec‘𝑇)) ∧ (𝐵 ∈ (eigvec‘𝑇) ∧ ((eigval‘𝑇)‘𝐴) ≠ ((eigval‘𝑇)‘𝐵))) → (𝐴 ·ih 𝐵) = 0)
Theorem	nmopnegi 31892	Value of the norm of the negative of a Hilbert space operator. Unlike nmophmi 31958, the operator does not have to be bounded. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ (normop‘(-1 ·op 𝑇)) = (normop‘𝑇)
Theorem	lnop0 31893	The value of a linear Hilbert space operator at zero is zero. Remark in [Beran] p. 99. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinOp → (𝑇‘0ℎ) = 0ℎ)
Theorem	lnopmul 31894	Multiplicative property of a linear Hilbert space operator. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ LinOp ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 ·ℎ 𝐵)) = (𝐴 ·ℎ (𝑇‘𝐵)))
Theorem	lnopli 31895	Basic scalar product property of a linear Hilbert space operator. (Contributed by NM, 23-Jan-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘((𝐴 ·ℎ 𝐵) +ℎ 𝐶)) = ((𝐴 ·ℎ (𝑇‘𝐵)) +ℎ (𝑇‘𝐶)))
Theorem	lnopfi 31896	A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 23-Jan-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    ⇒   ⊢ 𝑇: ℋ⟶ ℋ
Theorem	lnop0i 31897	The value of a linear Hilbert space operator at zero is zero. Remark in [Beran] p. 99. (Contributed by NM, 11-May-2005.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    ⇒   ⊢ (𝑇‘0ℎ) = 0ℎ
Theorem	lnopaddi 31898	Additive property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 +ℎ 𝐵)) = ((𝑇‘𝐴) +ℎ (𝑇‘𝐵)))
Theorem	lnopmuli 31899	Multiplicative property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 ·ℎ 𝐵)) = (𝐴 ·ℎ (𝑇‘𝐵)))
Theorem	lnopaddmuli 31900	Sum/product property of a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘(𝐵 +ℎ (𝐴 ·ℎ 𝐶))) = ((𝑇‘𝐵) +ℎ (𝐴 ·ℎ (𝑇‘𝐶))))