Metamath Proof Explorer


Theorem axhvmul0-zf

Description: Derive Axiom ax-hvmul0 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 axhvmul0-zf
|- ( A e. ~H -> ( 0 .h A ) = 0h )

Proof

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 df-h0v
 |-  0h = ( 0vec ` <. <. +h , .h >. , normh >. )
9 1 fveq2i
 |-  ( 0vec ` U ) = ( 0vec ` <. <. +h , .h >. , normh >. )
10 8 9 eqtr4i
 |-  0h = ( 0vec ` U )
11 5 7 10 hlmul0
 |-  ( ( U e. CHilOLD /\ A e. ~H ) -> ( 0 .h A ) = 0h )
12 2 11 mpan
 |-  ( A e. ~H -> ( 0 .h A ) = 0h )