Metamath Proof Explorer

Theorem lbslsat

Description: A nonzero vector X is a basis of a line spanned by the singleton X . Spans of nonzero singletons are sometimes called "atoms", see df-lsatoms and for example lsatlspsn . (Contributed by Thierry Arnoux, 20-May-2023)

Ref Expression
Hypotheses lbslsat.v 
|- V = ( Base ` W )
lbslsat.n 
|- N = ( LSpan ` W )
lbslsat.z 
|- .0. = ( 0g ` W )
lbslsat.y 
|- Y = ( W |`s ( N ` { X } ) )
Assertion lbslsat 
|- ( ( W e. LVec /\ X e. V /\ X =/= .0. ) -> { X } e. ( LBasis ` Y ) )

Proof

Step Hyp Ref Expression
1 lbslsat.v 
 |-  V = ( Base ` W )
2 lbslsat.n 
 |-  N = ( LSpan ` W )
3 lbslsat.z 
 |-  .0. = ( 0g ` W )
4 lbslsat.y 
 |-  Y = ( W |`s ( N ` { X } ) )
5 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
6 5 adantr 
 |-  ( ( W e. LVec /\ X e. V ) -> W e. LMod )
7 snssi 
 |-  ( X e. V -> { X } C_ V )
8 7 adantl 
 |-  ( ( W e. LVec /\ X e. V ) -> { X } C_ V )
9 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
10 1 9 2 lspcl 
 |-  ( ( W e. LMod /\ { X } C_ V ) -> ( N ` { X } ) e. ( LSubSp ` W ) )
11 6 8 10 syl2anc 
 |-  ( ( W e. LVec /\ X e. V ) -> ( N ` { X } ) e. ( LSubSp ` W ) )
12 4 9 lsslvec 
 |-  ( ( W e. LVec /\ ( N ` { X } ) e. ( LSubSp ` W ) ) -> Y e. LVec )
13 11 12 syldan 
 |-  ( ( W e. LVec /\ X e. V ) -> Y e. LVec )
14 13 3adant3 
 |-  ( ( W e. LVec /\ X e. V /\ X =/= .0. ) -> Y e. LVec )
15 1 2 lspssid 
 |-  ( ( W e. LMod /\ { X } C_ V ) -> { X } C_ ( N ` { X } ) )
16 6 8 15 syl2anc 
 |-  ( ( W e. LVec /\ X e. V ) -> { X } C_ ( N ` { X } ) )
17 1 2 lspssv 
 |-  ( ( W e. LMod /\ { X } C_ V ) -> ( N ` { X } ) C_ V )
18 6 8 17 syl2anc 
 |-  ( ( W e. LVec /\ X e. V ) -> ( N ` { X } ) C_ V )
19 4 1 ressbas2 
 |-  ( ( N ` { X } ) C_ V -> ( N ` { X } ) = ( Base ` Y ) )
20 18 19 syl 
 |-  ( ( W e. LVec /\ X e. V ) -> ( N ` { X } ) = ( Base ` Y ) )
21 16 20 sseqtrd 
 |-  ( ( W e. LVec /\ X e. V ) -> { X } C_ ( Base ` Y ) )
22 21 3adant3 
 |-  ( ( W e. LVec /\ X e. V /\ X =/= .0. ) -> { X } C_ ( Base ` Y ) )
23 6 3adant3 
 |-  ( ( W e. LVec /\ X e. V /\ X =/= .0. ) -> W e. LMod )
24 11 3adant3 
 |-  ( ( W e. LVec /\ X e. V /\ X =/= .0. ) -> ( N ` { X } ) e. ( LSubSp ` W ) )
