Metamath Proof Explorer

Theorem lindssn

Description: Any singleton of a nonzero element is an independent set. (Contributed by Thierry Arnoux, 5-Aug-2023)

Ref Expression
Hypotheses lindssn.1 
|- B = ( Base ` W )
lindssn.2 
|- .0. = ( 0g ` W )
Assertion lindssn 
|- ( ( W e. LVec /\ X e. B /\ X =/= .0. ) -> { X } e. ( LIndS ` W ) )

Proof

Step Hyp Ref Expression
1 lindssn.1 
 |-  B = ( Base ` W )
2 lindssn.2 
 |-  .0. = ( 0g ` W )
3 simp1 
 |-  ( ( W e. LVec /\ X e. B /\ X =/= .0. ) -> W e. LVec )
4 snssi 
 |-  ( X e. B -> { X } C_ B )
5 4 3ad2ant2 
 |-  ( ( W e. LVec /\ X e. B /\ X =/= .0. ) -> { X } C_ B )
6 simpr 
 |-  ( ( ( W e. LVec /\ X e. B /\ X =/= .0. ) /\ y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) )
7 eldifsni 
 |-  ( y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -> y =/= ( 0g ` ( Scalar ` W ) ) )
8 6 7 syl 
 |-  ( ( ( W e. LVec /\ X e. B /\ X =/= .0. ) /\ y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> y =/= ( 0g ` ( Scalar ` W ) ) )
9 8 neneqd 
 |-  ( ( ( W e. LVec /\ X e. B /\ X =/= .0. ) /\ y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> -. y = ( 0g ` ( Scalar ` W ) ) )
10 simpl3 
 |-  ( ( ( W e. LVec /\ X e. B /\ X =/= .0. ) /\ y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> X =/= .0. )
11 10 neneqd 
 |-  ( ( ( W e. LVec /\ X e. B /\ X =/= .0. ) /\ y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> -. X = .0. )
12 ioran 
 |-  ( -. ( y = ( 0g ` ( Scalar ` W ) ) \/ X = .0. ) <-> ( -. y = ( 0g ` ( Scalar ` W ) ) /\ -. X = .0. ) )
13 9 11 12 sylanbrc 
 |-  ( ( ( W e. LVec /\ X e. B /\ X =/= .0. ) /\ y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> -. ( y = ( 0g ` ( Scalar ` W ) ) \/ X = .0. ) )
14 eqid 
 |-  ( .s ` W ) = ( .s ` W )
15 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
16 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
17 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
18 3 adantr 
 |-  ( ( ( W e. LVec /\ X e. B /\ X =/= .0. ) /\ y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> W e. LVec )
19 6 eldifad 
 |-  ( ( ( W e. LVec /\ X e. B /\ X =/= .0. ) /\ y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> y e. ( Base ` ( Scalar ` W ) ) )
20 simpl2 
 |-  ( ( ( W e. LVec /\ X e. B /\ X =/= .0. ) /\ y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> X e. B )
21 1 14 15 16 17 2 18 19 20 lvecvs0or 
 |-  ( ( ( W e. LVec /\ X e. B /\ X =/= .0. ) /\ y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> ( ( y ( .s ` W ) X ) = .0. <-> ( y = ( 0g ` ( Scalar ` W ) ) \/ X = .0. ) ) )
22 21 necon3abid 
 |-  ( ( ( W e. LVec /\ X e. B /\ X =/= .0. ) /\ y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> ( ( y ( .s ` W ) X ) =/= .0. <-> -. ( y = ( 0g ` ( Scalar ` W ) ) \/ X = .0. ) ) )
23 13 22 mpbird 
 |-  ( ( ( W e. LVec /\ X e. B /\ X =/= .0. ) /\ y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> ( y ( .s ` W ) X ) =/= .0. )
24 nelsn 
 |-  ( ( y ( .s ` W ) X ) =/= .0. -> -. ( y ( .s ` W ) X ) e. { .0. } )
25 23 24 syl 
 |-  ( ( ( W e. LVec /\ X e. B /\ X =/= .0. ) /\ y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> -. ( y ( .s ` W ) X ) e. { .0. } )
26 difid 
 |-  ( { X } \ { X } ) = (/)
27 26 a1i 
 |-  ( ( ( W e. LVec /\ X e. B /\ X =/= .0. ) /\ y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> ( { X } \ { X } ) = (/) )
28 27 fveq2d 
 |-  ( ( ( W e. LVec /\ X e. B /\ X =/= .0. ) /\ y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> ( ( LSpan ` W ) ` ( { X } \ { X } ) ) = ( ( LSpan ` W ) ` (/) ) )
29 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
30 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
31 2 30 lsp0 
 |-  ( W e. LMod -> ( ( LSpan ` W ) ` (/) ) = { .0. } )
32 3 29 31 3syl 
 |-  ( ( W e. LVec /\ X e. B /\ X =/= .0. ) -> ( ( LSpan ` W ) ` (/) ) = { .0. } )
33 32 adantr 
 |-  ( ( ( W e. LVec /\ X e. B /\ X =/= .0. ) /\ y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> ( ( LSpan ` W ) ` (/) ) = { .0. } )
34 28 33 eqtrd 
 |-  ( ( ( W e. LVec /\ X e. B /\ X =/= .0. ) /\ y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> ( ( LSpan ` W ) ` ( { X } \ { X } ) ) = { .0. } )
35 25 34 neleqtrrd 
 |-  ( ( ( W e. LVec /\ X e. B /\ X =/= .0. ) /\ y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> -. ( y ( .s ` W ) X ) e. ( ( LSpan ` W ) ` ( { X } \ { X } ) ) )
36 35 ralrimiva 
 |-  ( ( W e. LVec /\ X e. B /\ X =/= .0. ) -> A. y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( y ( .s ` W ) X ) e. ( ( LSpan ` W ) ` ( { X } \ { X } ) ) )
37 oveq2 
 |-  ( x = X -> ( y ( .s ` W ) x ) = ( y ( .s ` W ) X ) )
38 sneq 
 |-  ( x = X -> { x } = { X } )
39 38 difeq2d 
 |-  ( x = X -> ( { X } \ { x } ) = ( { X } \ { X } ) )
40 39 fveq2d 
 |-  ( x = X -> ( ( LSpan ` W ) ` ( { X } \ { x } ) ) = ( ( LSpan ` W ) ` ( { X } \ { X } ) ) )
41 37 40 eleq12d 
 |-  ( x = X -> ( ( y ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( { X } \ { x } ) ) <-> ( y ( .s ` W ) X ) e. ( ( LSpan ` W ) ` ( { X } \ { X } ) ) ) )
42 41 notbid 
 |-  ( x = X -> ( -. ( y ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( { X } \ { x } ) ) <-> -. ( y ( .s ` W ) X ) e. ( ( LSpan ` W ) ` ( { X } \ { X } ) ) ) )
43 42 ralbidv 
 |-  ( x = X -> ( A. y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( y ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( { X } \ { x } ) ) <-> A. y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( y ( .s ` W ) X ) e. ( ( LSpan ` W ) ` ( { X } \ { X } ) ) ) )
44 43 ralsng 
 |-  ( X e. B -> ( A. x e. { X } A. y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( y ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( { X } \ { x } ) ) <-> A. y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( y ( .s ` W ) X ) e. ( ( LSpan ` W ) ` ( { X } \ { X } ) ) ) )
45 44 3ad2ant2 
 |-  ( ( W e. LVec /\ X e. B /\ X =/= .0. ) -> ( A. x e. { X } A. y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( y ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( { X } \ { x } ) ) <-> A. y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( y ( .s ` W ) X ) e. ( ( LSpan ` W ) ` ( { X } \ { X } ) ) ) )
46 36 45 mpbird 
 |-  ( ( W e. LVec /\ X e. B /\ X =/= .0. ) -> A. x e. { X } A. y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( y ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( { X } \ { x } ) ) )
47 1 14 30 15 16 17 islinds2 
 |-  ( W e. LVec -> ( { X } e. ( LIndS ` W ) <-> ( { X } C_ B /\ A. x e. { X } A. y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( y ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( { X } \ { x } ) ) ) ) )
48 47 biimpar 
 |-  ( ( W e. LVec /\ ( { X } C_ B /\ A. x e. { X } A. y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( y ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( { X } \ { x } ) ) ) ) -> { X } e. ( LIndS ` W ) )
49 3 5 46 48 syl12anc 
 |-  ( ( W e. LVec /\ X e. B /\ X =/= .0. ) -> { X } e. ( LIndS ` W ) )