P. 310 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 30901-31000   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	csm 30901	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 30902	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 4580.
class ·ih
Syntax	cno 30903	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 30904	Extend class notation with zero vector in Hilbert space.
class 0ℎ
Syntax	cmv 30905	Extend class notation with vector subtraction in Hilbert space.
class −ℎ
Syntax	ccauold 30906	Extend class notation with set of Cauchy sequences in Hilbert space.
class Cauchy
Syntax	chli 30907	Extend class notation with convergence relation in Hilbert space.
class ⇝𝑣
Syntax	csh 30908	Extend class notation with set of subspaces of a Hilbert space.
class Sℋ
Syntax	cch 30909	Extend class notation with set of closed subspaces of a Hilbert space.
class Cℋ
Syntax	cort 30910	Extend class notation with orthogonal complement in Cℋ.
class ⊥
Syntax	cph 30911	Extend class notation with subspace sum in Cℋ.
class +ℋ
Syntax	cspn 30912	Extend class notation with subspace span in Cℋ.
class span
Syntax	chj 30913	Extend class notation with join in Cℋ.
class ∨ℋ
Syntax	chsup 30914	Extend class notation with supremum of a collection in Cℋ.
class ∨ℋ
Syntax	c0h 30915	Extend class notation with zero of Cℋ.
class 0ℋ
Syntax	ccm 30916	Extend class notation with the commutes relation on a Hilbert lattice.
class 𝐶ℋ
Syntax	cpjh 30917	Extend class notation with set of projections on a Hilbert space.
class projℎ
Syntax	chos 30918	Extend class notation with sum of Hilbert space operators.
class +op
Syntax	chot 30919	Extend class notation with scalar product of a Hilbert space operator.
class ·op
Syntax	chod 30920	Extend class notation with difference of Hilbert space operators.
class −op
Syntax	chfs 30921	Extend class notation with sum of Hilbert space functionals.
class +fn
Syntax	chft 30922	Extend class notation with scalar product of Hilbert space functional.
class ·fn
Syntax	ch0o 30923	Extend class notation with the Hilbert space zero operator.
class 0hop
Syntax	chio 30924	Extend class notation with Hilbert space identity operator.
class Iop
Syntax	cnop 30925	Extend class notation with the operator norm function.
class normop
Syntax	ccop 30926	Extend class notation with set of continuous Hilbert space operators.
class ContOp
Syntax	clo 30927	Extend class notation with set of linear Hilbert space operators.
class LinOp
Syntax	cbo 30928	Extend class notation with set of bounded linear operators.
class BndLinOp
Syntax	cuo 30929	Extend class notation with set of unitary Hilbert space operators.
class UniOp
Syntax	cho 30930	Extend class notation with set of Hermitian Hilbert space operators.
class HrmOp
Syntax	cnmf 30931	Extend class notation with the functional norm function.
class normfn
Syntax	cnl 30932	Extend class notation with the functional nullspace function.
class null
Syntax	ccnfn 30933	Extend class notation with set of continuous Hilbert space functionals.
class ContFn
Syntax	clf 30934	Extend class notation with set of linear Hilbert space functionals.
class LinFn
Syntax	cado 30935	Extend class notation with Hilbert space adjoint function.
class adjℎ
Syntax	cbr 30936	Extend class notation with the bra of a vector in Dirac bra-ket notation.
class bra
Syntax	ck 30937	Extend class notation with the outer product of two vectors in Dirac bra-ket notation.
class ketbra
Syntax	cleo 30938	Extend class notation with positive operator ordering.
class ≤op
Syntax	cei 30939	Extend class notation with Hilbert space eigenvector function.
class eigvec
Syntax	cel 30940	Extend class notation with Hilbert space eigenvalue function.
class eigval
Syntax	cspc 30941	Extend class notation with the spectrum of an operator.
class Lambda
Syntax	cst 30942	Extend class notation with set of states on a Hilbert lattice.
class States
Syntax	chst 30943	Extend class notation with set of Hilbert-space-valued states on a Hilbert lattice.
class CHStates
Syntax	ccv 30944	Extend class notation with the covers relation on a Hilbert lattice.
class ⋖ℋ
Syntax	cat 30945	Extend class notation with set of atoms on a Hilbert lattice.
class HAtoms
Syntax	cmd 30946	Extend class notation with the modular pair relation on a Hilbert lattice.
class 𝑀ℋ
Syntax	cdmd 30947	Extend class notation with the dual modular pair relation on a Hilbert lattice.
class 𝑀ℋ*
20.1.2  Preliminary ZFC lemmas
Definition	df-hnorm 30948	Define the function for the norm of a vector of Hilbert space. See normval 31104 for its value and normcl 31105 for its closure. Theorems norm-i-i 31113, norm-ii-i 31117, and norm-iii-i 31119 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 30949	Define base set of Hilbert space, for use if we want to develop Hilbert space independently from the axioms (see comments in ax-hilex 30979). 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 31147. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
Definition	df-h0v 30950	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 31148. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 0ℎ = (0vec‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
Definition	df-hvsub 30951*	Define vector subtraction. See hvsubvali 31000 for its value and hvsubcli 31001 for its closure. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.)
⊢ −ℎ = (𝑥 ∈ ℋ, 𝑦 ∈ ℋ ↦ (𝑥 +ℎ (-1 ·ℎ 𝑦)))
Definition	df-hlim 30952*	Define the limit relation for Hilbert space. See hlimi 31168 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 30953*	Define the set of Cauchy sequences on a Hilbert space. See hcau 31164 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 30954	The group (addition) operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ NrmCVec    ⇒   ⊢ +ℎ = ( +𝑣 ‘𝑈)
Theorem	h2hsm 30955	The scalar product operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ NrmCVec    ⇒   ⊢ ·ℎ = ( ·𝑠OLD ‘𝑈)
Theorem	h2hnm 30956	The norm function of Hilbert space. (Contributed by NM, 5-Jun-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ NrmCVec    ⇒   ⊢ normℎ = (normCV‘𝑈)
Theorem	h2hvs 30957	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 30958	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 30959	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 30960	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 30961 through axhcompl-zf 30978, 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 30948 above. See also the comment in ax-hilex 30979.
Theorem	axhilex-zf 30961	Derive Axiom ax-hilex 30979 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ℋ ∈ V
Theorem	axhfvadd-zf 30962	Derive Axiom ax-hfvadd 30980 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ +ℎ :( ℋ × ℋ)⟶ ℋ
Theorem	axhvcom-zf 30963	Derive Axiom ax-hvcom 30981 from Hilbert space under ZF set theory. (Contributed by NM, 27-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴))
Theorem	axhvass-zf 30964	Derive Axiom ax-hvass 30982 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = (𝐴 +ℎ (𝐵 +ℎ 𝐶)))
Theorem	axhv0cl-zf 30965	Derive Axiom ax-hv0cl 30983 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ 0ℎ ∈ ℋ
Theorem	axhvaddid-zf 30966	Derive Axiom ax-hvaddid 30984 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)
Theorem	axhfvmul-zf 30967	Derive Axiom ax-hfvmul 30985 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ·ℎ :(ℂ × ℋ)⟶ ℋ
Theorem	axhvmulid-zf 30968	Derive Axiom ax-hvmulid 30986 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)
Theorem	axhvmulass-zf 30969	Derive Axiom ax-hvmulass 30987 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))
Theorem	axhvdistr1-zf 30970	Derive Axiom ax-hvdistr1 30988 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 +ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) +ℎ (𝐴 ·ℎ 𝐶)))
Theorem	axhvdistr2-zf 30971	Derive Axiom ax-hvdistr2 30989 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 + 𝐵) ·ℎ 𝐶) = ((𝐴 ·ℎ 𝐶) +ℎ (𝐵 ·ℎ 𝐶)))
Theorem	axhvmul0-zf 30972	Derive Axiom ax-hvmul0 30990 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ (𝐴 ∈ ℋ → (0 ·ℎ 𝐴) = 0ℎ)
Theorem	axhfi-zf 30973	Derive Axiom ax-hfi 31059 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 30974	Derive Axiom ax-his1 31062 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 30975	Derive Axiom ax-his2 31063 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 30976	Derive Axiom ax-his3 31064 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 30977	Derive Axiom ax-his4 31065 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 30978*	Derive Axiom ax-hcompl 31182 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 30979, ax-hfvadd 30980, ax-hvcom 30981, ax-hvass 30982, ax-hv0cl 30983, ax-hvaddid 30984, ax-hfvmul 30985, ax-hvmulid 30986, ax-hvmulass 30987, ax-hvdistr1 30988, ax-hvdistr2 30989, ax-hvmul0 30990, ax-hfi 31059, ax-his1 31062, ax-his2 31063, ax-his3 31064, ax-his4 31065, and ax-hcompl 31182. 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 30961, axhfvadd-zf 30962, axhvcom-zf 30963, axhvass-zf 30964, axhv0cl-zf 30965, axhvaddid-zf 30966, axhfvmul-zf 30967, axhvmulid-zf 30968, axhvmulass-zf 30969, axhvdistr1-zf 30970, axhvdistr2-zf 30971, axhvmul0-zf 30972, axhfi-zf 30973, axhis1-zf 30974, axhis2-zf 30975, axhis3-zf 30976, axhis4-zf 30977, and axhcompl-zf 30978 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 30961.
Axiom	ax-hilex 30979	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 30980	Vector addition is an operation on ℋ. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
⊢ +ℎ :( ℋ × ℋ)⟶ ℋ
Axiom	ax-hvcom 30981	Vector addition is commutative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴))
Axiom	ax-hvass 30982	Vector addition is associative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = (𝐴 +ℎ (𝐵 +ℎ 𝐶)))
Axiom	ax-hv0cl 30983	The zero vector is in the vector space. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)
⊢ 0ℎ ∈ ℋ
Axiom	ax-hvaddid 30984	Addition with the zero vector. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)
Axiom	ax-hfvmul 30985	Scalar multiplication is an operation on ℂ and ℋ. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
⊢ ·ℎ :(ℂ × ℋ)⟶ ℋ
Axiom	ax-hvmulid 30986	Scalar multiplication by one. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)
Axiom	ax-hvmulass 30987	Scalar multiplication associative law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))
Axiom	ax-hvdistr1 30988	Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 +ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) +ℎ (𝐴 ·ℎ 𝐶)))
Axiom	ax-hvdistr2 30989	Scalar multiplication distributive law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 + 𝐵) ·ℎ 𝐶) = ((𝐴 ·ℎ 𝐶) +ℎ (𝐵 ·ℎ 𝐶)))
Axiom	ax-hvmul0 30990	Scalar multiplication by zero. We can derive the existence of the negative of a vector from this axiom (see hvsubid 31006 and hvsubval 30996). (Contributed by NM, 29-May-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (0 ·ℎ 𝐴) = 0ℎ)
20.1.5  Vector operations
Theorem	hvmulex 30991	The Hilbert space scalar product operation is a set. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.)
⊢ ·ℎ ∈ V
Theorem	hvaddcl 30992	Closure of vector addition. (Contributed by NM, 18-Apr-2007.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) ∈ ℋ)
Theorem	hvmulcl 30993	Closure of scalar multiplication. (Contributed by NM, 19-Apr-2007.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ℎ 𝐵) ∈ ℋ)
Theorem	hvmulcli 30994	Closure inference for scalar multiplication. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 ·ℎ 𝐵) ∈ ℋ
Theorem	hvsubf 30995	Mapping domain and codomain of vector subtraction. (Contributed by NM, 6-Sep-2007.) (New usage is discouraged.)
⊢ −ℎ :( ℋ × ℋ)⟶ ℋ
Theorem	hvsubval 30996	Value of vector subtraction. (Contributed by NM, 5-Sep-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 −ℎ 𝐵) = (𝐴 +ℎ (-1 ·ℎ 𝐵)))
Theorem	hvsubcl 30997	Closure of vector subtraction. (Contributed by NM, 17-Aug-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 −ℎ 𝐵) ∈ ℋ)
Theorem	hvaddcli 30998	Closure of vector addition. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 +ℎ 𝐵) ∈ ℋ
Theorem	hvcomi 30999	Commutation of vector addition. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)
Theorem	hvsubvali 31000	Value of vector subtraction definition. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 −ℎ 𝐵) = (𝐴 +ℎ (-1 ·ℎ 𝐵))