Metamath Proof Explorer

Theorem phllvec

Description: A pre-Hilbert space is a left vector space. (Contributed by Mario Carneiro, 7-Oct-2015)

Ref Expression
Assertion phllvec 
|- ( W e. PreHil -> W e. LVec )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` W ) = ( Base ` W )
2 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
3 eqid 
 |-  ( .i ` W ) = ( .i ` W )
4 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
5 eqid 
 |-  ( *r ` ( Scalar ` W ) ) = ( *r ` ( Scalar ` W ) )
6 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
7 1 2 3 4 5 6 isphl 
 |-  ( W e. PreHil <-> ( W e. LVec /\ ( Scalar ` W ) e. *Ring /\ A. x e. ( Base ` W ) ( ( y e. ( Base ` W ) |-> ( y ( .i ` W ) x ) ) e. ( W LMHom ( ringLMod ` ( Scalar ` W ) ) ) /\ ( ( x ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) -> x = ( 0g ` W ) ) /\ A. y e. ( Base ` W ) ( ( *r ` ( Scalar ` W ) ) ` ( x ( .i ` W ) y ) ) = ( y ( .i ` W ) x ) ) ) )
8 7 simp1bi 
 |-  ( W e. PreHil -> W e. LVec )