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	nmfnleub2 32001*	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 32002	The norm of any Hilbert space functional is nonnegative. (Contributed by NM, 24-May-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ℂ → 0 ≤ (normfn‘𝑇))
Theorem	elnlfn 32003	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 32004	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 32005*	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 32006	Basic linearity property of a linear functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
⊢ (((𝑇 ∈ LinFn ∧ 𝐴 ∈ ℂ) ∧ (𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)) → (𝑇‘((𝐴 ·ℎ 𝐵) +ℎ 𝐶)) = ((𝐴 · (𝑇‘𝐵)) + (𝑇‘𝐶)))
Theorem	adjcl 32007	Closure of the adjoint of a Hilbert space operator. (Contributed by NM, 17-Jun-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ) → ((adjℎ‘𝑇)‘𝐴) ∈ ℋ)
Theorem	adj1 32008	Property of an adjoint Hilbert space operator. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih (𝑇‘𝐵)) = (((adjℎ‘𝑇)‘𝐴) ·ih 𝐵))
Theorem	adj2 32009	Property of an adjoint Hilbert space operator. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝑇‘𝐴) ·ih 𝐵) = (𝐴 ·ih ((adjℎ‘𝑇)‘𝐵)))
Theorem	adjeq 32010*	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 32011	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 32012*	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 32013	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 32014	A Hermitian operator is self-adjoint. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ HrmOp → (adjℎ‘𝑇) = 𝑇)
Theorem	hmdmadj 32015	Every Hermitian operator has an adjoint. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ HrmOp → 𝑇 ∈ dom adjℎ)
Theorem	hmopadj2 32016	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 32017	A Hermitian operator is linear. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ HrmOp → 𝑇 ∈ LinOp)
Theorem	brafval 32018*	The bra of a vector, expressed as ⟨𝐴 ∣ in Dirac notation. See df-bra 31925. (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (bra‘𝐴) = (𝑥 ∈ ℋ ↦ (𝑥 ·ih 𝐴)))
Theorem	braval 32019	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 32020	Linearity property of bra for addition. (Contributed by NM, 23-May-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((bra‘𝐴)‘(𝐵 +ℎ 𝐶)) = (((bra‘𝐴)‘𝐵) + ((bra‘𝐴)‘𝐶)))
Theorem	bramul 32021	Linearity property of bra for multiplication. (Contributed by NM, 23-May-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((bra‘𝐴)‘(𝐵 ·ℎ 𝐶)) = (𝐵 · ((bra‘𝐴)‘𝐶)))
Theorem	brafn 32022	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 32023	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 32024	Closure of the bra function. (Contributed by NM, 23-May-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((bra‘𝐴)‘𝐵) ∈ ℂ)
Theorem	bra0 32025	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 32026	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 32027*	The outer product of two vectors, expressed as ∣ 𝐴⟩⟨𝐵 ∣ in Dirac notation. See df-kb 31926. (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ketbra 𝐵) = (𝑥 ∈ ℋ ↦ ((𝑥 ·ih 𝐵) ·ℎ 𝐴)))
Theorem	kbop 32028	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 32029	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 32030	Multiplication property of outer product. (Contributed by NM, 31-May-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ketbra 𝐶) = (𝐵 ketbra ((∗‘𝐴) ·ℎ 𝐶)))
Theorem	kbpj 32031	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 32032*	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 32033	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 32034	Closure of an eigenvector of a Hilbert space operator. (Contributed by NM, 23-Mar-2006.) (New usage is discouraged.)
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ (eigvec‘𝑇)) → 𝐴 ∈ ℋ)
Theorem	eigvalval 32035	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 32036	An eigenvalue is a complex number. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ (eigvec‘𝑇)) → ((eigval‘𝑇)‘𝐴) ∈ ℂ)
Theorem	eigvec1 32037	Property of an eigenvector. (Contributed by NM, 12-Mar-2006.) (New usage is discouraged.)
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ (eigvec‘𝑇)) → ((𝑇‘𝐴) = (((eigval‘𝑇)‘𝐴) ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ))
Theorem	eighmre 32038	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 32039	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 32040	Value of the norm of the negative of a Hilbert space operator. Unlike nmophmi 32106, the operator does not have to be bounded. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ (normop‘(-1 ·op 𝑇)) = (normop‘𝑇)
Theorem	lnop0 32041	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 32042	Multiplicative property of a linear Hilbert space operator. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ LinOp ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 ·ℎ 𝐵)) = (𝐴 ·ℎ (𝑇‘𝐵)))
Theorem	lnopli 32043	Basic scalar product property of a linear Hilbert space operator. (Contributed by NM, 23-Jan-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘((𝐴 ·ℎ 𝐵) +ℎ 𝐶)) = ((𝐴 ·ℎ (𝑇‘𝐵)) +ℎ (𝑇‘𝐶)))
Theorem	lnopfi 32044	A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 23-Jan-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    ⇒   ⊢ 𝑇: ℋ⟶ ℋ
Theorem	lnop0i 32045	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 32046	Additive property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 +ℎ 𝐵)) = ((𝑇‘𝐴) +ℎ (𝑇‘𝐵)))
Theorem	lnopmuli 32047	Multiplicative property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 ·ℎ 𝐵)) = (𝐴 ·ℎ (𝑇‘𝐵)))
Theorem	lnopaddmuli 32048	Sum/product property of a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘(𝐵 +ℎ (𝐴 ·ℎ 𝐶))) = ((𝑇‘𝐵) +ℎ (𝐴 ·ℎ (𝑇‘𝐶))))
Theorem	lnopsubi 32049	Subtraction property for a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 −ℎ 𝐵)) = ((𝑇‘𝐴) −ℎ (𝑇‘𝐵)))
Theorem	lnopsubmuli 32050	Subtraction/product property of a linear Hilbert space operator. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘(𝐵 −ℎ (𝐴 ·ℎ 𝐶))) = ((𝑇‘𝐵) −ℎ (𝐴 ·ℎ (𝑇‘𝐶))))
Theorem	lnopmulsubi 32051	Product/subtraction property of a linear Hilbert space operator. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑇‘((𝐴 ·ℎ 𝐵) −ℎ 𝐶)) = ((𝐴 ·ℎ (𝑇‘𝐵)) −ℎ (𝑇‘𝐶)))
Theorem	homco2 32052	Move a scalar product out of a composition of operators. The operator 𝑇 must be linear, unlike homco1 31876 that works for any operators. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑇 ∈ LinOp ∧ 𝑈: ℋ⟶ ℋ) → (𝑇 ∘ (𝐴 ·op 𝑈)) = (𝐴 ·op (𝑇 ∘ 𝑈)))
Theorem	idunop 32053	The identity function (restricted to Hilbert space) is a unitary operator. (Contributed by NM, 21-Jan-2006.) (New usage is discouraged.)
⊢ ( I ↾ ℋ) ∈ UniOp
Theorem	0cnop 32054	The identically zero function is a continuous Hilbert space operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
⊢ 0hop ∈ ContOp
Theorem	0cnfn 32055	The identically zero function is a continuous Hilbert space functional. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
⊢ ( ℋ × {0}) ∈ ContFn
Theorem	idcnop 32056	The identity function (restricted to Hilbert space) is a continuous operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
⊢ ( I ↾ ℋ) ∈ ContOp
Theorem	idhmop 32057	The Hilbert space identity operator is a Hermitian operator. (Contributed by NM, 22-Apr-2006.) (New usage is discouraged.)
⊢ Iop ∈ HrmOp
Theorem	0hmop 32058	The identically zero function is a Hermitian operator. (Contributed by NM, 8-Aug-2006.) (New usage is discouraged.)
⊢ 0hop ∈ HrmOp
Theorem	0lnop 32059	The identically zero function is a linear Hilbert space operator. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
⊢ 0hop ∈ LinOp
Theorem	0lnfn 32060	The identically zero function is a linear Hilbert space functional. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
⊢ ( ℋ × {0}) ∈ LinFn
Theorem	nmop0 32061	The norm of the zero operator is zero. (Contributed by NM, 8-Feb-2006.) (New usage is discouraged.)
⊢ (normop‘ 0hop ) = 0
Theorem	nmfn0 32062	The norm of the identically zero functional is zero. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
⊢ (normfn‘( ℋ × {0})) = 0
Theorem	hmopbdoptHIL 32063	A Hermitian operator is a bounded linear operator (Hellinger-Toeplitz Theorem). (Contributed by NM, 18-Jan-2008.) (New usage is discouraged.)
⊢ (𝑇 ∈ HrmOp → 𝑇 ∈ BndLinOp)
Theorem	hoddii 32064	Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri 31855 does not require linearity.) (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
⊢ 𝑅 ∈ LinOp    &   ⊢ 𝑆: ℋ⟶ ℋ    &   ⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ (𝑅 ∘ (𝑆 −op 𝑇)) = ((𝑅 ∘ 𝑆) −op (𝑅 ∘ 𝑇))
Theorem	hoddi 32065	Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri 31855 does not require linearity.) (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑅 ∈ LinOp ∧ 𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑅 ∘ (𝑆 −op 𝑇)) = ((𝑅 ∘ 𝑆) −op (𝑅 ∘ 𝑇)))
Theorem	nmop0h 32066	The norm of any operator on the trivial Hilbert space is zero. (This is the reason we need ℋ ≠ 0ℋ in nmopun 32089.) (Contributed by NM, 24-Feb-2006.) (New usage is discouraged.)
⊢ (( ℋ = 0ℋ ∧ 𝑇: ℋ⟶ ℋ) → (normop‘𝑇) = 0)
Theorem	idlnop 32067	The identity function (restricted to Hilbert space) is a linear operator. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.)
⊢ ( I ↾ ℋ) ∈ LinOp
Theorem	0bdop 32068	The identically zero operator is bounded. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
⊢ 0hop ∈ BndLinOp
Theorem	adj0 32069	Adjoint of the zero operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.)
⊢ (adjℎ‘ 0hop ) = 0hop
Theorem	nmlnop0iALT 32070	A linear operator with a zero norm is identically zero. (Contributed by NM, 8-Feb-2006.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑇 ∈ LinOp    ⇒   ⊢ ((normop‘𝑇) = 0 ↔ 𝑇 = 0hop )
Theorem	nmlnop0iHIL 32071	A linear operator with a zero norm is identically zero. (Contributed by NM, 18-Jan-2008.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    ⇒   ⊢ ((normop‘𝑇) = 0 ↔ 𝑇 = 0hop )
Theorem	nmlnopgt0i 32072	A linear Hilbert space operator that is not identically zero has a positive norm. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    ⇒   ⊢ (𝑇 ≠ 0hop ↔ 0 < (normop‘𝑇))
Theorem	nmlnop0 32073	A linear operator with a zero norm is identically zero. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinOp → ((normop‘𝑇) = 0 ↔ 𝑇 = 0hop ))
Theorem	nmlnopne0 32074	A linear operator with a nonzero norm is nonzero. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinOp → ((normop‘𝑇) ≠ 0 ↔ 𝑇 ≠ 0hop ))
Theorem	lnopmi 32075	The scalar product of a linear operator is a linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    ⇒   ⊢ (𝐴 ∈ ℂ → (𝐴 ·op 𝑇) ∈ LinOp)
Theorem	lnophsi 32076	The sum of two linear operators is linear. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
⊢ 𝑆 ∈ LinOp    &   ⊢ 𝑇 ∈ LinOp    ⇒   ⊢ (𝑆 +op 𝑇) ∈ LinOp
Theorem	lnophdi 32077	The difference of two linear operators is linear. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.)
⊢ 𝑆 ∈ LinOp    &   ⊢ 𝑇 ∈ LinOp    ⇒   ⊢ (𝑆 −op 𝑇) ∈ LinOp
Theorem	lnopcoi 32078	The composition of two linear operators is linear. (Contributed by NM, 8-Mar-2006.) (New usage is discouraged.)
⊢ 𝑆 ∈ LinOp    &   ⊢ 𝑇 ∈ LinOp    ⇒   ⊢ (𝑆 ∘ 𝑇) ∈ LinOp
Theorem	lnopco0i 32079	The composition of a linear operator with one whose norm is zero. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
⊢ 𝑆 ∈ LinOp    &   ⊢ 𝑇 ∈ LinOp    ⇒   ⊢ ((normop‘𝑇) = 0 → (normop‘(𝑆 ∘ 𝑇)) = 0)
Theorem	lnopeq0lem1 32080	Lemma for lnopeq0i 32082. Apply the generalized polarization identity polid2i 31232 to the quadratic form ((𝑇‘𝑥), 𝑥). (Contributed by NM, 26-Jul-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ ((𝑇‘𝐴) ·ih 𝐵) = (((((𝑇‘(𝐴 +ℎ 𝐵)) ·ih (𝐴 +ℎ 𝐵)) − ((𝑇‘(𝐴 −ℎ 𝐵)) ·ih (𝐴 −ℎ 𝐵))) + (i · (((𝑇‘(𝐴 +ℎ (i ·ℎ 𝐵))) ·ih (𝐴 +ℎ (i ·ℎ 𝐵))) − ((𝑇‘(𝐴 −ℎ (i ·ℎ 𝐵))) ·ih (𝐴 −ℎ (i ·ℎ 𝐵)))))) / 4)
Theorem	lnopeq0lem2 32081	Lemma for lnopeq0i 32082. (Contributed by NM, 26-Jul-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝑇‘𝐴) ·ih 𝐵) = (((((𝑇‘(𝐴 +ℎ 𝐵)) ·ih (𝐴 +ℎ 𝐵)) − ((𝑇‘(𝐴 −ℎ 𝐵)) ·ih (𝐴 −ℎ 𝐵))) + (i · (((𝑇‘(𝐴 +ℎ (i ·ℎ 𝐵))) ·ih (𝐴 +ℎ (i ·ℎ 𝐵))) − ((𝑇‘(𝐴 −ℎ (i ·ℎ 𝐵))) ·ih (𝐴 −ℎ (i ·ℎ 𝐵)))))) / 4))
Theorem	lnopeq0i 32082*	A condition implying that a linear Hilbert space operator is identically zero. Unlike ho01i 31903 for arbitrary operators, when the operator is linear we need to consider only the values of the quadratic form (𝑇‘𝑥) ·ih 𝑥). (Contributed by NM, 26-Jul-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    ⇒   ⊢ (∀𝑥 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑥) = 0 ↔ 𝑇 = 0hop )
Theorem	lnopeqi 32083*	Two linear Hilbert space operators are equal iff their quadratic forms are equal. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑈 ∈ LinOp    ⇒   ⊢ (∀𝑥 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑥) = ((𝑈‘𝑥) ·ih 𝑥) ↔ 𝑇 = 𝑈)
Theorem	lnopeq 32084*	Two linear Hilbert space operators are equal iff their quadratic forms are equal. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ LinOp ∧ 𝑈 ∈ LinOp) → (∀𝑥 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑥) = ((𝑈‘𝑥) ·ih 𝑥) ↔ 𝑇 = 𝑈))
Theorem	lnopunilem1 32085*	Lemma for lnopunii 32087. (Contributed by NM, 14-May-2005.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ ∀𝑥 ∈ ℋ (normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ (ℜ‘(𝐶 · ((𝑇‘𝐴) ·ih (𝑇‘𝐵)))) = (ℜ‘(𝐶 · (𝐴 ·ih 𝐵)))
Theorem	lnopunilem2 32086*	Lemma for lnopunii 32087. (Contributed by NM, 12-May-2005.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ ∀𝑥 ∈ ℋ (normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ ((𝑇‘𝐴) ·ih (𝑇‘𝐵)) = (𝐴 ·ih 𝐵)
Theorem	lnopunii 32087*	If a linear operator (whose range is ℋ) is idempotent in the norm, the operator is unitary. Similar to theorem in [AkhiezerGlazman] p. 73. (Contributed by NM, 23-Jan-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ 𝑇: ℋ–onto→ ℋ    &   ⊢ ∀𝑥 ∈ ℋ (normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)    ⇒   ⊢ 𝑇 ∈ UniOp
Theorem	elunop2 32088*	An operator is unitary iff it is linear, onto, and idempotent in the norm. Similar to theorem in [AkhiezerGlazman] p. 73, and its converse. (Contributed by NM, 24-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ UniOp ↔ (𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ (normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)))
Theorem	nmopun 32089	Norm of a unitary Hilbert space operator. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.)
⊢ (( ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → (normop‘𝑇) = 1)
Theorem	unopbd 32090	A unitary operator is a bounded linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ UniOp → 𝑇 ∈ BndLinOp)
Theorem	lnophmlem1 32091*	Lemma for lnophmi 32093. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝑇 ∈ LinOp    &   ⊢ ∀𝑥 ∈ ℋ (𝑥 ·ih (𝑇‘𝑥)) ∈ ℝ    ⇒   ⊢ (𝐴 ·ih (𝑇‘𝐴)) ∈ ℝ
Theorem	lnophmlem2 32092*	Lemma for lnophmi 32093. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝑇 ∈ LinOp    &   ⊢ ∀𝑥 ∈ ℋ (𝑥 ·ih (𝑇‘𝑥)) ∈ ℝ    ⇒   ⊢ (𝐴 ·ih (𝑇‘𝐵)) = ((𝑇‘𝐴) ·ih 𝐵)
Theorem	lnophmi 32093*	A linear operator is Hermitian if 𝑥 ·ih (𝑇‘𝑥) takes only real values. Remark in [ReedSimon] p. 195. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ LinOp    &   ⊢ ∀𝑥 ∈ ℋ (𝑥 ·ih (𝑇‘𝑥)) ∈ ℝ    ⇒   ⊢ 𝑇 ∈ HrmOp
Theorem	lnophm 32094*	A linear operator is Hermitian if 𝑥 ·ih (𝑇‘𝑥) takes only real values. Remark in [ReedSimon] p. 195. (Contributed by NM, 24-Jan-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ LinOp ∧ ∀𝑥 ∈ ℋ (𝑥 ·ih (𝑇‘𝑥)) ∈ ℝ) → 𝑇 ∈ HrmOp)
Theorem	hmops 32095	The sum of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 +op 𝑈) ∈ HrmOp)
Theorem	hmopm 32096	The scalar product of a Hermitian operator with a real is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp) → (𝐴 ·op 𝑇) ∈ HrmOp)
Theorem	hmopd 32097	The difference of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 −op 𝑈) ∈ HrmOp)
Theorem	hmopco 32098	The composition of two commuting Hermitian operators is Hermitian. (Contributed by NM, 22-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) → (𝑇 ∘ 𝑈) ∈ HrmOp)
Theorem	nmbdoplbi 32099	A lower bound for the norm of a bounded linear operator. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
⊢ 𝑇 ∈ BndLinOp    ⇒   ⊢ (𝐴 ∈ ℋ → (normℎ‘(𝑇‘𝐴)) ≤ ((normop‘𝑇) · (normℎ‘𝐴)))
Theorem	nmbdoplb 32100	A lower bound for the norm of a bounded linear Hilbert space operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
⊢ ((𝑇 ∈ BndLinOp ∧ 𝐴 ∈ ℋ) → (normℎ‘(𝑇‘𝐴)) ≤ ((normop‘𝑇) · (normℎ‘𝐴)))