Metamath Proof Explorer

Theorem obslbs

Description: An orthogonal basis is a linear basis iff the span of the basis elements is closed (which is usually not true). (Contributed by Mario Carneiro, 29-Oct-2015)

Ref Expression
Hypotheses obslbs.j 
|- J = ( LBasis ` W )
obslbs.n 
|- N = ( LSpan ` W )
obslbs.c 
|- C = ( ClSubSp ` W )
Assertion obslbs 
|- ( B e. ( OBasis ` W ) -> ( B e. J <-> ( N ` B ) e. C ) )

Proof

Step Hyp Ref Expression
1 obslbs.j 
 |-  J = ( LBasis ` W )
2 obslbs.n 
 |-  N = ( LSpan ` W )
3 obslbs.c 
 |-  C = ( ClSubSp ` W )
4 obsrcl 
 |-  ( B e. ( OBasis ` W ) -> W e. PreHil )
5 eqid 
 |-  ( Base ` W ) = ( Base ` W )
6 5 obsss 
 |-  ( B e. ( OBasis ` W ) -> B C_ ( Base ` W ) )
7 eqid 
 |-  ( ocv ` W ) = ( ocv ` W )
8 5 7 2 ocvlsp 
 |-  ( ( W e. PreHil /\ B C_ ( Base ` W ) ) -> ( ( ocv ` W ) ` ( N ` B ) ) = ( ( ocv ` W ) ` B ) )
9 4 6 8 syl2anc 
 |-  ( B e. ( OBasis ` W ) -> ( ( ocv ` W ) ` ( N ` B ) ) = ( ( ocv ` W ) ` B ) )
10 9 fveq2d 
 |-  ( B e. ( OBasis ` W ) -> ( ( ocv ` W ) ` ( ( ocv ` W ) ` ( N ` B ) ) ) = ( ( ocv ` W ) ` ( ( ocv ` W ) ` B ) ) )
11 7 5 obs2ocv 
 |-  ( B e. ( OBasis ` W ) -> ( ( ocv ` W ) ` ( ( ocv ` W ) ` B ) ) = ( Base ` W ) )
12 10 11 eqtrd 
 |-  ( B e. ( OBasis ` W ) -> ( ( ocv ` W ) ` ( ( ocv ` W ) ` ( N ` B ) ) ) = ( Base ` W ) )
13 12 eqeq2d 
 |-  ( B e. ( OBasis ` W ) -> ( ( N ` B ) = ( ( ocv ` W ) ` ( ( ocv ` W ) ` ( N ` B ) ) ) <-> ( N ` B ) = ( Base ` W ) ) )
14 7 3 iscss 
 |-  ( W e. PreHil -> ( ( N ` B ) e. C <-> ( N ` B ) = ( ( ocv ` W ) ` ( ( ocv ` W ) ` ( N ` B ) ) ) ) )
15 4 14 syl 
 |-  ( B e. ( OBasis ` W ) -> ( ( N ` B ) e. C <-> ( N ` B ) = ( ( ocv ` W ) ` ( ( ocv ` W ) ` ( N ` B ) ) ) ) )
16 phllvec 
 |-  ( W e. PreHil -> W e. LVec )
17 4 16 syl 
 |-  ( B e. ( OBasis ` W ) -> W e. LVec )
18 pssnel 
 |-  ( x C. B -> E. y ( y e. B /\ -. y e. x ) )
19 18 adantl 
 |-  ( ( B e. ( OBasis ` W ) /\ x C. B ) -> E. y ( y e. B /\ -. y e. x ) )
20 simpll 
 |-  ( ( ( B e. ( OBasis ` W ) /\ x C. B ) /\ y e. B ) -> B e. ( OBasis ` W ) )
21 pssss 
 |-  ( x C. B -> x C_ B )
22 21 ad2antlr 
 |-  ( ( ( B e. ( OBasis ` W ) /\ x C. B ) /\ y e. B ) -> x C_ B )
23 simpr 
 |-  ( ( ( B e. ( OBasis ` W ) /\ x C. B ) /\ y e. B ) -> y e. B )
24 7 obselocv 
 |-  ( ( B e. ( OBasis ` W ) /\ x C_ B /\ y e. B ) -> ( y e. ( ( ocv ` W ) ` x ) <-> -. y e. x ) )
25 20 22 23 24 syl3anc 
 |-  ( ( ( B e. ( OBasis ` W ) /\ x C. B ) /\ y e. B ) -> ( y e. ( ( ocv ` W ) ` x ) <-> -. y e. x ) )
26 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
27 26 obsne0 
 |-  ( ( B e. ( OBasis ` W ) /\ y e. B ) -> y =/= ( 0g ` W ) )
28 20 23 27 syl2anc 
 |-  ( ( ( B e. ( OBasis ` W ) /\ x C. B ) /\ y e. B ) -> y =/= ( 0g ` W ) )
29 nelsn 
 |-  ( y =/= ( 0g ` W ) -> -. y e. { ( 0g ` W ) } )
30 28 29 syl 
 |-  ( ( ( B e. ( OBasis ` W ) /\ x C. B ) /\ y e. B ) -> -. y e. { ( 0g ` W ) } )
31 nelne1 
 |-  ( ( y e. ( ( ocv ` W ) ` x ) /\ -. y e. { ( 0g ` W ) } ) -> ( ( ocv ` W ) ` x ) =/= { ( 0g ` W ) } )
32 31 expcom 
 |-  ( -. y e. { ( 0g ` W ) } -> ( y e. ( ( ocv ` W ) ` x ) -> ( ( ocv ` W ) ` x ) =/= { ( 0g ` W ) } ) )
33 30 32 syl 
 |-  ( ( ( B e. ( OBasis ` W ) /\ x C. B ) /\ y e. B ) -> ( y e. ( ( ocv ` W ) ` x ) -> ( ( ocv ` W ) ` x ) =/= { ( 0g ` W ) } ) )
34 25 33 sylbird 
 |-  ( ( ( B e. ( OBasis ` W ) /\ x C. B ) /\ y e. B ) -> ( -. y e. x -> ( ( ocv ` W ) ` x ) =/= { ( 0g ` W ) } ) )
35 npss 
 |-  ( -. ( N ` x ) C. ( Base ` W ) <-> ( ( N ` x ) C_ ( Base ` W ) -> ( N ` x ) = ( Base ` W ) ) )
36 phllmod 
 |-  ( W e. PreHil -> W e. LMod )
37 4 36 syl 
 |-  ( B e. ( OBasis ` W ) -> W e. LMod )
38 37 ad2antrr 
 |-  ( ( ( B e. ( OBasis ` W ) /\ x C. B ) /\ y e. B ) -> W e. LMod )
