| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2736 | . . . . 5
⊢
(Base‘𝑊) =
(Base‘𝑊) | 
| 2 | 1 | linds1 21831 | . . . 4
⊢ (𝐹 ∈ (LIndS‘𝑊) → 𝐹 ⊆ (Base‘𝑊)) | 
| 3 |  | eldifi 4130 | . . . . 5
⊢ (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) → 𝑋 ∈ (Base‘𝑊)) | 
| 4 | 3 | snssd 4808 | . . . 4
⊢ (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) → {𝑋} ⊆ (Base‘𝑊)) | 
| 5 |  | unss 4189 | . . . . 5
⊢ ((𝐹 ⊆ (Base‘𝑊) ∧ {𝑋} ⊆ (Base‘𝑊)) ↔ (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊)) | 
| 6 | 5 | biimpi 216 | . . . 4
⊢ ((𝐹 ⊆ (Base‘𝑊) ∧ {𝑋} ⊆ (Base‘𝑊)) → (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊)) | 
| 7 | 2, 4, 6 | syl2an 596 | . . 3
⊢ ((𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊)) | 
| 8 | 7 | 3adant1 1130 | . 2
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊)) | 
| 9 |  | eldifn 4131 | . . . . . . 7
⊢ (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) → ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)) | 
| 10 | 9 | 3ad2ant3 1135 | . . . . . 6
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)) | 
| 11 | 10 | adantr 480 | . . . . 5
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)) | 
| 12 |  | simpll1 1212 | . . . . . . . 8
⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → 𝑊 ∈ LVec) | 
| 13 | 2 | ssdifssd 4146 | . . . . . . . . . 10
⊢ (𝐹 ∈ (LIndS‘𝑊) → (𝐹 ∖ {𝑥}) ⊆ (Base‘𝑊)) | 
| 14 | 13 | 3ad2ant2 1134 | . . . . . . . . 9
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∖ {𝑥}) ⊆ (Base‘𝑊)) | 
| 15 | 14 | ad2antrr 726 | . . . . . . . 8
⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → (𝐹 ∖ {𝑥}) ⊆ (Base‘𝑊)) | 
| 16 | 3 | 3ad2ant3 1135 | . . . . . . . . 9
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → 𝑋 ∈ (Base‘𝑊)) | 
| 17 | 16 | ad2antrr 726 | . . . . . . . 8
⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → 𝑋 ∈ (Base‘𝑊)) | 
| 18 |  | simpr 484 | . . . . . . . . 9
⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) | 
| 19 |  | lveclmod 21106 | . . . . . . . . . . . . 13
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) | 
| 20 | 19 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → 𝑊 ∈ LMod) | 
| 21 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) | 
| 22 | 21 | lmodring 20867 | . . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ LMod →
(Scalar‘𝑊) ∈
Ring) | 
| 23 | 19, 22 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝑊 ∈ LVec →
(Scalar‘𝑊) ∈
Ring) | 
| 24 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) | 
| 25 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) | 
| 26 | 24, 25 | ringelnzr 20524 | . . . . . . . . . . . . . 14
⊢
(((Scalar‘𝑊)
∈ Ring ∧ 𝑘 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → (Scalar‘𝑊) ∈ NzRing) | 
| 27 | 23, 26 | sylan 580 | . . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LVec ∧ 𝑘 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → (Scalar‘𝑊) ∈ NzRing) | 
| 28 | 27 | ad2ant2rl 749 | . . . . . . . . . . . 12
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → (Scalar‘𝑊) ∈
NzRing) | 
| 29 |  | simplr 768 | . . . . . . . . . . . 12
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → 𝐹 ∈ (LIndS‘𝑊)) | 
| 30 |  | simprl 770 | . . . . . . . . . . . 12
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → 𝑥 ∈ 𝐹) | 
| 31 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(LSpan‘𝑊) =
(LSpan‘𝑊) | 
| 32 | 31, 21 | lindsind2 21840 | . . . . . . . . . . . 12
⊢ (((𝑊 ∈ LMod ∧
(Scalar‘𝑊) ∈
NzRing) ∧ 𝐹 ∈
(LIndS‘𝑊) ∧ 𝑥 ∈ 𝐹) → ¬ 𝑥 ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥}))) | 
| 33 | 20, 28, 29, 30, 32 | syl211anc 1377 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → ¬ 𝑥 ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥}))) | 
| 34 | 33 | 3adantl3 1168 | . . . . . . . . . 10
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → ¬ 𝑥 ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥}))) | 
| 35 | 34 | adantr 480 | . . . . . . . . 9
⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → ¬ 𝑥 ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥}))) | 
| 36 | 18, 35 | eldifd 3961 | . . . . . . . 8
⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → 𝑥 ∈ (((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ∖ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥})))) | 
| 37 |  | eqid 2736 | . . . . . . . . 9
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) | 
| 38 | 1, 37, 31 | lspsolv 21146 | . . . . . . . 8
⊢ ((𝑊 ∈ LVec ∧ ((𝐹 ∖ {𝑥}) ⊆ (Base‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊) ∧ 𝑥 ∈ (((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ∖ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥}))))) → 𝑋 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥}))) | 
| 39 | 12, 15, 17, 36, 38 | syl13anc 1373 | . . . . . . 7
⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → 𝑋 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥}))) | 
| 40 | 39 | ex 412 | . . . . . 6
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) → 𝑋 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))) | 
| 41 |  | eldif 3960 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) ↔ (𝑋 ∈ (Base‘𝑊) ∧ ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))) | 
| 42 |  | snssi 4807 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑋 ∈ 𝐹 → {𝑋} ⊆ 𝐹) | 
| 43 | 1, 31 | lspss 20983 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑊 ∈ LMod ∧ 𝐹 ⊆ (Base‘𝑊) ∧ {𝑋} ⊆ 𝐹) → ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹)) | 
| 44 | 19, 2, 42, 43 | syl3an 1160 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ 𝐹) → ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹)) | 
| 45 | 44 | ad4ant124 1173 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑋 ∈ 𝐹) → ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹)) | 
| 46 | 1, 31 | lspsnid 20992 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ (Base‘𝑊)) → 𝑋 ∈ ((LSpan‘𝑊)‘{𝑋})) | 
| 47 | 19, 46 | sylan 580 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) → 𝑋 ∈ ((LSpan‘𝑊)‘{𝑋})) | 
| 48 | 47 | ad4ant13 751 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑋 ∈ 𝐹) → 𝑋 ∈ ((LSpan‘𝑊)‘{𝑋})) | 
| 49 | 45, 48 | sseldd 3983 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑋 ∈ 𝐹) → 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)) | 
| 50 | 49 | ex 412 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝑋 ∈ 𝐹 → 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))) | 
| 51 | 50 | con3d 152 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) → (¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹) → ¬ 𝑋 ∈ 𝐹)) | 
| 52 | 51 | expimpd 453 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) → ((𝑋 ∈ (Base‘𝑊) ∧ ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)) → ¬ 𝑋 ∈ 𝐹)) | 
| 53 | 52 | 3impia 1117 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ (𝑋 ∈ (Base‘𝑊) ∧ ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))) → ¬ 𝑋 ∈ 𝐹) | 
| 54 | 41, 53 | syl3an3b 1406 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ¬ 𝑋 ∈ 𝐹) | 
| 55 |  | eleq1 2828 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑋 = 𝑥 → (𝑋 ∈ 𝐹 ↔ 𝑥 ∈ 𝐹)) | 
| 56 | 55 | notbid 318 | . . . . . . . . . . . . . . . . 17
⊢ (𝑋 = 𝑥 → (¬ 𝑋 ∈ 𝐹 ↔ ¬ 𝑥 ∈ 𝐹)) | 
| 57 | 54, 56 | syl5ibcom 245 | . . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝑋 = 𝑥 → ¬ 𝑥 ∈ 𝐹)) | 
| 58 | 57 | necon2ad 2954 | . . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝑥 ∈ 𝐹 → 𝑋 ≠ 𝑥)) | 
| 59 | 58 | imp 406 | . . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → 𝑋 ≠ 𝑥) | 
| 60 |  | disjsn2 4711 | . . . . . . . . . . . . . 14
⊢ (𝑋 ≠ 𝑥 → ({𝑋} ∩ {𝑥}) = ∅) | 
| 61 | 59, 60 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → ({𝑋} ∩ {𝑥}) = ∅) | 
| 62 |  | disj3 4453 | . . . . . . . . . . . . 13
⊢ (({𝑋} ∩ {𝑥}) = ∅ ↔ {𝑋} = ({𝑋} ∖ {𝑥})) | 
| 63 | 61, 62 | sylib 218 | . . . . . . . . . . . 12
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → {𝑋} = ({𝑋} ∖ {𝑥})) | 
| 64 | 63 | uneq2d 4167 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → ((𝐹 ∖ {𝑥}) ∪ {𝑋}) = ((𝐹 ∖ {𝑥}) ∪ ({𝑋} ∖ {𝑥}))) | 
| 65 |  | difundir 4290 | . . . . . . . . . . 11
⊢ ((𝐹 ∪ {𝑋}) ∖ {𝑥}) = ((𝐹 ∖ {𝑥}) ∪ ({𝑋} ∖ {𝑥})) | 
| 66 | 64, 65 | eqtr4di 2794 | . . . . . . . . . 10
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → ((𝐹 ∖ {𝑥}) ∪ {𝑋}) = ((𝐹 ∪ {𝑋}) ∖ {𝑥})) | 
| 67 | 66 | fveq2d 6909 | . . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) = ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))) | 
| 68 | 67 | eleq2d 2826 | . . . . . . . 8
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ↔ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))) | 
| 69 | 68 | adantrr 717 | . . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ↔ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))) | 
| 70 |  | simpl 482 | . . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LVec ∧ 𝑘 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → 𝑊 ∈ LVec) | 
| 71 |  | eldifsn 4785 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ↔ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠
(0g‘(Scalar‘𝑊)))) | 
| 72 | 71 | biimpi 216 | . . . . . . . . . . . . . 14
⊢ (𝑘 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) → (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠
(0g‘(Scalar‘𝑊)))) | 
| 73 | 72 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LVec ∧ 𝑘 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠
(0g‘(Scalar‘𝑊)))) | 
| 74 | 2 | sselda 3982 | . . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (LIndS‘𝑊) ∧ 𝑥 ∈ 𝐹) → 𝑥 ∈ (Base‘𝑊)) | 
| 75 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) | 
| 76 | 1, 21, 75, 25, 24, 31 | lspsnvs 21117 | . . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LVec ∧ (𝑘 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠
(0g‘(Scalar‘𝑊))) ∧ 𝑥 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑥)}) = ((LSpan‘𝑊)‘{𝑥})) | 
| 77 | 70, 73, 74, 76 | syl2an3an 1423 | . . . . . . . . . . . 12
⊢ (((𝑊 ∈ LVec ∧ 𝑘 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) ∧ (𝐹 ∈ (LIndS‘𝑊) ∧ 𝑥 ∈ 𝐹)) → ((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑥)}) = ((LSpan‘𝑊)‘{𝑥})) | 
| 78 | 77 | an42s 661 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → ((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑥)}) = ((LSpan‘𝑊)‘{𝑥})) | 
| 79 | 78 | sseq1d 4014 | . . . . . . . . . 10
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → (((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑥)}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{𝑥}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))) | 
| 80 | 79 | 3adantl3 1168 | . . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → (((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑥)}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{𝑥}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))) | 
| 81 |  | eldifi 4130 | . . . . . . . . . 10
⊢ (𝑘 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) → 𝑘 ∈ (Base‘(Scalar‘𝑊))) | 
| 82 | 19 | 3ad2ant1 1133 | . . . . . . . . . . . 12
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → 𝑊 ∈ LMod) | 
| 83 | 82 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)))) → 𝑊 ∈ LMod) | 
| 84 |  | snssi 4807 | . . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ (Base‘𝑊) → {𝑋} ⊆ (Base‘𝑊)) | 
| 85 | 2, 84, 6 | syl2an 596 | . . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊)) | 
| 86 | 85 | ssdifssd 4146 | . . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → ((𝐹 ∪ {𝑋}) ∖ {𝑥}) ⊆ (Base‘𝑊)) | 
| 87 | 1, 37, 31 | lspcl 20975 | . . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ LMod ∧ ((𝐹 ∪ {𝑋}) ∖ {𝑥}) ⊆ (Base‘𝑊)) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊)) | 
| 88 | 19, 86, 87 | syl2an 596 | . . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LVec ∧ (𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊))) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊)) | 
| 89 | 88 | 3impb 1114 | . . . . . . . . . . . 12
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊)) | 
| 90 | 89 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)))) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊)) | 
| 91 | 19 | anim1i 615 | . . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ LVec ∧ 𝑘 ∈
(Base‘(Scalar‘𝑊))) → (𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)))) | 
| 92 | 1, 21, 75, 25 | lmodvscl 20877 | . . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑘( ·𝑠
‘𝑊)𝑥) ∈ (Base‘𝑊)) | 
| 93 | 92 | 3expa 1118 | . . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ LMod ∧ 𝑘 ∈
(Base‘(Scalar‘𝑊))) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑘( ·𝑠
‘𝑊)𝑥) ∈ (Base‘𝑊)) | 
| 94 | 91, 74, 93 | syl2an 596 | . . . . . . . . . . . . 13
⊢ (((𝑊 ∈ LVec ∧ 𝑘 ∈
(Base‘(Scalar‘𝑊))) ∧ (𝐹 ∈ (LIndS‘𝑊) ∧ 𝑥 ∈ 𝐹)) → (𝑘( ·𝑠
‘𝑊)𝑥) ∈ (Base‘𝑊)) | 
| 95 | 94 | an42s 661 | . . . . . . . . . . . 12
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)))) → (𝑘( ·𝑠
‘𝑊)𝑥) ∈ (Base‘𝑊)) | 
| 96 | 95 | 3adantl3 1168 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)))) → (𝑘( ·𝑠
‘𝑊)𝑥) ∈ (Base‘𝑊)) | 
| 97 | 1, 37, 31, 83, 90, 96 | ellspsn5b 20994 | . . . . . . . . . 10
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)))) → ((𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑥)}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))) | 
| 98 | 81, 97 | sylanr2 683 | . . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → ((𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑥)}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))) | 
| 99 | 82 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑥 ∈ 𝐹) → 𝑊 ∈ LMod) | 
| 100 | 89 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑥 ∈ 𝐹) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊)) | 
| 101 | 74 | 3ad2antl2 1186 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑥 ∈ 𝐹) → 𝑥 ∈ (Base‘𝑊)) | 
| 102 | 1, 37, 31, 99, 100, 101 | ellspsn5b 20994 | . . . . . . . . . 10
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑥 ∈ 𝐹) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{𝑥}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))) | 
| 103 | 102 | adantrr 717 | . . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{𝑥}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))) | 
| 104 | 80, 98, 103 | 3bitr4rd 312 | . . . . . . . 8
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))) | 
| 105 | 3, 104 | syl3anl3 1415 | . . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))) | 
| 106 | 69, 105 | bitrd 279 | . . . . . 6
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ↔ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))) | 
| 107 |  | difsnid 4809 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝐹 → ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = 𝐹) | 
| 108 | 107 | fveq2d 6909 | . . . . . . . 8
⊢ (𝑥 ∈ 𝐹 → ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((LSpan‘𝑊)‘𝐹)) | 
| 109 | 108 | eleq2d 2826 | . . . . . . 7
⊢ (𝑥 ∈ 𝐹 → (𝑋 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) ↔ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))) | 
| 110 | 109 | ad2antrl 728 | . . . . . 6
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → (𝑋 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) ↔ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))) | 
| 111 | 40, 106, 110 | 3imtr3d 293 | . . . . 5
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → ((𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) → 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))) | 
| 112 | 11, 111 | mtod 198 | . . . 4
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))) | 
| 113 | 112 | ralrimivva 3201 | . . 3
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))) | 
| 114 | 10 | adantr 480 | . . . . . 6
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)) | 
| 115 |  | difsn 4797 | . . . . . . . . . . 11
⊢ (¬
𝑋 ∈ 𝐹 → (𝐹 ∖ {𝑋}) = 𝐹) | 
| 116 | 54, 115 | syl 17 | . . . . . . . . . 10
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∖ {𝑋}) = 𝐹) | 
| 117 | 116 | fveq2d 6909 | . . . . . . . . 9
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})) = ((LSpan‘𝑊)‘𝐹)) | 
| 118 | 117 | eleq2d 2826 | . . . . . . . 8
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ((𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})) ↔ (𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹))) | 
| 119 | 118 | adantr 480 | . . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → ((𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})) ↔ (𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹))) | 
| 120 | 1, 21, 75, 25, 24, 31 | lspsnvs 21117 | . . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ LVec ∧ (𝑘 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠
(0g‘(Scalar‘𝑊))) ∧ 𝑋 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑋)}) = ((LSpan‘𝑊)‘{𝑋})) | 
| 121 | 120 | 3expa 1118 | . . . . . . . . . . . . 13
⊢ (((𝑊 ∈ LVec ∧ (𝑘 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠
(0g‘(Scalar‘𝑊)))) ∧ 𝑋 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑋)}) = ((LSpan‘𝑊)‘{𝑋})) | 
| 122 | 121 | an32s 652 | . . . . . . . . . . . 12
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠
(0g‘(Scalar‘𝑊)))) → ((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑋)}) = ((LSpan‘𝑊)‘{𝑋})) | 
| 123 | 71, 122 | sylan2b 594 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → ((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑋)}) = ((LSpan‘𝑊)‘{𝑋})) | 
| 124 | 123 | sseq1d 4014 | . . . . . . . . . 10
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → (((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑋)}) ⊆ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹))) | 
| 125 | 124 | 3adantl2 1167 | . . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → (((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑋)}) ⊆ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹))) | 
| 126 | 82 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → 𝑊 ∈ LMod) | 
| 127 | 1, 37, 31 | lspcl 20975 | . . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ LMod ∧ 𝐹 ⊆ (Base‘𝑊)) → ((LSpan‘𝑊)‘𝐹) ∈ (LSubSp‘𝑊)) | 
| 128 | 19, 2, 127 | syl2an 596 | . . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) → ((LSpan‘𝑊)‘𝐹) ∈ (LSubSp‘𝑊)) | 
| 129 | 128 | 3adant3 1132 | . . . . . . . . . . . 12
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘𝐹) ∈ (LSubSp‘𝑊)) | 
| 130 | 129 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → ((LSpan‘𝑊)‘𝐹) ∈ (LSubSp‘𝑊)) | 
| 131 | 1, 21, 75, 25 | lmodvscl 20877 | . . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝑘( ·𝑠
‘𝑊)𝑋) ∈ (Base‘𝑊)) | 
| 132 | 131 | 3expa 1118 | . . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ LMod ∧ 𝑘 ∈
(Base‘(Scalar‘𝑊))) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝑘( ·𝑠
‘𝑊)𝑋) ∈ (Base‘𝑊)) | 
| 133 | 132 | an32s 652 | . . . . . . . . . . . . 13
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑘( ·𝑠
‘𝑊)𝑋) ∈ (Base‘𝑊)) | 
| 134 | 19, 133 | sylanl1 680 | . . . . . . . . . . . 12
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑘( ·𝑠
‘𝑊)𝑋) ∈ (Base‘𝑊)) | 
| 135 | 134 | 3adantl2 1167 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑘( ·𝑠
‘𝑊)𝑋) ∈ (Base‘𝑊)) | 
| 136 | 1, 37, 31, 126, 130, 135 | ellspsn5b 20994 | . . . . . . . . . 10
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → ((𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑋)}) ⊆ ((LSpan‘𝑊)‘𝐹))) | 
| 137 | 81, 136 | sylan2 593 | . . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → ((𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑋)}) ⊆ ((LSpan‘𝑊)‘𝐹))) | 
| 138 |  | simp3 1138 | . . . . . . . . . . 11
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → 𝑋 ∈ (Base‘𝑊)) | 
| 139 | 1, 37, 31, 82, 129, 138 | ellspsn5b 20994 | . . . . . . . . . 10
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝑋 ∈ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹))) | 
| 140 | 139 | adantr 480 | . . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → (𝑋 ∈ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹))) | 
| 141 | 125, 137,
140 | 3bitr4d 311 | . . . . . . . 8
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → ((𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹) ↔ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))) | 
| 142 | 3, 141 | syl3anl3 1415 | . . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → ((𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹) ↔ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))) | 
| 143 | 119, 142 | bitrd 279 | . . . . . 6
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → ((𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})) ↔ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))) | 
| 144 | 114, 143 | mtbird 325 | . . . . 5
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → ¬ (𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋}))) | 
| 145 | 144 | ralrimiva 3145 | . . . 4
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋}))) | 
| 146 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝑘( ·𝑠
‘𝑊)𝑥) = (𝑘( ·𝑠
‘𝑊)𝑋)) | 
| 147 |  | sneq 4635 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑋 → {𝑥} = {𝑋}) | 
| 148 | 147 | difeq2d 4125 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → ((𝐹 ∪ {𝑋}) ∖ {𝑥}) = ((𝐹 ∪ {𝑋}) ∖ {𝑋})) | 
| 149 |  | difun2 4480 | . . . . . . . . . . 11
⊢ ((𝐹 ∪ {𝑋}) ∖ {𝑋}) = (𝐹 ∖ {𝑋}) | 
| 150 | 148, 149 | eqtrdi 2792 | . . . . . . . . . 10
⊢ (𝑥 = 𝑋 → ((𝐹 ∪ {𝑋}) ∖ {𝑥}) = (𝐹 ∖ {𝑋})) | 
| 151 | 150 | fveq2d 6909 | . . . . . . . . 9
⊢ (𝑥 = 𝑋 → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) = ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋}))) | 
| 152 | 146, 151 | eleq12d 2834 | . . . . . . . 8
⊢ (𝑥 = 𝑋 → ((𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ (𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})))) | 
| 153 | 152 | notbid 318 | . . . . . . 7
⊢ (𝑥 = 𝑋 → (¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ¬ (𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})))) | 
| 154 | 153 | ralbidv 3177 | . . . . . 6
⊢ (𝑥 = 𝑋 → (∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})))) | 
| 155 | 154 | ralsng 4674 | . . . . 5
⊢ (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) → (∀𝑥 ∈ {𝑋}∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})))) | 
| 156 | 155 | 3ad2ant3 1135 | . . . 4
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (∀𝑥 ∈ {𝑋}∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})))) | 
| 157 | 145, 156 | mpbird 257 | . . 3
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ∀𝑥 ∈ {𝑋}∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))) | 
| 158 |  | ralunb 4196 | . . 3
⊢
(∀𝑥 ∈
(𝐹 ∪ {𝑋})∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ (∀𝑥 ∈ 𝐹 ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∧ ∀𝑥 ∈ {𝑋}∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))) | 
| 159 | 113, 157,
158 | sylanbrc 583 | . 2
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ∀𝑥 ∈ (𝐹 ∪ {𝑋})∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))) | 
| 160 | 1, 75, 31, 21, 25, 24 | islinds2 21834 | . . 3
⊢ (𝑊 ∈ LVec → ((𝐹 ∪ {𝑋}) ∈ (LIndS‘𝑊) ↔ ((𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊) ∧ ∀𝑥 ∈ (𝐹 ∪ {𝑋})∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))) | 
| 161 | 160 | 3ad2ant1 1133 | . 2
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ((𝐹 ∪ {𝑋}) ∈ (LIndS‘𝑊) ↔ ((𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊) ∧ ∀𝑥 ∈ (𝐹 ∪ {𝑋})∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))) | 
| 162 | 8, 159, 161 | mpbir2and 713 | 1
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∪ {𝑋}) ∈ (LIndS‘𝑊)) |