Step |
Hyp |
Ref |
Expression |
1 |
|
ocv2ss.o |
|- ._|_ = ( ocv ` W ) |
2 |
|
ocvin.l |
|- L = ( LSubSp ` W ) |
3 |
|
ocvin.z |
|- .0. = ( 0g ` W ) |
4 |
|
eqid |
|- ( Base ` W ) = ( Base ` W ) |
5 |
|
eqid |
|- ( .i ` W ) = ( .i ` W ) |
6 |
|
eqid |
|- ( Scalar ` W ) = ( Scalar ` W ) |
7 |
|
eqid |
|- ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) ) |
8 |
4 5 6 7 1
|
ocvi |
|- ( ( x e. ( ._|_ ` S ) /\ x e. S ) -> ( x ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) ) |
9 |
8
|
ancoms |
|- ( ( x e. S /\ x e. ( ._|_ ` S ) ) -> ( x ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) ) |
10 |
9
|
adantl |
|- ( ( ( W e. PreHil /\ S e. L ) /\ ( x e. S /\ x e. ( ._|_ ` S ) ) ) -> ( x ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) ) |
11 |
|
simpll |
|- ( ( ( W e. PreHil /\ S e. L ) /\ ( x e. S /\ x e. ( ._|_ ` S ) ) ) -> W e. PreHil ) |
12 |
4 2
|
lssel |
|- ( ( S e. L /\ x e. S ) -> x e. ( Base ` W ) ) |
13 |
12
|
ad2ant2lr |
|- ( ( ( W e. PreHil /\ S e. L ) /\ ( x e. S /\ x e. ( ._|_ ` S ) ) ) -> x e. ( Base ` W ) ) |
14 |
6 5 4 7 3
|
ipeq0 |
|- ( ( W e. PreHil /\ x e. ( Base ` W ) ) -> ( ( x ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) <-> x = .0. ) ) |
15 |
11 13 14
|
syl2anc |
|- ( ( ( W e. PreHil /\ S e. L ) /\ ( x e. S /\ x e. ( ._|_ ` S ) ) ) -> ( ( x ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) <-> x = .0. ) ) |
16 |
10 15
|
mpbid |
|- ( ( ( W e. PreHil /\ S e. L ) /\ ( x e. S /\ x e. ( ._|_ ` S ) ) ) -> x = .0. ) |
17 |
16
|
ex |
|- ( ( W e. PreHil /\ S e. L ) -> ( ( x e. S /\ x e. ( ._|_ ` S ) ) -> x = .0. ) ) |
18 |
|
elin |
|- ( x e. ( S i^i ( ._|_ ` S ) ) <-> ( x e. S /\ x e. ( ._|_ ` S ) ) ) |
19 |
|
velsn |
|- ( x e. { .0. } <-> x = .0. ) |
20 |
17 18 19
|
3imtr4g |
|- ( ( W e. PreHil /\ S e. L ) -> ( x e. ( S i^i ( ._|_ ` S ) ) -> x e. { .0. } ) ) |
21 |
20
|
ssrdv |
|- ( ( W e. PreHil /\ S e. L ) -> ( S i^i ( ._|_ ` S ) ) C_ { .0. } ) |
22 |
|
phllmod |
|- ( W e. PreHil -> W e. LMod ) |
23 |
4 2
|
lssss |
|- ( S e. L -> S C_ ( Base ` W ) ) |
24 |
4 1 2
|
ocvlss |
|- ( ( W e. PreHil /\ S C_ ( Base ` W ) ) -> ( ._|_ ` S ) e. L ) |
25 |
23 24
|
sylan2 |
|- ( ( W e. PreHil /\ S e. L ) -> ( ._|_ ` S ) e. L ) |
26 |
2
|
lssincl |
|- ( ( W e. LMod /\ S e. L /\ ( ._|_ ` S ) e. L ) -> ( S i^i ( ._|_ ` S ) ) e. L ) |
27 |
22 26
|
syl3an1 |
|- ( ( W e. PreHil /\ S e. L /\ ( ._|_ ` S ) e. L ) -> ( S i^i ( ._|_ ` S ) ) e. L ) |
28 |
25 27
|
mpd3an3 |
|- ( ( W e. PreHil /\ S e. L ) -> ( S i^i ( ._|_ ` S ) ) e. L ) |
29 |
3 2
|
lss0ss |
|- ( ( W e. LMod /\ ( S i^i ( ._|_ ` S ) ) e. L ) -> { .0. } C_ ( S i^i ( ._|_ ` S ) ) ) |
30 |
22 28 29
|
syl2an2r |
|- ( ( W e. PreHil /\ S e. L ) -> { .0. } C_ ( S i^i ( ._|_ ` S ) ) ) |
31 |
21 30
|
eqssd |
|- ( ( W e. PreHil /\ S e. L ) -> ( S i^i ( ._|_ ` S ) ) = { .0. } ) |