Metamath Proof Explorer

Theorem obselocv

Description: A basis element is in the orthocomplement of a subset of the basis iff it is not in the subset. (Contributed by Mario Carneiro, 23-Oct-2015)

Ref Expression
Hypothesis obselocv.o 
|- ._|_ = ( ocv ` W )
Assertion obselocv 
|- ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) -> ( A e. ( ._|_ ` C ) <-> -. A e. C ) )

Proof

Step Hyp Ref Expression
1 obselocv.o 
 |-  ._|_ = ( ocv ` W )
2 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
3 2 obsne0 
 |-  ( ( B e. ( OBasis ` W ) /\ A e. B ) -> A =/= ( 0g ` W ) )
4 3 3adant2 
 |-  ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) -> A =/= ( 0g ` W ) )
5 elin 
 |-  ( A e. ( C i^i ( ._|_ ` C ) ) <-> ( A e. C /\ A e. ( ._|_ ` C ) ) )
6 obsrcl 
 |-  ( B e. ( OBasis ` W ) -> W e. PreHil )
7 6 3ad2ant1 
 |-  ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) -> W e. PreHil )
8 phllmod 
 |-  ( W e. PreHil -> W e. LMod )
9 7 8 syl 
 |-  ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) -> W e. LMod )
10 simp2 
 |-  ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) -> C C_ B )
11 eqid 
 |-  ( Base ` W ) = ( Base ` W )
12 11 obsss 
 |-  ( B e. ( OBasis ` W ) -> B C_ ( Base ` W ) )
13 12 3ad2ant1 
 |-  ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) -> B C_ ( Base ` W ) )
14 10 13 sstrd 
 |-  ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) -> C C_ ( Base ` W ) )
15 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
16 11 15 lspssid 
 |-  ( ( W e. LMod /\ C C_ ( Base ` W ) ) -> C C_ ( ( LSpan ` W ) ` C ) )
17 9 14 16 syl2anc 
 |-  ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) -> C C_ ( ( LSpan ` W ) ` C ) )
18 17 ssrind 
 |-  ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) -> ( C i^i ( ._|_ ` C ) ) C_ ( ( ( LSpan ` W ) ` C ) i^i ( ._|_ ` C ) ) )
19 11 1 15 ocvlsp 
 |-  ( ( W e. PreHil /\ C C_ ( Base ` W ) ) -> ( ._|_ ` ( ( LSpan ` W ) ` C ) ) = ( ._|_ ` C ) )
20 7 14 19 syl2anc 
 |-  ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) -> ( ._|_ ` ( ( LSpan ` W ) ` C ) ) = ( ._|_ ` C ) )
21 20 ineq2d 
 |-  ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) -> ( ( ( LSpan ` W ) ` C ) i^i ( ._|_ ` ( ( LSpan ` W ) ` C ) ) ) = ( ( ( LSpan ` W ) ` C ) i^i ( ._|_ ` C ) ) )
22 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
23 11 22 15 lspcl 
 |-  ( ( W e. LMod /\ C C_ ( Base ` W ) ) -> ( ( LSpan ` W ) ` C ) e. ( LSubSp ` W ) )
24 9 14 23 syl2anc 
 |-  ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) -> ( ( LSpan ` W ) ` C ) e. ( LSubSp ` W ) )
25 1 22 2 ocvin 
 |-  ( ( W e. PreHil /\ ( ( LSpan ` W ) ` C ) e. ( LSubSp ` W ) ) -> ( ( ( LSpan ` W ) ` C ) i^i ( ._|_ ` ( ( LSpan ` W ) ` C ) ) ) = { ( 0g ` W ) } )
26 7 24 25 syl2anc 
 |-  ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) -> ( ( ( LSpan ` W ) ` C ) i^i ( ._|_ ` ( ( LSpan ` W ) ` C ) ) ) = { ( 0g ` W ) } )
27 21 26 eqtr3d 
 |-  ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) -> ( ( ( LSpan ` W ) ` C ) i^i ( ._|_ ` C ) ) = { ( 0g ` W ) } )
28 18 27 sseqtrd 
 |-  ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) -> ( C i^i ( ._|_ ` C ) ) C_ { ( 0g ` W ) } )
29 28 sseld 
 |-  ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) -> ( A e. ( C i^i ( ._|_ ` C ) ) -> A e. { ( 0g ` W ) } ) )
30 5 29 biimtrrid 
 |-  ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) -> ( ( A e. C /\ A e. ( ._|_ ` C ) ) -> A e. { ( 0g ` W ) } ) )
31 elsni 
 |-  ( A e. { ( 0g ` W ) } -> A = ( 0g ` W ) )
32 30 31 syl6 
 |-  ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) -> ( ( A e. C /\ A e. ( ._|_ ` C ) ) -> A = ( 0g ` W ) ) )
33 32 necon3ad 
 |-  ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) -> ( A =/= ( 0g ` W ) -> -. ( A e. C /\ A e. ( ._|_ ` C ) ) ) )
34 4 33 mpd 
 |-  ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) -> -. ( A e. C /\ A e. ( ._|_ ` C ) ) )
35 imnan 
 |-  ( ( A e. C -> -. A e. ( ._|_ ` C ) ) <-> -. ( A e. C /\ A e. ( ._|_ ` C ) ) )
36 34 35 sylibr 
 |-  ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) -> ( A e. C -> -. A e. ( ._|_ ` C ) ) )
37 36 con2d 
 |-  ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) -> ( A e. ( ._|_ ` C ) -> -. A e. C ) )
