Metamath Proof Explorer


Theorem ocvin

Description: An orthocomplement has trivial intersection with the original subspace. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses ocv2ss.o
|- ._|_ = ( ocv ` W )
ocvin.l
|- L = ( LSubSp ` W )
ocvin.z
|- .0. = ( 0g ` W )
Assertion ocvin
|- ( ( W e. PreHil /\ S e. L ) -> ( S i^i ( ._|_ ` S ) ) = { .0. } )

Proof

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