Metamath Proof Explorer

Theorem lindsadd

Description: In a vector space, the union of an independent set and a vector not in its span is an independent set. (Contributed by Brendan Leahy, 4-Mar-2023)

Ref Expression
Assertion lindsadd 
|- ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) -> ( F u. { X } ) e. ( LIndS ` W ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` W ) = ( Base ` W )
2 1 linds1 
 |-  ( F e. ( LIndS ` W ) -> F C_ ( Base ` W ) )
3 eldifi 
 |-  ( X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) -> X e. ( Base ` W ) )
4 3 snssd 
 |-  ( X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) -> { X } C_ ( Base ` W ) )
5 unss 
 |-  ( ( F C_ ( Base ` W ) /\ { X } C_ ( Base ` W ) ) <-> ( F u. { X } ) C_ ( Base ` W ) )
6 5 biimpi 
 |-  ( ( F C_ ( Base ` W ) /\ { X } C_ ( Base ` W ) ) -> ( F u. { X } ) C_ ( Base ` W ) )
7 2 4 6 syl2an 
 |-  ( ( F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) -> ( F u. { X } ) C_ ( Base ` W ) )
8 7 3adant1 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) -> ( F u. { X } ) C_ ( Base ` W ) )
9 eldifn 
 |-  ( X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) -> -. X e. ( ( LSpan ` W ) ` F ) )
10 9 3ad2ant3 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) -> -. X e. ( ( LSpan ` W ) ` F ) )
11 10 adantr 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) /\ ( x e. F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> -. X e. ( ( LSpan ` W ) ` F ) )
12 simpll1 
 |-  ( ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) /\ ( x e. F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) /\ x e. ( ( LSpan ` W ) ` ( ( F \ { x } ) u. { X } ) ) ) -> W e. LVec )
13 2 ssdifssd 
 |-  ( F e. ( LIndS ` W ) -> ( F \ { x } ) C_ ( Base ` W ) )
14 13 3ad2ant2 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) -> ( F \ { x } ) C_ ( Base ` W ) )
15 14 ad2antrr 
 |-  ( ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) /\ ( x e. F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) /\ x e. ( ( LSpan ` W ) ` ( ( F \ { x } ) u. { X } ) ) ) -> ( F \ { x } ) C_ ( Base ` W ) )
16 3 3ad2ant3 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) -> X e. ( Base ` W ) )
17 16 ad2antrr 
 |-  ( ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) /\ ( x e. F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) /\ x e. ( ( LSpan ` W ) ` ( ( F \ { x } ) u. { X } ) ) ) -> X e. ( Base ` W ) )
18 simpr 
 |-  ( ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) /\ ( x e. F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) /\ x e. ( ( LSpan ` W ) ` ( ( F \ { x } ) u. { X } ) ) ) -> x e. ( ( LSpan ` W ) ` ( ( F \ { x } ) u. { X } ) ) )
19 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
20 19 ad2antrr 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) ) /\ ( x e. F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> W e. LMod )
21 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
22 21 lmodring 
 |-  ( W e. LMod -> ( Scalar ` W ) e. Ring )
23 19 22 syl 
 |-  ( W e. LVec -> ( Scalar ` W ) e. Ring )
24 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
25 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
26 24 25 ringelnzr 
 |-  ( ( ( Scalar ` W ) e. Ring /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> ( Scalar ` W ) e. NzRing )
27 23 26 sylan 
 |-  ( ( W e. LVec /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> ( Scalar ` W ) e. NzRing )
