![]() |
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 30881). 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 31049. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
Ref | Expression |
---|---|
df-hba | ⊢ ℋ = (BaseSet‘〈〈 +ℎ , ·ℎ 〉, normℎ〉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | chba 30801 | . 2 class ℋ | |
2 | cva 30802 | . . . . 5 class +ℎ | |
3 | csm 30803 | . . . . 5 class ·ℎ | |
4 | 2, 3 | cop 4636 | . . . 4 class 〈 +ℎ , ·ℎ 〉 |
5 | cno 30805 | . . . 4 class normℎ | |
6 | 4, 5 | cop 4636 | . . 3 class 〈〈 +ℎ , ·ℎ 〉, normℎ〉 |
7 | cba 30468 | . . 3 class BaseSet | |
8 | 6, 7 | cfv 6549 | . 2 class (BaseSet‘〈〈 +ℎ , ·ℎ 〉, normℎ〉) |
9 | 1, 8 | wceq 1533 | 1 wff ℋ = (BaseSet‘〈〈 +ℎ , ·ℎ 〉, normℎ〉) |
Colors of variables: wff setvar class |
This definition is referenced by: axhilex-zf 30863 axhfvadd-zf 30864 axhvcom-zf 30865 axhvass-zf 30866 axhv0cl-zf 30867 axhvaddid-zf 30868 axhfvmul-zf 30869 axhvmulid-zf 30870 axhvmulass-zf 30871 axhvdistr1-zf 30872 axhvdistr2-zf 30873 axhvmul0-zf 30874 axhfi-zf 30875 axhis1-zf 30876 axhis2-zf 30877 axhis3-zf 30878 axhis4-zf 30879 axhcompl-zf 30880 bcsiHIL 31062 hlimadd 31075 hhssabloilem 31143 pjhthlem2 31274 nmopsetretHIL 31746 nmopub2tHIL 31792 hmopbdoptHIL 31870 |
Copyright terms: Public domain | W3C validator |