| 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
|
bilani |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) |
| 73 |
2
|
sselda |
⊢ ( ( 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑥 ∈ 𝐹 ) → 𝑥 ∈ ( Base ‘ 𝑊 ) ) |
| 74 |
|
eqid |
⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 ) |
| 75 |
1 21 74 25 24 31
|
lspsnvs |
⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) } ) = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) |
| 76 |
70 72 73 75
|
syl2an3an |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ∧ ( 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑥 ∈ 𝐹 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) } ) = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) |
| 77 |
76
|
an42s |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) } ) = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ) |
| 78 |
77
|
sseq1d |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ( ( ( LSpan ‘ 𝑊 ) ‘ { ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ↔ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ) ) |
| 79 |
78
|
3adantl3 |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ( ( ( LSpan ‘ 𝑊 ) ‘ { ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ↔ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ) ) |
| 80 |
|
eldifi |
⊢ ( 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) → 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) |
| 81 |
19
|
3ad2ant1 |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) → 𝑊 ∈ LMod ) |
| 82 |
81
|
adantr |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ) → 𝑊 ∈ LMod ) |
| 83 |
|
snssi |
⊢ ( 𝑋 ∈ ( Base ‘ 𝑊 ) → { 𝑋 } ⊆ ( Base ‘ 𝑊 ) ) |
| 84 |
2 83 6
|
syl2an |
⊢ ( ( 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) → ( 𝐹 ∪ { 𝑋 } ) ⊆ ( Base ‘ 𝑊 ) ) |
| 85 |
84
|
ssdifssd |
⊢ ( ( 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) → ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ⊆ ( Base ‘ 𝑊 ) ) |
| 86 |
1 37 31
|
lspcl |
⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ⊆ ( Base ‘ 𝑊 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ∈ ( LSubSp ‘ 𝑊 ) ) |
| 87 |
19 85 86
|
syl2an |
⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ∈ ( LSubSp ‘ 𝑊 ) ) |
| 88 |
87
|
3impb |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ∈ ( LSubSp ‘ 𝑊 ) ) |
| 89 |
88
|
adantr |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ) → ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ∈ ( LSubSp ‘ 𝑊 ) ) |
| 90 |
19
|
anim1i |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑊 ∈ LMod ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ) |
| 91 |
1 21 74 25
|
lmodvscl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( Base ‘ 𝑊 ) ) |
| 92 |
91
|
3expa |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( Base ‘ 𝑊 ) ) |
| 93 |
90 73 92
|
syl2an |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑥 ∈ 𝐹 ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( Base ‘ 𝑊 ) ) |
| 94 |
93
|
an42s |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( Base ‘ 𝑊 ) ) |
| 95 |
94
|
3adantl3 |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( Base ‘ 𝑊 ) ) |
| 96 |
1 37 31 82 89 95
|
ellspsn5b |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ↔ ( ( LSpan ‘ 𝑊 ) ‘ { ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ) ) |
| 97 |
80 96
|
sylanr2 |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ↔ ( ( LSpan ‘ 𝑊 ) ‘ { ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ) ) |
| 98 |
81
|
adantr |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑥 ∈ 𝐹 ) → 𝑊 ∈ LMod ) |
| 99 |
88
|
adantr |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑥 ∈ 𝐹 ) → ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ∈ ( LSubSp ‘ 𝑊 ) ) |
| 100 |
73
|
3ad2antl2 |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑥 ∈ 𝐹 ) → 𝑥 ∈ ( Base ‘ 𝑊 ) ) |
| 101 |
1 37 31 98 99 100
|
ellspsn5b |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑥 ∈ 𝐹 ) → ( 𝑥 ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ↔ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ) ) |
| 102 |
101
|
adantrr |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ( 𝑥 ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ↔ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ) ) |
| 103 |
79 97 102
|
3bitr4rd |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ( 𝑥 ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ↔ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ) ) |
| 104 |
3 103
|
syl3anl3 |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( ( Base ‘ 𝑊 ) ∖ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ( 𝑥 ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ↔ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ) ) |
| 105 |
69 104
|
bitrd |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( ( Base ‘ 𝑊 ) ∖ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ( 𝑥 ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∖ { 𝑥 } ) ∪ { 𝑋 } ) ) ↔ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ) ) |
| 106 |
|
difsnid |
⊢ ( 𝑥 ∈ 𝐹 → ( ( 𝐹 ∖ { 𝑥 } ) ∪ { 𝑥 } ) = 𝐹 ) |
| 107 |
106
|
fveq2d |
⊢ ( 𝑥 ∈ 𝐹 → ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ) = ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) |
| 108 |
107
|
eleq2d |
⊢ ( 𝑥 ∈ 𝐹 → ( 𝑋 ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ) ↔ 𝑋 ∈ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) |
| 109 |
108
|
ad2antrl |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( ( Base ‘ 𝑊 ) ∖ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ( 𝑋 ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ) ↔ 𝑋 ∈ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) |
| 110 |
40 105 109
|
3imtr3d |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( ( Base ‘ 𝑊 ) ∖ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) → 𝑋 ∈ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) |
| 111 |
11 110
|
mtod |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( ( Base ‘ 𝑊 ) ∖ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ) |
| 112 |
111
|
ralrimivva |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( ( Base ‘ 𝑊 ) ∖ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) → ∀ 𝑥 ∈ 𝐹 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ) |
| 113 |
10
|
adantr |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( ( Base ‘ 𝑊 ) ∖ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ¬ 𝑋 ∈ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) |
| 114 |
|
difsn |
⊢ ( ¬ 𝑋 ∈ 𝐹 → ( 𝐹 ∖ { 𝑋 } ) = 𝐹 ) |
| 115 |
54 114
|
syl |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( ( Base ‘ 𝑊 ) ∖ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) → ( 𝐹 ∖ { 𝑋 } ) = 𝐹 ) |
| 116 |
115
|
fveq2d |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( ( Base ‘ 𝑊 ) ∖ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) → ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 𝑋 } ) ) = ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) |
| 117 |
116
|
eleq2d |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( ( Base ‘ 𝑊 ) ∖ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 𝑋 } ) ) ↔ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) |
| 118 |
117
|
adantr |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( ( Base ‘ 𝑊 ) ∖ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 𝑋 } ) ) ↔ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) |
| 119 |
1 21 74 25 24 31
|
lspsnvs |
⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) } ) = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑋 } ) ) |
| 120 |
119
|
3expa |
⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) } ) = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑋 } ) ) |
| 121 |
120
|
an32s |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) } ) = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑋 } ) ) |
| 122 |
71 121
|
sylan2b |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) } ) = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑋 } ) ) |
| 123 |
122
|
sseq1d |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( ( ( LSpan ‘ 𝑊 ) ‘ { ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ↔ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑋 } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) |
| 124 |
123
|
3adantl2 |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( ( ( LSpan ‘ 𝑊 ) ‘ { ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ↔ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑋 } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) |
| 125 |
81
|
adantr |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑊 ∈ LMod ) |
| 126 |
1 37 31
|
lspcl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 ⊆ ( Base ‘ 𝑊 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ∈ ( LSubSp ‘ 𝑊 ) ) |
| 127 |
19 2 126
|
syl2an |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ∈ ( LSubSp ‘ 𝑊 ) ) |
| 128 |
127
|
3adant3 |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ∈ ( LSubSp ‘ 𝑊 ) ) |
| 129 |
128
|
adantr |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ∈ ( LSubSp ‘ 𝑊 ) ) |
| 130 |
1 21 74 25
|
lmodvscl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ ( Base ‘ 𝑊 ) ) |
| 131 |
130
|
3expa |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ ( Base ‘ 𝑊 ) ) |
| 132 |
131
|
an32s |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ ( Base ‘ 𝑊 ) ) |
| 133 |
19 132
|
sylanl1 |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ ( Base ‘ 𝑊 ) ) |
| 134 |
133
|
3adantl2 |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ ( Base ‘ 𝑊 ) ) |
| 135 |
1 37 31 125 129 134
|
ellspsn5b |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ↔ ( ( LSpan ‘ 𝑊 ) ‘ { ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) |
| 136 |
80 135
|
sylan2 |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ↔ ( ( LSpan ‘ 𝑊 ) ‘ { ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) |
| 137 |
|
simp3 |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) → 𝑋 ∈ ( Base ‘ 𝑊 ) ) |
| 138 |
1 37 31 81 128 137
|
ellspsn5b |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑋 ∈ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ↔ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑋 } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) |
| 139 |
138
|
adantr |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( 𝑋 ∈ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ↔ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑋 } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) |
| 140 |
124 136 139
|
3bitr4d |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ↔ 𝑋 ∈ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) |
| 141 |
3 140
|
syl3anl3 |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( ( Base ‘ 𝑊 ) ∖ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ↔ 𝑋 ∈ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) |
| 142 |
118 141
|
bitrd |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( ( Base ‘ 𝑊 ) ∖ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 𝑋 } ) ) ↔ 𝑋 ∈ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) |
| 143 |
113 142
|
mtbird |
⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( ( Base ‘ 𝑊 ) ∖ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 𝑋 } ) ) ) |
| 144 |
143
|
ralrimiva |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( ( Base ‘ 𝑊 ) ∖ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) → ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 𝑋 } ) ) ) |
| 145 |
|
oveq2 |
⊢ ( 𝑥 = 𝑋 → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) |
| 146 |
|
sneq |
⊢ ( 𝑥 = 𝑋 → { 𝑥 } = { 𝑋 } ) |
| 147 |
146
|
difeq2d |
⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) = ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑋 } ) ) |
| 148 |
|
difun2 |
⊢ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑋 } ) = ( 𝐹 ∖ { 𝑋 } ) |
| 149 |
147 148
|
eqtrdi |
⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) = ( 𝐹 ∖ { 𝑋 } ) ) |
| 150 |
149
|
fveq2d |
⊢ ( 𝑥 = 𝑋 → ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) = ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 𝑋 } ) ) ) |
| 151 |
145 150
|
eleq12d |
⊢ ( 𝑥 = 𝑋 → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ↔ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 𝑋 } ) ) ) ) |
| 152 |
151
|
notbid |
⊢ ( 𝑥 = 𝑋 → ( ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ↔ ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 𝑋 } ) ) ) ) |
| 153 |
152
|
ralbidv |
⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ↔ ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 𝑋 } ) ) ) ) |
| 154 |
153
|
ralsng |
⊢ ( 𝑋 ∈ ( ( Base ‘ 𝑊 ) ∖ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) → ( ∀ 𝑥 ∈ { 𝑋 } ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ↔ ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 𝑋 } ) ) ) ) |
| 155 |
154
|
3ad2ant3 |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( ( Base ‘ 𝑊 ) ∖ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) → ( ∀ 𝑥 ∈ { 𝑋 } ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ↔ ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 𝑋 } ) ) ) ) |
| 156 |
144 155
|
mpbird |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( ( Base ‘ 𝑊 ) ∖ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) → ∀ 𝑥 ∈ { 𝑋 } ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ) |
| 157 |
|
ralunb |
⊢ ( ∀ 𝑥 ∈ ( 𝐹 ∪ { 𝑋 } ) ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ↔ ( ∀ 𝑥 ∈ 𝐹 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ∧ ∀ 𝑥 ∈ { 𝑋 } ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ) ) |
| 158 |
112 156 157
|
sylanbrc |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( ( Base ‘ 𝑊 ) ∖ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) → ∀ 𝑥 ∈ ( 𝐹 ∪ { 𝑋 } ) ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ) |
| 159 |
1 74 31 21 25 24
|
islinds2 |
⊢ ( 𝑊 ∈ LVec → ( ( 𝐹 ∪ { 𝑋 } ) ∈ ( LIndS ‘ 𝑊 ) ↔ ( ( 𝐹 ∪ { 𝑋 } ) ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( 𝐹 ∪ { 𝑋 } ) ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ) ) ) |
| 160 |
159
|
3ad2ant1 |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( ( Base ‘ 𝑊 ) ∖ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) → ( ( 𝐹 ∪ { 𝑋 } ) ∈ ( LIndS ‘ 𝑊 ) ↔ ( ( 𝐹 ∪ { 𝑋 } ) ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( 𝐹 ∪ { 𝑋 } ) ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∪ { 𝑋 } ) ∖ { 𝑥 } ) ) ) ) ) |
| 161 |
8 158 160
|
mpbir2and |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝑋 ∈ ( ( Base ‘ 𝑊 ) ∖ ( ( LSpan ‘ 𝑊 ) ‘ 𝐹 ) ) ) → ( 𝐹 ∪ { 𝑋 } ) ∈ ( LIndS ‘ 𝑊 ) ) |