28 27 ad2ant2rl 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) ) /\ ( x e. F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> ( Scalar ` W ) e. NzRing )
29 simplr 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) ) /\ ( x e. F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> F e. ( LIndS ` W ) )
30 simprl 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) ) /\ ( x e. F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> x e. F )
31 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
32 31 21 lindsind2 
 |-  ( ( ( W e. LMod /\ ( Scalar ` W ) e. NzRing ) /\ F e. ( LIndS ` W ) /\ x e. F ) -> -. x e. ( ( LSpan ` W ) ` ( F \ { x } ) ) )
33 20 28 29 30 32 syl211anc 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) ) /\ ( x e. F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> -. x e. ( ( LSpan ` W ) ` ( F \ { x } ) ) )
34 33 3adantl3 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) /\ ( x e. F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> -. x e. ( ( LSpan ` W ) ` ( F \ { x } ) ) )
35 34 adantr 
 |-  ( ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) /\ ( x e. F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) /\ x e. ( ( LSpan ` W ) ` ( ( F \ { x } ) u. { X } ) ) ) -> -. x e. ( ( LSpan ` W ) ` ( F \ { x } ) ) )
36 18 35 eldifd 
 |-  ( ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) /\ ( x e. F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) /\ x e. ( ( LSpan ` W ) ` ( ( F \ { x } ) u. { X } ) ) ) -> x e. ( ( ( LSpan ` W ) ` ( ( F \ { x } ) u. { X } ) ) \ ( ( LSpan ` W ) ` ( F \ { x } ) ) ) )
37 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
38 1 37 31 lspsolv 
 |-  ( ( W e. LVec /\ ( ( F \ { x } ) C_ ( Base ` W ) /\ X e. ( Base ` W ) /\ x e. ( ( ( LSpan ` W ) ` ( ( F \ { x } ) u. { X } ) ) \ ( ( LSpan ` W ) ` ( F \ { x } ) ) ) ) ) -> X e. ( ( LSpan ` W ) ` ( ( F \ { x } ) u. { x } ) ) )
39 12 15 17 36 38 syl13anc 
 |-  ( ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) /\ ( x e. F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) /\ x e. ( ( LSpan ` W ) ` ( ( F \ { x } ) u. { X } ) ) ) -> X e. ( ( LSpan ` W ) ` ( ( F \ { x } ) u. { x } ) ) )
40 39 ex 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) /\ ( x e. F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> ( x e. ( ( LSpan ` W ) ` ( ( F \ { x } ) u. { X } ) ) -> X e. ( ( LSpan ` W ) ` ( ( F \ { x } ) u. { x } ) ) ) )
41 eldif 
 |-  ( X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) <-> ( X e. ( Base ` W ) /\ -. X e. ( ( LSpan ` W ) ` F ) ) )
42 snssi 
 |-  ( X e. F -> { X } C_ F )
43 1 31 lspss 
 |-  ( ( W e. LMod /\ F C_ ( Base ` W ) /\ { X } C_ F ) -> ( ( LSpan ` W ) ` { X } ) C_ ( ( LSpan ` W ) ` F ) )
44 19 2 42 43 syl3an 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. F ) -> ( ( LSpan ` W ) ` { X } ) C_ ( ( LSpan ` W ) ` F ) )
45 44 ad4ant124 
 |-  ( ( ( ( W e. LVec /\ F e. ( LIndS ` W ) ) /\ X e. ( Base ` W ) ) /\ X e. F ) -> ( ( LSpan ` W ) ` { X } ) C_ ( ( LSpan ` W ) ` F ) )
46 1 31 lspsnid 
 |-  ( ( W e. LMod /\ X e. ( Base ` W ) ) -> X e. ( ( LSpan ` W ) ` { X } ) )
47 19 46 sylan 
 |-  ( ( W e. LVec /\ X e. ( Base ` W ) ) -> X e. ( ( LSpan ` W ) ` { X } ) )
48 47 ad4ant13 
 |-  ( ( ( ( W e. LVec /\ F e. ( LIndS ` W ) ) /\ X e. ( Base ` W ) ) /\ X e. F ) -> X e. ( ( LSpan ` W ) ` { X } ) )
49 45 48 sseldd 
 |-  ( ( ( ( W e. LVec /\ F e. ( LIndS ` W ) ) /\ X e. ( Base ` W ) ) /\ X e. F ) -> X e. ( ( LSpan ` W ) ` F ) )
50 49 ex 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) ) /\ X e. ( Base ` W ) ) -> ( X e. F -> X e. ( ( LSpan ` W ) ` F ) ) )
51 50 con3d 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) ) /\ X e. ( Base ` W ) ) -> ( -. X e. ( ( LSpan ` W ) ` F ) -> -. X e. F ) )
52 51 expimpd 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) ) -> ( ( X e. ( Base ` W ) /\ -. X e. ( ( LSpan ` W ) ` F ) ) -> -. X e. F ) )
53 52 3impia 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ ( X e. ( Base ` W ) /\ -. X e. ( ( LSpan ` W ) ` F ) ) ) -> -. X e. F )
54 41 53 syl3an3b 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) -> -. X e. F )
55 eleq1 
 |-  ( X = x -> ( X e. F <-> x e. F ) )
56 55 notbid 
 |-  ( X = x -> ( -. X e. F <-> -. x e. F ) )
57 54 56 syl5ibcom 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) -> ( X = x -> -. x e. F ) )
58 57 necon2ad 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) -> ( x e. F -> X =/= x ) )
59 58 imp 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) /\ x e. F ) -> X =/= x )
60 disjsn2 
 |-  ( X =/= x -> ( { X } i^i { x } ) = (/) )
