Home Metamath Proof ExplorerTheorem List (p. 297 of 454) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

 Color key: Metamath Proof Explorer (1-28711) Hilbert Space Explorer (28712-30234) Users' Mathboxes (30235-45374)

Theorem List for Metamath Proof Explorer - 29601-29700   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremhosubdi 29601 Scalar product distributive law for operator difference. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)
((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝐴 ·op (𝑇op 𝑈)) = ((𝐴 ·op 𝑇) −op (𝐴 ·op 𝑈)))

Theoremhonegdi 29602 Distribution of negative over addition. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (-1 ·op (𝑇 +op 𝑈)) = ((-1 ·op 𝑇) +op (-1 ·op 𝑈)))

Theoremhonegsubdi 29603 Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (-1 ·op (𝑇op 𝑈)) = ((-1 ·op 𝑇) +op 𝑈))

Theoremhonegsubdi2 29604 Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (-1 ·op (𝑇op 𝑈)) = (𝑈op 𝑇))

Theoremhosubsub2 29605 Law for double subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑆op (𝑇op 𝑈)) = (𝑆 +op (𝑈op 𝑇)))

Theoremhosub4 29606 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 𝑈)))

Theoremhosubadd4 29607 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 𝑇)))

Theoremhoaddsubass 29608 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 𝑈)))

Theoremhoaddsub 29609 Law for operator addition and subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.)
((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ((𝑆 +op 𝑇) −op 𝑈) = ((𝑆op 𝑈) +op 𝑇))

Theoremhosubsub 29610 Law for double subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.)
((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑆op (𝑇op 𝑈)) = ((𝑆op 𝑇) +op 𝑈))

Theoremhosubsub4 29611 Law for double subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.)
((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ((𝑆op 𝑇) −op 𝑈) = (𝑆op (𝑇 +op 𝑈)))

Theoremho2times 29612 Two times a Hilbert space operator. (Contributed by NM, 26-Aug-2006.) (New usage is discouraged.)
(𝑇: ℋ⟶ ℋ → (2 ·op 𝑇) = (𝑇 +op 𝑇))

Theoremhoaddsubassi 29613 Associativity of sum and difference of Hilbert space operators. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.)
𝑅: ℋ⟶ ℋ    &   𝑆: ℋ⟶ ℋ    &   𝑇: ℋ⟶ ℋ       ((𝑅 +op 𝑆) −op 𝑇) = (𝑅 +op (𝑆op 𝑇))

Theoremhoaddsubi 29614 Law for sum and difference of Hilbert space operators. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.)
𝑅: ℋ⟶ ℋ    &   𝑆: ℋ⟶ ℋ    &   𝑇: ℋ⟶ ℋ       ((𝑅 +op 𝑆) −op 𝑇) = ((𝑅op 𝑇) +op 𝑆)

Theoremhosd1i 29615 Hilbert space operator sum expressed in terms of difference. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.)
𝑇: ℋ⟶ ℋ    &   𝑈: ℋ⟶ ℋ       (𝑇 +op 𝑈) = (𝑇op ( 0hopop 𝑈))

Theoremhosd2i 29616 Hilbert space operator sum expressed in terms of difference. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.)
𝑇: ℋ⟶ ℋ    &   𝑈: ℋ⟶ ℋ       (𝑇 +op 𝑈) = (𝑇op ((𝑈op 𝑈) −op 𝑈))

Theoremhopncani 29617 Hilbert space operator cancellation law. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
𝑇: ℋ⟶ ℋ    &   𝑈: ℋ⟶ ℋ       ((𝑇 +op 𝑈) −op 𝑈) = 𝑇

Theoremhonpcani 29618 Hilbert space operator cancellation law. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
𝑇: ℋ⟶ ℋ    &   𝑈: ℋ⟶ ℋ       ((𝑇op 𝑈) +op 𝑈) = 𝑇

Theoremhosubeq0i 29619 If the difference between two operators is zero, they are equal. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.)
𝑇: ℋ⟶ ℋ    &   𝑈: ℋ⟶ ℋ       ((𝑇op 𝑈) = 0hop𝑇 = 𝑈)

Theoremhonpncani 29620 Hilbert space operator cancellation law. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
𝑅: ℋ⟶ ℋ    &   𝑆: ℋ⟶ ℋ    &   𝑇: ℋ⟶ ℋ       ((𝑅op 𝑆) +op (𝑆op 𝑇)) = (𝑅op 𝑇)

