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 ) |