61 59 60 syl 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) /\ x e. F ) -> ( { X } i^i { x } ) = (/) )
62 disj3 
 |-  ( ( { X } i^i { x } ) = (/) <-> { X } = ( { X } \ { x } ) )
63 61 62 sylib 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) /\ x e. F ) -> { X } = ( { X } \ { x } ) )
64 63 uneq2d 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) /\ x e. F ) -> ( ( F \ { x } ) u. { X } ) = ( ( F \ { x } ) u. ( { X } \ { x } ) ) )
65 difundir 
 |-  ( ( F u. { X } ) \ { x } ) = ( ( F \ { x } ) u. ( { X } \ { x } ) )
66 64 65 eqtr4di 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) /\ x e. F ) -> ( ( F \ { x } ) u. { X } ) = ( ( F u. { X } ) \ { x } ) )
67 66 fveq2d 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) /\ x e. F ) -> ( ( LSpan ` W ) ` ( ( F \ { x } ) u. { X } ) ) = ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) )
68 67 eleq2d 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) /\ x e. F ) -> ( x e. ( ( LSpan ` W ) ` ( ( F \ { x } ) u. { X } ) ) <-> x e. ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) ) )
69 68 adantrr 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) /\ ( x e. F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> ( x e. ( ( LSpan ` W ) ` ( ( F \ { x } ) u. { X } ) ) <-> x e. ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) ) )
70 simpl 
 |-  ( ( W e. LVec /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> W e. LVec )
71 eldifsn 
 |-  ( k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) <-> ( k e. ( Base ` ( Scalar ` W ) ) /\ k =/= ( 0g ` ( Scalar ` W ) ) ) )
72 71 bilani 
 |-  ( ( W e. LVec /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> ( k e. ( Base ` ( Scalar ` W ) ) /\ k =/= ( 0g ` ( Scalar ` W ) ) ) )
73 2 sselda 
 |-  ( ( F e. ( LIndS ` W ) /\ x e. F ) -> x e. ( Base ` W ) )
74 eqid 
 |-  ( .s ` W ) = ( .s ` W )
75 1 21 74 25 24 31 lspsnvs 
 |-  ( ( W e. LVec /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ k =/= ( 0g ` ( Scalar ` W ) ) ) /\ x e. ( Base ` W ) ) -> ( ( LSpan ` W ) ` { ( k ( .s ` W ) x ) } ) = ( ( LSpan ` W ) ` { x } ) )
76 70 72 73 75 syl2an3an 
 |-  ( ( ( W e. LVec /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) /\ ( F e. ( LIndS ` W ) /\ x e. F ) ) -> ( ( LSpan ` W ) ` { ( k ( .s ` W ) x ) } ) = ( ( LSpan ` W ) ` { x } ) )
77 76 an42s 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) ) /\ ( x e. F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> ( ( LSpan ` W ) ` { ( k ( .s ` W ) x ) } ) = ( ( LSpan ` W ) ` { x } ) )
78 77 sseq1d 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) ) /\ ( x e. F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> ( ( ( LSpan ` W ) ` { ( k ( .s ` W ) x ) } ) C_ ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) <-> ( ( LSpan ` W ) ` { x } ) C_ ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) ) )
79 78 3adantl3 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) /\ ( x e. F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> ( ( ( LSpan ` W ) ` { ( k ( .s ` W ) x ) } ) C_ ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) <-> ( ( LSpan ` W ) ` { x } ) C_ ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) ) )
80 eldifi 
 |-  ( k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -> k e. ( Base ` ( Scalar ` W ) ) )
81 19 3ad2ant1 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) -> W e. LMod )
82 81 adantr 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) /\ ( x e. F /\ k e. ( Base ` ( Scalar ` W ) ) ) ) -> W e. LMod )
83 snssi 
 |-  ( X e. ( Base ` W ) -> { X } C_ ( Base ` W ) )
84 2 83 6 syl2an 
 |-  ( ( F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) -> ( F u. { X } ) C_ ( Base ` W ) )
85 84 ssdifssd 
 |-  ( ( F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) -> ( ( F u. { X } ) \ { x } ) C_ ( Base ` W ) )
86 1 37 31 lspcl 
 |-  ( ( W e. LMod /\ ( ( F u. { X } ) \ { x } ) C_ ( Base ` W ) ) -> ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) e. ( LSubSp ` W ) )
87 19 85 86 syl2an 
 |-  ( ( W e. LVec /\ ( F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) ) -> ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) e. ( LSubSp ` W ) )
88 87 3impb 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) -> ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) e. ( LSubSp ` W ) )
89 88 adantr 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) /\ ( x e. F /\ k e. ( Base ` ( Scalar ` W ) ) ) ) -> ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) e. ( LSubSp ` W ) )
90 19 anim1i 
 |-  ( ( W e. LVec /\ k e. ( Base ` ( Scalar ` W ) ) ) -> ( W e. LMod /\ k e. ( Base ` ( Scalar ` W ) ) ) )
