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