38 simpr 
 |-  ( ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) /\ x e. C ) -> x e. C )
39 eleq1 
 |-  ( A = x -> ( A e. C <-> x e. C ) )
40 38 39 syl5ibrcom 
 |-  ( ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) /\ x e. C ) -> ( A = x -> A e. C ) )
41 40 con3d 
 |-  ( ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) /\ x e. C ) -> ( -. A e. C -> -. A = x ) )
42 simpl1 
 |-  ( ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) /\ x e. C ) -> B e. ( OBasis ` W ) )
43 simpl3 
 |-  ( ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) /\ x e. C ) -> A e. B )
44 10 sselda 
 |-  ( ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) /\ x e. C ) -> x e. B )
45 eqid 
 |-  ( .i ` W ) = ( .i ` W )
46 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
47 eqid 
 |-  ( 1r ` ( Scalar ` W ) ) = ( 1r ` ( Scalar ` W ) )
48 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
49 11 45 46 47 48 obsip 
 |-  ( ( B e. ( OBasis ` W ) /\ A e. B /\ x e. B ) -> ( A ( .i ` W ) x ) = if ( A = x , ( 1r ` ( Scalar ` W ) ) , ( 0g ` ( Scalar ` W ) ) ) )
50 42 43 44 49 syl3anc 
 |-  ( ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) /\ x e. C ) -> ( A ( .i ` W ) x ) = if ( A = x , ( 1r ` ( Scalar ` W ) ) , ( 0g ` ( Scalar ` W ) ) ) )
51 iffalse 
 |-  ( -. A = x -> if ( A = x , ( 1r ` ( Scalar ` W ) ) , ( 0g ` ( Scalar ` W ) ) ) = ( 0g ` ( Scalar ` W ) ) )
52 51 eqeq2d 
 |-  ( -. A = x -> ( ( A ( .i ` W ) x ) = if ( A = x , ( 1r ` ( Scalar ` W ) ) , ( 0g ` ( Scalar ` W ) ) ) <-> ( A ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) ) )
53 50 52 syl5ibcom 
 |-  ( ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) /\ x e. C ) -> ( -. A = x -> ( A ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) ) )
54 41 53 syld 
 |-  ( ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) /\ x e. C ) -> ( -. A e. C -> ( A ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) ) )
55 54 ralrimdva 
 |-  ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) -> ( -. A e. C -> A. x e. C ( A ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) ) )
56 simp3 
 |-  ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) -> A e. B )
57 13 56 sseldd 
 |-  ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) -> A e. ( Base ` W ) )
58 11 45 46 48 1 elocv 
 |-  ( A e. ( ._|_ ` C ) <-> ( C C_ ( Base ` W ) /\ A e. ( Base ` W ) /\ A. x e. C ( A ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) ) )
59 df-3an 
 |-  ( ( C C_ ( Base ` W ) /\ A e. ( Base ` W ) /\ A. x e. C ( A ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) ) <-> ( ( C C_ ( Base ` W ) /\ A e. ( Base ` W ) ) /\ A. x e. C ( A ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) ) )
60 58 59 bitri 
 |-  ( A e. ( ._|_ ` C ) <-> ( ( C C_ ( Base ` W ) /\ A e. ( Base ` W ) ) /\ A. x e. C ( A ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) ) )
61 60 baib 
 |-  ( ( C C_ ( Base ` W ) /\ A e. ( Base ` W ) ) -> ( A e. ( ._|_ ` C ) <-> A. x e. C ( A ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) ) )
62 14 57 61 syl2anc 
 |-  ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) -> ( A e. ( ._|_ ` C ) <-> A. x e. C ( A ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) ) )
63 55 62 sylibrd 
 |-  ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) -> ( -. A e. C -> A e. ( ._|_ ` C ) ) )
64 37 63 impbid 
 |-  ( ( B e. ( OBasis ` W ) /\ C C_ B /\ A e. B ) -> ( A e. ( ._|_ ` C ) <-> -. A e. C ) )