Step |
Hyp |
Ref |
Expression |
1 |
|
ocvss.v |
|- V = ( Base ` W ) |
2 |
|
ocvss.o |
|- ._|_ = ( ocv ` W ) |
3 |
1 2
|
ocvss |
|- ( ._|_ ` S ) C_ V |
4 |
3
|
a1i |
|- ( ( ( W e. PreHil /\ S C_ V ) /\ x e. S ) -> ( ._|_ ` S ) C_ V ) |
5 |
|
simpr |
|- ( ( W e. PreHil /\ S C_ V ) -> S C_ V ) |
6 |
5
|
sselda |
|- ( ( ( W e. PreHil /\ S C_ V ) /\ x e. S ) -> x e. V ) |
7 |
|
eqid |
|- ( .i ` W ) = ( .i ` W ) |
8 |
|
eqid |
|- ( Scalar ` W ) = ( Scalar ` W ) |
9 |
|
eqid |
|- ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) ) |
10 |
1 7 8 9 2
|
ocvi |
|- ( ( y e. ( ._|_ ` S ) /\ x e. S ) -> ( y ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) ) |
11 |
10
|
ancoms |
|- ( ( x e. S /\ y e. ( ._|_ ` S ) ) -> ( y ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) ) |
12 |
11
|
adantll |
|- ( ( ( ( W e. PreHil /\ S C_ V ) /\ x e. S ) /\ y e. ( ._|_ ` S ) ) -> ( y ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) ) |
13 |
|
simplll |
|- ( ( ( ( W e. PreHil /\ S C_ V ) /\ x e. S ) /\ y e. ( ._|_ ` S ) ) -> W e. PreHil ) |
14 |
4
|
sselda |
|- ( ( ( ( W e. PreHil /\ S C_ V ) /\ x e. S ) /\ y e. ( ._|_ ` S ) ) -> y e. V ) |
15 |
6
|
adantr |
|- ( ( ( ( W e. PreHil /\ S C_ V ) /\ x e. S ) /\ y e. ( ._|_ ` S ) ) -> x e. V ) |
16 |
8 7 1 9
|
iporthcom |
|- ( ( W e. PreHil /\ y e. V /\ x e. V ) -> ( ( y ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) <-> ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) |
17 |
13 14 15 16
|
syl3anc |
|- ( ( ( ( W e. PreHil /\ S C_ V ) /\ x e. S ) /\ y e. ( ._|_ ` S ) ) -> ( ( y ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) <-> ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) |
18 |
12 17
|
mpbid |
|- ( ( ( ( W e. PreHil /\ S C_ V ) /\ x e. S ) /\ y e. ( ._|_ ` S ) ) -> ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) |
19 |
18
|
ralrimiva |
|- ( ( ( W e. PreHil /\ S C_ V ) /\ x e. S ) -> A. y e. ( ._|_ ` S ) ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) |
20 |
1 7 8 9 2
|
elocv |
|- ( x e. ( ._|_ ` ( ._|_ ` S ) ) <-> ( ( ._|_ ` S ) C_ V /\ x e. V /\ A. y e. ( ._|_ ` S ) ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) |
21 |
4 6 19 20
|
syl3anbrc |
|- ( ( ( W e. PreHil /\ S C_ V ) /\ x e. S ) -> x e. ( ._|_ ` ( ._|_ ` S ) ) ) |
22 |
21
|
ex |
|- ( ( W e. PreHil /\ S C_ V ) -> ( x e. S -> x e. ( ._|_ ` ( ._|_ ` S ) ) ) ) |
23 |
22
|
ssrdv |
|- ( ( W e. PreHil /\ S C_ V ) -> S C_ ( ._|_ ` ( ._|_ ` S ) ) ) |