P. 302 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 30101-30200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dipsubdir 30101	Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑀𝐵)𝑃𝐶) = ((𝐴𝑃𝐶) − (𝐵𝑃𝐶)))
Theorem	dipsubdi 30102	Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑃(𝐵𝑀𝐶)) = ((𝐴𝑃𝐵) − (𝐴𝑃𝐶)))
Theorem	pythi 30103	The Pythagorean theorem for an arbitrary complex inner product (pre-Hilbert) space 𝑈. The square of the norm of the sum of two orthogonal vectors (i.e. whose inner product is 0) is the sum of the squares of their norms. Problem 2 in [Kreyszig] p. 135. (Contributed by NM, 17-Apr-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐴 ∈ 𝑋    &   ⊢ 𝐵 ∈ 𝑋    ⇒   ⊢ ((𝐴𝑃𝐵) = 0 → ((𝑁‘(𝐴𝐺𝐵))↑2) = (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2)))
Theorem	siilem1 30104	Lemma for sii 30107. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐴 ∈ 𝑋    &   ⊢ 𝐵 ∈ 𝑋    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ (𝐶 · (𝐴𝑃𝐵)) ∈ ℝ    &   ⊢ 0 ≤ (𝐶 · (𝐴𝑃𝐵))    ⇒   ⊢ ((𝐵𝑃𝐴) = (𝐶 · ((𝑁‘𝐵)↑2)) → (√‘((𝐴𝑃𝐵) · (𝐶 · ((𝑁‘𝐵)↑2)))) ≤ ((𝑁‘𝐴) · (𝑁‘𝐵)))
Theorem	siilem2 30105	Lemma for sii 30107. (Contributed by NM, 24-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐴 ∈ 𝑋    &   ⊢ 𝐵 ∈ 𝑋    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝐶 ∈ ℂ ∧ (𝐶 · (𝐴𝑃𝐵)) ∈ ℝ ∧ 0 ≤ (𝐶 · (𝐴𝑃𝐵))) → ((𝐵𝑃𝐴) = (𝐶 · ((𝑁‘𝐵)↑2)) → (√‘((𝐴𝑃𝐵) · (𝐶 · ((𝑁‘𝐵)↑2)))) ≤ ((𝑁‘𝐴) · (𝑁‘𝐵))))
Theorem	siii 30106	Inference from sii 30107. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐴 ∈ 𝑋    &   ⊢ 𝐵 ∈ 𝑋    ⇒   ⊢ (abs‘(𝐴𝑃𝐵)) ≤ ((𝑁‘𝐴) · (𝑁‘𝐵))
Theorem	sii 30107	Obsolete version of ipcau 24755 as of 22-Sep-2024. Schwarz inequality. Part of Lemma 3-2.1(a) of [Kreyszig] p. 137. This is also called the Cauchy-Schwarz inequality by some authors and Bunjakovaskij-Cauchy-Schwarz inequality by others. See also Theorems bcseqi 30373, bcsiALT 30432, bcsiHIL 30433, csbren 24916. (Contributed by NM, 12-Jan-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    ⇒   ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (abs‘(𝐴𝑃𝐵)) ≤ ((𝑁‘𝐴) · (𝑁‘𝐵)))
Theorem	ipblnfi 30108*	A function 𝐹 generated by varying the first argument of an inner product (with its second argument a fixed vector 𝐴) is a bounded linear functional, i.e. a bounded linear operator from the vector space to ℂ. (Contributed by NM, 12-Jan-2008.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐶 = ⟨⟨ + , · ⟩, abs⟩    &   ⊢ 𝐵 = (𝑈 BLnOp 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ (𝑥𝑃𝐴))    ⇒   ⊢ (𝐴 ∈ 𝑋 → 𝐹 ∈ 𝐵)
Theorem	ip2eqi 30109*	Two vectors are equal iff their inner products with all other vectors are equal. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    ⇒   ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (∀𝑥 ∈ 𝑋 (𝑥𝑃𝐴) = (𝑥𝑃𝐵) ↔ 𝐴 = 𝐵))
Theorem	phoeqi 30110*	A condition implying that two operators are equal. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    ⇒   ⊢ ((𝑆:𝑌⟶𝑋 ∧ 𝑇:𝑌⟶𝑋) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥𝑃(𝑆‘𝑦)) = (𝑥𝑃(𝑇‘𝑦)) ↔ 𝑆 = 𝑇))
Theorem	ajmoi 30111*	Every operator has at most one adjoint. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    ⇒   ⊢ ∃*𝑠(𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑇‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))
Theorem	ajfuni 30112	The adjoint function is a function. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.)
⊢ 𝐴 = (𝑈adj𝑊)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝑊 ∈ NrmCVec    ⇒   ⊢ Fun 𝐴
Theorem	ajfun 30113	The adjoint function is a function. This is not immediately apparent from df-aj 30003 but results from the uniqueness shown by ajmoi 30111. (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.)
⊢ 𝐴 = (𝑈adj𝑊)    ⇒   ⊢ ((𝑈 ∈ CPreHilOLD ∧ 𝑊 ∈ NrmCVec) → Fun 𝐴)
Theorem	ajval 30114*	Value of the adjoint function. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑄 = (·𝑖OLD‘𝑊)    &   ⊢ 𝐴 = (𝑈adj𝑊)    ⇒   ⊢ ((𝑈 ∈ CPreHilOLD ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → (𝐴‘𝑇) = (℩𝑠(𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑇‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))))
19.6  Complex Banach spaces
19.6.1  Definition and basic properties
Syntax	ccbn 30115	Extend class notation with the class of all complex Banach spaces.
class CBan
Definition	df-cbn 30116	Define the class of all complex Banach spaces. (Contributed by NM, 5-Dec-2006.) Use df-bn 24853 instead. (New usage is discouraged.)
⊢ CBan = {𝑢 ∈ NrmCVec ∣ (IndMet‘𝑢) ∈ (CMet‘(BaseSet‘𝑢))}
Theorem	iscbn 30117	A complex Banach space is a normed complex vector space with a complete induced metric. (Contributed by NM, 5-Dec-2006.) Use isbn 24855 instead. (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ (𝑈 ∈ CBan ↔ (𝑈 ∈ NrmCVec ∧ 𝐷 ∈ (CMet‘𝑋)))
Theorem	cbncms 30118	The induced metric on complex Banach space is complete. (Contributed by NM, 8-Sep-2007.) Use bncmet 24864 (or preferably bncms 24861) instead. (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ (𝑈 ∈ CBan → 𝐷 ∈ (CMet‘𝑋))
Theorem	bnnv 30119	Every complex Banach space is a normed complex vector space. (Contributed by NM, 17-Mar-2007.) Use bnnvc 24857 instead. (New usage is discouraged.)
⊢ (𝑈 ∈ CBan → 𝑈 ∈ NrmCVec)
Theorem	bnrel 30120	The class of all complex Banach spaces is a relation. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.)
⊢ Rel CBan
Theorem	bnsscmcl 30121	A subspace of a Banach space is a Banach space iff it is closed in the norm-induced metric of the parent space. (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐻 = (SubSp‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    ⇒   ⊢ ((𝑈 ∈ CBan ∧ 𝑊 ∈ 𝐻) → (𝑊 ∈ CBan ↔ 𝑌 ∈ (Clsd‘𝐽)))
19.6.2  Examples of complex Banach spaces
Theorem	cnbn 30122	The set of complex numbers is a complex Banach space. (Contributed by Steve Rodriguez, 4-Jan-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ + , · ⟩, abs⟩    ⇒   ⊢ 𝑈 ∈ CBan
19.6.3  Uniform Boundedness Theorem
Theorem	ubthlem1 30123*	Lemma for ubth 30126. The function 𝐴 exhibits a countable collection of sets that are closed, being the inverse image under 𝑡 of the closed ball of radius 𝑘, and by assumption they cover 𝑋. Thus, by the Baire Category theorem bcth2 24847, for some 𝑛 the set 𝐴‘𝑛 has an interior, meaning that there is a closed ball {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} in the set. (Contributed by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑊)    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝑈 ∈ CBan    &   ⊢ 𝑊 ∈ NrmCVec    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑈 BLnOp 𝑊))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐)    &   ⊢ 𝐴 = (𝑘 ∈ ℕ ↦ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘})    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ ℕ ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))
Theorem	ubthlem2 30124*	Lemma for ubth 30126. Given that there is a closed ball 𝐵(𝑃, 𝑅) in 𝐴‘𝐾, for any 𝑥 ∈ 𝐵(0, 1), we have 𝑃 + 𝑅 · 𝑥 ∈ 𝐵(𝑃, 𝑅) and 𝑃 ∈ 𝐵(𝑃, 𝑅), so both of these have norm(𝑡(𝑧)) ≤ 𝐾 and so norm(𝑡(𝑥 )) ≤ (norm(𝑡(𝑃)) + norm(𝑡(𝑃 + 𝑅 · 𝑥))) / 𝑅 ≤ ( 𝐾 + 𝐾) / 𝑅, which is our desired uniform bound. (Contributed by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑊)    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝑈 ∈ CBan    &   ⊢ 𝑊 ∈ NrmCVec    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑈 BLnOp 𝑊))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐)    &   ⊢ 𝐴 = (𝑘 ∈ ℕ ↦ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘})    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → {𝑧 ∈ 𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅} ⊆ (𝐴‘𝐾))    ⇒   ⊢ (𝜑 → ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)
Theorem	ubthlem3 30125*	Lemma for ubth 30126. Prove the reverse implication, using nmblolbi 30053. (Contributed by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑊)    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝑈 ∈ CBan    &   ⊢ 𝑊 ∈ NrmCVec    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑈 BLnOp 𝑊))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑))
Theorem	ubth 30126*	Uniform Boundedness Theorem, also called the Banach-Steinhaus Theorem. Let 𝑇 be a collection of bounded linear operators on a Banach space. If, for every vector 𝑥, the norms of the operators' values are bounded, then the operators' norms are also bounded. Theorem 4.7-3 of [Kreyszig] p. 249. See also http://en.wikipedia.org/wiki/Uniform_boundedness_principle. (Contributed by NM, 7-Nov-2007.) (Proof shortened by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑊)    &   ⊢ 𝑀 = (𝑈 normOpOLD 𝑊)    ⇒   ⊢ ((𝑈 ∈ CBan ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ⊆ (𝑈 BLnOp 𝑊)) → (∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑀‘𝑡) ≤ 𝑑))
19.6.4  Minimizing Vector Theorem
Theorem	minvecolem1 30127*	Lemma for minveco 30137. The set of all distances from points of 𝑌 to 𝐴 are a nonempty set of nonnegative reals. (Contributed by Mario Carneiro, 8-May-2014.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ (𝜑 → 𝑈 ∈ CPreHilOLD)    &   ⊢ (𝜑 → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))    ⇒   ⊢ (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
Theorem	minvecolem2 30128*	Lemma for minveco 30137. Any two points 𝐾 and 𝐿 in 𝑌 are close to each other if they are close to the infimum of distance to 𝐴. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ (𝜑 → 𝑈 ∈ CPreHilOLD)    &   ⊢ (𝜑 → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐿 ∈ 𝑌)    &   ⊢ (𝜑 → ((𝐴𝐷𝐾)↑2) ≤ ((𝑆↑2) + 𝐵))    &   ⊢ (𝜑 → ((𝐴𝐷𝐿)↑2) ≤ ((𝑆↑2) + 𝐵))    ⇒   ⊢ (𝜑 → ((𝐾𝐷𝐿)↑2) ≤ (4 · 𝐵))
Theorem	minvecolem3 30129*	Lemma for minveco 30137. The sequence formed by taking elements successively closer to the infimum is Cauchy. (Contributed by Mario Carneiro, 8-May-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ (𝜑 → 𝑈 ∈ CPreHilOLD)    &   ⊢ (𝜑 → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ (𝜑 → 𝐹:ℕ⟶𝑌)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴𝐷(𝐹‘𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷))
Theorem	minvecolem4a 30130*	Lemma for minveco 30137. 𝐹 is convergent in the subspace topology on 𝑌. (Contributed by Mario Carneiro, 7-May-2014.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ (𝜑 → 𝑈 ∈ CPreHilOLD)    &   ⊢ (𝜑 → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ (𝜑 → 𝐹:ℕ⟶𝑌)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴𝐷(𝐹‘𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))    ⇒   ⊢ (𝜑 → 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹))
Theorem	minvecolem4b 30131*	Lemma for minveco 30137. The convergent point of the cauchy sequence 𝐹 is a member of the base space. (Contributed by Mario Carneiro, 16-Jun-2014.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ (𝜑 → 𝑈 ∈ CPreHilOLD)    &   ⊢ (𝜑 → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ (𝜑 → 𝐹:ℕ⟶𝑌)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴𝐷(𝐹‘𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))    ⇒   ⊢ (𝜑 → ((⇝𝑡‘𝐽)‘𝐹) ∈ 𝑋)
Theorem	minvecolem4c 30132*	Lemma for minveco 30137. The infimum of the distances to 𝐴 is a real number. (Contributed by Mario Carneiro, 16-Jun-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ (𝜑 → 𝑈 ∈ CPreHilOLD)    &   ⊢ (𝜑 → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ (𝜑 → 𝐹:ℕ⟶𝑌)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴𝐷(𝐹‘𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))    ⇒   ⊢ (𝜑 → 𝑆 ∈ ℝ)
Theorem	minvecolem4 30133*	Lemma for minveco 30137. The convergent point of the cauchy sequence 𝐹 attains the minimum distance, and so is closer to 𝐴 than any other point in 𝑌. (Contributed by Mario Carneiro, 7-May-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ (𝜑 → 𝑈 ∈ CPreHilOLD)    &   ⊢ (𝜑 → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ (𝜑 → 𝐹:ℕ⟶𝑌)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴𝐷(𝐹‘𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))    &   ⊢ 𝑇 = (1 / (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)))
Theorem	minvecolem5 30134*	Lemma for minveco 30137. Discharge the assumption about the sequence 𝐹 by applying countable choice ax-cc 10430. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ (𝜑 → 𝑈 ∈ CPreHilOLD)    &   ⊢ (𝜑 → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)))
Theorem	minvecolem6 30135*	Lemma for minveco 30137. Any minimal point is less than 𝑆 away from 𝐴. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ (𝜑 → 𝑈 ∈ CPreHilOLD)    &   ⊢ (𝜑 → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦))))
Theorem	minvecolem7 30136*	Lemma for minveco 30137. Since any two minimal points are distance zero away from each other, the minimal point is unique. (Contributed by Mario Carneiro, 9-May-2014.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ (𝜑 → 𝑈 ∈ CPreHilOLD)    &   ⊢ (𝜑 → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)))
Theorem	minveco 30137*	Minimizing vector theorem, or the Hilbert projection theorem. There is exactly one vector in a complete subspace 𝑊 that minimizes the distance to an arbitrary vector 𝐴 in a parent inner product space. Theorem 3.3-1 of [Kreyszig] p. 144, specialized to subspaces instead of convex subsets. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Mario Carneiro, 9-May-2014.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ (𝜑 → 𝑈 ∈ CPreHilOLD)    &   ⊢ (𝜑 → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)))
19.7  Complex Hilbert spaces
19.7.1  Definition and basic properties
Syntax	chlo 30138	Extend class notation with the class of all complex Hilbert spaces.
class CHilOLD
Definition	df-hlo 30139	Define the class of all complex Hilbert spaces. A Hilbert space is a Banach space which is also an inner product space. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.)
⊢ CHilOLD = (CBan ∩ CPreHilOLD)
Theorem	ishlo 30140	The predicate "is a complex Hilbert space." A Hilbert space is a Banach space which is also an inner product space, i.e. whose norm satisfies the parallelogram law. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.)
⊢ (𝑈 ∈ CHilOLD ↔ (𝑈 ∈ CBan ∧ 𝑈 ∈ CPreHilOLD))
Theorem	hlobn 30141	Every complex Hilbert space is a complex Banach space. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.)
⊢ (𝑈 ∈ CHilOLD → 𝑈 ∈ CBan)
Theorem	hlph 30142	Every complex Hilbert space is an inner product space (also called a pre-Hilbert space). (Contributed by NM, 28-Apr-2007.) (New usage is discouraged.)
⊢ (𝑈 ∈ CHilOLD → 𝑈 ∈ CPreHilOLD)
Theorem	hlrel 30143	The class of all complex Hilbert spaces is a relation. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.)
⊢ Rel CHilOLD
Theorem	hlnv 30144	Every complex Hilbert space is a normed complex vector space. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.)
⊢ (𝑈 ∈ CHilOLD → 𝑈 ∈ NrmCVec)
Theorem	hlnvi 30145	Every complex Hilbert space is a normed complex vector space. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.)
⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ 𝑈 ∈ NrmCVec
Theorem	hlvc 30146	Every complex Hilbert space is a complex vector space. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑊 = (1st ‘𝑈)    ⇒   ⊢ (𝑈 ∈ CHilOLD → 𝑊 ∈ CVecOLD)
Theorem	hlcmet 30147	The induced metric on a complex Hilbert space is complete. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ (𝑈 ∈ CHilOLD → 𝐷 ∈ (CMet‘𝑋))
Theorem	hlmet 30148	The induced metric on a complex Hilbert space. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ (𝑈 ∈ CHilOLD → 𝐷 ∈ (Met‘𝑋))
Theorem	hlpar2 30149	The parallelogram law satisfied by Hilbert space vectors. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝑁‘(𝐴𝐺𝐵))↑2) + ((𝑁‘(𝐴𝑀𝐵))↑2)) = (2 · (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2))))
Theorem	hlpar 30150	The parallelogram law satisfied by Hilbert space vectors. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝑁‘(𝐴𝐺𝐵))↑2) + ((𝑁‘(𝐴𝐺(-1𝑆𝐵)))↑2)) = (2 · (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2))))
19.7.2  Standard axioms for a complex Hilbert space
Theorem	hlex 30151	The base set of a Hilbert space is a set. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    ⇒   ⊢ 𝑋 ∈ V
Theorem	hladdf 30152	Mapping for Hilbert space vector addition. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    ⇒   ⊢ (𝑈 ∈ CHilOLD → 𝐺:(𝑋 × 𝑋)⟶𝑋)
Theorem	hlcom 30153	Hilbert space vector addition is commutative. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) = (𝐵𝐺𝐴))
Theorem	hlass 30154	Hilbert space vector addition is associative. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = (𝐴𝐺(𝐵𝐺𝐶)))
Theorem	hl0cl 30155	The Hilbert space zero vector. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    ⇒   ⊢ (𝑈 ∈ CHilOLD → 𝑍 ∈ 𝑋)
Theorem	hladdid 30156	Hilbert space addition with the zero vector. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺𝑍) = 𝐴)
Theorem	hlmulf 30157	Mapping for Hilbert space scalar multiplication. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ (𝑈 ∈ CHilOLD → 𝑆:(ℂ × 𝑋)⟶𝑋)
Theorem	hlmulid 30158	Hilbert space scalar multiplication by one. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋) → (1𝑆𝐴) = 𝐴)
Theorem	hlmulass 30159	Hilbert space scalar multiplication associative law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → ((𝐴 · 𝐵)𝑆𝐶) = (𝐴𝑆(𝐵𝑆𝐶)))
Theorem	hldi 30160	Hilbert space scalar multiplication distributive law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑆(𝐵𝐺𝐶)) = ((𝐴𝑆𝐵)𝐺(𝐴𝑆𝐶)))
Theorem	hldir 30161	Hilbert space scalar multiplication distributive law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → ((𝐴 + 𝐵)𝑆𝐶) = ((𝐴𝑆𝐶)𝐺(𝐵𝑆𝐶)))
Theorem	hlmul0 30162	Hilbert space scalar multiplication by zero. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋) → (0𝑆𝐴) = 𝑍)
Theorem	hlipf 30163	Mapping for Hilbert space inner product. (Contributed by NM, 19-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ (𝑈 ∈ CHilOLD → 𝑃:(𝑋 × 𝑋)⟶ℂ)
Theorem	hlipcj 30164	Conjugate law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑃𝐵) = (∗‘(𝐵𝑃𝐴)))
Theorem	hlipdir 30165	Distributive law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝑃𝐶) = ((𝐴𝑃𝐶) + (𝐵𝑃𝐶)))
Theorem	hlipass 30166	Associative law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑆𝐵)𝑃𝐶) = (𝐴 · (𝐵𝑃𝐶)))
Theorem	hlipgt0 30167	The inner product of a Hilbert space vector by itself is positive. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 𝑍) → 0 < (𝐴𝑃𝐴))
Theorem	hlcompl 30168	Completeness of a Hilbert space. (Contributed by NM, 8-Sep-2007.) (Revised by Mario Carneiro, 9-May-2014.) (New usage is discouraged.)
⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐹 ∈ (Cau‘𝐷)) → 𝐹 ∈ dom (⇝𝑡‘𝐽))
19.7.3  Examples of complex Hilbert spaces
Theorem	cnchl 30169	The set of complex numbers is a complex Hilbert space. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ + , · ⟩, abs⟩    ⇒   ⊢ 𝑈 ∈ CHilOLD
19.7.4  Hellinger-Toeplitz Theorem
Theorem	htthlem 30170*	Lemma for htth 30171. The collection 𝐾, which consists of functions 𝐹(𝑧)(𝑤) = ⟨𝑤 ∣ 𝑇(𝑧)⟩ = ⟨𝑇(𝑤) ∣ 𝑧⟩ for each 𝑧 in the unit ball, is a collection of bounded linear functions by ipblnfi 30108, so by the Uniform Boundedness theorem ubth 30126, there is a uniform bound 𝑦 on ∥ 𝐹(𝑥) ∥ for all 𝑥 in the unit ball. Then ∣ 𝑇(𝑥) ∣ ↑2 = ⟨𝑇(𝑥) ∣ 𝑇(𝑥)⟩ = 𝐹(𝑥)( 𝑇(𝑥)) ≤ 𝑦 ∣ 𝑇(𝑥) ∣, so ∣ 𝑇(𝑥) ∣ ≤ 𝑦 and 𝑇 is bounded. (Contributed by NM, 11-Jan-2008.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑈)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑈 ∈ CHilOLD    &   ⊢ 𝑊 = ⟨⟨ + , · ⟩, abs⟩    &   ⊢ (𝜑 → 𝑇 ∈ 𝐿)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑃(𝑇‘𝑦)) = ((𝑇‘𝑥)𝑃𝑦))    &   ⊢ 𝐹 = (𝑧 ∈ 𝑋 ↦ (𝑤 ∈ 𝑋 ↦ (𝑤𝑃(𝑇‘𝑧))))    &   ⊢ 𝐾 = (𝐹 “ {𝑧 ∈ 𝑋 ∣ (𝑁‘𝑧) ≤ 1})    ⇒   ⊢ (𝜑 → 𝑇 ∈ 𝐵)
Theorem	htth 30171*	Hellinger-Toeplitz Theorem: any self-adjoint linear operator defined on all of Hilbert space is bounded. Theorem 10.1-1 of [Kreyszig] p. 525. Discovered by E. Hellinger and O. Toeplitz in 1910, "it aroused both admiration and puzzlement since the theorem establishes a relation between properties of two different kinds, namely, the properties of being defined everywhere and being bounded." (Contributed by NM, 11-Jan-2008.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑈)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ 𝑇 ∈ 𝐿 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑃(𝑇‘𝑦)) = ((𝑇‘𝑥)𝑃𝑦)) → 𝑇 ∈ 𝐵)
PART 20  COMPLEX HILBERT SPACE EXPLORER (DEPRECATED) This part contains the definitions and theorems used by the Hilbert Space Explorer (HSE), mmhil.html. Because it axiomatizes a single complex Hilbert space whose existence is assumed, its usefulness is limited. For example, it cannot work with real or quaternion Hilbert spaces and it cannot study relationships between two Hilbert spaces. More information can be found on the Hilbert Space Explorer page. Future development should instead work with general Hilbert spaces as defined by df-hil 21259; note that df-hil 21259 uses extensible structures. The intent is for this deprecated section to be deleted once all its theorems have been translated into extensible structure versions (or are not useful). Many of the theorems in this section have already been translated to extensible structure versions, but there is still a lot in this section that might be useful for future reference. It is much easier to translate these by hand from this section than to start from scratch from textbook proofs, since the HSE omits no details.
20.1  Axiomatization of complex pre-Hilbert spaces
20.1.1  Basic Hilbert space definitions
Syntax	chba 30172	Extend class notation with Hilbert vector space.
class ℋ
Syntax	cva 30173	Extend class notation with vector addition in Hilbert space. In the literature, the subscript "h" is omitted, but we need it to avoid ambiguity with complex number addition + caddc 11113.
class +ℎ
Syntax	csm 30174	Extend class notation with scalar multiplication in Hilbert space. In the literature scalar multiplication is usually indicated by juxtaposition, but we need an explicit symbol to prevent ambiguity.
class ·ℎ
Syntax	csp 30175	Extend class notation with inner (scalar) product in Hilbert space. In the literature, the inner product of 𝐴 and 𝐵 is usually written ⟨𝐴, 𝐵⟩ but our operation notation allows to use existing theorems about operations and also eliminates ambiguity with the definition of an ordered pair df-op 4636.
class ·ih
Syntax	cno 30176	Extend class notation with the norm function in Hilbert space. In the literature, the norm of 𝐴 is usually written "|| 𝐴 ||", but we use function notation to take advantage of our existing theorems about functions.
class normℎ
Syntax	c0v 30177	Extend class notation with zero vector in Hilbert space.
class 0ℎ
Syntax	cmv 30178	Extend class notation with vector subtraction in Hilbert space.
class −ℎ
Syntax	ccauold 30179	Extend class notation with set of Cauchy sequences in Hilbert space.
class Cauchy
Syntax	chli 30180	Extend class notation with convergence relation in Hilbert space.
class ⇝𝑣
Syntax	csh 30181	Extend class notation with set of subspaces of a Hilbert space.
class Sℋ
Syntax	cch 30182	Extend class notation with set of closed subspaces of a Hilbert space.
class Cℋ
Syntax	cort 30183	Extend class notation with orthogonal complement in Cℋ.
class ⊥
Syntax	cph 30184	Extend class notation with subspace sum in Cℋ.
class +ℋ
Syntax	cspn 30185	Extend class notation with subspace span in Cℋ.
class span
Syntax	chj 30186	Extend class notation with join in Cℋ.
class ∨ℋ
Syntax	chsup 30187	Extend class notation with supremum of a collection in Cℋ.
class ∨ℋ
Syntax	c0h 30188	Extend class notation with zero of Cℋ.
class 0ℋ
Syntax	ccm 30189	Extend class notation with the commutes relation on a Hilbert lattice.
class 𝐶ℋ
Syntax	cpjh 30190	Extend class notation with set of projections on a Hilbert space.
class projℎ
Syntax	chos 30191	Extend class notation with sum of Hilbert space operators.
class +op
Syntax	chot 30192	Extend class notation with scalar product of a Hilbert space operator.
class ·op
Syntax	chod 30193	Extend class notation with difference of Hilbert space operators.
class −op
Syntax	chfs 30194	Extend class notation with sum of Hilbert space functionals.
class +fn
Syntax	chft 30195	Extend class notation with scalar product of Hilbert space functional.
class ·fn
Syntax	ch0o 30196	Extend class notation with the Hilbert space zero operator.
class 0hop
Syntax	chio 30197	Extend class notation with Hilbert space identity operator.
class Iop
Syntax	cnop 30198	Extend class notation with the operator norm function.
class normop
Syntax	ccop 30199	Extend class notation with set of continuous Hilbert space operators.
class ContOp
Syntax	clo 30200	Extend class notation with set of linear Hilbert space operators.
class LinOp