P. 312 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 31101-31200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ipasslem11 31101	Lemma for ipassi 31102. Show the inner product associative law for all complex numbers. (Contributed by NM, 25-Aug-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐴 ∈ 𝑋    &   ⊢ 𝐵 ∈ 𝑋    ⇒   ⊢ (𝐶 ∈ ℂ → ((𝐶𝑆𝐴)𝑃𝐵) = (𝐶 · (𝐴𝑃𝐵)))
Theorem	ipassi 31102	Associative law for inner product. Equation I2 of [Ponnusamy] p. 363. (Contributed by NM, 25-Aug-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝑆𝐵)𝑃𝐶) = (𝐴 · (𝐵𝑃𝐶)))
Theorem	dipdir 31103	Distributive law for inner product. Equation I3 of [Ponnusamy] p. 362. (Contributed by NM, 25-Aug-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝑃𝐶) = ((𝐴𝑃𝐶) + (𝐵𝑃𝐶)))
Theorem	dipdi 31104	Distributive law for inner product. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑃(𝐵𝐺𝐶)) = ((𝐴𝑃𝐵) + (𝐴𝑃𝐶)))
Theorem	ip2dii 31105	Inner product of two sums. (Contributed by NM, 17-Apr-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐴 ∈ 𝑋    &   ⊢ 𝐵 ∈ 𝑋    &   ⊢ 𝐶 ∈ 𝑋    &   ⊢ 𝐷 ∈ 𝑋    ⇒   ⊢ ((𝐴𝐺𝐵)𝑃(𝐶𝐺𝐷)) = (((𝐴𝑃𝐶) + (𝐵𝑃𝐷)) + ((𝐴𝑃𝐷) + (𝐵𝑃𝐶)))
Theorem	dipass 31106	Associative law for inner product. Equation I2 of [Ponnusamy] p. 363. (Contributed by NM, 25-Aug-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑆𝐵)𝑃𝐶) = (𝐴 · (𝐵𝑃𝐶)))
Theorem	dipassr 31107	"Associative" law for second argument of inner product (compare dipass 31106). (Contributed by NM, 22-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑃(𝐵𝑆𝐶)) = ((∗‘𝐵) · (𝐴𝑃𝐶)))
Theorem	dipassr2 31108	"Associative" law for inner product. Conjugate version of dipassr 31107. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑃((∗‘𝐵)𝑆𝐶)) = (𝐵 · (𝐴𝑃𝐶)))
Theorem	dipsubdir 31109	Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑀𝐵)𝑃𝐶) = ((𝐴𝑃𝐶) − (𝐵𝑃𝐶)))
Theorem	dipsubdi 31110	Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑃(𝐵𝑀𝐶)) = ((𝐴𝑃𝐵) − (𝐴𝑃𝐶)))
Theorem	pythi 31111	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 31112	Lemma for sii 31115. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐴 ∈ 𝑋    &   ⊢ 𝐵 ∈ 𝑋    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ (𝐶 · (𝐴𝑃𝐵)) ∈ ℝ    &   ⊢ 0 ≤ (𝐶 · (𝐴𝑃𝐵))    ⇒   ⊢ ((𝐵𝑃𝐴) = (𝐶 · ((𝑁‘𝐵)↑2)) → (√‘((𝐴𝑃𝐵) · (𝐶 · ((𝑁‘𝐵)↑2)))) ≤ ((𝑁‘𝐴) · (𝑁‘𝐵)))
Theorem	siilem2 31113	Lemma for sii 31115. (Contributed by NM, 24-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐴 ∈ 𝑋    &   ⊢ 𝐵 ∈ 𝑋    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝐶 ∈ ℂ ∧ (𝐶 · (𝐴𝑃𝐵)) ∈ ℝ ∧ 0 ≤ (𝐶 · (𝐴𝑃𝐵))) → ((𝐵𝑃𝐴) = (𝐶 · ((𝑁‘𝐵)↑2)) → (√‘((𝐴𝑃𝐵) · (𝐶 · ((𝑁‘𝐵)↑2)))) ≤ ((𝑁‘𝐴) · (𝑁‘𝐵))))
Theorem	siii 31114	Inference from sii 31115. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐴 ∈ 𝑋    &   ⊢ 𝐵 ∈ 𝑋    ⇒   ⊢ (abs‘(𝐴𝑃𝐵)) ≤ ((𝑁‘𝐴) · (𝑁‘𝐵))
Theorem	sii 31115	Obsolete version of ipcau 25358 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 31381, bcsiALT 31440, bcsiHIL 31441, csbren 25519. (Contributed by NM, 12-Jan-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    ⇒   ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (abs‘(𝐴𝑃𝐵)) ≤ ((𝑁‘𝐴) · (𝑁‘𝐵)))
Theorem	ipblnfi 31116*	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 31117*	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 31118*	A condition implying that two operators are equal. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    ⇒   ⊢ ((𝑆:𝑌⟶𝑋 ∧ 𝑇:𝑌⟶𝑋) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥𝑃(𝑆‘𝑦)) = (𝑥𝑃(𝑇‘𝑦)) ↔ 𝑆 = 𝑇))
Theorem	ajmoi 31119*	Every operator has at most one adjoint. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    ⇒   ⊢ ∃*𝑠(𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑇‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))
Theorem	ajfuni 31120	The adjoint function is a function. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.)
⊢ 𝐴 = (𝑈adj𝑊)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝑊 ∈ NrmCVec    ⇒   ⊢ Fun 𝐴
Theorem	ajfun 31121	The adjoint function is a function. This is not immediately apparent from df-aj 31011 but results from the uniqueness shown by ajmoi 31119. (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.)
⊢ 𝐴 = (𝑈adj𝑊)    ⇒   ⊢ ((𝑈 ∈ CPreHilOLD ∧ 𝑊 ∈ NrmCVec) → Fun 𝐴)
Theorem	ajval 31122*	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 31123	Extend class notation with the class of all complex Banach spaces.
class CBan
Definition	df-cbn 31124	Define the class of all complex Banach spaces. (Contributed by NM, 5-Dec-2006.) Use df-bn 25456 instead. (New usage is discouraged.)
⊢ CBan = {𝑢 ∈ NrmCVec ∣ (IndMet‘𝑢) ∈ (CMet‘(BaseSet‘𝑢))}
Theorem	iscbn 31125	A complex Banach space is a normed complex vector space with a complete induced metric. (Contributed by NM, 5-Dec-2006.) Use isbn 25458 instead. (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ (𝑈 ∈ CBan ↔ (𝑈 ∈ NrmCVec ∧ 𝐷 ∈ (CMet‘𝑋)))
Theorem	cbncms 31126	The induced metric on complex Banach space is complete. (Contributed by NM, 8-Sep-2007.) Use bncmet 25467 (or preferably bncms 25464) instead. (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ (𝑈 ∈ CBan → 𝐷 ∈ (CMet‘𝑋))
Theorem	bnnv 31127	Every complex Banach space is a normed complex vector space. (Contributed by NM, 17-Mar-2007.) Use bnnvc 25460 instead. (New usage is discouraged.)
⊢ (𝑈 ∈ CBan → 𝑈 ∈ NrmCVec)
Theorem	bnrel 31128	The class of all complex Banach spaces is a relation. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.)
⊢ Rel CBan
Theorem	bnsscmcl 31129	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 31130	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 31131*	Lemma for ubth 31134. 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 25450, 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 31132*	Lemma for ubth 31134. 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 31133*	Lemma for ubth 31134. Prove the reverse implication, using nmblolbi 31061. (Contributed by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑊)    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝑈 ∈ CBan    &   ⊢ 𝑊 ∈ NrmCVec    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑈 BLnOp 𝑊))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑))
Theorem	ubth 31134*	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 31135*	Lemma for minveco 31145. 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 31136*	Lemma for minveco 31145. 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 31137*	Lemma for minveco 31145. 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 31138*	Lemma for minveco 31145. 𝐹 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 31139*	Lemma for minveco 31145. 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 31140*	Lemma for minveco 31145. 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 31141*	Lemma for minveco 31145. 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 31142*	Lemma for minveco 31145. Discharge the assumption about the sequence 𝐹 by applying countable choice ax-cc 10407. (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 31143*	Lemma for minveco 31145. 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 31144*	Lemma for minveco 31145. 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 31145*	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 31146	Extend class notation with the class of all complex Hilbert spaces.
class CHilOLD
Definition	df-hlo 31147	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 31148	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 31149	Every complex Hilbert space is a complex Banach space. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.)
⊢ (𝑈 ∈ CHilOLD → 𝑈 ∈ CBan)
Theorem	hlph 31150	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 31151	The class of all complex Hilbert spaces is a relation. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.)
⊢ Rel CHilOLD
Theorem	hlnv 31152	Every complex Hilbert space is a normed complex vector space. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.)
⊢ (𝑈 ∈ CHilOLD → 𝑈 ∈ NrmCVec)
Theorem	hlnvi 31153	Every complex Hilbert space is a normed complex vector space. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.)
⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ 𝑈 ∈ NrmCVec
Theorem	hlvc 31154	Every complex Hilbert space is a complex vector space. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑊 = (1st ‘𝑈)    ⇒   ⊢ (𝑈 ∈ CHilOLD → 𝑊 ∈ CVecOLD)
Theorem	hlcmet 31155	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 31156	The induced metric on a complex Hilbert space. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ (𝑈 ∈ CHilOLD → 𝐷 ∈ (Met‘𝑋))
Theorem	hlpar2 31157	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 31158	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 31159	The base set of a Hilbert space is a set. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    ⇒   ⊢ 𝑋 ∈ V
Theorem	hladdf 31160	Mapping for Hilbert space vector addition. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    ⇒   ⊢ (𝑈 ∈ CHilOLD → 𝐺:(𝑋 × 𝑋)⟶𝑋)
Theorem	hlcom 31161	Hilbert space vector addition is commutative. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) = (𝐵𝐺𝐴))
Theorem	hlass 31162	Hilbert space vector addition is associative. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = (𝐴𝐺(𝐵𝐺𝐶)))
Theorem	hl0cl 31163	The Hilbert space zero vector. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    ⇒   ⊢ (𝑈 ∈ CHilOLD → 𝑍 ∈ 𝑋)
Theorem	hladdid 31164	Hilbert space addition with the zero vector. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺𝑍) = 𝐴)
Theorem	hlmulf 31165	Mapping for Hilbert space scalar multiplication. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ (𝑈 ∈ CHilOLD → 𝑆:(ℂ × 𝑋)⟶𝑋)
Theorem	hlmulid 31166	Hilbert space scalar multiplication by one. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋) → (1𝑆𝐴) = 𝐴)
Theorem	hlmulass 31167	Hilbert space scalar multiplication associative law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → ((𝐴 · 𝐵)𝑆𝐶) = (𝐴𝑆(𝐵𝑆𝐶)))
Theorem	hldi 31168	Hilbert space scalar multiplication distributive law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑆(𝐵𝐺𝐶)) = ((𝐴𝑆𝐵)𝐺(𝐴𝑆𝐶)))
Theorem	hldir 31169	Hilbert space scalar multiplication distributive law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → ((𝐴 + 𝐵)𝑆𝐶) = ((𝐴𝑆𝐶)𝐺(𝐵𝑆𝐶)))
Theorem	hlmul0 31170	Hilbert space scalar multiplication by zero. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋) → (0𝑆𝐴) = 𝑍)
Theorem	hlipf 31171	Mapping for Hilbert space inner product. (Contributed by NM, 19-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ (𝑈 ∈ CHilOLD → 𝑃:(𝑋 × 𝑋)⟶ℂ)
Theorem	hlipcj 31172	Conjugate law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑃𝐵) = (∗‘(𝐵𝑃𝐴)))
Theorem	hlipdir 31173	Distributive law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝑃𝐶) = ((𝐴𝑃𝐶) + (𝐵𝑃𝐶)))
Theorem	hlipass 31174	Associative law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑆𝐵)𝑃𝐶) = (𝐴 · (𝐵𝑃𝐶)))
Theorem	hlipgt0 31175	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 31176	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 31177	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 31178*	Lemma for htth 31179. The collection 𝐾, which consists of functions 𝐹(𝑧)(𝑤) = ⟨𝑤 ∣ 𝑇(𝑧)⟩ = ⟨𝑇(𝑤) ∣ 𝑧⟩ for each 𝑧 in the unit ball, is a collection of bounded linear functions by ipblnfi 31116, so by the Uniform Boundedness theorem ubth 31134, 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 31179*	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 21814; note that df-hil 21814 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 31180	Extend class notation with Hilbert vector space.
class ℋ
Syntax	cva 31181	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 11091.
class +ℎ
Syntax	csm 31182	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 31183	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 4592.
class ·ih
Syntax	cno 31184	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 31185	Extend class notation with zero vector in Hilbert space.
class 0ℎ
Syntax	cmv 31186	Extend class notation with vector subtraction in Hilbert space.
class −ℎ
Syntax	ccauold 31187	Extend class notation with set of Cauchy sequences in Hilbert space.
class Cauchy
Syntax	chli 31188	Extend class notation with convergence relation in Hilbert space.
class ⇝𝑣
Syntax	csh 31189	Extend class notation with set of subspaces of a Hilbert space.
class Sℋ
Syntax	cch 31190	Extend class notation with set of closed subspaces of a Hilbert space.
class Cℋ
Syntax	cort 31191	Extend class notation with orthogonal complement in Cℋ.
class ⊥
Syntax	cph 31192	Extend class notation with subspace sum in Cℋ.
class +ℋ
Syntax	cspn 31193	Extend class notation with subspace span in Cℋ.
class span
Syntax	chj 31194	Extend class notation with join in Cℋ.
class ∨ℋ
Syntax	chsup 31195	Extend class notation with supremum of a collection in Cℋ.
class ∨ℋ
Syntax	c0h 31196	Extend class notation with zero of Cℋ.
class 0ℋ
Syntax	ccm 31197	Extend class notation with the commutes relation on a Hilbert lattice.
class 𝐶ℋ
Syntax	cpjh 31198	Extend class notation with set of projections on a Hilbert space.
class projℎ
Syntax	chos 31199	Extend class notation with sum of Hilbert space operators.
class +op
Syntax	chot 31200	Extend class notation with scalar product of a Hilbert space operator.
class ·op