91 1 21 74 25 lmodvscl 
 |-  ( ( W e. LMod /\ k e. ( Base ` ( Scalar ` W ) ) /\ x e. ( Base ` W ) ) -> ( k ( .s ` W ) x ) e. ( Base ` W ) )
92 91 3expa 
 |-  ( ( ( W e. LMod /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ x e. ( Base ` W ) ) -> ( k ( .s ` W ) x ) e. ( Base ` W ) )
93 90 73 92 syl2an 
 |-  ( ( ( W e. LVec /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ ( F e. ( LIndS ` W ) /\ x e. F ) ) -> ( k ( .s ` W ) x ) e. ( Base ` W ) )
94 93 an42s 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) ) /\ ( x e. F /\ k e. ( Base ` ( Scalar ` W ) ) ) ) -> ( k ( .s ` W ) x ) e. ( Base ` W ) )
95 94 3adantl3 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) /\ ( x e. F /\ k e. ( Base ` ( Scalar ` W ) ) ) ) -> ( k ( .s ` W ) x ) e. ( Base ` W ) )
96 1 37 31 82 89 95 ellspsn5b 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) /\ ( x e. F /\ k e. ( Base ` ( Scalar ` W ) ) ) ) -> ( ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) <-> ( ( LSpan ` W ) ` { ( k ( .s ` W ) x ) } ) C_ ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) ) )
97 80 96 sylanr2 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) /\ ( x e. F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> ( ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) <-> ( ( LSpan ` W ) ` { ( k ( .s ` W ) x ) } ) C_ ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) ) )
98 81 adantr 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) /\ x e. F ) -> W e. LMod )
99 88 adantr 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) /\ x e. F ) -> ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) e. ( LSubSp ` W ) )
100 73 3ad2antl2 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) /\ x e. F ) -> x e. ( Base ` W ) )
101 1 37 31 98 99 100 ellspsn5b 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) /\ x e. F ) -> ( x e. ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) <-> ( ( LSpan ` W ) ` { x } ) C_ ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) ) )
102 101 adantrr 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) /\ ( x e. F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> ( x e. ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) <-> ( ( LSpan ` W ) ` { x } ) C_ ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) ) )
103 79 97 102 3bitr4rd 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) /\ ( x e. F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> ( x e. ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) <-> ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) ) )
104 3 103 syl3anl3 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) /\ ( x e. F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> ( x e. ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) <-> ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) ) )
105 69 104 bitrd 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) /\ ( x e. F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> ( x e. ( ( LSpan ` W ) ` ( ( F \ { x } ) u. { X } ) ) <-> ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) ) )
106 difsnid 
 |-  ( x e. F -> ( ( F \ { x } ) u. { x } ) = F )
107 106 fveq2d 
 |-  ( x e. F -> ( ( LSpan ` W ) ` ( ( F \ { x } ) u. { x } ) ) = ( ( LSpan ` W ) ` F ) )
108 107 eleq2d 
 |-  ( x e. F -> ( X e. ( ( LSpan ` W ) ` ( ( F \ { x } ) u. { x } ) ) <-> X e. ( ( LSpan ` W ) ` F ) ) )
109 108 ad2antrl 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) /\ ( x e. F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> ( X e. ( ( LSpan ` W ) ` ( ( F \ { x } ) u. { x } ) ) <-> X e. ( ( LSpan ` W ) ` F ) ) )
110 40 105 109 3imtr3d 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) /\ ( x e. F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> ( ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) -> X e. ( ( LSpan ` W ) ` F ) ) )
111 11 110 mtod 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) /\ ( x e. F /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> -. ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) )
112 111 ralrimivva 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) -> A. x e. F A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) )
113 10 adantr 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> -. X e. ( ( LSpan ` W ) ` F ) )
114 difsn 
 |-  ( -. X e. F -> ( F \ { X } ) = F )
115 54 114 syl 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) -> ( F \ { X } ) = F )
116 115 fveq2d 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) -> ( ( LSpan ` W ) ` ( F \ { X } ) ) = ( ( LSpan ` W ) ` F ) )
117 116 eleq2d 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) -> ( ( k ( .s ` W ) X ) e. ( ( LSpan ` W ) ` ( F \ { X } ) ) <-> ( k ( .s ` W ) X ) e. ( ( LSpan ` W ) ` F ) ) )
118 117 adantr 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> ( ( k ( .s ` W ) X ) e. ( ( LSpan ` W ) ` ( F \ { X } ) ) <-> ( k ( .s ` W ) X ) e. ( ( LSpan ` W ) ` F ) ) )
119 1 21 74 25 24 31 lspsnvs 
 |-  ( ( W e. LVec /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ k =/= ( 0g ` ( Scalar ` W ) ) ) /\ X e. ( Base ` W ) ) -> ( ( LSpan ` W ) ` { ( k ( .s ` W ) X ) } ) = ( ( LSpan ` W ) ` { X } ) )
120 119 3expa 
 |-  ( ( ( W e. LVec /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ k =/= ( 0g ` ( Scalar ` W ) ) ) ) /\ X e. ( Base ` W ) ) -> ( ( LSpan ` W ) ` { ( k ( .s ` W ) X ) } ) = ( ( LSpan ` W ) ` { X } ) )
121 120 an32s 
 |-  ( ( ( W e. LVec /\ X e. ( Base ` W ) ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ k =/= ( 0g ` ( Scalar ` W ) ) ) ) -> ( ( LSpan ` W ) ` { ( k ( .s ` W ) X ) } ) = ( ( LSpan ` W ) ` { X } ) )
122 71 121 sylan2b 
 |-  ( ( ( W e. LVec /\ X e. ( Base ` W ) ) /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> ( ( LSpan ` W ) ` { ( k ( .s ` W ) X ) } ) = ( ( LSpan ` W ) ` { X } ) )
123 122 sseq1d 
 |-  ( ( ( W e. LVec /\ X e. ( Base ` W ) ) /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> ( ( ( LSpan ` W ) ` { ( k ( .s ` W ) X ) } ) C_ ( ( LSpan ` W ) ` F ) <-> ( ( LSpan ` W ) ` { X } ) C_ ( ( LSpan ` W ) ` F ) ) )
124 123 3adantl2 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> ( ( ( LSpan ` W ) ` { ( k ( .s ` W ) X ) } ) C_ ( ( LSpan ` W ) ` F ) <-> ( ( LSpan ` W ) ` { X } ) C_ ( ( LSpan ` W ) ` F ) ) )
125 81 adantr 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) -> W e. LMod )
126 1 37 31 lspcl 
 |-  ( ( W e. LMod /\ F C_ ( Base ` W ) ) -> ( ( LSpan ` W ) ` F ) e. ( LSubSp ` W ) )
127 19 2 126 syl2an 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) ) -> ( ( LSpan ` W ) ` F ) e. ( LSubSp ` W ) )
128 127 3adant3 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) -> ( ( LSpan ` W ) ` F ) e. ( LSubSp ` W ) )
129 128 adantr 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) -> ( ( LSpan ` W ) ` F ) e. ( LSubSp ` W ) )
130 1 21 74 25 lmodvscl 
 |-  ( ( W e. LMod /\ k e. ( Base ` ( Scalar ` W ) ) /\ X e. ( Base ` W ) ) -> ( k ( .s ` W ) X ) e. ( Base ` W ) )
131 130 3expa 
 |-  ( ( ( W e. LMod /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X e. ( Base ` W ) ) -> ( k ( .s ` W ) X ) e. ( Base ` W ) )
132 131 an32s 
 |-  ( ( ( W e. LMod /\ X e. ( Base ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) -> ( k ( .s ` W ) X ) e. ( Base ` W ) )
133 19 132 sylanl1 
 |-  ( ( ( W e. LVec /\ X e. ( Base ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) -> ( k ( .s ` W ) X ) e. ( Base ` W ) )
134 133 3adantl2 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) -> ( k ( .s ` W ) X ) e. ( Base ` W ) )
135 1 37 31 125 129 134 ellspsn5b 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) -> ( ( k ( .s ` W ) X ) e. ( ( LSpan ` W ) ` F ) <-> ( ( LSpan ` W ) ` { ( k ( .s ` W ) X ) } ) C_ ( ( LSpan ` W ) ` F ) ) )
136 80 135 sylan2 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> ( ( k ( .s ` W ) X ) e. ( ( LSpan ` W ) ` F ) <-> ( ( LSpan ` W ) ` { ( k ( .s ` W ) X ) } ) C_ ( ( LSpan ` W ) ` F ) ) )
137 simp3 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) -> X e. ( Base ` W ) )
138 1 37 31 81 128 137 ellspsn5b 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) -> ( X e. ( ( LSpan ` W ) ` F ) <-> ( ( LSpan ` W ) ` { X } ) C_ ( ( LSpan ` W ) ` F ) ) )
139 138 adantr 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> ( X e. ( ( LSpan ` W ) ` F ) <-> ( ( LSpan ` W ) ` { X } ) C_ ( ( LSpan ` W ) ` F ) ) )
140 124 136 139 3bitr4d 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> ( ( k ( .s ` W ) X ) e. ( ( LSpan ` W ) ` F ) <-> X e. ( ( LSpan ` W ) ` F ) ) )
141 3 140 syl3anl3 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> ( ( k ( .s ` W ) X ) e. ( ( LSpan ` W ) ` F ) <-> X e. ( ( LSpan ` W ) ` F ) ) )
142 118 141 bitrd 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> ( ( k ( .s ` W ) X ) e. ( ( LSpan ` W ) ` ( F \ { X } ) ) <-> X e. ( ( LSpan ` W ) ` F ) ) )
143 113 142 mtbird 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> -. ( k ( .s ` W ) X ) e. ( ( LSpan ` W ) ` ( F \ { X } ) ) )
144 143 ralrimiva 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) -> A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) X ) e. ( ( LSpan ` W ) ` ( F \ { X } ) ) )
145 oveq2 
 |-  ( x = X -> ( k ( .s ` W ) x ) = ( k ( .s ` W ) X ) )
146 sneq 
 |-  ( x = X -> { x } = { X } )
147 146 difeq2d 
 |-  ( x = X -> ( ( F u. { X } ) \ { x } ) = ( ( F u. { X } ) \ { X } ) )
148 difun2 
 |-  ( ( F u. { X } ) \ { X } ) = ( F \ { X } )
149 147 148 eqtrdi 
 |-  ( x = X -> ( ( F u. { X } ) \ { x } ) = ( F \ { X } ) )
150 149 fveq2d 
 |-  ( x = X -> ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) = ( ( LSpan ` W ) ` ( F \ { X } ) ) )
151 145 150 eleq12d 
 |-  ( x = X -> ( ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) <-> ( k ( .s ` W ) X ) e. ( ( LSpan ` W ) ` ( F \ { X } ) ) ) )
152 151 notbid 
 |-  ( x = X -> ( -. ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) <-> -. ( k ( .s ` W ) X ) e. ( ( LSpan ` W ) ` ( F \ { X } ) ) ) )
153 152 ralbidv 
 |-  ( x = X -> ( A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) <-> A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) X ) e. ( ( LSpan ` W ) ` ( F \ { X } ) ) ) )
154 153 ralsng 
 |-  ( X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) -> ( A. x e. { X } A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) <-> A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) X ) e. ( ( LSpan ` W ) ` ( F \ { X } ) ) ) )
155 154 3ad2ant3 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) -> ( A. x e. { X } A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) <-> A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) X ) e. ( ( LSpan ` W ) ` ( F \ { X } ) ) ) )
156 144 155 mpbird 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) -> A. x e. { X } A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) )
157 ralunb 
 |-  ( A. x e. ( F u. { X } ) A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) <-> ( A. x e. F A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) /\ A. x e. { X } A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) ) )
158 112 156 157 sylanbrc 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) -> A. x e. ( F u. { X } ) A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) )
159 1 74 31 21 25 24 islinds2 
 |-  ( W e. LVec -> ( ( F u. { X } ) e. ( LIndS ` W ) <-> ( ( F u. { X } ) C_ ( Base ` W ) /\ A. x e. ( F u. { X } ) A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) ) ) )
160 159 3ad2ant1 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) -> ( ( F u. { X } ) e. ( LIndS ` W ) <-> ( ( F u. { X } ) C_ ( Base ` W ) /\ A. x e. ( F u. { X } ) A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) ) ) )
161 8 158 160 mpbir2and 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) -> ( F u. { X } ) e. ( LIndS ` W ) )