This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-hba

Description: Define base set of Hilbert space, for use if we want to develop Hilbert space independently from the axioms (see comments in ax-hilex ). Note that ~H 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 . (Contributed by NM, 31-May-2008) (New usage is discouraged.)

		Ref	Expression
	Assertion	df-hba	$⊢ ℋ = BaseSet (⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chba	$class ℋ$
1		cba	$class BaseSet$
2		cva	$class +_{ℎ}$
3		csm	$class \cdot_{ℎ}$
4	2 3	cop	$class ⟨+_{ℎ}, \cdot_{ℎ}⟩$
5		cno	$class {norm}_{ℎ}$
6	4 5	cop	$class ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩$
7	6 1	cfv	$class BaseSet (⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩)$
8	0 7	wceq	$wff ℋ = BaseSet (⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩)$