P. 319 of Theorem List - Metamath Proof Explorer

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

Type	Label	Description
Statement
Theorem	hoaddass 31801	Associativity of sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑅: ℋ⟶ ℋ ∧ 𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → ((𝑅 +op 𝑆) +op 𝑇) = (𝑅 +op (𝑆 +op 𝑇)))
Theorem	hoadd32 31802	Commutative/associative law for Hilbert space operator sum that swaps the second and third terms. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑅: ℋ⟶ ℋ ∧ 𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → ((𝑅 +op 𝑆) +op 𝑇) = ((𝑅 +op 𝑇) +op 𝑆))
Theorem	hoadd4 31803	Rearrangement of 4 terms in a sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
⊢ (((𝑅: ℋ⟶ ℋ ∧ 𝑆: ℋ⟶ ℋ) ∧ (𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ)) → ((𝑅 +op 𝑆) +op (𝑇 +op 𝑈)) = ((𝑅 +op 𝑇) +op (𝑆 +op 𝑈)))
Theorem	hocsubdir 31804	Distributive law for Hilbert space operator difference. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑅: ℋ⟶ ℋ ∧ 𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → ((𝑅 −op 𝑆) ∘ 𝑇) = ((𝑅 ∘ 𝑇) −op (𝑆 ∘ 𝑇)))
Theorem	hoaddridi 31805	Sum of a Hilbert space operator with the zero operator. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.)
⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ (𝑇 +op 0hop ) = 𝑇
Theorem	hodidi 31806	Difference of a Hilbert space operator from itself. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ (𝑇 −op 𝑇) = 0hop
Theorem	ho0coi 31807	Composition of the zero operator and a Hilbert space operator. (Contributed by NM, 9-Aug-2006.) (New usage is discouraged.)
⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ ( 0hop ∘ 𝑇) = 0hop
Theorem	hoid1i 31808	Composition of Hilbert space operator with unit identity. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.)
⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ (𝑇 ∘ Iop ) = 𝑇
Theorem	hoid1ri 31809	Composition of Hilbert space operator with unit identity. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.)
⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ ( Iop ∘ 𝑇) = 𝑇
Theorem	hoaddrid 31810	Sum of a Hilbert space operator with the zero operator. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → (𝑇 +op 0hop ) = 𝑇)
Theorem	hodid 31811	Difference of a Hilbert space operator from itself. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → (𝑇 −op 𝑇) = 0hop )
Theorem	hon0 31812	A Hilbert space operator is not empty. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → ¬ 𝑇 = ∅)
Theorem	hodseqi 31813	Subtraction and addition of equal Hilbert space operators. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.)
⊢ 𝑆: ℋ⟶ ℋ    &   ⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ (𝑆 +op (𝑇 −op 𝑆)) = 𝑇
Theorem	ho0subi 31814	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 31815	Relationship between Hilbert operator addition and subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
⊢ 𝑆: ℋ⟶ ℋ    &   ⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ (𝑆 +op (-1 ·op 𝑇)) = (𝑆 −op 𝑇)
Theorem	ho0sub 31816	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 31817	The zero operator subtracted from a Hilbert space operator. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → (𝑇 −op 0hop ) = 𝑇)
Theorem	honegsub 31818	Relationship between Hilbert space operator addition and subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑇 +op (-1 ·op 𝑈)) = (𝑇 −op 𝑈))
Theorem	homullid 31819	An operator equals its scalar product with one. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → (1 ·op 𝑇) = 𝑇)
Theorem	homco1 31820	Associative law for scalar product and composition of operators. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ((𝐴 ·op 𝑇) ∘ 𝑈) = (𝐴 ·op (𝑇 ∘ 𝑈)))
Theorem	homulass 31821	Scalar product associative law for Hilbert space operators. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → ((𝐴 · 𝐵) ·op 𝑇) = (𝐴 ·op (𝐵 ·op 𝑇)))
Theorem	hoadddi 31822	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 31823	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 31824	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 31825	Double negative of a Hilbert space operator. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → (-1 ·op (-1 ·op 𝑇)) = 𝑇)
Theorem	hosubneg 31826	Relationship between operator subtraction and negative. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑇 −op (-1 ·op 𝑈)) = (𝑇 +op 𝑈))
Theorem	hosubdi 31827	Scalar product distributive law for operator difference. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝐴 ·op (𝑇 −op 𝑈)) = ((𝐴 ·op 𝑇) −op (𝐴 ·op 𝑈)))
Theorem	honegdi 31828	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 31829	Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (-1 ·op (𝑇 −op 𝑈)) = ((-1 ·op 𝑇) +op 𝑈))
Theorem	honegsubdi2 31830	Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (-1 ·op (𝑇 −op 𝑈)) = (𝑈 −op 𝑇))
Theorem	hosubsub2 31831	Law for double subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑆 −op (𝑇 −op 𝑈)) = (𝑆 +op (𝑈 −op 𝑇)))
Theorem	hosub4 31832	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 31833	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 31834	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 31835	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 31836	Law for double subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑆 −op (𝑇 −op 𝑈)) = ((𝑆 −op 𝑇) +op 𝑈))
Theorem	hosubsub4 31837	Law for double subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.)
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ((𝑆 −op 𝑇) −op 𝑈) = (𝑆 −op (𝑇 +op 𝑈)))
Theorem	ho2times 31838	Two times a Hilbert space operator. (Contributed by NM, 26-Aug-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → (2 ·op 𝑇) = (𝑇 +op 𝑇))
Theorem	hoaddsubassi 31839	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 31840	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 31841	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 31842	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 31843	Hilbert space operator cancellation law. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
⊢ 𝑇: ℋ⟶ ℋ    &   ⊢ 𝑈: ℋ⟶ ℋ    ⇒   ⊢ ((𝑇 +op 𝑈) −op 𝑈) = 𝑇
Theorem	honpcani 31844	Hilbert space operator cancellation law. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
⊢ 𝑇: ℋ⟶ ℋ    &   ⊢ 𝑈: ℋ⟶ ℋ    ⇒   ⊢ ((𝑇 −op 𝑈) +op 𝑈) = 𝑇
Theorem	hosubeq0i 31845	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 31846	Hilbert space operator cancellation law. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
⊢ 𝑅: ℋ⟶ ℋ    &   ⊢ 𝑆: ℋ⟶ ℋ    &   ⊢ 𝑇: ℋ⟶ ℋ    ⇒   ⊢ ((𝑅 −op 𝑆) +op (𝑆 −op 𝑇)) = (𝑅 −op 𝑇)
Theorem	ho01i 31847*	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 31848*	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 31849*	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 31850*	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 31851*	Every Hilbert space operator has at most one adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
⊢ ∃*𝑢(𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦))
Theorem	adjsym 31852*	Symmetry property of an adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·ih 𝑦)))
Theorem	eigrei 31853	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 31854	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 31855	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 31856	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 31857	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 31858*	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 31859*	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 31860*	Define the set of linear operators on Hilbert space. (See df-hosum 31749 for definition of operator.) (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
⊢ LinOp = {𝑡 ∈ ( ℋ ↑m ℋ) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 ·ℎ (𝑡‘𝑦)) +ℎ (𝑡‘𝑧))}
Definition	df-bdop 31861	Define the set of bounded linear Hilbert space operators. (See df-hosum 31749 for definition of operator.) (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
⊢ BndLinOp = {𝑡 ∈ LinOp ∣ (normop‘𝑡) < +∞}
Definition	df-unop 31862*	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 31863*	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 31864*	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 31865	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 31866*	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 31867*	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 31868*	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 32102) 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 31869*	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 31963. The reversal of the inner product arguments not only makes the bra-ket behavior consistent with physics literature (see comments under ax-his3 31103) but is also required in order for the associative law kbass2 32136 to work. Our definition of bra and the associated outer product df-kb 31870 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 31870, under the 17-May-2006 entry. (Contributed by NM, 15-May-2006.) (New usage is discouraged.)
⊢ bra = (𝑥 ∈ ℋ ↦ (𝑦 ∈ ℋ ↦ (𝑦 ·ih 𝑥)))
Definition	df-kb 31870*	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 31869, 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 31871*	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 31872*	Define the eigenvector function. Theorem eleigveccl 31978 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 31873*	Define the eigenvalue function. The range of eigval‘𝑇 is the set of eigenvalues of Hilbert space operator 𝑇. Theorem eigvalcl 31980 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 31874*	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 31875*	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 31876*	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 31877*	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 31878	A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ LinOp → 𝑇: ℋ⟶ ℋ)
Theorem	elbdop 31879	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 31880	A bounded linear Hilbert space operator is a linear operator. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ BndLinOp → 𝑇 ∈ LinOp)
Theorem	bdopf 31881	A bounded linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ BndLinOp → 𝑇: ℋ⟶ ℋ)
Theorem	nmopsetretALT 31882*	The set in the supremum of the operator norm definition df-nmop 31858 is a set of reals. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ⊆ ℝ)
Theorem	nmopsetretHIL 31883*	The set in the supremum of the operator norm definition df-nmop 31858 is a set of reals. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ⊆ ℝ)
Theorem	nmopsetn0 31884*	The set in the supremum of the operator norm definition df-nmop 31858 is nonempty. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.)
⊢ (normℎ‘(𝑇‘0ℎ)) ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}
Theorem	nmopxr 31885	The norm of a Hilbert space operator is an extended real. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → (normop‘𝑇) ∈ ℝ*)
Theorem	nmoprepnf 31886	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 31887	The norm of a Hilbert space operator is not minus infinity. (Contributed by NM, 2-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ ℋ → -∞ < (normop‘𝑇))
Theorem	nmopreltpnf 31888	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 31889	The norm of a bounded operator is a real number. (Contributed by NM, 29-Jan-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ BndLinOp → (normop‘𝑇) ∈ ℝ)
Theorem	elbdop2 31890	Property defining a bounded linear Hilbert space operator. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ BndLinOp ↔ (𝑇 ∈ LinOp ∧ (normop‘𝑇) ∈ ℝ))
Theorem	elunop 31891*	Property defining a unitary Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ UniOp ↔ (𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih (𝑇‘𝑦)) = (𝑥 ·ih 𝑦)))
Theorem	elhmop 31892*	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 31893	A Hermitian operator is a Hilbert space operator (mapping). (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.)
⊢ (𝑇 ∈ HrmOp → 𝑇: ℋ⟶ ℋ)
Theorem	hmopex 31894	The class of Hermitian operators is a set. (Contributed by NM, 17-Aug-2006.) (New usage is discouraged.)
⊢ HrmOp ∈ V
Theorem	nmfnval 31895*	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 31896*	The set in the supremum of the functional norm definition df-nmfn 31864 is a set of reals. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ℂ → {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘(𝑇‘𝑦)))} ⊆ ℝ)
Theorem	nmfnsetn0 31897*	The set in the supremum of the functional norm definition df-nmfn 31864 is nonempty. (Contributed by NM, 14-Feb-2006.) (New usage is discouraged.)
⊢ (abs‘(𝑇‘0ℎ)) ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ ((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (abs‘(𝑇‘𝑦)))}
Theorem	nmfnxr 31898	The norm of any Hilbert space functional is an extended real. (Contributed by NM, 9-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ℂ → (normfn‘𝑇) ∈ ℝ*)
Theorem	nmfnrepnf 31899	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 31900	Value of the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
⊢ (𝑇: ℋ⟶ℂ → (null‘𝑇) = (◡𝑇 “ {0}))