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 ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( ( Base ‘ 𝑊 ) ∖ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) → ( 𝐹 ∪ { 𝑋 } ) ∈ ( LIndS ‘ 𝑊 ) )

Proof

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