Theoremho01i 29621* 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 )

Theoremho02i 29622* 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 )

Theoremhoeq1 29623* 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 𝑦) ↔ 𝑆 = 𝑇))

Theoremhoeq2 29624* 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 (𝑇𝑦)) ↔ 𝑆 = 𝑇))

Theoremadjmo 29625* Every Hilbert space operator has at most one adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
∃*𝑢(𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑢𝑥) ·ih 𝑦))

Theoremadjsym 29626* Symmetry property of an adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑆𝑦)) = ((𝑇𝑥) ·ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑆𝑥) ·ih 𝑦)))

Theoremeigrei 29627 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 𝐴) ↔ 𝐵 ∈ ℝ))

Theoremeigre 29628 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 𝐴) ↔ 𝐵 ∈ ℝ))

Theoremeigposi 29629 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 ≤ 𝐵))

Theoremeigorthi 29630 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))

Theoremeigorth 29631 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))

19.6.4  Linear, continuous, bounded, Hermitian, unitary operators and norms

Definitiondf-nmop 29632* Define the norm of a Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
normop = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))}, ℝ*, < ))

Definitiondf-cnop 29633* 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‘((𝑡𝑤) − (𝑡𝑥))) < 𝑦)}

Definitiondf-lnop 29634* Define the set of linear operators on Hilbert space. (See df-hosum 29523 for definition of operator.) (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
LinOp = {𝑡 ∈ ( ℋ ↑m ℋ) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 · 𝑦) + 𝑧)) = ((𝑥 · (𝑡𝑦)) + (𝑡𝑧))}

Definitiondf-bdop 29635 Define the set of bounded linear Hilbert space operators. (See df-hosum 29523 for definition of operator.) (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
BndLinOp = {𝑡 ∈ LinOp ∣ (normop𝑡) < +∞}

Definitiondf-unop 29636* Define the set of unitary operators on Hilbert space. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
UniOp = {𝑡 ∣ (𝑡: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡𝑥) ·ih (𝑡𝑦)) = (𝑥 ·ih 𝑦))}

Definitiondf-hmop 29637* 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 𝑦)}

19.6.5  Linear and continuous functionals and norms

Definitiondf-nmfn 29638* Define the norm of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
normfn = (𝑡 ∈ (ℂ ↑m ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (abs‘(𝑡𝑧)))}, ℝ*, < ))

Definitiondf-nlfn 29639 Define the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
null = (𝑡 ∈ (ℂ ↑m ℋ) ↦ (𝑡 “ {0}))

Definitiondf-cnfn 29640* 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‘((𝑡𝑤) − (𝑡𝑥))) < 𝑦)}

Definitiondf-lnfn 29641* Define the set of linear functionals on Hilbert space. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
LinFn = {𝑡 ∈ (ℂ ↑m ℋ) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 · 𝑦) + 𝑧)) = ((𝑥 · (𝑡𝑦)) + (𝑡𝑧))}

Definitiondf-adjh 29642* 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 29876) that the adjoint exists for a bounded linear operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.)
adj = {⟨𝑡, 𝑢⟩ ∣ (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢𝑦)))}

19.6.7  Dirac bra-ket notation

Definitiondf-bra 29643* 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 29737. The reversal of the inner product arguments not only makes the bra-ket behavior consistent with physics literature (see comments under ax-his3 28877) but is also required in order for the associative law kbass2 29910 to work.

Our definition of bra and the associated outer product df-kb 29644 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 29644, under the 17-May-2006 entry. (Contributed by NM, 15-May-2006.) (New usage is discouraged.)

bra = (𝑥 ∈ ℋ ↦ (𝑦 ∈ ℋ ↦ (𝑦 ·ih 𝑥)))

Definitiondf-kb 29644* 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 29643, 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 𝑦) · 𝑥)))

19.6.8  Positive operators

Definitiondf-leop 29645* 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 𝑥))}

19.6.9  Eigenvectors, eigenvalues, spectrum

Definitiondf-eigvec 29646* Define the eigenvector function. Theorem eleigveccl 29752 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) ∣ ∃𝑧 ∈ ℂ (𝑡𝑥) = (𝑧 · 𝑥)})

