P. 300 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29901-30000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hlpar2 29901	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 29902	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 29903	The base set of a Hilbert space is a set. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    ⇒   ⊢ 𝑋 ∈ V
Theorem	hladdf 29904	Mapping for Hilbert space vector addition. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    ⇒   ⊢ (𝑈 ∈ CHilOLD → 𝐺:(𝑋 × 𝑋)⟶𝑋)
Theorem	hlcom 29905	Hilbert space vector addition is commutative. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) = (𝐵𝐺𝐴))
Theorem	hlass 29906	Hilbert space vector addition is associative. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = (𝐴𝐺(𝐵𝐺𝐶)))
Theorem	hl0cl 29907	The Hilbert space zero vector. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    ⇒   ⊢ (𝑈 ∈ CHilOLD → 𝑍 ∈ 𝑋)
Theorem	hladdid 29908	Hilbert space addition with the zero vector. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺𝑍) = 𝐴)
Theorem	hlmulf 29909	Mapping for Hilbert space scalar multiplication. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ (𝑈 ∈ CHilOLD → 𝑆:(ℂ × 𝑋)⟶𝑋)
Theorem	hlmulid 29910	Hilbert space scalar multiplication by one. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋) → (1𝑆𝐴) = 𝐴)
Theorem	hlmulass 29911	Hilbert space scalar multiplication associative law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → ((𝐴 · 𝐵)𝑆𝐶) = (𝐴𝑆(𝐵𝑆𝐶)))
Theorem	hldi 29912	Hilbert space scalar multiplication distributive law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑆(𝐵𝐺𝐶)) = ((𝐴𝑆𝐵)𝐺(𝐴𝑆𝐶)))
Theorem	hldir 29913	Hilbert space scalar multiplication distributive law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → ((𝐴 + 𝐵)𝑆𝐶) = ((𝐴𝑆𝐶)𝐺(𝐵𝑆𝐶)))
Theorem	hlmul0 29914	Hilbert space scalar multiplication by zero. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋) → (0𝑆𝐴) = 𝑍)
Theorem	hlipf 29915	Mapping for Hilbert space inner product. (Contributed by NM, 19-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ (𝑈 ∈ CHilOLD → 𝑃:(𝑋 × 𝑋)⟶ℂ)
Theorem	hlipcj 29916	Conjugate law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑃𝐵) = (∗‘(𝐵𝑃𝐴)))
Theorem	hlipdir 29917	Distributive law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝑃𝐶) = ((𝐴𝑃𝐶) + (𝐵𝑃𝐶)))
Theorem	hlipass 29918	Associative law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑆𝐵)𝑃𝐶) = (𝐴 · (𝐵𝑃𝐶)))
Theorem	hlipgt0 29919	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 29920	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 29921	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 29922*	Lemma for htth 29923. The collection 𝐾, which consists of functions 𝐹(𝑧)(𝑤) = ⟨𝑤 ∣ 𝑇(𝑧)⟩ = ⟨𝑇(𝑤) ∣ 𝑧⟩ for each 𝑧 in the unit ball, is a collection of bounded linear functions by ipblnfi 29860, so by the Uniform Boundedness theorem ubth 29878, 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 29923*	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 21147; note that df-hil 21147 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 29924	Extend class notation with Hilbert vector space.
class ℋ
Syntax	cva 29925	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 11063.
class +ℎ
Syntax	csm 29926	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 29927	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 4598.
class ·ih
Syntax	cno 29928	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 29929	Extend class notation with zero vector in Hilbert space.
class 0ℎ
Syntax	cmv 29930	Extend class notation with vector subtraction in Hilbert space.
class −ℎ
Syntax	ccauold 29931	Extend class notation with set of Cauchy sequences in Hilbert space.
class Cauchy
Syntax	chli 29932	Extend class notation with convergence relation in Hilbert space.
class ⇝𝑣
Syntax	csh 29933	Extend class notation with set of subspaces of a Hilbert space.
class Sℋ
Syntax	cch 29934	Extend class notation with set of closed subspaces of a Hilbert space.
class Cℋ
Syntax	cort 29935	Extend class notation with orthogonal complement in Cℋ.
class ⊥
Syntax	cph 29936	Extend class notation with subspace sum in Cℋ.
class +ℋ
Syntax	cspn 29937	Extend class notation with subspace span in Cℋ.
class span
Syntax	chj 29938	Extend class notation with join in Cℋ.
class ∨ℋ
Syntax	chsup 29939	Extend class notation with supremum of a collection in Cℋ.
class ∨ℋ
Syntax	c0h 29940	Extend class notation with zero of Cℋ.
class 0ℋ
Syntax	ccm 29941	Extend class notation with the commutes relation on a Hilbert lattice.
class 𝐶ℋ
Syntax	cpjh 29942	Extend class notation with set of projections on a Hilbert space.
class projℎ
Syntax	chos 29943	Extend class notation with sum of Hilbert space operators.
class +op
Syntax	chot 29944	Extend class notation with scalar product of a Hilbert space operator.
class ·op
Syntax	chod 29945	Extend class notation with difference of Hilbert space operators.
class −op
Syntax	chfs 29946	Extend class notation with sum of Hilbert space functionals.
class +fn
Syntax	chft 29947	Extend class notation with scalar product of Hilbert space functional.
class ·fn
Syntax	ch0o 29948	Extend class notation with the Hilbert space zero operator.
class 0hop
Syntax	chio 29949	Extend class notation with Hilbert space identity operator.
class Iop
Syntax	cnop 29950	Extend class notation with the operator norm function.
class normop
Syntax	ccop 29951	Extend class notation with set of continuous Hilbert space operators.
class ContOp
Syntax	clo 29952	Extend class notation with set of linear Hilbert space operators.
class LinOp
Syntax	cbo 29953	Extend class notation with set of bounded linear operators.
class BndLinOp
Syntax	cuo 29954	Extend class notation with set of unitary Hilbert space operators.
class UniOp
Syntax	cho 29955	Extend class notation with set of Hermitian Hilbert space operators.
class HrmOp
Syntax	cnmf 29956	Extend class notation with the functional norm function.
class normfn
Syntax	cnl 29957	Extend class notation with the functional nullspace function.
class null
Syntax	ccnfn 29958	Extend class notation with set of continuous Hilbert space functionals.
class ContFn
Syntax	clf 29959	Extend class notation with set of linear Hilbert space functionals.
class LinFn
Syntax	cado 29960	Extend class notation with Hilbert space adjoint function.
class adjℎ
Syntax	cbr 29961	Extend class notation with the bra of a vector in Dirac bra-ket notation.
class bra
Syntax	ck 29962	Extend class notation with the outer product of two vectors in Dirac bra-ket notation.
class ketbra
Syntax	cleo 29963	Extend class notation with positive operator ordering.
class ≤op
Syntax	cei 29964	Extend class notation with Hilbert space eigenvector function.
class eigvec
Syntax	cel 29965	Extend class notation with Hilbert space eigenvalue function.
class eigval
Syntax	cspc 29966	Extend class notation with the spectrum of an operator.
class Lambda
Syntax	cst 29967	Extend class notation with set of states on a Hilbert lattice.
class States
Syntax	chst 29968	Extend class notation with set of Hilbert-space-valued states on a Hilbert lattice.
class CHStates
Syntax	ccv 29969	Extend class notation with the covers relation on a Hilbert lattice.
class ⋖ℋ
Syntax	cat 29970	Extend class notation with set of atoms on a Hilbert lattice.
class HAtoms
Syntax	cmd 29971	Extend class notation with the modular pair relation on a Hilbert lattice.
class 𝑀ℋ
Syntax	cdmd 29972	Extend class notation with the dual modular pair relation on a Hilbert lattice.
class 𝑀ℋ*
20.1.2  Preliminary ZFC lemmas
Definition	df-hnorm 29973	Define the function for the norm of a vector of Hilbert space. See normval 30129 for its value and normcl 30130 for its closure. Theorems norm-i-i 30138, norm-ii-i 30142, and norm-iii-i 30144 show it has the expected properties of a norm. In the literature, the norm of 𝐴 is usually written "|| 𝐴 ||", but we use function notation to take advantage of our existing theorems about functions. Definition of norm in [Beran] p. 96. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.)
⊢ normℎ = (𝑥 ∈ dom dom ·ih ↦ (√‘(𝑥 ·ih 𝑥)))
Definition	df-hba 29974	Define base set of Hilbert space, for use if we want to develop Hilbert space independently from the axioms (see comments in ax-hilex 30004). Note that ℋ is considered a primitive in the Hilbert space axioms below, and we don't use this definition outside of this section. This definition can be proved independently from those axioms as Theorem hhba 30172. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
Definition	df-h0v 29975	Define the zero vector of Hilbert space. Note that 0vec is considered a primitive in the Hilbert space axioms below, and we don't use this definition outside of this section. It is proved from the axioms as Theorem hh0v 30173. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 0ℎ = (0vec‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
Definition	df-hvsub 29976*	Define vector subtraction. See hvsubvali 30025 for its value and hvsubcli 30026 for its closure. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.)
⊢ −ℎ = (𝑥 ∈ ℋ, 𝑦 ∈ ℋ ↦ (𝑥 +ℎ (-1 ·ℎ 𝑦)))
Definition	df-hlim 29977*	Define the limit relation for Hilbert space. See hlimi 30193 for its relational expression. Note that 𝑓:ℕ⟶ ℋ is an infinite sequence of vectors, i.e. a mapping from integers to vectors. Definition of converge in [Beran] p. 96. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.)
⊢ ⇝𝑣 = {⟨𝑓, 𝑤⟩ ∣ ((𝑓:ℕ⟶ ℋ ∧ 𝑤 ∈ ℋ) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑧) −ℎ 𝑤)) < 𝑥)}
Definition	df-hcau 29978*	Define the set of Cauchy sequences on a Hilbert space. See hcau 30189 for its membership relation. Note that 𝑓:ℕ⟶ ℋ is an infinite sequence of vectors, i.e. a mapping from integers to vectors. Definition of Cauchy sequence in [Beran] p. 96. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.)
⊢ Cauchy = {𝑓 ∈ ( ℋ ↑m ℕ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥}
Theorem	h2hva 29979	The group (addition) operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ NrmCVec    ⇒   ⊢ +ℎ = ( +𝑣 ‘𝑈)
Theorem	h2hsm 29980	The scalar product operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ NrmCVec    ⇒   ⊢ ·ℎ = ( ·𝑠OLD ‘𝑈)
Theorem	h2hnm 29981	The norm function of Hilbert space. (Contributed by NM, 5-Jun-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ NrmCVec    ⇒   ⊢ normℎ = (normCV‘𝑈)
Theorem	h2hvs 29982	The vector subtraction operation of Hilbert space. (Contributed by NM, 6-Jun-2008.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ ℋ = (BaseSet‘𝑈)    ⇒   ⊢ −ℎ = ( −𝑣 ‘𝑈)
Theorem	h2hmetdval 29983	Value of the distance function of the metric space of Hilbert space. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ ℋ = (BaseSet‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴𝐷𝐵) = (normℎ‘(𝐴 −ℎ 𝐵)))
Theorem	h2hcau 29984	The Cauchy sequences of Hilbert space. (Contributed by NM, 6-Jun-2008.) (Revised by Mario Carneiro, 13-May-2014.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ ℋ = (BaseSet‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ Cauchy = ((Cau‘𝐷) ∩ ( ℋ ↑m ℕ))
Theorem	h2hlm 29985	The limit sequences of Hilbert space. (Contributed by NM, 6-Jun-2008.) (Revised by Mario Carneiro, 13-May-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ ℋ = (BaseSet‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ⇝𝑣 = ((⇝𝑡‘𝐽) ↾ ( ℋ ↑m ℕ))
20.1.3  Derive the Hilbert space axioms from ZFC set theory Before introducing the 18 axioms for Hilbert space, we first prove them as the conclusions of Theorems axhilex-zf 29986 through axhcompl-zf 30003, using ZFC set theory only. These show that if we are given a known, fixed Hilbert space 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ that satisfies their hypotheses, then we can derive the Hilbert space axioms as theorems of ZFC set theory. In practice, in order to use these theorems to convert the Hilbert Space explorer to a ZFC-only subtheory, we would also have to provide definitions for the 3 (otherwise primitive) class constants +ℎ, ·ℎ, and ·ih before df-hnorm 29973 above. See also the comment in ax-hilex 30004.
Theorem	axhilex-zf 29986	Derive Axiom ax-hilex 30004 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ℋ ∈ V
Theorem	axhfvadd-zf 29987	Derive Axiom ax-hfvadd 30005 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ +ℎ :( ℋ × ℋ)⟶ ℋ
Theorem	axhvcom-zf 29988	Derive Axiom ax-hvcom 30006 from Hilbert space under ZF set theory. (Contributed by NM, 27-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴))
Theorem	axhvass-zf 29989	Derive Axiom ax-hvass 30007 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = (𝐴 +ℎ (𝐵 +ℎ 𝐶)))
Theorem	axhv0cl-zf 29990	Derive Axiom ax-hv0cl 30008 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ 0ℎ ∈ ℋ
Theorem	axhvaddid-zf 29991	Derive Axiom ax-hvaddid 30009 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)
Theorem	axhfvmul-zf 29992	Derive Axiom ax-hfvmul 30010 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ·ℎ :(ℂ × ℋ)⟶ ℋ
Theorem	axhvmulid-zf 29993	Derive Axiom ax-hvmulid 30011 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)
Theorem	axhvmulass-zf 29994	Derive Axiom ax-hvmulass 30012 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))
Theorem	axhvdistr1-zf 29995	Derive Axiom ax-hvdistr1 30013 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 +ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) +ℎ (𝐴 ·ℎ 𝐶)))
Theorem	axhvdistr2-zf 29996	Derive Axiom ax-hvdistr2 30014 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 + 𝐵) ·ℎ 𝐶) = ((𝐴 ·ℎ 𝐶) +ℎ (𝐵 ·ℎ 𝐶)))
Theorem	axhvmul0-zf 29997	Derive Axiom ax-hvmul0 30015 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ (𝐴 ∈ ℋ → (0 ·ℎ 𝐴) = 0ℎ)
Theorem	axhfi-zf 29998	Derive Axiom ax-hfi 30084 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    &   ⊢ ·ih = (·𝑖OLD‘𝑈)    ⇒   ⊢ ·ih :( ℋ × ℋ)⟶ℂ
Theorem	axhis1-zf 29999	Derive Axiom ax-his1 30087 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    &   ⊢ ·ih = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih 𝐵) = (∗‘(𝐵 ·ih 𝐴)))
Theorem	axhis2-zf 30000	Derive Axiom ax-his2 30088 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    &   ⊢ ·ih = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) ·ih 𝐶) = ((𝐴 ·ih 𝐶) + (𝐵 ·ih 𝐶)))