Definition df-hba 10470

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 10501). 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 as theorem hhba 10667.

Assertion

Ref	Expression
df-hba	|- ~H = (BaseSet` <.<. +h , .h >., normh>.)

Detailed syntax breakdown of Definition df-hba

Step	Hyp	Ref	Expression
1		chil 10420	. 2 class ~H
2		cva 10421	. . . . 5 class +h
3		csm 10422	. . . . 5 class .h
4	2, 3	cop 3046	. . . 4 class <. +h , .h >.
5		cno 10426	. . . 4 class normh
6	4, 5	cop 3046	. . 3 class <.<. +h , .h >., normh>.
7		cba 9537	. . 3 class BaseSet
8	6, 7	cfv 3998	. 2 class (BaseSet` <.<. +h , .h >., normh>.)
9	1, 8	wceq 1298	1 wff ~H = (BaseSet` <.<. +h , .h >., normh>.)

This definition is referenced by:  axhilex 10483  axhfvadd 10484  axhvcom 10485  axhvass 10486  axhv0cl 10487  axhvaddid 10488  axhfvmul 10489  axhvmulid 10490  axhvmulass 10491  axhvdistr1 10492  axhvdistr2 10493  axhvmul0 10494  axhfi 10495  axhis1 10496  axhis2 10497  axhis3 10498  axhis4 10499  axhcompl 10500

Copyright terms: Public domain