Metamath Proof Explorer

Theorem ocvlsp

Description: The orthocomplement of a linear span. (Contributed by Mario Carneiro, 23-Oct-2015)

Ref Expression
Hypotheses ocvlsp.v 
|- V = ( Base ` W )
ocvlsp.o 
|- ._|_ = ( ocv ` W )
ocvlsp.n 
|- N = ( LSpan ` W )
Assertion ocvlsp 
|- ( ( W e. PreHil /\ S C_ V ) -> ( ._|_ ` ( N ` S ) ) = ( ._|_ ` S ) )

Proof

Step Hyp Ref Expression
1 ocvlsp.v 
 |-  V = ( Base ` W )
2 ocvlsp.o 
 |-  ._|_ = ( ocv ` W )
3 ocvlsp.n 
 |-  N = ( LSpan ` W )
4 phllmod 
 |-  ( W e. PreHil -> W e. LMod )
5 1 3 lspssid 
 |-  ( ( W e. LMod /\ S C_ V ) -> S C_ ( N ` S ) )
6 4 5 sylan 
 |-  ( ( W e. PreHil /\ S C_ V ) -> S C_ ( N ` S ) )
7 2 ocv2ss 
 |-  ( S C_ ( N ` S ) -> ( ._|_ ` ( N ` S ) ) C_ ( ._|_ ` S ) )
8 6 7 syl 
 |-  ( ( W e. PreHil /\ S C_ V ) -> ( ._|_ ` ( N ` S ) ) C_ ( ._|_ ` S ) )
9 1 2 ocvss 
 |-  ( ._|_ ` S ) C_ V
10 9 a1i 
 |-  ( ( W e. PreHil /\ S C_ V ) -> ( ._|_ ` S ) C_ V )
11 1 2 ocvocv 
 |-  ( ( W e. PreHil /\ ( ._|_ ` S ) C_ V ) -> ( ._|_ ` S ) C_ ( ._|_ ` ( ._|_ ` ( ._|_ ` S ) ) ) )
12 10 11 syldan 
 |-  ( ( W e. PreHil /\ S C_ V ) -> ( ._|_ ` S ) C_ ( ._|_ ` ( ._|_ ` ( ._|_ ` S ) ) ) )
13 4 adantr 
 |-  ( ( W e. PreHil /\ S C_ V ) -> W e. LMod )
14 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
15 1 2 14 ocvlss 
 |-  ( ( W e. PreHil /\ ( ._|_ ` S ) C_ V ) -> ( ._|_ ` ( ._|_ ` S ) ) e. ( LSubSp ` W ) )
16 10 15 syldan 
 |-  ( ( W e. PreHil /\ S C_ V ) -> ( ._|_ ` ( ._|_ ` S ) ) e. ( LSubSp ` W ) )
17 1 2 ocvocv 
 |-  ( ( W e. PreHil /\ S C_ V ) -> S C_ ( ._|_ ` ( ._|_ ` S ) ) )
18 14 3 lspssp 
 |-  ( ( W e. LMod /\ ( ._|_ ` ( ._|_ ` S ) ) e. ( LSubSp ` W ) /\ S C_ ( ._|_ ` ( ._|_ ` S ) ) ) -> ( N ` S ) C_ ( ._|_ ` ( ._|_ ` S ) ) )
19 13 16 17 18 syl3anc 
 |-  ( ( W e. PreHil /\ S C_ V ) -> ( N ` S ) C_ ( ._|_ ` ( ._|_ ` S ) ) )
20 2 ocv2ss 
 |-  ( ( N ` S ) C_ ( ._|_ ` ( ._|_ ` S ) ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` S ) ) ) C_ ( ._|_ ` ( N ` S ) ) )
21 19 20 syl 
 |-  ( ( W e. PreHil /\ S C_ V ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` S ) ) ) C_ ( ._|_ ` ( N ` S ) ) )
22 12 21 sstrd 
 |-  ( ( W e. PreHil /\ S C_ V ) -> ( ._|_ ` S ) C_ ( ._|_ ` ( N ` S ) ) )
23 8 22 eqssd 
 |-  ( ( W e. PreHil /\ S C_ V ) -> ( ._|_ ` ( N ` S ) ) = ( ._|_ ` S ) )