P. 314 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 31301-31400   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	chos 31301	Extend class notation with sum of Hilbert space operators.
class +op
Syntax	chot 31302	Extend class notation with scalar product of a Hilbert space operator.
class ·op
Syntax	chod 31303	Extend class notation with difference of Hilbert space operators.
class −op
Syntax	chfs 31304	Extend class notation with sum of Hilbert space functionals.
class +fn
Syntax	chft 31305	Extend class notation with scalar product of Hilbert space functional.
class ·fn
Syntax	ch0o 31306	Extend class notation with the Hilbert space zero operator.
class 0hop
Syntax	chio 31307	Extend class notation with Hilbert space identity operator.
class Iop
Syntax	cnop 31308	Extend class notation with the operator norm function.
class normop
Syntax	ccop 31309	Extend class notation with set of continuous Hilbert space operators.
class ContOp
Syntax	clo 31310	Extend class notation with set of linear Hilbert space operators.
class LinOp
Syntax	cbo 31311	Extend class notation with set of bounded linear operators.
class BndLinOp
Syntax	cuo 31312	Extend class notation with set of unitary Hilbert space operators.
class UniOp
Syntax	cho 31313	Extend class notation with set of Hermitian Hilbert space operators.
class HrmOp
Syntax	cnmf 31314	Extend class notation with the functional norm function.
class normfn
Syntax	cnl 31315	Extend class notation with the functional nullspace function.
class null
Syntax	ccnfn 31316	Extend class notation with set of continuous Hilbert space functionals.
class ContFn
Syntax	clf 31317	Extend class notation with set of linear Hilbert space functionals.
class LinFn
Syntax	cado 31318	Extend class notation with Hilbert space adjoint function.
class adjℎ
Syntax	cbr 31319	Extend class notation with the bra of a vector in Dirac bra-ket notation.
class bra
Syntax	ck 31320	Extend class notation with the outer product of two vectors in Dirac bra-ket notation.
class ketbra
Syntax	cleo 31321	Extend class notation with positive operator ordering.
class ≤op
Syntax	cei 31322	Extend class notation with Hilbert space eigenvector function.
class eigvec
Syntax	cel 31323	Extend class notation with Hilbert space eigenvalue function.
class eigval
Syntax	cspc 31324	Extend class notation with the spectrum of an operator.
class Lambda
Syntax	cst 31325	Extend class notation with set of states on a Hilbert lattice.
class States
Syntax	chst 31326	Extend class notation with set of Hilbert-space-valued states on a Hilbert lattice.
class CHStates
Syntax	ccv 31327	Extend class notation with the covers relation on a Hilbert lattice.
class ⋖ℋ
Syntax	cat 31328	Extend class notation with set of atoms on a Hilbert lattice.
class HAtoms
Syntax	cmd 31329	Extend class notation with the modular pair relation on a Hilbert lattice.
class 𝑀ℋ
Syntax	cdmd 31330	Extend class notation with the dual modular pair relation on a Hilbert lattice.
class 𝑀ℋ*
20.1.2  Preliminary ZFC lemmas
Definition	df-hnorm 31331	Define the function for the norm of a vector of Hilbert space. See normval 31487 for its value and normcl 31488 for its closure. Theorems norm-i-i 31496, norm-ii-i 31500, and norm-iii-i 31502 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 31332	Define base set of Hilbert space, for use if we want to develop Hilbert space independently from the axioms (see comments in ax-hilex 31362). 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 31530. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
Definition	df-h0v 31333	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 31531. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 0ℎ = (0vec‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
Definition	df-hvsub 31334*	Define vector subtraction. See hvsubvali 31383 for its value and hvsubcli 31384 for its closure. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.)
⊢ −ℎ = (𝑥 ∈ ℋ, 𝑦 ∈ ℋ ↦ (𝑥 +ℎ (-1 ·ℎ 𝑦)))
Definition	df-hlim 31335*	Define the limit relation for Hilbert space. See hlimi 31551 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 31336*	Define the set of Cauchy sequences on a Hilbert space. See hcau 31547 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 31337	The group (addition) operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ NrmCVec    ⇒   ⊢ +ℎ = ( +𝑣 ‘𝑈)
Theorem	h2hsm 31338	The scalar product operation of Hilbert space. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ NrmCVec    ⇒   ⊢ ·ℎ = ( ·𝑠OLD ‘𝑈)
Theorem	h2hnm 31339	The norm function of Hilbert space. (Contributed by NM, 5-Jun-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ NrmCVec    ⇒   ⊢ normℎ = (normCV‘𝑈)
Theorem	h2hvs 31340	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 31341	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 31342	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 31343	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 31344 through axhcompl-zf 31361, 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 31331 above. See also the comment in ax-hilex 31362.
Theorem	axhilex-zf 31344	Derive Axiom ax-hilex 31362 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ℋ ∈ V
Theorem	axhfvadd-zf 31345	Derive Axiom ax-hfvadd 31363 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ +ℎ :( ℋ × ℋ)⟶ ℋ
Theorem	axhvcom-zf 31346	Derive Axiom ax-hvcom 31364 from Hilbert space under ZF set theory. (Contributed by NM, 27-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴))
Theorem	axhvass-zf 31347	Derive Axiom ax-hvass 31365 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = (𝐴 +ℎ (𝐵 +ℎ 𝐶)))
Theorem	axhv0cl-zf 31348	Derive Axiom ax-hv0cl 31366 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ 0ℎ ∈ ℋ
Theorem	axhvaddid-zf 31349	Derive Axiom ax-hvaddid 31367 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)
Theorem	axhfvmul-zf 31350	Derive Axiom ax-hfvmul 31368 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ·ℎ :(ℂ × ℋ)⟶ ℋ
Theorem	axhvmulid-zf 31351	Derive Axiom ax-hvmulid 31369 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)
Theorem	axhvmulass-zf 31352	Derive Axiom ax-hvmulass 31370 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))
Theorem	axhvdistr1-zf 31353	Derive Axiom ax-hvdistr1 31371 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 +ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) +ℎ (𝐴 ·ℎ 𝐶)))
Theorem	axhvdistr2-zf 31354	Derive Axiom ax-hvdistr2 31372 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 + 𝐵) ·ℎ 𝐶) = ((𝐴 ·ℎ 𝐶) +ℎ (𝐵 ·ℎ 𝐶)))
Theorem	axhvmul0-zf 31355	Derive Axiom ax-hvmul0 31373 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝑈 ∈ CHilOLD    ⇒   ⊢ (𝐴 ∈ ℋ → (0 ·ℎ 𝐴) = 0ℎ)
Theorem	axhfi-zf 31356	Derive Axiom ax-hfi 31442 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 31357	Derive Axiom ax-his1 31445 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 31358	Derive Axiom ax-his2 31446 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 31359	Derive Axiom ax-his3 31447 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 31360	Derive Axiom ax-his4 31448 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 31361*	Derive Axiom ax-hcompl 31565 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 31362, ax-hfvadd 31363, ax-hvcom 31364, ax-hvass 31365, ax-hv0cl 31366, ax-hvaddid 31367, ax-hfvmul 31368, ax-hvmulid 31369, ax-hvmulass 31370, ax-hvdistr1 31371, ax-hvdistr2 31372, ax-hvmul0 31373, ax-hfi 31442, ax-his1 31445, ax-his2 31446, ax-his3 31447, ax-his4 31448, and ax-hcompl 31565. 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 31344, axhfvadd-zf 31345, axhvcom-zf 31346, axhvass-zf 31347, axhv0cl-zf 31348, axhvaddid-zf 31349, axhfvmul-zf 31350, axhvmulid-zf 31351, axhvmulass-zf 31352, axhvdistr1-zf 31353, axhvdistr2-zf 31354, axhvmul0-zf 31355, axhfi-zf 31356, axhis1-zf 31357, axhis2-zf 31358, axhis3-zf 31359, axhis4-zf 31360, and axhcompl-zf 31361 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 31344.
Axiom	ax-hilex 31362	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 31363	Vector addition is an operation on ℋ. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
⊢ +ℎ :( ℋ × ℋ)⟶ ℋ
Axiom	ax-hvcom 31364	Vector addition is commutative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴))
Axiom	ax-hvass 31365	Vector addition is associative. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = (𝐴 +ℎ (𝐵 +ℎ 𝐶)))
Axiom	ax-hv0cl 31366	The zero vector is in the vector space. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)
⊢ 0ℎ ∈ ℋ
Axiom	ax-hvaddid 31367	Addition with the zero vector. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)
Axiom	ax-hfvmul 31368	Scalar multiplication is an operation on ℂ and ℋ. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
⊢ ·ℎ :(ℂ × ℋ)⟶ ℋ
Axiom	ax-hvmulid 31369	Scalar multiplication by one. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)
Axiom	ax-hvmulass 31370	Scalar multiplication associative law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))
Axiom	ax-hvdistr1 31371	Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 +ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) +ℎ (𝐴 ·ℎ 𝐶)))
Axiom	ax-hvdistr2 31372	Scalar multiplication distributive law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 + 𝐵) ·ℎ 𝐶) = ((𝐴 ·ℎ 𝐶) +ℎ (𝐵 ·ℎ 𝐶)))
Axiom	ax-hvmul0 31373	Scalar multiplication by zero. We can derive the existence of the negative of a vector from this axiom (see hvsubid 31389 and hvsubval 31379). (Contributed by NM, 29-May-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (0 ·ℎ 𝐴) = 0ℎ)
20.1.5  Vector operations
Theorem	hvmulex 31374	The Hilbert space scalar product operation is a set. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.)
⊢ ·ℎ ∈ V
Theorem	hvaddcl 31375	Closure of vector addition. (Contributed by NM, 18-Apr-2007.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) ∈ ℋ)
Theorem	hvmulcl 31376	Closure of scalar multiplication. (Contributed by NM, 19-Apr-2007.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ℎ 𝐵) ∈ ℋ)
Theorem	hvmulcli 31377	Closure inference for scalar multiplication. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 ·ℎ 𝐵) ∈ ℋ
Theorem	hvsubf 31378	Mapping domain and codomain of vector subtraction. (Contributed by NM, 6-Sep-2007.) (New usage is discouraged.)
⊢ −ℎ :( ℋ × ℋ)⟶ ℋ
Theorem	hvsubval 31379	Value of vector subtraction. (Contributed by NM, 5-Sep-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 −ℎ 𝐵) = (𝐴 +ℎ (-1 ·ℎ 𝐵)))
Theorem	hvsubcl 31380	Closure of vector subtraction. (Contributed by NM, 17-Aug-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 −ℎ 𝐵) ∈ ℋ)
Theorem	hvaddcli 31381	Closure of vector addition. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 +ℎ 𝐵) ∈ ℋ
Theorem	hvcomi 31382	Commutation of vector addition. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴)
Theorem	hvsubvali 31383	Value of vector subtraction definition. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 −ℎ 𝐵) = (𝐴 +ℎ (-1 ·ℎ 𝐵))
Theorem	hvsubcli 31384	Closure of vector subtraction. (Contributed by NM, 2-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 −ℎ 𝐵) ∈ ℋ
Theorem	ifhvhv0 31385	Prove if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ. (Contributed by David A. Wheeler, 7-Dec-2018.) (New usage is discouraged.)
⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ
Theorem	hvaddlid 31386	Addition with the zero vector. (Contributed by NM, 18-Oct-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (0ℎ +ℎ 𝐴) = 𝐴)
Theorem	hvmul0 31387	Scalar multiplication with the zero vector. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℂ → (𝐴 ·ℎ 0ℎ) = 0ℎ)
Theorem	hvmul0or 31388	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 31389	Subtraction of a vector from itself. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (𝐴 −ℎ 𝐴) = 0ℎ)
Theorem	hvnegid 31390	Addition of negative of a vector to itself. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ (-1 ·ℎ 𝐴)) = 0ℎ)
Theorem	hv2neg 31391	Two ways to express the negative of a vector. (Contributed by NM, 23-May-2005.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (0ℎ −ℎ 𝐴) = (-1 ·ℎ 𝐴))
Theorem	hvaddlidi 31392	Addition with the zero vector. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    ⇒   ⊢ (0ℎ +ℎ 𝐴) = 𝐴
Theorem	hvnegidi 31393	Addition of negative of a vector to itself. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    ⇒   ⊢ (𝐴 +ℎ (-1 ·ℎ 𝐴)) = 0ℎ
Theorem	hv2negi 31394	Two ways to express the negative of a vector. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    ⇒   ⊢ (0ℎ −ℎ 𝐴) = (-1 ·ℎ 𝐴)
Theorem	hvm1neg 31395	Convert minus one times a scalar product to the negative of the scalar. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (-1 ·ℎ (𝐴 ·ℎ 𝐵)) = (-𝐴 ·ℎ 𝐵))
Theorem	hvaddsubval 31396	Value of vector addition in terms of vector subtraction. (Contributed by NM, 10-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐴 −ℎ (-1 ·ℎ 𝐵)))
Theorem	hvadd32 31397	Commutative/associative law. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = ((𝐴 +ℎ 𝐶) +ℎ 𝐵))
Theorem	hvadd12 31398	Commutative/associative law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 +ℎ (𝐵 +ℎ 𝐶)) = (𝐵 +ℎ (𝐴 +ℎ 𝐶)))
Theorem	hvadd4 31399	Hilbert vector space addition law. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.)
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 +ℎ 𝐵) +ℎ (𝐶 +ℎ 𝐷)) = ((𝐴 +ℎ 𝐶) +ℎ (𝐵 +ℎ 𝐷)))
Theorem	hvsub4 31400	Hilbert vector space addition/subtraction law. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.)
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 +ℎ 𝐵) −ℎ (𝐶 +ℎ 𝐷)) = ((𝐴 −ℎ 𝐶) +ℎ (𝐵 −ℎ 𝐷)))