Metamath Proof Explorer


Theorem axhis3-zf

Description: Derive Axiom ax-his3 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
axhfi.1
|- .ih = ( .iOLD ` U )
Assertion axhis3-zf
|- ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( ( A .h B ) .ih C ) = ( A x. ( B .ih C ) ) )

Proof

Step Hyp Ref Expression
1 axhil.1
 |-  U = <. <. +h , .h >. , normh >.
2 axhil.2
 |-  U e. CHilOLD
3 axhfi.1
 |-  .ih = ( .iOLD ` U )
4 df-hba
 |-  ~H = ( BaseSet ` <. <. +h , .h >. , normh >. )
5 1 fveq2i
 |-  ( BaseSet ` U ) = ( BaseSet ` <. <. +h , .h >. , normh >. )
6 4 5 eqtr4i
 |-  ~H = ( BaseSet ` U )
7 2 hlnvi
 |-  U e. NrmCVec
8 1 7 h2hsm
 |-  .h = ( .sOLD ` U )
9 6 8 3 hlipass
 |-  ( ( U e. CHilOLD /\ ( A e. CC /\ B e. ~H /\ C e. ~H ) ) -> ( ( A .h B ) .ih C ) = ( A x. ( B .ih C ) ) )
10 2 9 mpan
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( ( A .h B ) .ih C ) = ( A x. ( B .ih C ) ) )