Description: Derive Axiom ax-hfvmul from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | axhil.1 | |- U = <. <. +h , .h >. , normh >. |
|
axhil.2 | |- U e. CHilOLD |
||
Assertion | axhfvmul-zf | |- .h : ( CC X. ~H ) --> ~H |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axhil.1 | |- U = <. <. +h , .h >. , normh >. |
|
2 | axhil.2 | |- U e. CHilOLD |
|
3 | df-hba | |- ~H = ( BaseSet ` <. <. +h , .h >. , normh >. ) |
|
4 | 1 | fveq2i | |- ( BaseSet ` U ) = ( BaseSet ` <. <. +h , .h >. , normh >. ) |
5 | 3 4 | eqtr4i | |- ~H = ( BaseSet ` U ) |
6 | 2 | hlnvi | |- U e. NrmCVec |
7 | 1 6 | h2hsm | |- .h = ( .sOLD ` U ) |
8 | 5 7 | hlmulf | |- ( U e. CHilOLD -> .h : ( CC X. ~H ) --> ~H ) |
9 | 2 8 | ax-mp | |- .h : ( CC X. ~H ) --> ~H |