![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > df-hba | Structured version Visualization version GIF version |
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 28571). 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 28739. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
Ref | Expression |
---|---|
df-hba | ⊢ ℋ = (BaseSet‘〈〈 +ℎ , ·ℎ 〉, normℎ〉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | chba 28491 | . 2 class ℋ | |
2 | cva 28492 | . . . . 5 class +ℎ | |
3 | csm 28493 | . . . . 5 class ·ℎ | |
4 | 2, 3 | cop 4442 | . . . 4 class 〈 +ℎ , ·ℎ 〉 |
5 | cno 28495 | . . . 4 class normℎ | |
6 | 4, 5 | cop 4442 | . . 3 class 〈〈 +ℎ , ·ℎ 〉, normℎ〉 |
7 | cba 28156 | . . 3 class BaseSet | |
8 | 6, 7 | cfv 6186 | . 2 class (BaseSet‘〈〈 +ℎ , ·ℎ 〉, normℎ〉) |
9 | 1, 8 | wceq 1508 | 1 wff ℋ = (BaseSet‘〈〈 +ℎ , ·ℎ 〉, normℎ〉) |
Colors of variables: wff setvar class |
This definition is referenced by: axhilex-zf 28553 axhfvadd-zf 28554 axhvcom-zf 28555 axhvass-zf 28556 axhv0cl-zf 28557 axhvaddid-zf 28558 axhfvmul-zf 28559 axhvmulid-zf 28560 axhvmulass-zf 28561 axhvdistr1-zf 28562 axhvdistr2-zf 28563 axhvmul0-zf 28564 axhfi-zf 28565 axhis1-zf 28566 axhis2-zf 28567 axhis3-zf 28568 axhis4-zf 28569 axhcompl-zf 28570 bcsiHIL 28752 hlimadd 28765 hhssabloilem 28833 pjhthlem2 28966 nmopsetretHIL 29438 nmopub2tHIL 29484 hmopbdoptHIL 29562 |
Copyright terms: Public domain | W3C validator |