P. 317 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 31601-31700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hoadddir 31601	Scalar product reverse distributive law for Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → ((𝐴 + 𝐵) ·op 𝑇) = ((𝐴 ·op 𝑇) +op (𝐵 ·op 𝑇)))
Theorem	homul12 31602	Swap first and second factors in a nested operator scalar product. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → (𝐴 ·op (𝐵 ·op 𝑇)) = (𝐵 ·op (𝐴 ·op 𝑇)))
Theorem	honegneg 31603	Double negative of a Hilbert space operator. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → (-1 ·op (-1 ·op 𝑇)) = 𝑇)
Theorem	hosubneg 31604	Relationship between operator subtraction and negative. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑇 −op (-1 ·op 𝑈)) = (𝑇 +op 𝑈))
Theorem	hosubdi 31605	Scalar product distributive law for operator difference. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝐴 ·op (𝑇 −op 𝑈)) = ((𝐴 ·op 𝑇) −op (𝐴 ·op 𝑈)))
Theorem	honegdi 31606	Distribution of negative over addition. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (-1 ·op (𝑇 +op 𝑈)) = ((-1 ·op 𝑇) +op (-1 ·op 𝑈)))
Theorem	honegsubdi 31607	Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (-1 ·op (𝑇 −op 𝑈)) = ((-1 ·op 𝑇) +op 𝑈))
Theorem	honegsubdi2 31608	Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (-1 ·op (𝑇 −op 𝑈)) = (𝑈 −op 𝑇))
Theorem	hosubsub2 31609	Law for double subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑆 −op (𝑇 −op 𝑈)) = (𝑆 +op (𝑈 −op 𝑇)))
Theorem	hosub4 31610	Rearrangement of 4 terms in a mixed addition and subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
⊢ (((𝑅: ℋ⟶ ℋ ∧ 𝑆: ℋ⟶ ℋ) ∧ (𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ)) → ((𝑅 +op 𝑆) −op (𝑇 +op 𝑈)) = ((𝑅 −op 𝑇) +op (𝑆 −op 𝑈)))
Theorem	hosubadd4 31611	Rearrangement of 4 terms in a mixed addition and subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
⊢ (((𝑅: ℋ⟶ ℋ ∧ 𝑆: ℋ⟶ ℋ) ∧ (𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ)) → ((𝑅 −op 𝑆) −op (𝑇 −op 𝑈)) = ((𝑅 +op 𝑈) −op (𝑆 +op 𝑇)))
Theorem	hoaddsubass 31612	Associative-type law for addition and subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ((𝑆 +op 𝑇) −op 𝑈) = (𝑆 +op (𝑇 −op 𝑈)))
Theorem	hoaddsub 31613	Law for operator addition and subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ((𝑆 +op 𝑇) −op 𝑈) = ((𝑆 −op 𝑈) +op 𝑇))
Theorem	hosubsub 31614	Law for double subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑆 −op (𝑇 −op 𝑈)) = ((𝑆 −op 𝑇) +op 𝑈))
Theorem	hosubsub4 31615	Law for double subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ((𝑆 −op 𝑇) −op 𝑈) = (𝑆 −op (𝑇 +op 𝑈)))
Theorem	ho2times 31616	Two times a Hilbert space operator. (Contributed by NM, 26-Aug-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → (2 ·op 𝑇) = (𝑇 +op 𝑇))
Theorem	hoaddsubassi 31617	Associativity of sum and difference of Hilbert space operators. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.)
⊢ 𝑅: ℋ⟶ ℋ    &   ⊢ 𝑆: ℋ⟶ ℋ    &   ⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ ((𝑅 +op 𝑆) −op 𝑇) = (𝑅 +op (𝑆 −op 𝑇))
Theorem	hoaddsubi 31618	Law for sum and difference of Hilbert space operators. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.)
⊢ 𝑅: ℋ⟶ ℋ    &   ⊢ 𝑆: ℋ⟶ ℋ    &   ⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ ((𝑅 +op 𝑆) −op 𝑇) = ((𝑅 −op 𝑇) +op 𝑆)
Theorem	hosd1i 31619	Hilbert space operator sum expressed in terms of difference. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.)
⊢ 𝑇: ℋ⟶ ℋ    &   ⊢ 𝑈: ℋ⟶ ℋ    ⇒   ⊢ (𝑇 +op 𝑈) = (𝑇 −op ( 0hop −op 𝑈))
Theorem	hosd2i 31620	Hilbert space operator sum expressed in terms of difference. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.)
⊢ 𝑇: ℋ⟶ ℋ    &   ⊢ 𝑈: ℋ⟶ ℋ    ⇒   ⊢ (𝑇 +op 𝑈) = (𝑇 −op ((𝑈 −op 𝑈) −op 𝑈))
Theorem	hopncani 31621	Hilbert space operator cancellation law. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
⊢ 𝑇: ℋ⟶ ℋ    &   ⊢ 𝑈: ℋ⟶ ℋ    ⇒   ⊢ ((𝑇 +op 𝑈) −op 𝑈) = 𝑇
Theorem	honpcani 31622	Hilbert space operator cancellation law. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
⊢ 𝑇: ℋ⟶ ℋ    &   ⊢ 𝑈: ℋ⟶ ℋ    ⇒   ⊢ ((𝑇 −op 𝑈) +op 𝑈) = 𝑇
Theorem	hosubeq0i 31623	If the difference between two operators is zero, they are equal. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.)
⊢ 𝑇: ℋ⟶ ℋ    &   ⊢ 𝑈: ℋ⟶ ℋ    ⇒   ⊢ ((𝑇 −op 𝑈) = 0hop ↔ 𝑇 = 𝑈)
Theorem	honpncani 31624	Hilbert space operator cancellation law. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
⊢ 𝑅: ℋ⟶ ℋ    &   ⊢ 𝑆: ℋ⟶ ℋ    &   ⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ ((𝑅 −op 𝑆) +op (𝑆 −op 𝑇)) = (𝑅 −op 𝑇)
Theorem	ho01i 31625*	A condition implying that a Hilbert space operator is identically zero. Lemma 3.2(S8) of [Beran] p. 95. (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.)
⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑦) = 0 ↔ 𝑇 = 0hop )
Theorem	ho02i 31626*	A condition implying that a Hilbert space operator is identically zero. Lemma 3.2(S10) of [Beran] p. 95. (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.)
⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = 0 ↔ 𝑇 = 0hop )
Theorem	hoeq1 31627*	A condition implying that two Hilbert space operators are equal. Lemma 3.2(S9) of [Beran] p. 95. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑆‘𝑥) ·ih 𝑦) = ((𝑇‘𝑥) ·ih 𝑦) ↔ 𝑆 = 𝑇))
Theorem	hoeq2 31628*	A condition implying that two Hilbert space operators are equal. Lemma 3.2(S11) of [Beran] p. 95. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑆‘𝑦)) = (𝑥 ·ih (𝑇‘𝑦)) ↔ 𝑆 = 𝑇))
Theorem	adjmo 31629*	Every Hilbert space operator has at most one adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
⊢ ∃*𝑢(𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦))
Theorem	adjsym 31630*	Symmetry property of an adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦)))
Theorem	eigrei 31631	A necessary and sufficient condition (that holds when 𝑇 is a Hermitian operator) for an eigenvalue 𝐵 to be real. Generalization of Equation 1.30 of [Hughes] p. 49. (Contributed by NM, 21-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ) → ((𝐴 ·ih (𝑇‘𝐴)) = ((𝑇‘𝐴) ·ih 𝐴) ↔ 𝐵 ∈ ℝ))
Theorem	eigre 31632	A necessary and sufficient condition (that holds when 𝑇 is a Hermitian operator) for an eigenvalue 𝐵 to be real. Generalization of Equation 1.30 of [Hughes] p. 49. (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.)
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → ((𝐴 ·ih (𝑇‘𝐴)) = ((𝑇‘𝐴) ·ih 𝐴) ↔ 𝐵 ∈ ℝ))
Theorem	eigposi 31633	A sufficient condition (first conjunct pair, that holds when 𝑇 is a positive operator) for an eigenvalue 𝐵 (second conjunct pair) to be nonnegative. Remark (ii) in [Hughes] p. 137. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((((𝐴 ·ih (𝑇‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝐴 ·ih (𝑇‘𝐴))) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵))
Theorem	eigorthi 31634	A necessary and sufficient condition (that holds when 𝑇 is a Hermitian operator) for two eigenvectors 𝐴 and 𝐵 to be orthogonal. Generalization of Equation 1.31 of [Hughes] p. 49. (Contributed by NM, 23-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐷 ∈ ℂ    ⇒   ⊢ ((((𝑇‘𝐴) = (𝐶 ·ℎ 𝐴) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)) ∧ 𝐶 ≠ (∗‘𝐷)) → ((𝐴 ·ih (𝑇‘𝐵)) = ((𝑇‘𝐴) ·ih 𝐵) ↔ (𝐴 ·ih 𝐵) = 0))
Theorem	eigorth 31635	A necessary and sufficient condition (that holds when 𝑇 is a Hermitian operator) for two eigenvectors 𝐴 and 𝐵 to be orthogonal. Generalization of Equation 1.31 of [Hughes] p. 49. (Contributed by NM, 23-Mar-2006.) (New usage is discouraged.)
⊢ ((((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) ∧ (((𝑇‘𝐴) = (𝐶 ·ℎ 𝐴) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)) ∧ 𝐶 ≠ (∗‘𝐷))) → ((𝐴 ·ih (𝑇‘𝐵)) = ((𝑇‘𝐴) ·ih 𝐵) ↔ (𝐴 ·ih 𝐵) = 0))
20.6.4  Linear, continuous, bounded, Hermitian, unitary operators and norms
Definition	df-nmop 31636*	Define the norm of a Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
⊢ normop = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑡‘𝑧)))}, ℝ*, < ))
Definition	df-cnop 31637*	Define the set of continuous operators on Hilbert space. For every "epsilon" (𝑦) there is a "delta" (𝑧) such that... (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.)
⊢ ContOp = {𝑡 ∈ ( ℋ ↑m ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥))) < 𝑦)}
Definition	df-lnop 31638*	Define the set of linear operators on Hilbert space. (See df-hosum 31527 for definition of operator.) (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
⊢ LinOp = {𝑡 ∈ ( ℋ ↑m ℋ) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑡‘𝑦)) +ℎ (𝑡‘𝑧))}
Definition	df-bdop 31639	Define the set of bounded linear Hilbert space operators. (See df-hosum 31527 for definition of operator.) (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
⊢ BndLinOp = {𝑡 ∈ LinOp ∣ (normop‘𝑡) < +∞}
Definition	df-unop 31640*	Define the set of unitary operators on Hilbert space. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
⊢ UniOp = {𝑡 ∣ (𝑡: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡‘𝑥) ·ih (𝑡‘𝑦)) = (𝑥 ·ih 𝑦))}
Definition	df-hmop 31641*	Define the set of Hermitian operators on Hilbert space. Some books call these "symmetric operators" and others call them "self-adjoint operators", sometimes with slightly different technical meanings. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
⊢ HrmOp = {𝑡 ∈ ( ℋ ↑m ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦)}
20.6.5  Linear and continuous functionals and norms
Definition	df-nmfn 31642*	Define the norm of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
⊢ normfn = (𝑡 ∈ (ℂ ↑m ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (abs‘(𝑡‘𝑧)))}, ℝ*, < ))
Definition	df-nlfn 31643	Define the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
⊢ null = (𝑡 ∈ (ℂ ↑m ℋ) ↦ (◡𝑡 “ {0}))
Definition	df-cnfn 31644*	Define the set of continuous functionals on Hilbert space. For every "epsilon" (𝑦) there is a "delta" (𝑧) such that... (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
⊢ ContFn = {𝑡 ∈ (ℂ ↑m ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (abs‘((𝑡‘𝑤) − (𝑡‘𝑥))) < 𝑦)}
Definition	df-lnfn 31645*	Define the set of linear functionals on Hilbert space. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
⊢ LinFn = {𝑡 ∈ (ℂ ↑m ℋ) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))}
20.6.6  Adjoint
Definition	df-adjh 31646*	Define the adjoint of a Hilbert space operator (if it exists). The domain of adjℎ is the set of all adjoint operators. Definition of adjoint in [Kalmbach2] p. 8. Unlike Kalmbach (and most authors), we do not demand that the operator be linear, but instead show (in adjbdln 31880) that the adjoint exists for a bounded linear operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.)
⊢ adjℎ = {⟨𝑡, 𝑢⟩ ∣ (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢‘𝑦)))}
20.6.7  Dirac bra-ket notation
Definition	df-bra 31647*	Define the bra of a vector used by Dirac notation. Based on definition of bra in [Prugovecki] p. 186 (p. 180 in 1971 edition). In Dirac bra-ket notation, ⟨𝐴 ∣ 𝐵⟩ is a complex number equal to the inner product (𝐵 ·ih 𝐴). But physicists like to talk about the individual components ⟨𝐴 ∣ and ∣ 𝐵⟩, called bra and ket respectively. In order for their properties to make sense formally, we define the ket ∣ 𝐵⟩ as the vector 𝐵 itself, and the bra ⟨𝐴 ∣ as a functional from ℋ to ℂ. We represent the Dirac notation ⟨𝐴 ∣ 𝐵⟩ by ((bra‘𝐴)‘𝐵); see braval 31741. The reversal of the inner product arguments not only makes the bra-ket behavior consistent with physics literature (see comments under ax-his3 30881) but is also required in order for the associative law kbass2 31914 to work. Our definition of bra and the associated outer product df-kb 31648 differs from, but is equivalent to, a common approach in the literature that makes use of mappings to a dual space. Our approach eliminates the need to have a parallel development of this dual space and instead keeps everything in Hilbert space. For an extensive discussion about how our notation maps to the bra-ket notation in physics textbooks, see mmnotes.txt 31648, under the 17-May-2006 entry. (Contributed by NM, 15-May-2006.) (New usage is discouraged.)
⊢ bra = (𝑥 ∈ ℋ ↦ (𝑦 ∈ ℋ ↦ (𝑦 ·ih 𝑥)))
Definition	df-kb 31648*	Define a commuted bra and ket juxtaposition used by Dirac notation. In Dirac notation, ∣ 𝐴⟩⟨𝐵 ∣ is an operator known as the outer product of 𝐴 and 𝐵, which we represent by (𝐴 ketbra 𝐵). Based on Equation 8.1 of [Prugovecki] p. 376. This definition, combined with Definition df-bra 31647, allows any legal juxtaposition of bras and kets to make sense formally and also to obey the associative law when mapped back to Dirac notation. (Contributed by NM, 15-May-2006.) (New usage is discouraged.)
⊢ ketbra = (𝑥 ∈ ℋ, 𝑦 ∈ ℋ ↦ (𝑧 ∈ ℋ ↦ ((𝑧 ·ih 𝑦) ·ℎ 𝑥)))
20.6.8  Positive operators
Definition	df-leop 31649*	Define positive operator ordering. Definition VI.1 of [Retherford] p. 49. Note that ( ℋ × 0ℋ) ≤op 𝑇 means that 𝑇 is a positive operator. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
⊢ ≤op = {⟨𝑡, 𝑢⟩ ∣ ((𝑢 −op 𝑡) ∈ HrmOp ∧ ∀𝑥 ∈ ℋ 0 ≤ (((𝑢 −op 𝑡)‘𝑥) ·ih 𝑥))}
20.6.9  Eigenvectors, eigenvalues, spectrum
Definition	df-eigvec 31650*	Define the eigenvector function. Theorem eleigveccl 31756 shows that eigvec‘𝑇, the set of eigenvectors of Hilbert space operator 𝑇, are Hilbert space vectors. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
⊢ eigvec = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ {𝑥 ∈ ( ℋ ∖ 0ℋ) ∣ ∃𝑧 ∈ ℂ (𝑡‘𝑥) = (𝑧 ·ℎ 𝑥)})
Definition	df-eigval 31651*	Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 31758 shows that (eigval‘𝑇)‘𝐴, the eigenvalue associated with eigenvector 𝐴, is a complex number. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
⊢ eigval = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ (eigvec‘𝑡) ↦ (((𝑡‘𝑥) ·ih 𝑥) / ((normℎ‘𝑥)↑2))))
Definition	df-spec 31652*	Define the spectrum of an operator. Definition of spectrum in [Halmos] p. 50. (Contributed by NM, 11-Apr-2006.) (New usage is discouraged.)
⊢ Lambda = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ {𝑥 ∈ ℂ ∣ ¬ (𝑡 −op (𝑥 ·op ( I ↾ ℋ))): ℋ–1-1→ ℋ})
20.6.10  Theorems about operators and functionals
Theorem	nmopval 31653*	Value of the norm of a Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → (normop‘𝑇) = sup({𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}, ℝ*, < ))
Theorem	elcnop 31654*	Property defining a continuous Hilbert space operator. (Contributed by NM, 28-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ (𝑇 ∈ ContOp ↔ (𝑇: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (normℎ‘((𝑇‘𝑤) −ℎ (𝑇‘𝑥))) < 𝑦)))
Theorem	ellnop 31655*	Property defining a linear Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinOp ↔ (𝑇: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑇‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑇‘𝑦)) +ℎ (𝑇‘𝑧))))
Theorem	lnopf 31656	A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinOp → 𝑇: ℋ⟶ ℋ)
Theorem	elbdop 31657	Property defining a bounded linear Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ (𝑇 ∈ BndLinOp ↔ (𝑇 ∈ LinOp ∧ (normop‘𝑇) < +∞))
Theorem	bdopln 31658	A bounded linear Hilbert space operator is a linear operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ BndLinOp → 𝑇 ∈ LinOp)
Theorem	bdopf 31659	A bounded linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ BndLinOp → 𝑇: ℋ⟶ ℋ)
Theorem	nmopsetretALT 31660*	The set in the supremum of the operator norm definition df-nmop 31636 is a set of reals. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ⊆ ℝ)
Theorem	nmopsetretHIL 31661*	The set in the supremum of the operator norm definition df-nmop 31636 is a set of reals. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ⊆ ℝ)
Theorem	nmopsetn0 31662*	The set in the supremum of the operator norm definition df-nmop 31636 is nonempty. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.)
⊢ (normℎ‘(𝑇‘0ℎ)) ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}
Theorem	nmopxr 31663	The norm of a Hilbert space operator is an extended real. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → (normop‘𝑇) ∈ ℝ*)
Theorem	nmoprepnf 31664	The norm of a Hilbert space operator is either real or plus infinity. (Contributed by NM, 5-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → ((normop‘𝑇) ∈ ℝ ↔ (normop‘𝑇) ≠ +∞))
Theorem	nmopgtmnf 31665	The norm of a Hilbert space operator is not minus infinity. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → -∞ < (normop‘𝑇))
Theorem	nmopreltpnf 31666	The norm of a Hilbert space operator is real iff it is less than infinity. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → ((normop‘𝑇) ∈ ℝ ↔ (normop‘𝑇) < +∞))
Theorem	nmopre 31667	The norm of a bounded operator is a real number. (Contributed by NM, 29-Jan-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ BndLinOp → (normop‘𝑇) ∈ ℝ)
Theorem	elbdop2 31668	Property defining a bounded linear Hilbert space operator. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ BndLinOp ↔ (𝑇 ∈ LinOp ∧ (normop‘𝑇) ∈ ℝ))
Theorem	elunop 31669*	Property defining a unitary Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ UniOp ↔ (𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih (𝑇‘𝑦)) = (𝑥 ·ih 𝑦)))
Theorem	elhmop 31670*	Property defining a Hermitian Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ (𝑇 ∈ HrmOp ↔ (𝑇: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦)))
Theorem	hmopf 31671	A Hermitian operator is a Hilbert space operator (mapping). (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ HrmOp → 𝑇: ℋ⟶ ℋ)
Theorem	hmopex 31672	The class of Hermitian operators is a set. (Contributed by NM, 17-Aug-2006.) (New usage is discouraged.)
⊢ HrmOp ∈ V
Theorem	nmfnval 31673*	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 31674*	The set in the supremum of the functional norm definition df-nmfn 31642 is a set of reals. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ℂ → {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘(𝑇‘𝑦)))} ⊆ ℝ)
Theorem	nmfnsetn0 31675*	The set in the supremum of the functional norm definition df-nmfn 31642 is nonempty. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
⊢ (abs‘(𝑇‘0ℎ)) ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘(𝑇‘𝑦)))}
Theorem	nmfnxr 31676	The norm of any Hilbert space functional is an extended real. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ℂ → (normfn‘𝑇) ∈ ℝ*)
Theorem	nmfnrepnf 31677	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 31678	Value of the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ℂ → (null‘𝑇) = (◡𝑇 “ {0}))
Theorem	elcnfn 31679*	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 31680*	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 31681	A linear Hilbert space functional is a functional. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinFn → 𝑇: ℋ⟶ℂ)
Theorem	dfadj2 31682*	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 31683	Functionality of the adjoint function. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
⊢ Fun adjℎ
Theorem	dmadjss 31684	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 31685	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 31686*	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 31687*	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 31688*	Value of the adjoint function. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ dom adjℎ → (adjℎ‘𝑇) = (℩𝑢 ∈ ( ℋ ↑m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢‘𝑦))))
Theorem	cnvadj 31689	The adjoint function equals its converse. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
⊢ ◡adjℎ = adjℎ
Theorem	funcnvadj 31690	The converse of the adjoint function is a function. (Contributed by NM, 25-Jan-2006.) (New usage is discouraged.)
⊢ Fun ◡adjℎ
Theorem	adj1o 31691	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 31692	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 31693*	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 31694*	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 31695*	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 31696	The spectrum of an operator is a set of complex numbers. (Contributed by NM, 11-Apr-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → (Lambda‘𝑇) ⊆ ℂ)
Theorem	hhlnoi 31697	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 31698	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 31699	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 31700	The zero operator in Hilbert space. (Contributed by NM, 7-Dec-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑍 = (𝑈 0op 𝑈)    ⇒   ⊢ 0hop = 𝑍