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 36945
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 2731 . . . . 5 (Base‘𝑊) = (Base‘𝑊)
21linds1 21675 . . . 4 (𝐹 ∈ (LIndS‘𝑊) → 𝐹 ⊆ (Base‘𝑊))
3 eldifi 4126 . . . . 5 (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) → 𝑋 ∈ (Base‘𝑊))
43snssd 4812 . . . 4 (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) → {𝑋} ⊆ (Base‘𝑊))
5 unss 4184 . . . . 5 ((𝐹 ⊆ (Base‘𝑊) ∧ {𝑋} ⊆ (Base‘𝑊)) ↔ (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊))
65biimpi 215 . . . 4 ((𝐹 ⊆ (Base‘𝑊) ∧ {𝑋} ⊆ (Base‘𝑊)) → (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊))
72, 4, 6syl2an 595 . . 3 ((𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊))
873adant1 1129 . 2 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊))
9 eldifn 4127 . . . . . . 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 4142 . . . . . . . . . 10 (𝐹 ∈ (LIndS‘𝑊) → (𝐹 ∖ {𝑥}) ⊆ (Base‘𝑊))
14133ad2ant2 1133 . . . . . . . . 9 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∖ {𝑥}) ⊆ (Base‘𝑊))
1514ad2antrr 723 . . . . . . . 8 ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → (𝐹 ∖ {𝑥}) ⊆ (Base‘𝑊))
1633ad2ant3 1134 . . . . . . . . 9 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → 𝑋 ∈ (Base‘𝑊))
1716ad2antrr 723 . . . . . . . 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 20950 . . . . . . . . . . . . 13 (𝑊 ∈ LVec → 𝑊 ∈ LMod)
2019ad2antrr 723 . . . . . . . . . . . 12 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → 𝑊 ∈ LMod)
21 eqid 2731 . . . . . . . . . . . . . . . 16 (Scalar‘𝑊) = (Scalar‘𝑊)
2221lmodring 20710 . . . . . . . . . . . . . . 15 (𝑊 ∈ LMod → (Scalar‘𝑊) ∈ Ring)
2319, 22syl 17 . . . . . . . . . . . . . 14 (𝑊 ∈ LVec → (Scalar‘𝑊) ∈ Ring)
24 eqid 2731 . . . . . . . . . . . . . . 15 (0g‘(Scalar‘𝑊)) = (0g‘(Scalar‘𝑊))
25 eqid 2731 . . . . . . . . . . . . . . 15 (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
2624, 25ringelnzr 20419 . . . . . . . . . . . . . 14 (((Scalar‘𝑊) ∈ Ring ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))})) → (Scalar‘𝑊) ∈ NzRing)
2723, 26sylan 579 . . . . . . . . . . . . 13 ((𝑊 ∈ LVec ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))})) → (Scalar‘𝑊) ∈ NzRing)
2827ad2ant2rl 746 . . . . . . . . . . . 12 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → (Scalar‘𝑊) ∈ NzRing)
29 simplr 766 . . . . . . . . . . . 12 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → 𝐹 ∈ (LIndS‘𝑊))
30 simprl 768 . . . . . . . . . . . 12 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → 𝑥𝐹)
31 eqid 2731 . . . . . . . . . . . . 13 (LSpan‘𝑊) = (LSpan‘𝑊)
3231, 21lindsind2 21684 . . . . . . . . . . . 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 3959 . . . . . . . 8 ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → 𝑥 ∈ (((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ∖ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥}))))
37 eqid 2731 . . . . . . . . 9 (LSubSp‘𝑊) = (LSubSp‘𝑊)
381, 37, 31lspsolv 20990 . . . . . . . 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 3958 . . . . . . . . . . . . . . . . . 18 (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) ↔ (𝑋 ∈ (Base‘𝑊) ∧ ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)))
42 snssi 4811 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑋𝐹 → {𝑋} ⊆ 𝐹)
431, 31lspss 20827 . . . . . . . . . . . . . . . . . . . . . . . . 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 20836 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑊 ∈ LMod ∧ 𝑋 ∈ (Base‘𝑊)) → 𝑋 ∈ ((LSpan‘𝑊)‘{𝑋}))
4719, 46sylan 579 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) → 𝑋 ∈ ((LSpan‘𝑊)‘{𝑋}))
4847ad4ant13 748 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑋𝐹) → 𝑋 ∈ ((LSpan‘𝑊)‘{𝑋}))
4945, 48sseldd 3983 . . . . . . . . . . . . . . . . . . . . . 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 2820 . . . . . . . . . . . . . . . . . 18 (𝑋 = 𝑥 → (𝑋𝐹𝑥𝐹))
5655notbid 318 . . . . . . . . . . . . . . . . 17 (𝑋 = 𝑥 → (¬ 𝑋𝐹 ↔ ¬ 𝑥𝐹))
5754, 56syl5ibcom 244 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝑋 = 𝑥 → ¬ 𝑥𝐹))
5857necon2ad 2954 . . . . . . . . . . . . . . 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 4453 . . . . . . . . . . . . 13 (({𝑋} ∩ {𝑥}) = ∅ ↔ {𝑋} = ({𝑋} ∖ {𝑥}))
6361, 62sylib 217 . . . . . . . . . . . 12 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥𝐹) → {𝑋} = ({𝑋} ∖ {𝑥}))
6463uneq2d 4163 . . . . . . . . . . 11 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥𝐹) → ((𝐹 ∖ {𝑥}) ∪ {𝑋}) = ((𝐹 ∖ {𝑥}) ∪ ({𝑋} ∖ {𝑥})))
65 difundir 4280 . . . . . . . . . . 11 ((𝐹 ∪ {𝑋}) ∖ {𝑥}) = ((𝐹 ∖ {𝑥}) ∪ ({𝑋} ∖ {𝑥}))
6664, 65eqtr4di 2789 . . . . . . . . . 10 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥𝐹) → ((𝐹 ∖ {𝑥}) ∪ {𝑋}) = ((𝐹 ∪ {𝑋}) ∖ {𝑥}))
6766fveq2d 6895 . . . . . . . . 9 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥𝐹) → ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) = ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))
6867eleq2d 2818 . . . . . . . 8 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥𝐹) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ↔ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
6968adantrr 714 . . . . . . 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 215 . . . . . . . . . . . . . 14 (𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) → (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0g‘(Scalar‘𝑊))))
7372adantl 481 . . . . . . . . . . . . 13 ((𝑊 ∈ LVec ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))})) → (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0g‘(Scalar‘𝑊))))
742sselda 3982 . . . . . . . . . . . . 13 ((𝐹 ∈ (LIndS‘𝑊) ∧ 𝑥𝐹) → 𝑥 ∈ (Base‘𝑊))
75 eqid 2731 . . . . . . . . . . . . . 14 ( ·𝑠𝑊) = ( ·𝑠𝑊)
761, 21, 75, 25, 24, 31lspsnvs 20961 . . . . . . . . . . . . 13 ((𝑊 ∈ LVec ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0g‘(Scalar‘𝑊))) ∧ 𝑥 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘{(𝑘( ·𝑠𝑊)𝑥)}) = ((LSpan‘𝑊)‘{𝑥}))
7770, 73, 74, 76syl2an3an 1421 . . . . . . . . . . . 12 (((𝑊 ∈ LVec ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))})) ∧ (𝐹 ∈ (LIndS‘𝑊) ∧ 𝑥𝐹)) → ((LSpan‘𝑊)‘{(𝑘( ·𝑠𝑊)𝑥)}) = ((LSpan‘𝑊)‘{𝑥}))
7877an42s 658 . . . . . . . . . . 11 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → ((LSpan‘𝑊)‘{(𝑘( ·𝑠𝑊)𝑥)}) = ((LSpan‘𝑊)‘{𝑥}))
7978sseq1d 4013 . . . . . . . . . 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 4126 . . . . . . . . . 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 4811 . . . . . . . . . . . . . . . 16 (𝑋 ∈ (Base‘𝑊) → {𝑋} ⊆ (Base‘𝑊))
852, 84, 6syl2an 595 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊))
8685ssdifssd 4142 . . . . . . . . . . . . . 14 ((𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → ((𝐹 ∪ {𝑋}) ∖ {𝑥}) ⊆ (Base‘𝑊))
871, 37, 31lspcl 20819 . . . . . . . . . . . . . 14 ((𝑊 ∈ LMod ∧ ((𝐹 ∪ {𝑋}) ∖ {𝑥}) ⊆ (Base‘𝑊)) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊))
8819, 86, 87syl2an 595 . . . . . . . . . . . . 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 614 . . . . . . . . . . . . . 14 ((𝑊 ∈ LVec ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))))
921, 21, 75, 25lmodvscl 20720 . . . . . . . . . . . . . . 15 ((𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑘( ·𝑠𝑊)𝑥) ∈ (Base‘𝑊))
93923expa 1117 . . . . . . . . . . . . . 14 (((𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑘( ·𝑠𝑊)𝑥) ∈ (Base‘𝑊))
9491, 74, 93syl2an 595 . . . . . . . . . . . . 13 (((𝑊 ∈ LVec ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝐹 ∈ (LIndS‘𝑊) ∧ 𝑥𝐹)) → (𝑘( ·𝑠𝑊)𝑥) ∈ (Base‘𝑊))
9594an42s 658 . . . . . . . . . . . 12 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥𝐹𝑘 ∈ (Base‘(Scalar‘𝑊)))) → (𝑘( ·𝑠𝑊)𝑥) ∈ (Base‘𝑊))
96953adantl3 1167 . . . . . . . . . . 11 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥𝐹𝑘 ∈ (Base‘(Scalar‘𝑊)))) → (𝑘( ·𝑠𝑊)𝑥) ∈ (Base‘𝑊))
971, 37, 31, 83, 90, 96lspsnel5 20838 . . . . . . . . . 10 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥𝐹𝑘 ∈ (Base‘(Scalar‘𝑊)))) → ((𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{(𝑘( ·𝑠𝑊)𝑥)}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
9881, 97sylanr2 680 . . . . . . . . 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, 101lspsnel5 20838 . . . . . . . . . 10 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑥𝐹) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{𝑥}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
103102adantrr 714 . . . . . . . . 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 4813 . . . . . . . . 9 (𝑥𝐹 → ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = 𝐹)
108107fveq2d 6895 . . . . . . . 8 (𝑥𝐹 → ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((LSpan‘𝑊)‘𝐹))
109108eleq2d 2818 . . . . . . 7 (𝑥𝐹 → (𝑋 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) ↔ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)))
110109ad2antrl 725 . . . . . 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 197 . . . 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 4801 . . . . . . . . . . 11 𝑋𝐹 → (𝐹 ∖ {𝑋}) = 𝐹)
11654, 115syl 17 . . . . . . . . . 10 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∖ {𝑋}) = 𝐹)
117116fveq2d 6895 . . . . . . . . 9 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})) = ((LSpan‘𝑊)‘𝐹))
118117eleq2d 2818 . . . . . . . 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 20961 . . . . . . . . . . . . . 14 ((𝑊 ∈ LVec ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0g‘(Scalar‘𝑊))) ∧ 𝑋 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘{(𝑘( ·𝑠𝑊)𝑋)}) = ((LSpan‘𝑊)‘{𝑋}))
1211203expa 1117 . . . . . . . . . . . . 13 (((𝑊 ∈ LVec ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0g‘(Scalar‘𝑊)))) ∧ 𝑋 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘{(𝑘( ·𝑠𝑊)𝑋)}) = ((LSpan‘𝑊)‘{𝑋}))
122121an32s 649 . . . . . . . . . . . 12 (((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0g‘(Scalar‘𝑊)))) → ((LSpan‘𝑊)‘{(𝑘( ·𝑠𝑊)𝑋)}) = ((LSpan‘𝑊)‘{𝑋}))
12371, 122sylan2b 593 . . . . . . . . . . 11 (((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))})) → ((LSpan‘𝑊)‘{(𝑘( ·𝑠𝑊)𝑋)}) = ((LSpan‘𝑊)‘{𝑋}))
124123sseq1d 4013 . . . . . . . . . 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 20819 . . . . . . . . . . . . . 14 ((𝑊 ∈ LMod ∧ 𝐹 ⊆ (Base‘𝑊)) → ((LSpan‘𝑊)‘𝐹) ∈ (LSubSp‘𝑊))
12819, 2, 127syl2an 595 . . . . . . . . . . . . 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 20720 . . . . . . . . . . . . . . 15 ((𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝑘( ·𝑠𝑊)𝑋) ∈ (Base‘𝑊))
1321313expa 1117 . . . . . . . . . . . . . 14 (((𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝑘( ·𝑠𝑊)𝑋) ∈ (Base‘𝑊))
133132an32s 649 . . . . . . . . . . . . 13 (((𝑊 ∈ LMod ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑘( ·𝑠𝑊)𝑋) ∈ (Base‘𝑊))
13419, 133sylanl1 677 . . . . . . . . . . . 12 (((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑘( ·𝑠𝑊)𝑋) ∈ (Base‘𝑊))
1351343adantl2 1166 . . . . . . . . . . 11 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑘( ·𝑠𝑊)𝑋) ∈ (Base‘𝑊))
1361, 37, 31, 126, 130, 135lspsnel5 20838 . . . . . . . . . 10 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → ((𝑘( ·𝑠𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{(𝑘( ·𝑠𝑊)𝑋)}) ⊆ ((LSpan‘𝑊)‘𝐹)))
13781, 136sylan2 592 . . . . . . . . 9 (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))})) → ((𝑘( ·𝑠𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{(𝑘( ·𝑠𝑊)𝑋)}) ⊆ ((LSpan‘𝑊)‘𝐹)))
138 simp3 1137 . . . . . . . . . . 11 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → 𝑋 ∈ (Base‘𝑊))
1391, 37, 31, 82, 129, 138lspsnel5 20838 . . . . . . . . . 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 3145 . . . 4 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})))
146 oveq2 7420 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑘( ·𝑠𝑊)𝑥) = (𝑘( ·𝑠𝑊)𝑋))
147 sneq 4638 . . . . . . . . . . . 12 (𝑥 = 𝑋 → {𝑥} = {𝑋})
148147difeq2d 4122 . . . . . . . . . . 11 (𝑥 = 𝑋 → ((𝐹 ∪ {𝑋}) ∖ {𝑥}) = ((𝐹 ∪ {𝑋}) ∖ {𝑋}))
149 difun2 4480 . . . . . . . . . . 11 ((𝐹 ∪ {𝑋}) ∖ {𝑋}) = (𝐹 ∖ {𝑋})
150148, 149eqtrdi 2787 . . . . . . . . . 10 (𝑥 = 𝑋 → ((𝐹 ∪ {𝑋}) ∖ {𝑥}) = (𝐹 ∖ {𝑋}))
151150fveq2d 6895 . . . . . . . . 9 (𝑥 = 𝑋 → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) = ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})))
152146, 151eleq12d 2826 . . . . . . . 8 (𝑥 = 𝑋 → ((𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ (𝑘( ·𝑠𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋}))))
153152notbid 318 . . . . . . 7 (𝑥 = 𝑋 → (¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ¬ (𝑘( ·𝑠𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋}))))
154153ralbidv 3176 . . . . . 6 (𝑥 = 𝑋 → (∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋}))))
155154ralsng 4677 . . . . 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 4191 . . 3 (∀𝑥 ∈ (𝐹 ∪ {𝑋})∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ (∀𝑥𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∧ ∀𝑥 ∈ {𝑋}∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
159113, 157, 158sylanbrc 582 . 2 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ∀𝑥 ∈ (𝐹 ∪ {𝑋})∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))
1601, 75, 31, 21, 25, 24islinds2 21678 . . 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 710 1 ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∪ {𝑋}) ∈ (LIndS‘𝑊))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  w3a 1086   = wceq 1540  wcel 2105  wne 2939  wral 3060  cdif 3945  cun 3946  cin 3947  wss 3948  c0 4322  {csn 4628  cfv 6543  (class class class)co 7412  Basecbs 17151  Scalarcsca 17207   ·𝑠 cvsca 17208  0gc0g 17392  Ringcrg 20134  NzRingcnzr 20410  LModclmod 20702  LSubSpclss 20774  LSpanclspn 20814  LVecclvec 20946  LIndSclinds 21670
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-cnex 11172  ax-resscn 11173  ax-1cn 11174  ax-icn 11175  ax-addcl 11176  ax-addrcl 11177  ax-mulcl 11178  ax-mulrcl 11179  ax-mulcom 11180  ax-addass 11181  ax-mulass 11182  ax-distr 11183  ax-i2m1 11184  ax-1ne0 11185  ax-1rid 11186  ax-rnegex 11187  ax-rrecex 11188  ax-cnre 11189  ax-pre-lttri 11190  ax-pre-lttrn 11191  ax-pre-ltadd 11192  ax-pre-mulgt0 11193
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7860  df-1st 7979  df-2nd 7980  df-tpos 8217  df-frecs 8272  df-wrecs 8303  df-recs 8377  df-rdg 8416  df-er 8709  df-en 8946  df-dom 8947  df-sdom 8948  df-pnf 11257  df-mnf 11258  df-xr 11259  df-ltxr 11260  df-le 11261  df-sub 11453  df-neg 11454  df-nn 12220  df-2 12282  df-3 12283  df-sets 17104  df-slot 17122  df-ndx 17134  df-base 17152  df-ress 17181  df-plusg 17217  df-mulr 17218  df-0g 17394  df-mgm 18571  df-sgrp 18650  df-mnd 18666  df-grp 18864  df-minusg 18865  df-sbg 18866  df-cmn 19698  df-abl 19699  df-mgp 20036  df-rng 20054  df-ur 20083  df-ring 20136  df-oppr 20232  df-dvdsr 20255  df-unit 20256  df-invr 20286  df-nzr 20411  df-drng 20585  df-lmod 20704  df-lss 20775  df-lsp 20815  df-lvec 20947  df-lindf 21671  df-linds 21672
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator