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 biimpi 
 |-  ( k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -> ( k e. ( Base ` ( Scalar ` W ) ) /\ k =/= ( 0g ` ( Scalar ` W ) ) ) )
73 72 adantl 
 |-  ( ( W e. LVec /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> ( k e. ( Base ` ( Scalar ` W ) ) /\ k =/= ( 0g ` ( Scalar ` W ) ) ) )
74 2 sselda 
 |-  ( ( F e. ( LIndS ` W ) /\ x e. F ) -> x e. ( Base ` W ) )
75 eqid 
 |-  ( .s ` W ) = ( .s ` W )
76 1 21 75 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 } ) )
77 70 73 74 76 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 } ) )
78 77 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 } ) )
79 78 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 } ) ) ) )
80 79 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 } ) ) ) )
81 eldifi 
 |-  ( k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -> k e. ( Base ` ( Scalar ` W ) ) )
82 19 3ad2ant1 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) -> W e. LMod )
83 82 adantr 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) /\ ( x e. F /\ k e. ( Base ` ( Scalar ` W ) ) ) ) -> W e. LMod )
84 snssi 
 |-  ( X e. ( Base ` W ) -> { X } C_ ( Base ` W ) )
85 2 84 6 syl2an 
 |-  ( ( F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) -> ( F u. { X } ) C_ ( Base ` W ) )
86 85 ssdifssd 
 |-  ( ( F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) -> ( ( F u. { X } ) \ { x } ) C_ ( Base ` W ) )
87 1 37 31 lspcl 
 |-  ( ( W e. LMod /\ ( ( F u. { X } ) \ { x } ) C_ ( Base ` W ) ) -> ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) e. ( LSubSp ` W ) )
88 19 86 87 syl2an 
 |-  ( ( W e. LVec /\ ( F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) ) -> ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) e. ( LSubSp ` W ) )
89 88 3impb 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) -> ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) e. ( LSubSp ` W ) )
90 89 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 ) )
91 19 anim1i 
 |-  ( ( W e. LVec /\ k e. ( Base ` ( Scalar ` W ) ) ) -> ( W e. LMod /\ k e. ( Base ` ( Scalar ` W ) ) ) )
92 1 21 75 25 lmodvscl 
 |-  ( ( W e. LMod /\ k e. ( Base ` ( Scalar ` W ) ) /\ x e. ( Base ` W ) ) -> ( k ( .s ` W ) x ) e. ( Base ` W ) )
93 92 3expa 
 |-  ( ( ( W e. LMod /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ x e. ( Base ` W ) ) -> ( k ( .s ` W ) x ) e. ( Base ` W ) )
94 91 74 93 syl2an 
 |-  ( ( ( W e. LVec /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ ( F e. ( LIndS ` W ) /\ x e. F ) ) -> ( k ( .s ` W ) x ) e. ( Base ` W ) )
95 94 an42s 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) ) /\ ( x e. F /\ k e. ( Base ` ( Scalar ` W ) ) ) ) -> ( k ( .s ` W ) x ) e. ( Base ` W ) )
96 95 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 ) )
97 1 37 31 83 90 96 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 } ) ) ) )
98 81 97 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 } ) ) ) )
99 82 adantr 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) /\ x e. F ) -> W e. LMod )
100 89 adantr 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) /\ x e. F ) -> ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) e. ( LSubSp ` W ) )
101 74 3ad2antl2 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) /\ x e. F ) -> x e. ( Base ` W ) )
102 1 37 31 99 100 101 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 } ) ) ) )
103 102 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 } ) ) ) )
104 80 98 103 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 } ) ) ) )
105 3 104 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 } ) ) ) )
106 69 105 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 } ) ) ) )
107 difsnid 
 |-  ( x e. F -> ( ( F \ { x } ) u. { x } ) = F )
108 107 fveq2d 
 |-  ( x e. F -> ( ( LSpan ` W ) ` ( ( F \ { x } ) u. { x } ) ) = ( ( LSpan ` W ) ` F ) )
109 108 eleq2d 
 |-  ( x e. F -> ( X e. ( ( LSpan ` W ) ` ( ( F \ { x } ) u. { x } ) ) <-> X e. ( ( LSpan ` W ) ` F ) ) )
110 109 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 ) ) )
111 40 106 110 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 ) ) )
112 11 111 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 } ) ) )
113 112 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 } ) ) )
114 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 ) )
115 difsn 
 |-  ( -. X e. F -> ( F \ { X } ) = F )
116 54 115 syl 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) -> ( F \ { X } ) = F )
117 116 fveq2d 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) -> ( ( LSpan ` W ) ` ( F \ { X } ) ) = ( ( LSpan ` W ) ` F ) )
118 117 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 ) ) )
119 118 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 ) ) )
120 1 21 75 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 } ) )
121 120 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 } ) )
122 121 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 } ) )
123 71 122 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 } ) )
124 123 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 ) ) )
125 124 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 ) ) )
126 82 adantr 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) -> W e. LMod )
127 1 37 31 lspcl 
 |-  ( ( W e. LMod /\ F C_ ( Base ` W ) ) -> ( ( LSpan ` W ) ` F ) e. ( LSubSp ` W ) )
128 19 2 127 syl2an 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) ) -> ( ( LSpan ` W ) ` F ) e. ( LSubSp ` W ) )
129 128 3adant3 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) -> ( ( LSpan ` W ) ` F ) e. ( LSubSp ` W ) )
130 129 adantr 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) -> ( ( LSpan ` W ) ` F ) e. ( LSubSp ` W ) )
131 1 21 75 25 lmodvscl 
 |-  ( ( W e. LMod /\ k e. ( Base ` ( Scalar ` W ) ) /\ X e. ( Base ` W ) ) -> ( k ( .s ` W ) X ) e. ( Base ` W ) )
132 131 3expa 
 |-  ( ( ( W e. LMod /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X e. ( Base ` W ) ) -> ( k ( .s ` W ) X ) e. ( Base ` W ) )
