P. 294 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29301-29400   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	cort 29301	Extend class notation with orthogonal complement in Cℋ.
class ⊥
Syntax	cph 29302	Extend class notation with subspace sum in Cℋ.
class +ℋ
Syntax	cspn 29303	Extend class notation with subspace span in Cℋ.
class span
Syntax	chj 29304	Extend class notation with join in Cℋ.
class ∨ℋ
Syntax	chsup 29305	Extend class notation with supremum of a collection in Cℋ.
class ∨ℋ
Syntax	c0h 29306	Extend class notation with zero of Cℋ.
class 0ℋ
Syntax	ccm 29307	Extend class notation with the commutes relation on a Hilbert lattice.
class 𝐶ℋ
Syntax	cpjh 29308	Extend class notation with set of projections on a Hilbert space.
class projℎ
Syntax	chos 29309	Extend class notation with sum of Hilbert space operators.
class +op
Syntax	chot 29310	Extend class notation with scalar product of a Hilbert space operator.
class ·op
Syntax	chod 29311	Extend class notation with difference of Hilbert space operators.
class −op
Syntax	chfs 29312	Extend class notation with sum of Hilbert space functionals.
class +fn
Syntax	chft 29313	Extend class notation with scalar product of Hilbert space functional.
class ·fn
Syntax	ch0o 29314	Extend class notation with the Hilbert space zero operator.
class 0hop
Syntax	chio 29315	Extend class notation with Hilbert space identity operator.
class Iop
Syntax	cnop 29316	Extend class notation with the operator norm function.
class normop
Syntax	ccop 29317	Extend class notation with set of continuous Hilbert space operators.
class ContOp
Syntax	clo 29318	Extend class notation with set of linear Hilbert space operators.
class LinOp
Syntax	cbo 29319	Extend class notation with set of bounded linear operators.
class BndLinOp
Syntax	cuo 29320	Extend class notation with set of unitary Hilbert space operators.
class UniOp
Syntax	cho 29321	Extend class notation with set of Hermitian Hilbert space operators.
class HrmOp
Syntax	cnmf 29322	Extend class notation with the functional norm function.
class normfn
Syntax	cnl 29323	Extend class notation with the functional nullspace function.
class null
Syntax	ccnfn 29324	Extend class notation with set of continuous Hilbert space functionals.
class ContFn
Syntax	clf 29325	Extend class notation with set of linear Hilbert space functionals.
class LinFn
Syntax	cado 29326	Extend class notation with Hilbert space adjoint function.
class adjℎ
Syntax	cbr 29327	Extend class notation with the bra of a vector in Dirac bra-ket notation.
class bra
Syntax	ck 29328	Extend class notation with the outer product of two vectors in Dirac bra-ket notation.
class ketbra
Syntax	cleo 29329	Extend class notation with positive operator ordering.
class ≤op
Syntax	cei 29330	Extend class notation with Hilbert space eigenvector function.
class eigvec
Syntax	cel 29331	Extend class notation with Hilbert space eigenvalue function.
class eigval
Syntax	cspc 29332	Extend class notation with the spectrum of an operator.
class Lambda
Syntax	cst 29333	Extend class notation with set of states on a Hilbert lattice.
class States
Syntax	chst 29334	Extend class notation with set of Hilbert-space-valued states on a Hilbert lattice.
class CHStates
Syntax	ccv 29335	Extend class notation with the covers relation on a Hilbert lattice.
class ⋖ℋ
Syntax	cat 29336	Extend class notation with set of atoms on a Hilbert lattice.
class HAtoms
Syntax	cmd 29337	Extend class notation with the modular pair relation on a Hilbert lattice.
class 𝑀ℋ
Syntax	cdmd 29338	Extend class notation with the dual modular pair relation on a Hilbert lattice.
class 𝑀ℋ*
19.1.2  Preliminary ZFC lemmas
Definition	df-hnorm 29339	Define the function for the norm of a vector of Hilbert space. See normval 29495 for its value and normcl 29496 for its closure. Theorems norm-i-i 29504, norm-ii-i 29508, and norm-iii-i 29510 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 29340	Define base set of Hilbert space, for use if we want to develop Hilbert space independently from the axioms (see comments in ax-hilex 29370). 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 29538. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
Definition	df-h0v 29341	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 29539. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 0ℎ = (0vec‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
Definition	df-hvsub 29342*	Define vector subtraction. See hvsubvali 29391 for its value and hvsubcli 29392 for its closure. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.)
⊢ −ℎ = (𝑥 ∈ ℋ, 𝑦 ∈ ℋ ↦ (𝑥 +ℎ (-1 ·ℎ 𝑦)))
Definition	df-hlim 29343*	Define the limit relation for Hilbert space. See hlimi 29559 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 29344*	Define the set of Cauchy sequences on a Hilbert space. See hcau 29555 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 29345	The group (addition) operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ NrmCVec    ⇒   ⊢ +ℎ = ( +𝑣 ‘𝑈)
Theorem	h2hsm 29346	The scalar product operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ NrmCVec    ⇒   ⊢ ·ℎ = ( ·𝑠OLD ‘𝑈)
Theorem	h2hnm 29347	The norm function of Hilbert space. (Contributed by NM, 5-Jun-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ NrmCVec    ⇒   ⊢ normℎ = (normCV‘𝑈)
Theorem	h2hvs 29348	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 29349	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 29350	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 29351	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 ℕ))
19.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 29352 through axhcompl-zf 29369, 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 29339 above. See also the comment in ax-hilex 29370.
Theorem	axhilex-zf 29352	Derive Axiom ax-hilex 29370 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ℋ ∈ V
Theorem	axhfvadd-zf 29353	Derive Axiom ax-hfvadd 29371 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ +ℎ :( ℋ × ℋ)⟶ ℋ
Theorem	axhvcom-zf 29354	Derive Axiom ax-hvcom 29372 from Hilbert space under ZF set theory. (Contributed by NM, 27-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴))
Theorem	axhvass-zf 29355	Derive Axiom ax-hvass 29373 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = (𝐴 +ℎ (𝐵 +ℎ 𝐶)))
Theorem	axhv0cl-zf 29356	Derive Axiom ax-hv0cl 29374 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ 0ℎ ∈ ℋ
Theorem	axhvaddid-zf 29357	Derive Axiom ax-hvaddid 29375 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)
Theorem	axhfvmul-zf 29358	Derive Axiom ax-hfvmul 29376 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ·ℎ :(ℂ × ℋ)⟶ ℋ
Theorem	axhvmulid-zf 29359	Derive Axiom ax-hvmulid 29377 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)
Theorem	axhvmulass-zf 29360	Derive Axiom ax-hvmulass 29378 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))
Theorem	axhvdistr1-zf 29361	Derive Axiom ax-hvdistr1 29379 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 +ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) +ℎ (𝐴 ·ℎ 𝐶)))
Theorem	axhvdistr2-zf 29362	Derive Axiom ax-hvdistr2 29380 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 + 𝐵) ·ℎ 𝐶) = ((𝐴 ·ℎ 𝐶) +ℎ (𝐵 ·ℎ 𝐶)))
Theorem	axhvmul0-zf 29363	Derive Axiom ax-hvmul0 29381 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ (𝐴 ∈ ℋ → (0 ·ℎ 𝐴) = 0ℎ)
Theorem	axhfi-zf 29364	Derive Axiom ax-hfi 29450 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 29365	Derive Axiom ax-his1 29453 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 29366	Derive Axiom ax-his2 29454 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 29367	Derive Axiom ax-his3 29455 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 29368	Derive Axiom ax-his4 29456 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 29369*	Derive Axiom ax-hcompl 29573 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 → ∃𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥)
19.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 29370, ax-hfvadd 29371, ax-hvcom 29372, ax-hvass 29373, ax-hv0cl 29374, ax-hvaddid 29375, ax-hfvmul 29376, ax-hvmulid 29377, ax-hvmulass 29378, ax-hvdistr1 29379, ax-hvdistr2 29380, ax-hvmul0 29381, ax-hfi 29450, ax-his1 29453, ax-his2 29454, ax-his3 29455, ax-his4 29456, and ax-hcompl 29573. 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 29352, axhfvadd-zf 29353, axhvcom-zf 29354, axhvass-zf 29355, axhv0cl-zf 29356, axhvaddid-zf 29357, axhfvmul-zf 29358, axhvmulid-zf 29359, axhvmulass-zf 29360, axhvdistr1-zf 29361, axhvdistr2-zf 29362, axhvmul0-zf 29363, axhfi-zf 29364, axhis1-zf 29365, axhis2-zf 29366, axhis3-zf 29367, axhis4-zf 29368, and axhcompl-zf 29369 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 29352.
Axiom	ax-hilex 29370	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 29371	Vector addition is an operation on ℋ. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
⊢ +ℎ :( ℋ × ℋ)⟶ ℋ
Axiom	ax-hvcom 29372	Vector addition is commutative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴))
Axiom	ax-hvass 29373	Vector addition is associative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = (𝐴 +ℎ (𝐵 +ℎ 𝐶)))
Axiom	ax-hv0cl 29374	The zero vector is in the vector space. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)
⊢ 0ℎ ∈ ℋ
Axiom	ax-hvaddid 29375	Addition with the zero vector. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)
Axiom	ax-hfvmul 29376	Scalar multiplication is an operation on ℂ and ℋ. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
⊢ ·ℎ :(ℂ × ℋ)⟶ ℋ
Axiom	ax-hvmulid 29377	Scalar multiplication by one. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)
Axiom	ax-hvmulass 29378	Scalar multiplication associative law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))
Axiom	ax-hvdistr1 29379	Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 +ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) +ℎ (𝐴 ·ℎ 𝐶)))
Axiom	ax-hvdistr2 29380	Scalar multiplication distributive law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 + 𝐵) ·ℎ 𝐶) = ((𝐴 ·ℎ 𝐶) +ℎ (𝐵 ·ℎ 𝐶)))
Axiom	ax-hvmul0 29381	Scalar multiplication by zero. We can derive the existence of the negative of a vector from this axiom (see hvsubid 29397 and hvsubval 29387). (Contributed by NM, 29-May-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (0 ·ℎ 𝐴) = 0ℎ)
19.1.5  Vector operations
Theorem	hvmulex 29382	The Hilbert space scalar product operation is a set. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.)
⊢ ·ℎ ∈ V
Theorem	hvaddcl 29383	Closure of vector addition. (Contributed by NM, 18-Apr-2007.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) ∈ ℋ)
Theorem	hvmulcl 29384	Closure of scalar multiplication. (Contributed by NM, 19-Apr-2007.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ℎ 𝐵) ∈ ℋ)
Theorem	hvmulcli 29385	Closure inference for scalar multiplication. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 ·ℎ 𝐵) ∈ ℋ
Theorem	hvsubf 29386	Mapping domain and codomain of vector subtraction. (Contributed by NM, 6-Sep-2007.) (New usage is discouraged.)
⊢ −ℎ :( ℋ × ℋ)⟶ ℋ
Theorem	hvsubval 29387	Value of vector subtraction. (Contributed by NM, 5-Sep-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 −ℎ 𝐵) = (𝐴 +ℎ (-1 ·ℎ 𝐵)))
Theorem	hvsubcl 29388	Closure of vector subtraction. (Contributed by NM, 17-Aug-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 −ℎ 𝐵) ∈ ℋ)
Theorem	hvaddcli 29389	Closure of vector addition. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 +ℎ 𝐵) ∈ ℋ
Theorem	hvcomi 29390	Commutation of vector addition. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)
Theorem	hvsubvali 29391	Value of vector subtraction definition. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 −ℎ 𝐵) = (𝐴 +ℎ (-1 ·ℎ 𝐵))
Theorem	hvsubcli 29392	Closure of vector subtraction. (Contributed by NM, 2-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 −ℎ 𝐵) ∈ ℋ
Theorem	ifhvhv0 29393	Prove if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ. (Contributed by David A. Wheeler, 7-Dec-2018.) (New usage is discouraged.)
⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ
Theorem	hvaddid2 29394	Addition with the zero vector. (Contributed by NM, 18-Oct-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (0ℎ +ℎ 𝐴) = 𝐴)
Theorem	hvmul0 29395	Scalar multiplication with the zero vector. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℂ → (𝐴 ·ℎ 0ℎ) = 0ℎ)
Theorem	hvmul0or 29396	If a scalar product is zero, one of its factors must be zero. (Contributed by NM, 19-May-2005.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) = 0ℎ ↔ (𝐴 = 0 ∨ 𝐵 = 0ℎ)))
Theorem	hvsubid 29397	Subtraction of a vector from itself. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (𝐴 −ℎ 𝐴) = 0ℎ)
Theorem	hvnegid 29398	Addition of negative of a vector to itself. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ (-1 ·ℎ 𝐴)) = 0ℎ)
Theorem	hv2neg 29399	Two ways to express the negative of a vector. (Contributed by NM, 23-May-2005.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (0ℎ −ℎ 𝐴) = (-1 ·ℎ 𝐴))
Theorem	hvaddid2i 29400	Addition with the zero vector. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    ⇒   ⊢ (0ℎ +ℎ 𝐴) = 𝐴