Step |
Hyp |
Ref |
Expression |
1 |
|
ocvz.v |
|- V = ( Base ` W ) |
2 |
|
ocvz.o |
|- ._|_ = ( ocv ` W ) |
3 |
|
ocvz.z |
|- .0. = ( 0g ` W ) |
4 |
1 2
|
ocvss |
|- ( ._|_ ` V ) C_ V |
5 |
|
sseqin2 |
|- ( ( ._|_ ` V ) C_ V <-> ( V i^i ( ._|_ ` V ) ) = ( ._|_ ` V ) ) |
6 |
4 5
|
mpbi |
|- ( V i^i ( ._|_ ` V ) ) = ( ._|_ ` V ) |
7 |
|
phllmod |
|- ( W e. PreHil -> W e. LMod ) |
8 |
|
eqid |
|- ( LSubSp ` W ) = ( LSubSp ` W ) |
9 |
1 8
|
lss1 |
|- ( W e. LMod -> V e. ( LSubSp ` W ) ) |
10 |
7 9
|
syl |
|- ( W e. PreHil -> V e. ( LSubSp ` W ) ) |
11 |
2 8 3
|
ocvin |
|- ( ( W e. PreHil /\ V e. ( LSubSp ` W ) ) -> ( V i^i ( ._|_ ` V ) ) = { .0. } ) |
12 |
10 11
|
mpdan |
|- ( W e. PreHil -> ( V i^i ( ._|_ ` V ) ) = { .0. } ) |
13 |
6 12
|
eqtr3id |
|- ( W e. PreHil -> ( ._|_ ` V ) = { .0. } ) |