HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-hba Structured version   Visualization version   GIF version

Definition df-hba 30988
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 31018). 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 31186. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
Assertion
Ref Expression
df-hba ℋ = (BaseSet‘⟨⟨ + , · ⟩, norm⟩)

Detailed syntax breakdown of Definition df-hba
StepHypRef Expression
1 chba 30938 . 2 class
2 cva 30939 . . . . 5 class +
3 csm 30940 . . . . 5 class ·
42, 3cop 4632 . . . 4 class ⟨ + , ·
5 cno 30942 . . . 4 class norm
64, 5cop 4632 . . 3 class ⟨⟨ + , · ⟩, norm
7 cba 30605 . . 3 class BaseSet
86, 7cfv 6561 . 2 class (BaseSet‘⟨⟨ + , · ⟩, norm⟩)
91, 8wceq 1540 1 wff ℋ = (BaseSet‘⟨⟨ + , · ⟩, norm⟩)
Colors of variables: wff setvar class
This definition is referenced by:  axhilex-zf  31000  axhfvadd-zf  31001  axhvcom-zf  31002  axhvass-zf  31003  axhv0cl-zf  31004  axhvaddid-zf  31005  axhfvmul-zf  31006  axhvmulid-zf  31007  axhvmulass-zf  31008  axhvdistr1-zf  31009  axhvdistr2-zf  31010  axhvmul0-zf  31011  axhfi-zf  31012  axhis1-zf  31013  axhis2-zf  31014  axhis3-zf  31015  axhis4-zf  31016  axhcompl-zf  31017  bcsiHIL  31199  hlimadd  31212  hhssabloilem  31280  pjhthlem2  31411  nmopsetretHIL  31883  nmopub2tHIL  31929  hmopbdoptHIL  32007
  Copyright terms: Public domain W3C validator