This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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