P. 325 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32401-32500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hodseqi 32401	Subtraction and addition of equal Hilbert space operators. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.)
⊢ 𝑆: ℋ⟶ ℋ    &   ⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ (𝑆 +op (𝑇 −op 𝑆)) = 𝑇
Theorem	ho0subi 32402	Subtraction of Hilbert space operators expressed in terms of difference from zero. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
⊢ 𝑆: ℋ⟶ ℋ    &   ⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ (𝑆 −op 𝑇) = (𝑆 +op ( 0hop −op 𝑇))
Theorem	honegsubi 32403	Relationship between Hilbert operator addition and subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
⊢ 𝑆: ℋ⟶ ℋ    &   ⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ (𝑆 +op ( -1 ·op 𝑇)) = (𝑆 −op 𝑇)
Theorem	ho0sub 32404	Subtraction of Hilbert space operators expressed in terms of difference from zero. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.)
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑆 −op 𝑇) = (𝑆 +op ( 0hop −op 𝑇)))
Theorem	hosubid1 32405	The zero operator subtracted from a Hilbert space operator. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → (𝑇 −op 0hop ) = 𝑇)
Theorem	honegsub 32406	Relationship between Hilbert space operator addition and subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑇 +op ( -1 ·op 𝑈)) = (𝑇 −op 𝑈))
Theorem	homullid 32407	An operator equals its scalar product with one. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → (1 ·op 𝑇) = 𝑇)
Theorem	homco1 32408	Associative law for scalar product and composition of operators. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ((𝐴 ·op 𝑇) ∘ 𝑈) = (𝐴 ·op (𝑇 ∘ 𝑈)))
Theorem	homulass 32409	Scalar product associative law for Hilbert space operators. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → ((𝐴 · 𝐵) ·op 𝑇) = (𝐴 ·op (𝐵 ·op 𝑇)))
Theorem	hoadddi 32410	Scalar product distributive law for Hilbert space operators. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝐴 ·op (𝑇 +op 𝑈)) = ((𝐴 ·op 𝑇) +op (𝐴 ·op 𝑈)))
Theorem	hoadddir 32411	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 32412	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 32413	Double negative of a Hilbert space operator. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → ( -1 ·op ( -1 ·op 𝑇)) = 𝑇)
Theorem	hosubneg 32414	Relationship between operator subtraction and negative. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑇 −op ( -1 ·op 𝑈)) = (𝑇 +op 𝑈))
Theorem	hosubdi 32415	Scalar product distributive law for operator difference. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝐴 ·op (𝑇 −op 𝑈)) = ((𝐴 ·op 𝑇) −op (𝐴 ·op 𝑈)))
Theorem	honegdi 32416	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 32417	Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ( -1 ·op (𝑇 −op 𝑈)) = (( -1 ·op 𝑇) +op 𝑈))
Theorem	honegsubdi2 32418	Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ( -1 ·op (𝑇 −op 𝑈)) = (𝑈 −op 𝑇))
Theorem	hosubsub2 32419	Law for double subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑆 −op (𝑇 −op 𝑈)) = (𝑆 +op (𝑈 −op 𝑇)))
Theorem	hosub4 32420	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 32421	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 32422	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 32423	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 32424	Law for double subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑆 −op (𝑇 −op 𝑈)) = ((𝑆 −op 𝑇) +op 𝑈))
Theorem	hosubsub4 32425	Law for double subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ((𝑆 −op 𝑇) −op 𝑈) = (𝑆 −op (𝑇 +op 𝑈)))
Theorem	ho2times 32426	Two times a Hilbert space operator. (Contributed by NM, 26-Aug-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → (2 ·op 𝑇) = (𝑇 +op 𝑇))
Theorem	hoaddsubassi 32427	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 32428	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 32429	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 32430	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 32431	Hilbert space operator cancellation law. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
⊢ 𝑇: ℋ⟶ ℋ    &   ⊢ 𝑈: ℋ⟶ ℋ    ⇒   ⊢ ((𝑇 +op 𝑈) −op 𝑈) = 𝑇
Theorem	honpcani 32432	Hilbert space operator cancellation law. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
⊢ 𝑇: ℋ⟶ ℋ    &   ⊢ 𝑈: ℋ⟶ ℋ    ⇒   ⊢ ((𝑇 −op 𝑈) +op 𝑈) = 𝑇
Theorem	hosubeq0i 32433	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 32434	Hilbert space operator cancellation law. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
⊢ 𝑅: ℋ⟶ ℋ    &   ⊢ 𝑆: ℋ⟶ ℋ    &   ⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ ((𝑅 −op 𝑆) +op (𝑆 −op 𝑇)) = (𝑅 −op 𝑇)
Theorem	ho01i 32435*	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 32436*	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 32437*	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 32438*	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 32439*	Every Hilbert space operator has at most one adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
⊢ ∃*𝑢(𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦))
Theorem	adjsym 32440*	Symmetry property of an adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦)))
Theorem	eigrei 32441	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 32442	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 32443	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 32444	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 32445	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 32446*	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 32447*	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 32448*	Define the set of linear operators on Hilbert space. (See df-hosum 32337 for definition of operator.) (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
⊢ LinOp = {𝑡 ∈ ( ℋ ↑m ℋ) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑡‘𝑦)) +ℎ (𝑡‘𝑧))}
Definition	df-bdop 32449	Define the set of bounded linear Hilbert space operators. (See df-hosum 32337 for definition of operator.) (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
⊢ BndLinOp = {𝑡 ∈ LinOp ∣ (normop‘𝑡) < +∞}
Definition	df-unop 32450*	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 32451*	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 32452*	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 32453	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 32454*	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 32455*	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 32456*	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 32690) 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 32457*	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 32551. The reversal of the inner product arguments not only makes the bra-ket behavior consistent with physics literature (see comments under ax-his3 31691) but is also required in order for the associative law kbass2 32724 to work. Our definition of bra and the associated outer product df-kb 32458 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 32458, under the 17-May-2006 entry. (Contributed by NM, 15-May-2006.) (New usage is discouraged.)
⊢ bra = (𝑥 ∈ ℋ ↦ (𝑦 ∈ ℋ ↦ (𝑦 ·ih 𝑥)))
Definition	df-kb 32458*	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 32457, 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 32459*	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 32460*	Define the eigenvector function. Theorem eleigveccl 32566 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 32461*	Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 32568 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 32462*	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 32463*	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 32464*	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 32465*	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 32466	A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinOp → 𝑇: ℋ⟶ ℋ)
Theorem	elbdop 32467	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 32468	A bounded linear Hilbert space operator is a linear operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ BndLinOp → 𝑇 ∈ LinOp)
Theorem	bdopf 32469	A bounded linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ BndLinOp → 𝑇: ℋ⟶ ℋ)
Theorem	nmopsetretALT 32470*	The set in the supremum of the operator norm definition df-nmop 32446 is a set of reals. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ⊆ ℝ)
Theorem	nmopsetretHIL 32471*	The set in the supremum of the operator norm definition df-nmop 32446 is a set of reals. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ⊆ ℝ)
Theorem	nmopsetn0 32472*	The set in the supremum of the operator norm definition df-nmop 32446 is nonempty. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.)
⊢ (normℎ‘(𝑇‘0ℎ)) ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}
Theorem	nmopxr 32473	The norm of a Hilbert space operator is an extended real. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → (normop‘𝑇) ∈ ℝ*)
Theorem	nmoprepnf 32474	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 32475	The norm of a Hilbert space operator is not minus infinity. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → -∞ < (normop‘𝑇))
Theorem	nmopreltpnf 32476	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 32477	The norm of a bounded operator is a real number. (Contributed by NM, 29-Jan-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ BndLinOp → (normop‘𝑇) ∈ ℝ)
Theorem	elbdop2 32478	Property defining a bounded linear Hilbert space operator. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ BndLinOp ↔ (𝑇 ∈ LinOp ∧ (normop‘𝑇) ∈ ℝ))
Theorem	elunop 32479*	Property defining a unitary Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ UniOp ↔ (𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih (𝑇‘𝑦)) = (𝑥 ·ih 𝑦)))
Theorem	elhmop 32480*	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 32481	A Hermitian operator is a Hilbert space operator (mapping). (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ HrmOp → 𝑇: ℋ⟶ ℋ)
Theorem	hmopex 32482	The class of Hermitian operators is a set. (Contributed by NM, 17-Aug-2006.) (New usage is discouraged.)
⊢ HrmOp ∈ V
Theorem	nmfnval 32483*	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 32484*	The set in the supremum of the functional norm definition df-nmfn 32452 is a set of reals. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ℂ → {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘(𝑇‘𝑦)))} ⊆ ℝ)
Theorem	nmfnsetn0 32485*	The set in the supremum of the functional norm definition df-nmfn 32452 is nonempty. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
⊢ (abs‘(𝑇‘0ℎ)) ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘(𝑇‘𝑦)))}
Theorem	nmfnxr 32486	The norm of any Hilbert space functional is an extended real. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ℂ → (normfn‘𝑇) ∈ ℝ*)
Theorem	nmfnrepnf 32487	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 32488	Value of the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ℂ → (null‘𝑇) = (◡𝑇 “ {0}))
Theorem	elcnfn 32489*	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 32490*	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 32491	A linear Hilbert space functional is a functional. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinFn → 𝑇: ℋ⟶ℂ)
Theorem	dfadj2 32492*	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 32493	Functionality of the adjoint function. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
⊢ Fun adjℎ
Theorem	dmadjss 32494	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 32495	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 32496*	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 32497*	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 32498*	Value of the adjoint function. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ dom adjℎ → (adjℎ‘𝑇) = (℩𝑢 ∈ ( ℋ ↑m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢‘𝑦))))
Theorem	cnvadj 32499	The adjoint function equals its converse. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
⊢ ◡adjℎ = adjℎ
Theorem	funcnvadj 32500	The converse of the adjoint function is a function. (Contributed by NM, 25-Jan-2006.) (New usage is discouraged.)
⊢ Fun ◡adjℎ