39 6 ad2antrr 
 |-  ( ( ( B e. ( OBasis ` W ) /\ x C. B ) /\ y e. B ) -> B C_ ( Base ` W ) )
40 22 39 sstrd 
 |-  ( ( ( B e. ( OBasis ` W ) /\ x C. B ) /\ y e. B ) -> x C_ ( Base ` W ) )
41 5 2 lspssv 
 |-  ( ( W e. LMod /\ x C_ ( Base ` W ) ) -> ( N ` x ) C_ ( Base ` W ) )
42 38 40 41 syl2anc 
 |-  ( ( ( B e. ( OBasis ` W ) /\ x C. B ) /\ y e. B ) -> ( N ` x ) C_ ( Base ` W ) )
43 fveq2 
 |-  ( ( N ` x ) = ( Base ` W ) -> ( ( ocv ` W ) ` ( N ` x ) ) = ( ( ocv ` W ) ` ( Base ` W ) ) )
44 4 ad2antrr 
 |-  ( ( ( B e. ( OBasis ` W ) /\ x C. B ) /\ y e. B ) -> W e. PreHil )
45 5 7 2 ocvlsp 
 |-  ( ( W e. PreHil /\ x C_ ( Base ` W ) ) -> ( ( ocv ` W ) ` ( N ` x ) ) = ( ( ocv ` W ) ` x ) )
46 44 40 45 syl2anc 
 |-  ( ( ( B e. ( OBasis ` W ) /\ x C. B ) /\ y e. B ) -> ( ( ocv ` W ) ` ( N ` x ) ) = ( ( ocv ` W ) ` x ) )
47 5 7 26 ocv1 
 |-  ( W e. PreHil -> ( ( ocv ` W ) ` ( Base ` W ) ) = { ( 0g ` W ) } )
48 44 47 syl 
 |-  ( ( ( B e. ( OBasis ` W ) /\ x C. B ) /\ y e. B ) -> ( ( ocv ` W ) ` ( Base ` W ) ) = { ( 0g ` W ) } )
49 46 48 eqeq12d 
 |-  ( ( ( B e. ( OBasis ` W ) /\ x C. B ) /\ y e. B ) -> ( ( ( ocv ` W ) ` ( N ` x ) ) = ( ( ocv ` W ) ` ( Base ` W ) ) <-> ( ( ocv ` W ) ` x ) = { ( 0g ` W ) } ) )
50 43 49 syl5ib 
 |-  ( ( ( B e. ( OBasis ` W ) /\ x C. B ) /\ y e. B ) -> ( ( N ` x ) = ( Base ` W ) -> ( ( ocv ` W ) ` x ) = { ( 0g ` W ) } ) )