Definitiondf-eigval 29647* Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 29754 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))))

Definitiondf-spec 29648* 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→ ℋ})

19.6.10  Theorems about operators and functionals

Theoremnmopval 29649* 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‘(𝑇𝑦)))}, ℝ*, < ))

Theoremelcnop 29650* 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‘((𝑇𝑤) − (𝑇𝑥))) < 𝑦)))

Theoremellnop 29651* 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 ↔ (𝑇: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑇‘((𝑥 · 𝑦) + 𝑧)) = ((𝑥 · (𝑇𝑦)) + (𝑇𝑧))))

Theoremlnopf 29652 A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
(𝑇 ∈ LinOp → 𝑇: ℋ⟶ ℋ)

Theoremelbdop 29653 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𝑇) < +∞))

Theorembdopln 29654 A bounded linear Hilbert space operator is a linear operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
(𝑇 ∈ BndLinOp → 𝑇 ∈ LinOp)

Theorembdopf 29655 A bounded linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.)
(𝑇 ∈ BndLinOp → 𝑇: ℋ⟶ ℋ)

TheoremnmopsetretALT 29656* The set in the supremum of the operator norm definition df-nmop 29632 is a set of reals. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) (Proof modification is discouraged.)
(𝑇: ℋ⟶ ℋ → {𝑥 ∣ ∃𝑦 ∈ ℋ ((norm𝑦) ≤ 1 ∧ 𝑥 = (norm‘(𝑇𝑦)))} ⊆ ℝ)

TheoremnmopsetretHIL 29657* The set in the supremum of the operator norm definition df-nmop 29632 is a set of reals. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.)
(𝑇: ℋ⟶ ℋ → {𝑥 ∣ ∃𝑦 ∈ ℋ ((norm𝑦) ≤ 1 ∧ 𝑥 = (norm‘(𝑇𝑦)))} ⊆ ℝ)

Theoremnmopsetn0 29658* The set in the supremum of the operator norm definition df-nmop 29632 is nonempty. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.)
(norm‘(𝑇‘0)) ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ ((norm𝑦) ≤ 1 ∧ 𝑥 = (norm‘(𝑇𝑦)))}

Theoremnmopxr 29659 The norm of a Hilbert space operator is an extended real. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.)
(𝑇: ℋ⟶ ℋ → (normop𝑇) ∈ ℝ*)

Theoremnmoprepnf 29660 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𝑇) ≠ +∞))

Theoremnmopgtmnf 29661 The norm of a Hilbert space operator is not minus infinity. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.)
(𝑇: ℋ⟶ ℋ → -∞ < (normop𝑇))

Theoremnmopreltpnf 29662 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𝑇) < +∞))

Theoremnmopre 29663 The norm of a bounded operator is a real number. (Contributed by NM, 29-Jan-2006.) (New usage is discouraged.)
(𝑇 ∈ BndLinOp → (normop𝑇) ∈ ℝ)

Theoremelbdop2 29664 Property defining a bounded linear Hilbert space operator. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
(𝑇 ∈ BndLinOp ↔ (𝑇 ∈ LinOp ∧ (normop𝑇) ∈ ℝ))

Theoremelunop 29665* Property defining a unitary Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
(𝑇 ∈ UniOp ↔ (𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇𝑥) ·ih (𝑇𝑦)) = (𝑥 ·ih 𝑦)))

Theoremelhmop 29666* 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 𝑦)))

Theoremhmopf 29667 A Hermitian operator is a Hilbert space operator (mapping). (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.)
(𝑇 ∈ HrmOp → 𝑇: ℋ⟶ ℋ)

Theoremhmopex 29668 The class of Hermitian operators is a set. (Contributed by NM, 17-Aug-2006.) (New usage is discouraged.)
HrmOp ∈ V

Theoremnmfnval 29669* 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‘(𝑇𝑦)))}, ℝ*, < ))

Theoremnmfnsetre 29670* The set in the supremum of the functional norm definition df-nmfn 29638 is a set of reals. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
(𝑇: ℋ⟶ℂ → {𝑥 ∣ ∃𝑦 ∈ ℋ ((norm𝑦) ≤ 1 ∧ 𝑥 = (abs‘(𝑇𝑦)))} ⊆ ℝ)