133 132 an32s 
 |-  ( ( ( W e. LMod /\ X e. ( Base ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) -> ( k ( .s ` W ) X ) e. ( Base ` W ) )
134 19 133 sylanl1 
 |-  ( ( ( W e. LVec /\ X e. ( Base ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) -> ( k ( .s ` W ) X ) e. ( Base ` W ) )
135 134 3adantl2 
 |-  ( ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) -> ( k ( .s ` W ) X ) e. ( Base ` W ) )
136 1 37 31 126 130 135 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 ) ) )
137 81 136 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 ) ) )
138 simp3 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) -> X e. ( Base ` W ) )
139 1 37 31 82 129 138 ellspsn5b 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( Base ` W ) ) -> ( X e. ( ( LSpan ` W ) ` F ) <-> ( ( LSpan ` W ) ` { X } ) C_ ( ( LSpan ` W ) ` F ) ) )
140 139 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 ) ) )
141 125 137 140 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 ) ) )
142 3 141 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 ) ) )
143 119 142 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 ) ) )
144 114 143 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 } ) ) )
145 144 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 } ) ) )
146 oveq2 
 |-  ( x = X -> ( k ( .s ` W ) x ) = ( k ( .s ` W ) X ) )
147 sneq 
 |-  ( x = X -> { x } = { X } )
148 147 difeq2d 
 |-  ( x = X -> ( ( F u. { X } ) \ { x } ) = ( ( F u. { X } ) \ { X } ) )
149 difun2 
 |-  ( ( F u. { X } ) \ { X } ) = ( F \ { X } )
150 148 149 eqtrdi 
 |-  ( x = X -> ( ( F u. { X } ) \ { x } ) = ( F \ { X } ) )
151 150 fveq2d 
 |-  ( x = X -> ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) = ( ( LSpan ` W ) ` ( F \ { X } ) ) )
152 146 151 eleq12d 
 |-  ( x = X -> ( ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) <-> ( k ( .s ` W ) X ) e. ( ( LSpan ` W ) ` ( F \ { X } ) ) ) )
153 152 notbid 
 |-  ( x = X -> ( -. ( k ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( ( F u. { X } ) \ { x } ) ) <-> -. ( k ( .s ` W ) X ) e. ( ( LSpan ` W ) ` ( F \ { X } ) ) ) )
154 153 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 } ) ) ) )
155 154 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 } ) ) ) )
156 155 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 } ) ) ) )
157 145 156 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 } ) ) )
158 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 } ) ) ) )
159 113 157 158 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 } ) ) )
160 1 75 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 } ) ) ) ) )
161 160 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 } ) ) ) ) )
162 8 159 161 mpbir2and 
 |-  ( ( W e. LVec /\ F e. ( LIndS ` W ) /\ X e. ( ( Base ` W ) \ ( ( LSpan ` W ) ` F ) ) ) -> ( F u. { X } ) e. ( LIndS ` W ) )