25 16 3adant3 
 |-  ( ( W e. LVec /\ X e. V /\ X =/= .0. ) -> { X } C_ ( N ` { X } ) )
26 eqid 
 |-  ( LSpan ` Y ) = ( LSpan ` Y )
27 4 2 26 9 lsslsp 
 |-  ( ( W e. LMod /\ ( N ` { X } ) e. ( LSubSp ` W ) /\ { X } C_ ( N ` { X } ) ) -> ( N ` { X } ) = ( ( LSpan ` Y ) ` { X } ) )
28 23 24 25 27 syl3anc 
 |-  ( ( W e. LVec /\ X e. V /\ X =/= .0. ) -> ( N ` { X } ) = ( ( LSpan ` Y ) ` { X } ) )
29 20 3adant3 
 |-  ( ( W e. LVec /\ X e. V /\ X =/= .0. ) -> ( N ` { X } ) = ( Base ` Y ) )
30 28 29 eqtr3d 
 |-  ( ( W e. LVec /\ X e. V /\ X =/= .0. ) -> ( ( LSpan ` Y ) ` { X } ) = ( Base ` Y ) )
31 difid 
 |-  ( { X } \ { X } ) = (/)
32 31 fveq2i 
 |-  ( ( LSpan ` Y ) ` ( { X } \ { X } ) ) = ( ( LSpan ` Y ) ` (/) )
33 32 a1i 
 |-  ( ( W e. LVec /\ X e. V ) -> ( ( LSpan ` Y ) ` ( { X } \ { X } ) ) = ( ( LSpan ` Y ) ` (/) ) )
34 33 eleq2d 
 |-  ( ( W e. LVec /\ X e. V ) -> ( X e. ( ( LSpan ` Y ) ` ( { X } \ { X } ) ) <-> X e. ( ( LSpan ` Y ) ` (/) ) ) )
35 34 biimpa 
 |-  ( ( ( W e. LVec /\ X e. V ) /\ X e. ( ( LSpan ` Y ) ` ( { X } \ { X } ) ) ) -> X e. ( ( LSpan ` Y ) ` (/) ) )
36 lveclmod 
 |-  ( Y e. LVec -> Y e. LMod )
37 eqid 
 |-  ( 0g ` Y ) = ( 0g ` Y )
38 37 26 lsp0 
 |-  ( Y e. LMod -> ( ( LSpan ` Y ) ` (/) ) = { ( 0g ` Y ) } )
39 13 36 38 3syl 
 |-  ( ( W e. LVec /\ X e. V ) -> ( ( LSpan ` Y ) ` (/) ) = { ( 0g ` Y ) } )
40 39 adantr 
 |-  ( ( ( W e. LVec /\ X e. V ) /\ X e. ( ( LSpan ` Y ) ` ( { X } \ { X } ) ) ) -> ( ( LSpan ` Y ) ` (/) ) = { ( 0g ` Y ) } )
41 35 40 eleqtrd 
 |-  ( ( ( W e. LVec /\ X e. V ) /\ X e. ( ( LSpan ` Y ) ` ( { X } \ { X } ) ) ) -> X e. { ( 0g ` Y ) } )
42 elsni 
 |-  ( X e. { ( 0g ` Y ) } -> X = ( 0g ` Y ) )
43 41 42 syl 
 |-  ( ( ( W e. LVec /\ X e. V ) /\ X e. ( ( LSpan ` Y ) ` ( { X } \ { X } ) ) ) -> X = ( 0g ` Y ) )
44 lmodgrp 
 |-  ( W e. LMod -> W e. Grp )
45 grpmnd 
 |-  ( W e. Grp -> W e. Mnd )
46 6 44 45 3syl 
 |-  ( ( W e. LVec /\ X e. V ) -> W e. Mnd )
47 3 1 2 0ellsp 
 |-  ( ( W e. LMod /\ { X } C_ V ) -> .0. e. ( N ` { X } ) )
48 6 8 47 syl2anc 
 |-  ( ( W e. LVec /\ X e. V ) -> .0. e. ( N ` { X } ) )
49 4 1 3 ress0g 
 |-  ( ( W e. Mnd /\ .0. e. ( N ` { X } ) /\ ( N ` { X } ) C_ V ) -> .0. = ( 0g ` Y ) )
50 46 48 18 49 syl3anc 
 |-  ( ( W e. LVec /\ X e. V ) -> .0. = ( 0g ` Y ) )