Theoremnmfnsetn0 29671* The set in the supremum of the functional norm definition df-nmfn 29638 is nonempty. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
(abs‘(𝑇‘0)) ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ ((norm𝑦) ≤ 1 ∧ 𝑥 = (abs‘(𝑇𝑦)))}

Theoremnmfnxr 29672 The norm of any Hilbert space functional is an extended real. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.)
(𝑇: ℋ⟶ℂ → (normfn𝑇) ∈ ℝ*)

Theoremnmfnrepnf 29673 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𝑇) ≠ +∞))

Theoremnlfnval 29674 Value of the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
(𝑇: ℋ⟶ℂ → (null‘𝑇) = (𝑇 “ {0}))

Theoremelcnfn 29675* 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‘((𝑇𝑤) − (𝑇𝑥))) < 𝑦)))

Theoremellnfn 29676* Property defining a linear functional. (Contributed by NM, 11-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
(𝑇 ∈ LinFn ↔ (𝑇: ℋ⟶ℂ ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑇‘((𝑥 · 𝑦) + 𝑧)) = ((𝑥 · (𝑇𝑦)) + (𝑇𝑧))))

Theoremlnfnf 29677 A linear Hilbert space functional is a functional. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
(𝑇 ∈ LinFn → 𝑇: ℋ⟶ℂ)

Theoremdfadj2 29678* Alternate definition of the adjoint of a Hilbert space operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.)
adj = {⟨𝑡, 𝑢⟩ ∣ (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡𝑦)) = ((𝑢𝑥) ·ih 𝑦))}

Theoremfunadj 29679 Functionality of the adjoint function. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)

Theoremdmadjss 29680 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 ℋ)

Theoremdmadjop 29681 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𝑇: ℋ⟶ ℋ)

Theoremadjeu 29682* 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 𝑦)))

Theoremadjval 29683* 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 𝑦)))

Theoremadjval2 29684* Value of the adjoint function. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)
(𝑇 ∈ dom adj → (adj𝑇) = (𝑢 ∈ ( ℋ ↑m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢𝑦))))

Theoremcnvadj 29685 The adjoint function equals its converse. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)

Theoremfuncnvadj 29686 The converse of the adjoint function is a function. (Contributed by NM, 25-Jan-2006.) (New usage is discouraged.)

Theoremadj1o 29687 The adjoint function maps one-to-one onto its domain. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)

Theoremdmadjrn 29688 The adjoint of an operator belongs to the adjoint function's domain. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)

Theoremeigvecval 29689* 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) ∣ ∃𝑦 ∈ ℂ (𝑇𝑥) = (𝑦 · 𝑥)})

Theoremeigvalfval 29690* The eigenvalues of eigenvectors of a Hilbert space operator. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
(𝑇: ℋ⟶ ℋ → (eigval‘𝑇) = (𝑥 ∈ (eigvec‘𝑇) ↦ (((𝑇𝑥) ·ih 𝑥) / ((norm𝑥)↑2))))

Theoremspecval 29691* 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→ ℋ})

Theoremspeccl 29692 The spectrum of an operator is a set of complex numbers. (Contributed by NM, 11-Apr-2006.) (New usage is discouraged.)
(𝑇: ℋ⟶ ℋ → (Lambda‘𝑇) ⊆ ℂ)

Theoremhhlnoi 29693 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 = 𝐿

Theoremhhnmoi 29694 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 = 𝑁

Theoremhhbloi 29695 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 = 𝐵

Theoremhh0oi 29696 The zero operator in Hilbert space. (Contributed by NM, 7-Dec-2007.) (New usage is discouraged.)
𝑈 = ⟨⟨ + , · ⟩, norm    &   𝑍 = (𝑈 0op 𝑈)        0hop = 𝑍

Theoremhhcno 29697 The continuous operators of Hilbert space. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
𝐷 = (norm ∘ − )    &   𝐽 = (MetOpen‘𝐷)       ContOp = (𝐽 Cn 𝐽)

Theoremhhcnf 29698 The continuous functionals of Hilbert space. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
𝐷 = (norm ∘ − )    &   𝐽 = (MetOpen‘𝐷)    &   𝐾 = (TopOpen‘ℂfld)       ContFn = (𝐽 Cn 𝐾)

Theoremdmadjrnb 29699 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 6676.) (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)