P. 311 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 31001-31100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hlmulid 31001	Hilbert space scalar multiplication by one. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋) → (1𝑆𝐴) = 𝐴)
Theorem	hlmulass 31002	Hilbert space scalar multiplication associative law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → ((𝐴 · 𝐵)𝑆𝐶) = (𝐴𝑆(𝐵𝑆𝐶)))
Theorem	hldi 31003	Hilbert space scalar multiplication distributive law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑆(𝐵𝐺𝐶)) = ((𝐴𝑆𝐵)𝐺(𝐴𝑆𝐶)))
Theorem	hldir 31004	Hilbert space scalar multiplication distributive law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → ((𝐴 + 𝐵)𝑆𝐶) = ((𝐴𝑆𝐶)𝐺(𝐵𝑆𝐶)))
Theorem	hlmul0 31005	Hilbert space scalar multiplication by zero. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋) → (0𝑆𝐴) = 𝑍)
Theorem	hlipf 31006	Mapping for Hilbert space inner product. (Contributed by NM, 19-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ (𝑈 ∈ CHilOLD → 𝑃:(𝑋 × 𝑋)⟶ℂ)
Theorem	hlipcj 31007	Conjugate law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑃𝐵) = (∗‘(𝐵𝑃𝐴)))
Theorem	hlipdir 31008	Distributive law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝑃𝐶) = ((𝐴𝑃𝐶) + (𝐵𝑃𝐶)))
Theorem	hlipass 31009	Associative law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑆𝐵)𝑃𝐶) = (𝐴 · (𝐵𝑃𝐶)))
Theorem	hlipgt0 31010	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 31011	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 31012	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 31013*	Lemma for htth 31014. The collection 𝐾, which consists of functions 𝐹(𝑧)(𝑤) = ⟨𝑤 ∣ 𝑇(𝑧)⟩ = ⟨𝑇(𝑤) ∣ 𝑧⟩ for each 𝑧 in the unit ball, is a collection of bounded linear functions by ipblnfi 30951, so by the Uniform Boundedness theorem ubth 30969, 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 31014*	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 21686; note that df-hil 21686 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 31015	Extend class notation with Hilbert vector space.
class ℋ
Syntax	cva 31016	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 11039.
class +ℎ
Syntax	csm 31017	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 31018	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 4569.
class ·ih
Syntax	cno 31019	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 31020	Extend class notation with zero vector in Hilbert space.
class 0ℎ
Syntax	cmv 31021	Extend class notation with vector subtraction in Hilbert space.
class −ℎ
Syntax	ccauold 31022	Extend class notation with set of Cauchy sequences in Hilbert space.
class Cauchy
Syntax	chli 31023	Extend class notation with convergence relation in Hilbert space.
class ⇝𝑣
Syntax	csh 31024	Extend class notation with set of subspaces of a Hilbert space.
class Sℋ
Syntax	cch 31025	Extend class notation with set of closed subspaces of a Hilbert space.
class Cℋ
Syntax	cort 31026	Extend class notation with orthogonal complement in Cℋ.
class ⊥
Syntax	cph 31027	Extend class notation with subspace sum in Cℋ.
class +ℋ
Syntax	cspn 31028	Extend class notation with subspace span in Cℋ.
class span
Syntax	chj 31029	Extend class notation with join in Cℋ.
class ∨ℋ
Syntax	chsup 31030	Extend class notation with supremum of a collection in Cℋ.
class ∨ℋ
Syntax	c0h 31031	Extend class notation with zero of Cℋ.
class 0ℋ
Syntax	ccm 31032	Extend class notation with the commutes relation on a Hilbert lattice.
class 𝐶ℋ
Syntax	cpjh 31033	Extend class notation with set of projections on a Hilbert space.
class projℎ
Syntax	chos 31034	Extend class notation with sum of Hilbert space operators.
class +op
Syntax	chot 31035	Extend class notation with scalar product of a Hilbert space operator.
class ·op
Syntax	chod 31036	Extend class notation with difference of Hilbert space operators.
class −op
Syntax	chfs 31037	Extend class notation with sum of Hilbert space functionals.
class +fn
Syntax	chft 31038	Extend class notation with scalar product of Hilbert space functional.
class ·fn
Syntax	ch0o 31039	Extend class notation with the Hilbert space zero operator.
class 0hop
Syntax	chio 31040	Extend class notation with Hilbert space identity operator.
class Iop
Syntax	cnop 31041	Extend class notation with the operator norm function.
class normop
Syntax	ccop 31042	Extend class notation with set of continuous Hilbert space operators.
class ContOp
Syntax	clo 31043	Extend class notation with set of linear Hilbert space operators.
class LinOp
Syntax	cbo 31044	Extend class notation with set of bounded linear operators.
class BndLinOp
Syntax	cuo 31045	Extend class notation with set of unitary Hilbert space operators.
class UniOp
Syntax	cho 31046	Extend class notation with set of Hermitian Hilbert space operators.
class HrmOp
Syntax	cnmf 31047	Extend class notation with the functional norm function.
class normfn
Syntax	cnl 31048	Extend class notation with the functional nullspace function.
class null
Syntax	ccnfn 31049	Extend class notation with set of continuous Hilbert space functionals.
class ContFn
Syntax	clf 31050	Extend class notation with set of linear Hilbert space functionals.
class LinFn
Syntax	cado 31051	Extend class notation with Hilbert space adjoint function.
class adjℎ
Syntax	cbr 31052	Extend class notation with the bra of a vector in Dirac bra-ket notation.
class bra
Syntax	ck 31053	Extend class notation with the outer product of two vectors in Dirac bra-ket notation.
class ketbra
Syntax	cleo 31054	Extend class notation with positive operator ordering.
class ≤op
Syntax	cei 31055	Extend class notation with Hilbert space eigenvector function.
class eigvec
Syntax	cel 31056	Extend class notation with Hilbert space eigenvalue function.
class eigval
Syntax	cspc 31057	Extend class notation with the spectrum of an operator.
class Lambda
Syntax	cst 31058	Extend class notation with set of states on a Hilbert lattice.
class States
Syntax	chst 31059	Extend class notation with set of Hilbert-space-valued states on a Hilbert lattice.
class CHStates
Syntax	ccv 31060	Extend class notation with the covers relation on a Hilbert lattice.
class ⋖ℋ
Syntax	cat 31061	Extend class notation with set of atoms on a Hilbert lattice.
class HAtoms
Syntax	cmd 31062	Extend class notation with the modular pair relation on a Hilbert lattice.
class 𝑀ℋ
Syntax	cdmd 31063	Extend class notation with the dual modular pair relation on a Hilbert lattice.
class 𝑀ℋ*
20.1.2  Preliminary ZFC lemmas
Definition	df-hnorm 31064	Define the function for the norm of a vector of Hilbert space. See normval 31220 for its value and normcl 31221 for its closure. Theorems norm-i-i 31229, norm-ii-i 31233, and norm-iii-i 31235 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 31065	Define base set of Hilbert space, for use if we want to develop Hilbert space independently from the axioms (see comments in ax-hilex 31095). 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 31263. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
Definition	df-h0v 31066	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 31264. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 0ℎ = (0vec‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
Definition	df-hvsub 31067*	Define vector subtraction. See hvsubvali 31116 for its value and hvsubcli 31117 for its closure. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.)
⊢ −ℎ = (𝑥 ∈ ℋ, 𝑦 ∈ ℋ ↦ (𝑥 +ℎ (-1 ·ℎ 𝑦)))
Definition	df-hlim 31068*	Define the limit relation for Hilbert space. See hlimi 31284 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 31069*	Define the set of Cauchy sequences on a Hilbert space. See hcau 31280 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 31070	The group (addition) operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ NrmCVec    ⇒   ⊢ +ℎ = ( +𝑣 ‘𝑈)
Theorem	h2hsm 31071	The scalar product operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ NrmCVec    ⇒   ⊢ ·ℎ = ( ·𝑠OLD ‘𝑈)
Theorem	h2hnm 31072	The norm function of Hilbert space. (Contributed by NM, 5-Jun-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ NrmCVec    ⇒   ⊢ normℎ = (normCV‘𝑈)
Theorem	h2hvs 31073	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 31074	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 31075	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 31076	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 31077 through axhcompl-zf 31094, 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 31064 above. See also the comment in ax-hilex 31095.
Theorem	axhilex-zf 31077	Derive Axiom ax-hilex 31095 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ℋ ∈ V
Theorem	axhfvadd-zf 31078	Derive Axiom ax-hfvadd 31096 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ +ℎ :( ℋ × ℋ)⟶ ℋ
Theorem	axhvcom-zf 31079	Derive Axiom ax-hvcom 31097 from Hilbert space under ZF set theory. (Contributed by NM, 27-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴))
Theorem	axhvass-zf 31080	Derive Axiom ax-hvass 31098 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = (𝐴 +ℎ (𝐵 +ℎ 𝐶)))
Theorem	axhv0cl-zf 31081	Derive Axiom ax-hv0cl 31099 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ 0ℎ ∈ ℋ
Theorem	axhvaddid-zf 31082	Derive Axiom ax-hvaddid 31100 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)
Theorem	axhfvmul-zf 31083	Derive Axiom ax-hfvmul 31101 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ·ℎ :(ℂ × ℋ)⟶ ℋ
Theorem	axhvmulid-zf 31084	Derive Axiom ax-hvmulid 31102 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)
Theorem	axhvmulass-zf 31085	Derive Axiom ax-hvmulass 31103 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))
Theorem	axhvdistr1-zf 31086	Derive Axiom ax-hvdistr1 31104 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 +ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) +ℎ (𝐴 ·ℎ 𝐶)))
Theorem	axhvdistr2-zf 31087	Derive Axiom ax-hvdistr2 31105 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 + 𝐵) ·ℎ 𝐶) = ((𝐴 ·ℎ 𝐶) +ℎ (𝐵 ·ℎ 𝐶)))
Theorem	axhvmul0-zf 31088	Derive Axiom ax-hvmul0 31106 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ (𝐴 ∈ ℋ → (0 ·ℎ 𝐴) = 0ℎ)
Theorem	axhfi-zf 31089	Derive Axiom ax-hfi 31175 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 31090	Derive Axiom ax-his1 31178 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 31091	Derive Axiom ax-his2 31179 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    &   ⊢ ·ih = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) ·ih 𝐶) = ((𝐴 ·ih 𝐶) + (𝐵 ·ih 𝐶)))
Theorem	axhis3-zf 31092	Derive Axiom ax-his3 31180 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    &   ⊢ ·ih = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))
Theorem	axhis4-zf 31093	Derive Axiom ax-his4 31181 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    &   ⊢ ·ih = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ) → 0 < (𝐴 ·ih 𝐴))
Theorem	axhcompl-zf 31094*	Derive Axiom ax-hcompl 31298 from Hilbert space under ZF set theory. (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ℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ (𝐹 ∈ Cauchy → ∃𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥)
20.1.4  Introduce the vector space axioms for a Hilbert space Here we introduce the axioms a complex Hilbert space, which is the foundation for quantum mechanics and quantum field theory. The 18 axioms for a complex Hilbert space consist of ax-hilex 31095, ax-hfvadd 31096, ax-hvcom 31097, ax-hvass 31098, ax-hv0cl 31099, ax-hvaddid 31100, ax-hfvmul 31101, ax-hvmulid 31102, ax-hvmulass 31103, ax-hvdistr1 31104, ax-hvdistr2 31105, ax-hvmul0 31106, ax-hfi 31175, ax-his1 31178, ax-his2 31179, ax-his3 31180, ax-his4 31181, and ax-hcompl 31298. The axioms specify the properties of 5 primitive symbols, ℋ, +ℎ, ·ℎ, 0ℎ, and ·ih. If we can prove in ZFC set theory that a class 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ is a complex Hilbert space, i.e. that 𝑈 ∈ CHilOLD, then these axioms can be proved as Theorems axhilex-zf 31077, axhfvadd-zf 31078, axhvcom-zf 31079, axhvass-zf 31080, axhv0cl-zf 31081, axhvaddid-zf 31082, axhfvmul-zf 31083, axhvmulid-zf 31084, axhvmulass-zf 31085, axhvdistr1-zf 31086, axhvdistr2-zf 31087, axhvmul0-zf 31088, axhfi-zf 31089, axhis1-zf 31090, axhis2-zf 31091, axhis3-zf 31092, axhis4-zf 31093, and axhcompl-zf 31094 respectively. In that case, the theorems of the Hilbert Space Explorer will become theorems of ZFC set theory. See also the comments in axhilex-zf 31077.
Axiom	ax-hilex 31095	This is our first axiom for a complex Hilbert space, which is the foundation for quantum mechanics and quantum field theory. We assume that there exists a primitive class, ℋ, which contains objects called vectors. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
⊢ ℋ ∈ V
Axiom	ax-hfvadd 31096	Vector addition is an operation on ℋ. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
⊢ +ℎ :( ℋ × ℋ)⟶ ℋ
Axiom	ax-hvcom 31097	Vector addition is commutative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴))
Axiom	ax-hvass 31098	Vector addition is associative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = (𝐴 +ℎ (𝐵 +ℎ 𝐶)))
Axiom	ax-hv0cl 31099	The zero vector is in the vector space. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)
⊢ 0ℎ ∈ ℋ
Axiom	ax-hvaddid 31100	Addition with the zero vector. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)