51 50 adantr 
 |-  ( ( ( W e. LVec /\ X e. V ) /\ X e. ( ( LSpan ` Y ) ` ( { X } \ { X } ) ) ) -> .0. = ( 0g ` Y ) )
52 43 51 eqtr4d 
 |-  ( ( ( W e. LVec /\ X e. V ) /\ X e. ( ( LSpan ` Y ) ` ( { X } \ { X } ) ) ) -> X = .0. )
53 52 ex 
 |-  ( ( W e. LVec /\ X e. V ) -> ( X e. ( ( LSpan ` Y ) ` ( { X } \ { X } ) ) -> X = .0. ) )
54 53 necon3ad 
 |-  ( ( W e. LVec /\ X e. V ) -> ( X =/= .0. -> -. X e. ( ( LSpan ` Y ) ` ( { X } \ { X } ) ) ) )
55 54 3impia 
 |-  ( ( W e. LVec /\ X e. V /\ X =/= .0. ) -> -. X e. ( ( LSpan ` Y ) ` ( { X } \ { X } ) ) )
56 id 
 |-  ( x = X -> x = X )
57 sneq 
 |-  ( x = X -> { x } = { X } )
58 57 difeq2d 
 |-  ( x = X -> ( { X } \ { x } ) = ( { X } \ { X } ) )
59 58 fveq2d 
 |-  ( x = X -> ( ( LSpan ` Y ) ` ( { X } \ { x } ) ) = ( ( LSpan ` Y ) ` ( { X } \ { X } ) ) )
60 56 59 eleq12d 
 |-  ( x = X -> ( x e. ( ( LSpan ` Y ) ` ( { X } \ { x } ) ) <-> X e. ( ( LSpan ` Y ) ` ( { X } \ { X } ) ) ) )
61 60 notbid 
 |-  ( x = X -> ( -. x e. ( ( LSpan ` Y ) ` ( { X } \ { x } ) ) <-> -. X e. ( ( LSpan ` Y ) ` ( { X } \ { X } ) ) ) )
62 61 ralsng 
 |-  ( X e. V -> ( A. x e. { X } -. x e. ( ( LSpan ` Y ) ` ( { X } \ { x } ) ) <-> -. X e. ( ( LSpan ` Y ) ` ( { X } \ { X } ) ) ) )
63 62 3ad2ant2 
 |-  ( ( W e. LVec /\ X e. V /\ X =/= .0. ) -> ( A. x e. { X } -. x e. ( ( LSpan ` Y ) ` ( { X } \ { x } ) ) <-> -. X e. ( ( LSpan ` Y ) ` ( { X } \ { X } ) ) ) )
64 55 63 mpbird 
 |-  ( ( W e. LVec /\ X e. V /\ X =/= .0. ) -> A. x e. { X } -. x e. ( ( LSpan ` Y ) ` ( { X } \ { x } ) ) )
65 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
66 eqid 
 |-  ( LBasis ` Y ) = ( LBasis ` Y )
67 65 66 26 islbs2 
 |-  ( Y e. LVec -> ( { X } e. ( LBasis ` Y ) <-> ( { X } C_ ( Base ` Y ) /\ ( ( LSpan ` Y ) ` { X } ) = ( Base ` Y ) /\ A. x e. { X } -. x e. ( ( LSpan ` Y ) ` ( { X } \ { x } ) ) ) ) )
68 67 biimpar 
 |-  ( ( Y e. LVec /\ ( { X } C_ ( Base ` Y ) /\ ( ( LSpan ` Y ) ` { X } ) = ( Base ` Y ) /\ A. x e. { X } -. x e. ( ( LSpan ` Y ) ` ( { X } \ { x } ) ) ) ) -> { X } e. ( LBasis ` Y ) )
69 14 22 30 64 68 syl13anc 
 |-  ( ( W e. LVec /\ X e. V /\ X =/= .0. ) -> { X } e. ( LBasis ` Y ) )