51 42 50 embantd 
 |-  ( ( ( B e. ( OBasis ` W ) /\ x C. B ) /\ y e. B ) -> ( ( ( N ` x ) C_ ( Base ` W ) -> ( N ` x ) = ( Base ` W ) ) -> ( ( ocv ` W ) ` x ) = { ( 0g ` W ) } ) )
52 35 51 syl5bi 
 |-  ( ( ( B e. ( OBasis ` W ) /\ x C. B ) /\ y e. B ) -> ( -. ( N ` x ) C. ( Base ` W ) -> ( ( ocv ` W ) ` x ) = { ( 0g ` W ) } ) )
53 52 necon1ad 
 |-  ( ( ( B e. ( OBasis ` W ) /\ x C. B ) /\ y e. B ) -> ( ( ( ocv ` W ) ` x ) =/= { ( 0g ` W ) } -> ( N ` x ) C. ( Base ` W ) ) )
54 34 53 syld 
 |-  ( ( ( B e. ( OBasis ` W ) /\ x C. B ) /\ y e. B ) -> ( -. y e. x -> ( N ` x ) C. ( Base ` W ) ) )
55 54 expimpd 
 |-  ( ( B e. ( OBasis ` W ) /\ x C. B ) -> ( ( y e. B /\ -. y e. x ) -> ( N ` x ) C. ( Base ` W ) ) )
56 55 exlimdv 
 |-  ( ( B e. ( OBasis ` W ) /\ x C. B ) -> ( E. y ( y e. B /\ -. y e. x ) -> ( N ` x ) C. ( Base ` W ) ) )
57 19 56 mpd 
 |-  ( ( B e. ( OBasis ` W ) /\ x C. B ) -> ( N ` x ) C. ( Base ` W ) )
58 57 ex 
 |-  ( B e. ( OBasis ` W ) -> ( x C. B -> ( N ` x ) C. ( Base ` W ) ) )
59 58 alrimiv 
 |-  ( B e. ( OBasis ` W ) -> A. x ( x C. B -> ( N ` x ) C. ( Base ` W ) ) )
60 5 1 2 islbs3 
 |-  ( W e. LVec -> ( B e. J <-> ( B C_ ( Base ` W ) /\ ( N ` B ) = ( Base ` W ) /\ A. x ( x C. B -> ( N ` x ) C. ( Base ` W ) ) ) ) )
61 3anan32 
 |-  ( ( B C_ ( Base ` W ) /\ ( N ` B ) = ( Base ` W ) /\ A. x ( x C. B -> ( N ` x ) C. ( Base ` W ) ) ) <-> ( ( B C_ ( Base ` W ) /\ A. x ( x C. B -> ( N ` x ) C. ( Base ` W ) ) ) /\ ( N ` B ) = ( Base ` W ) ) )
62 60 61 bitrdi 
 |-  ( W e. LVec -> ( B e. J <-> ( ( B C_ ( Base ` W ) /\ A. x ( x C. B -> ( N ` x ) C. ( Base ` W ) ) ) /\ ( N ` B ) = ( Base ` W ) ) ) )
63 62 baibd 
 |-  ( ( W e. LVec /\ ( B C_ ( Base ` W ) /\ A. x ( x C. B -> ( N ` x ) C. ( Base ` W ) ) ) ) -> ( B e. J <-> ( N ` B ) = ( Base ` W ) ) )
64 17 6 59 63 syl12anc 
 |-  ( B e. ( OBasis ` W ) -> ( B e. J <-> ( N ` B ) = ( Base ` W ) ) )
65 13 15 64 3bitr4rd 
 |-  ( B e. ( OBasis ` W ) -> ( B e. J <-> ( N ` B ) e. C ) )