| 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 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.) |
| Ref | Expression |
|---|---|
| df-hba | ⊢ ℋ = (BaseSet‘〈〈 +ℎ , ·ℎ 〉, normℎ〉) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | chba 30938 | . 2 class ℋ | |
| 2 | cva 30939 | . . . . 5 class +ℎ | |
| 3 | csm 30940 | . . . . 5 class ·ℎ | |
| 4 | 2, 3 | cop 4632 | . . . 4 class 〈 +ℎ , ·ℎ 〉 |
| 5 | cno 30942 | . . . 4 class normℎ | |
| 6 | 4, 5 | cop 4632 | . . 3 class 〈〈 +ℎ , ·ℎ 〉, normℎ〉 |
| 7 | cba 30605 | . . 3 class BaseSet | |
| 8 | 6, 7 | cfv 6561 | . 2 class (BaseSet‘〈〈 +ℎ , ·ℎ 〉, normℎ〉) |
| 9 | 1, 8 | wceq 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 |