Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lindsadd Structured version   Visualization version   GIF version

Theorem lindsadd 37599
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.)
Assertion
Ref Expression
lindsadd ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∪ {𝑋}) ∈ (LIndS‘𝑊))

Proof of Theorem lindsadd
Dummy variables 𝑥 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2734 . . . . 5 (Base‘𝑊) = (Base‘𝑊)
21linds1 21847 . . . 4 (𝐹 ∈ (LIndS‘𝑊) → 𝐹 ⊆ (Base‘𝑊))
3 eldifi 4140 . . . . 5 (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) → 𝑋 ∈ (Base‘𝑊))
43snssd 4813 . . . 4 (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) → {𝑋} ⊆ (Base‘𝑊))
5 unss 4199 . . . . 5 ((𝐹 ⊆ (Base‘𝑊) ∧ {𝑋} ⊆ (Base‘𝑊)) ↔ (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊))
65biimpi 216 . . . 4 ((𝐹 ⊆ (Base‘𝑊) ∧ {𝑋} ⊆ (Base‘𝑊)) → (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊))
72, 4, 6syl2an 596 . . 3 ((𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊))
873adant1 1129 . 2 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊))
9 eldifn 4141 . . . . . . 7 (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) → ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))
1093ad2ant3 1134 . . . . . 6 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))
1110adantr 480 . . . . 5 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))
12 simpll1 1211 . . . . . . . 8 ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → 𝑊 ∈ LVec)
132ssdifssd 4156 . . . . . . . . . 10 (𝐹 ∈ (LIndS‘𝑊) → (𝐹 ∖ {𝑥}) ⊆ (Base‘𝑊))
14133ad2ant2 1133 . . . . . . . . 9 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∖ {𝑥}) ⊆ (Base‘𝑊))
1514ad2antrr 726 . . . . . . . 8 ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → (𝐹 ∖ {𝑥}) ⊆ (Base‘𝑊))
1633ad2ant3 1134 . . . . . . . . 9 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → 𝑋 ∈ (Base‘𝑊))
1716ad2antrr 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 21122 . . . . . . . . . . . . 13 (𝑊 ∈ LVec → 𝑊 ∈ LMod)
2019ad2antrr 726 . . . . . . . . . . . 12 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → 𝑊 ∈ LMod)
21 eqid 2734 . . . . . . . . . . . . . . . 16 (Scalar‘𝑊) = (Scalar‘𝑊)
2221lmodring 20882 . . . . . . . . . . . . . . 15 (𝑊 ∈ LMod → (Scalar‘𝑊) ∈ Ring)
2319, 22syl 17 . . . . . . . . . . . . . 14 (𝑊 ∈ LVec → (Scalar‘𝑊) ∈ Ring)
24 eqid 2734 . . . . . . . . . . . . . . 15 (0g‘(Scalar‘𝑊)) = (0g‘(Scalar‘𝑊))
25 eqid 2734 . . . . . . . . . . . . . . 15 (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
2624, 25ringelnzr 20539 . . . . . . . . . . . . . 14 (((Scalar‘𝑊) ∈ Ring ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))})) → (Scalar‘𝑊) ∈ NzRing)
2723, 26sylan 580 . . . . . . . . . . . . 13 ((𝑊 ∈ LVec ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))})) → (Scalar‘𝑊) ∈ NzRing)
2827ad2ant2rl 749 . . . . . . . . . . . 12 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → (Scalar‘𝑊) ∈ NzRing)
29 simplr 769 . . . . . . . . . . . 12 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → 𝐹 ∈ (LIndS‘𝑊))
30 simprl 771 . . . . . . . . . . . 12 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → 𝑥𝐹)
31 eqid 2734 . . . . . . . . . . . . 13 (LSpan‘𝑊) = (LSpan‘𝑊)
3231, 21lindsind2 21856 . . . . . . . . . . . 12 (((𝑊 ∈ LMod ∧ (Scalar‘𝑊) ∈ NzRing) ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑥𝐹) → ¬ 𝑥 ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥})))
3320, 28, 29, 30, 32syl211anc 1375 . . . . . . . . . . 11 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → ¬ 𝑥 ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥})))
34333adantl3 1167 . . . . . . . . . 10 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → ¬ 𝑥 ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥})))
3534adantr 480 . . . . . . . . 9 ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → ¬ 𝑥 ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥})))
3618, 35eldifd 3973 . . . . . . . 8 ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → 𝑥 ∈ (((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ∖ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥}))))
37 eqid 2734 . . . . . . . . 9 (LSubSp‘𝑊) = (LSubSp‘𝑊)
381, 37, 31lspsolv 21162 . . . . . . . 8 ((𝑊 ∈ LVec ∧ ((𝐹 ∖ {𝑥}) ⊆ (Base‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊) ∧ 𝑥 ∈ (((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ∖ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥}))))) → 𝑋 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))
3912, 15, 17, 36, 38syl13anc 1371 . . . . . . 7 ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → 𝑋 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))
4039ex 412 . . . . . 6 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) → 𝑋 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥}))))
41 eldif 3972 . . . . . . . . . . . . . . . . . 18 (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) ↔ (𝑋 ∈ (Base‘𝑊) ∧ ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)))
42 snssi 4812 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑋𝐹 → {𝑋} ⊆ 𝐹)
431, 31lspss 20999 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑊 ∈ LMod ∧ 𝐹 ⊆ (Base‘𝑊) ∧ {𝑋} ⊆ 𝐹) → ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹))
4419, 2, 42, 43syl3an 1159 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋𝐹) → ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹))
4544ad4ant124 1172 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑋𝐹) → ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹))
461, 31lspsnid 21008 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑊 ∈ LMod ∧ 𝑋 ∈ (Base‘𝑊)) → 𝑋 ∈ ((LSpan‘𝑊)‘{𝑋}))
4719, 46sylan 580 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) → 𝑋 ∈ ((LSpan‘𝑊)‘{𝑋}))
4847ad4ant13 751 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑋𝐹) → 𝑋 ∈ ((LSpan‘𝑊)‘{𝑋}))
4945, 48sseldd 3995 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑋𝐹) → 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))
5049ex 412 . . . . . . . . . . . . . . . . . . . . 21 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝑋𝐹𝑋 ∈ ((LSpan‘𝑊)‘𝐹)))
5150con3d 152 . . . . . . . . . . . . . . . . . . . 20 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) → (¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹) → ¬ 𝑋𝐹))
5251expimpd 453 . . . . . . . . . . . . . . . . . . 19 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) → ((𝑋 ∈ (Base‘𝑊) ∧ ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)) → ¬ 𝑋𝐹))
53523impia 1116 . . . . . . . . . . . . . . . . . 18 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ (𝑋 ∈ (Base‘𝑊) ∧ ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))) → ¬ 𝑋𝐹)
5441, 53syl3an3b 1404 . . . . . . . . . . . . . . . . 17 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ¬ 𝑋𝐹)
55 eleq1 2826 . . . . . . . . . . . . . . . . . 18 (𝑋 = 𝑥 → (𝑋𝐹𝑥𝐹))
5655notbid 318 . . . . . . . . . . . . . . . . 17 (𝑋 = 𝑥 → (¬ 𝑋𝐹 ↔ ¬ 𝑥𝐹))
5754, 56syl5ibcom 245 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝑋 = 𝑥 → ¬ 𝑥𝐹))
5857necon2ad 2952 . . . . . . . . . . . . . . 15 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝑥𝐹𝑋𝑥))
5958imp 406 . . . . . . . . . . . . . 14 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥𝐹) → 𝑋𝑥)
60 disjsn2 4716 . . . . . . . . . . . . . 14 (𝑋𝑥 → ({𝑋} ∩ {𝑥}) = ∅)
6159, 60syl 17 . . . . . . . . . . . . 13 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥𝐹) → ({𝑋} ∩ {𝑥}) = ∅)
62 disj3 4459 . . . . . . . . . . . . 13 (({𝑋} ∩ {𝑥}) = ∅ ↔ {𝑋} = ({𝑋} ∖ {𝑥}))
6361, 62sylib 218 . . . . . . . . . . . 12 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥𝐹) → {𝑋} = ({𝑋} ∖ {𝑥}))
6463uneq2d 4177 . . . . . . . . . . 11 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥𝐹) → ((𝐹 ∖ {𝑥}) ∪ {𝑋}) = ((𝐹 ∖ {𝑥}) ∪ ({𝑋} ∖ {𝑥})))
65 difundir 4296 . . . . . . . . . . 11 ((𝐹 ∪ {𝑋}) ∖ {𝑥}) = ((𝐹 ∖ {𝑥}) ∪ ({𝑋} ∖ {𝑥}))
6664, 65eqtr4di 2792 . . . . . . . . . 10 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥𝐹) → ((𝐹 ∖ {𝑥}) ∪ {𝑋}) = ((𝐹 ∪ {𝑋}) ∖ {𝑥}))
6766fveq2d 6910 . . . . . . . . 9 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥𝐹) → ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) = ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))
6867eleq2d 2824 . . . . . . . 8 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥𝐹) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ↔ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
6968adantrr 717 . . . . . . 7 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ↔ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
70 simpl 482 . . . . . . . . . . . . 13 ((𝑊 ∈ LVec ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))})) → 𝑊 ∈ LVec)
71 eldifsn 4790 . . . . . . . . . . . . . . 15 (𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ↔ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0g‘(Scalar‘𝑊))))
7271biimpi 216 . . . . . . . . . . . . . 14 (𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) → (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0g‘(Scalar‘𝑊))))
7372adantl 481 . . . . . . . . . . . . 13 ((𝑊 ∈ LVec ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))})) → (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0g‘(Scalar‘𝑊))))
742sselda 3994 . . . . . . . . . . . . 13 ((𝐹 ∈ (LIndS‘𝑊) ∧ 𝑥𝐹) → 𝑥 ∈ (Base‘𝑊))
75 eqid 2734 . . . . . . . . . . . . . 14 ( ·𝑠𝑊) = ( ·𝑠𝑊)
761, 21, 75, 25, 24, 31lspsnvs 21133 . . . . . . . . . . . . 13 ((𝑊 ∈ LVec ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0g‘(Scalar‘𝑊))) ∧ 𝑥 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘{(𝑘( ·𝑠𝑊)𝑥)}) = ((LSpan‘𝑊)‘{𝑥}))
7770, 73, 74, 76syl2an3an 1421 . . . . . . . . . . . 12 (((𝑊 ∈ LVec ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))})) ∧ (𝐹 ∈ (LIndS‘𝑊) ∧ 𝑥𝐹)) → ((LSpan‘𝑊)‘{(𝑘( ·𝑠𝑊)𝑥)}) = ((LSpan‘𝑊)‘{𝑥}))
7877an42s 661 . . . . . . . . . . 11 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → ((LSpan‘𝑊)‘{(𝑘( ·𝑠𝑊)𝑥)}) = ((LSpan‘𝑊)‘{𝑥}))
7978sseq1d 4026 . . . . . . . . . 10 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → (((LSpan‘𝑊)‘{(𝑘( ·𝑠𝑊)𝑥)}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{𝑥}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
80793adantl3 1167 . . . . . . . . 9 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → (((LSpan‘𝑊)‘{(𝑘( ·𝑠𝑊)𝑥)}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{𝑥}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
81 eldifi 4140 . . . . . . . . . 10 (𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) → 𝑘 ∈ (Base‘(Scalar‘𝑊)))
82193ad2ant1 1132 . . . . . . . . . . . 12 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → 𝑊 ∈ LMod)
8382adantr 480 . . . . . . . . . . 11 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥𝐹𝑘 ∈ (Base‘(Scalar‘𝑊)))) → 𝑊 ∈ LMod)
84 snssi 4812 . . . . . . . . . . . . . . . 16 (𝑋 ∈ (Base‘𝑊) → {𝑋} ⊆ (Base‘𝑊))
852, 84, 6syl2an 596 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊))
8685ssdifssd 4156 . . . . . . . . . . . . . 14 ((𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → ((𝐹 ∪ {𝑋}) ∖ {𝑥}) ⊆ (Base‘𝑊))
871, 37, 31lspcl 20991 . . . . . . . . . . . . . 14 ((𝑊 ∈ LMod ∧ ((𝐹 ∪ {𝑋}) ∖ {𝑥}) ⊆ (Base‘𝑊)) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊))
8819, 86, 87syl2an 596 . . . . . . . . . . . . 13 ((𝑊 ∈ LVec ∧ (𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊))) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊))
89883impb 1114 . . . . . . . . . . . 12 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊))
9089adantr 480 . . . . . . . . . . 11 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥𝐹𝑘 ∈ (Base‘(Scalar‘𝑊)))) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊))
9119anim1i 615 . . . . . . . . . . . . . 14 ((𝑊 ∈ LVec ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))))
921, 21, 75, 25lmodvscl 20892 . . . . . . . . . . . . . . 15 ((𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑘( ·𝑠𝑊)𝑥) ∈ (Base‘𝑊))
93923expa 1117 . . . . . . . . . . . . . 14 (((𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑘( ·𝑠𝑊)𝑥) ∈ (Base‘𝑊))
9491, 74, 93syl2an 596 . . . . . . . . . . . . 13 (((𝑊 ∈ LVec ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝐹 ∈ (LIndS‘𝑊) ∧ 𝑥𝐹)) → (𝑘( ·𝑠𝑊)𝑥) ∈ (Base‘𝑊))
9594an42s 661 . . . . . . . . . . . 12 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥𝐹𝑘 ∈ (Base‘(Scalar‘𝑊)))) → (𝑘( ·𝑠𝑊)𝑥) ∈ (Base‘𝑊))
96953adantl3 1167 . . . . . . . . . . 11 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥𝐹𝑘 ∈ (Base‘(Scalar‘𝑊)))) → (𝑘( ·𝑠𝑊)𝑥) ∈ (Base‘𝑊))
971, 37, 31, 83, 90, 96ellspsn5b 21010 . . . . . . . . . 10 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥𝐹𝑘 ∈ (Base‘(Scalar‘𝑊)))) → ((𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{(𝑘( ·𝑠𝑊)𝑥)}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
9881, 97sylanr2 683 . . . . . . . . 9 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → ((𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{(𝑘( ·𝑠𝑊)𝑥)}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
9982adantr 480 . . . . . . . . . . 11 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑥𝐹) → 𝑊 ∈ LMod)
10089adantr 480 . . . . . . . . . . 11 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑥𝐹) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊))
101743ad2antl2 1185 . . . . . . . . . . 11 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑥𝐹) → 𝑥 ∈ (Base‘𝑊))
1021, 37, 31, 99, 100, 101ellspsn5b 21010 . . . . . . . . . 10 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑥𝐹) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{𝑥}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
103102adantrr 717 . . . . . . . . 9 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{𝑥}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
10480, 98, 1033bitr4rd 312 . . . . . . . 8 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
1053, 104syl3anl3 1413 . . . . . . 7 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
10669, 105bitrd 279 . . . . . 6 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ↔ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
107 difsnid 4814 . . . . . . . . 9 (𝑥𝐹 → ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = 𝐹)
108107fveq2d 6910 . . . . . . . 8 (𝑥𝐹 → ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((LSpan‘𝑊)‘𝐹))
109108eleq2d 2824 . . . . . . 7 (𝑥𝐹 → (𝑋 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) ↔ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)))
110109ad2antrl 728 . . . . . 6 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → (𝑋 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) ↔ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)))
11140, 106, 1103imtr3d 293 . . . . 5 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → ((𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) → 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)))
11211, 111mtod 198 . . . 4 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))
113112ralrimivva 3199 . . 3 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ∀𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))
11410adantr 480 . . . . . 6 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))})) → ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))
115 difsn 4802 . . . . . . . . . . 11 𝑋𝐹 → (𝐹 ∖ {𝑋}) = 𝐹)
11654, 115syl 17 . . . . . . . . . 10 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∖ {𝑋}) = 𝐹)
117116fveq2d 6910 . . . . . . . . 9 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})) = ((LSpan‘𝑊)‘𝐹))
118117eleq2d 2824 . . . . . . . 8 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ((𝑘( ·𝑠𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})) ↔ (𝑘( ·𝑠𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹)))
119118adantr 480 . . . . . . 7 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))})) → ((𝑘( ·𝑠𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})) ↔ (𝑘( ·𝑠𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹)))
1201, 21, 75, 25, 24, 31lspsnvs 21133 . . . . . . . . . . . . . 14 ((𝑊 ∈ LVec ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0g‘(Scalar‘𝑊))) ∧ 𝑋 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘{(𝑘( ·𝑠𝑊)𝑋)}) = ((LSpan‘𝑊)‘{𝑋}))
1211203expa 1117 . . . . . . . . . . . . 13 (((𝑊 ∈ LVec ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0g‘(Scalar‘𝑊)))) ∧ 𝑋 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘{(𝑘( ·𝑠𝑊)𝑋)}) = ((LSpan‘𝑊)‘{𝑋}))
122121an32s 652 . . . . . . . . . . . 12 (((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0g‘(Scalar‘𝑊)))) → ((LSpan‘𝑊)‘{(𝑘( ·𝑠𝑊)𝑋)}) = ((LSpan‘𝑊)‘{𝑋}))
12371, 122sylan2b 594 . . . . . . . . . . 11 (((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))})) → ((LSpan‘𝑊)‘{(𝑘( ·𝑠𝑊)𝑋)}) = ((LSpan‘𝑊)‘{𝑋}))
124123sseq1d 4026 . . . . . . . . . 10 (((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))})) → (((LSpan‘𝑊)‘{(𝑘( ·𝑠𝑊)𝑋)}) ⊆ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹)))
1251243adantl2 1166 . . . . . . . . 9 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))})) → (((LSpan‘𝑊)‘{(𝑘( ·𝑠𝑊)𝑋)}) ⊆ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹)))
12682adantr 480 . . . . . . . . . . 11 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → 𝑊 ∈ LMod)
1271, 37, 31lspcl 20991 . . . . . . . . . . . . . 14 ((𝑊 ∈ LMod ∧ 𝐹 ⊆ (Base‘𝑊)) → ((LSpan‘𝑊)‘𝐹) ∈ (LSubSp‘𝑊))
12819, 2, 127syl2an 596 . . . . . . . . . . . . 13 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) → ((LSpan‘𝑊)‘𝐹) ∈ (LSubSp‘𝑊))
1291283adant3 1131 . . . . . . . . . . . 12 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘𝐹) ∈ (LSubSp‘𝑊))
130129adantr 480 . . . . . . . . . . 11 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → ((LSpan‘𝑊)‘𝐹) ∈ (LSubSp‘𝑊))
1311, 21, 75, 25lmodvscl 20892 . . . . . . . . . . . . . . 15 ((𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝑘( ·𝑠𝑊)𝑋) ∈ (Base‘𝑊))
1321313expa 1117 . . . . . . . . . . . . . 14 (((𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝑘( ·𝑠𝑊)𝑋) ∈ (Base‘𝑊))
133132an32s 652 . . . . . . . . . . . . 13 (((𝑊 ∈ LMod ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑘( ·𝑠𝑊)𝑋) ∈ (Base‘𝑊))
13419, 133sylanl1 680 . . . . . . . . . . . 12 (((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑘( ·𝑠𝑊)𝑋) ∈ (Base‘𝑊))
1351343adantl2 1166 . . . . . . . . . . 11 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑘( ·𝑠𝑊)𝑋) ∈ (Base‘𝑊))
1361, 37, 31, 126, 130, 135ellspsn5b 21010 . . . . . . . . . 10 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → ((𝑘( ·𝑠𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{(𝑘( ·𝑠𝑊)𝑋)}) ⊆ ((LSpan‘𝑊)‘𝐹)))
13781, 136sylan2 593 . . . . . . . . 9 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))})) → ((𝑘( ·𝑠𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{(𝑘( ·𝑠𝑊)𝑋)}) ⊆ ((LSpan‘𝑊)‘𝐹)))
138 simp3 1137 . . . . . . . . . . 11 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → 𝑋 ∈ (Base‘𝑊))
1391, 37, 31, 82, 129, 138ellspsn5b 21010 . . . . . . . . . 10 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝑋 ∈ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹)))
140139adantr 480 . . . . . . . . 9 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))})) → (𝑋 ∈ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹)))
141125, 137, 1403bitr4d 311 . . . . . . . 8 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))})) → ((𝑘( ·𝑠𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹) ↔ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)))
1423, 141syl3anl3 1413 . . . . . . 7 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))})) → ((𝑘( ·𝑠𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹) ↔ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)))
143119, 142bitrd 279 . . . . . 6 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))})) → ((𝑘( ·𝑠𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})) ↔ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)))
144114, 143mtbird 325 . . . . 5 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))})) → ¬ (𝑘( ·𝑠𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})))
145144ralrimiva 3143 . . . 4 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})))
146 oveq2 7438 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑘( ·𝑠𝑊)𝑥) = (𝑘( ·𝑠𝑊)𝑋))
147 sneq 4640 . . . . . . . . . . . 12 (𝑥 = 𝑋 → {𝑥} = {𝑋})
148147difeq2d 4135 . . . . . . . . . . 11 (𝑥 = 𝑋 → ((𝐹 ∪ {𝑋}) ∖ {𝑥}) = ((𝐹 ∪ {𝑋}) ∖ {𝑋}))
149 difun2 4486 . . . . . . . . . . 11 ((𝐹 ∪ {𝑋}) ∖ {𝑋}) = (𝐹 ∖ {𝑋})
150148, 149eqtrdi 2790 . . . . . . . . . 10 (𝑥 = 𝑋 → ((𝐹 ∪ {𝑋}) ∖ {𝑥}) = (𝐹 ∖ {𝑋}))
151150fveq2d 6910 . . . . . . . . 9 (𝑥 = 𝑋 → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) = ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})))
152146, 151eleq12d 2832 . . . . . . . 8 (𝑥 = 𝑋 → ((𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ (𝑘( ·𝑠𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋}))))
153152notbid 318 . . . . . . 7 (𝑥 = 𝑋 → (¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ¬ (𝑘( ·𝑠𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋}))))
154153ralbidv 3175 . . . . . 6 (𝑥 = 𝑋 → (∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋}))))
155154ralsng 4679 . . . . 5 (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) → (∀𝑥 ∈ {𝑋}∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋}))))
1561553ad2ant3 1134 . . . 4 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (∀𝑥 ∈ {𝑋}∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋}))))
157145, 156mpbird 257 . . 3 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ∀𝑥 ∈ {𝑋}∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))
158 ralunb 4206 . . 3 (∀𝑥 ∈ (𝐹 ∪ {𝑋})∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ (∀𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∧ ∀𝑥 ∈ {𝑋}∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
159113, 157, 158sylanbrc 583 . 2 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ∀𝑥 ∈ (𝐹 ∪ {𝑋})∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))
1601, 75, 31, 21, 25, 24islinds2 21850 . . 3 (𝑊 ∈ LVec → ((𝐹 ∪ {𝑋}) ∈ (LIndS‘𝑊) ↔ ((𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊) ∧ ∀𝑥 ∈ (𝐹 ∪ {𝑋})∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))))
1611603ad2ant1 1132 . 2 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ((𝐹 ∪ {𝑋}) ∈ (LIndS‘𝑊) ↔ ((𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊) ∧ ∀𝑥 ∈ (𝐹 ∪ {𝑋})∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))))
1628, 159, 161mpbir2and 713 1 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∪ {𝑋}) ∈ (LIndS‘𝑊))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1536  wcel 2105  wne 2937  wral 3058  cdif 3959  cun 3960  cin 3961  wss 3962  c0 4338  {csn 4630  cfv 6562  (class class class)co 7430  Basecbs 17244  Scalarcsca 17300   ·𝑠 cvsca 17301  0gc0g 17485  Ringcrg 20250  NzRingcnzr 20528  LModclmod 20874  LSubSpclss 20946  LSpanclspn 20986  LVecclvec 21118  LIndSclinds 21842
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-tpos 8249  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-2 12326  df-3 12327  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-ress 17274  df-plusg 17310  df-mulr 17311  df-0g 17487  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-grp 18966  df-minusg 18967  df-sbg 18968  df-cmn 19814  df-abl 19815  df-mgp 20152  df-rng 20170  df-ur 20199  df-ring 20252  df-oppr 20350  df-dvdsr 20373  df-unit 20374  df-invr 20404  df-nzr 20529  df-drng 20747  df-lmod 20876  df-lss 20947  df-lsp 20987  df-lvec 21119  df-lindf 21843  df-linds 21844
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator