Step | Hyp | Ref
| Expression |
1 | | eqid 2825 |
. . . . 5
⊢
(Base‘𝑊) =
(Base‘𝑊) |
2 | 1 | linds1 20523 |
. . . 4
⊢ (𝐹 ∈ (LIndS‘𝑊) → 𝐹 ⊆ (Base‘𝑊)) |
3 | | eldifi 3961 |
. . . . 5
⊢ (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) → 𝑋 ∈ (Base‘𝑊)) |
4 | 3 | snssd 4560 |
. . . 4
⊢ (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) → {𝑋} ⊆ (Base‘𝑊)) |
5 | | unss 4016 |
. . . . 5
⊢ ((𝐹 ⊆ (Base‘𝑊) ∧ {𝑋} ⊆ (Base‘𝑊)) ↔ (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊)) |
6 | 5 | biimpi 208 |
. . . 4
⊢ ((𝐹 ⊆ (Base‘𝑊) ∧ {𝑋} ⊆ (Base‘𝑊)) → (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊)) |
7 | 2, 4, 6 | syl2an 589 |
. . 3
⊢ ((𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊)) |
8 | 7 | 3adant1 1164 |
. 2
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊)) |
9 | | eldifn 3962 |
. . . . . . 7
⊢ (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) → ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)) |
10 | 9 | 3ad2ant3 1169 |
. . . . . 6
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)) |
11 | 10 | adantr 474 |
. . . . 5
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)) |
12 | | simpll1 1273 |
. . . . . . . 8
⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → 𝑊 ∈ LVec) |
13 | 2 | ssdifssd 3977 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (LIndS‘𝑊) → (𝐹 ∖ {𝑥}) ⊆ (Base‘𝑊)) |
14 | 13 | 3ad2ant2 1168 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∖ {𝑥}) ⊆ (Base‘𝑊)) |
15 | 14 | ad2antrr 717 |
. . . . . . . 8
⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → (𝐹 ∖ {𝑥}) ⊆ (Base‘𝑊)) |
16 | 3 | 3ad2ant3 1169 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → 𝑋 ∈ (Base‘𝑊)) |
17 | 16 | ad2antrr 717 |
. . . . . . . 8
⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → 𝑋 ∈ (Base‘𝑊)) |
18 | | simpr 479 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) |
19 | | lveclmod 19472 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
20 | 19 | ad2antrr 717 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → 𝑊 ∈ LMod) |
21 | | eqid 2825 |
. . . . . . . . . . . . . . . 16
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
22 | 21 | lmodring 19234 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ LMod →
(Scalar‘𝑊) ∈
Ring) |
23 | 19, 22 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ LVec →
(Scalar‘𝑊) ∈
Ring) |
24 | 23 | ad2antrr 717 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → (Scalar‘𝑊) ∈ Ring) |
25 | | df2o2 7846 |
. . . . . . . . . . . . . . 15
⊢
2o = {∅, {∅}} |
26 | | 0nep0 5060 |
. . . . . . . . . . . . . . . . . . 19
⊢ ∅
≠ {∅} |
27 | | eldifsni 4542 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) → 𝑘 ≠
(0g‘(Scalar‘𝑊))) |
28 | | 0ex 5016 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∅
∈ V |
29 | | vex 3417 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑘 ∈ V |
30 | | p0ex 5085 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {∅}
∈ V |
31 | | fvex 6450 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(0g‘(Scalar‘𝑊)) ∈ V |
32 | | f1oprg 6426 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((∅ ∈ V ∧ 𝑘 ∈ V) ∧ ({∅} ∈ V ∧
(0g‘(Scalar‘𝑊)) ∈ V)) → ((∅ ≠
{∅} ∧ 𝑘 ≠
(0g‘(Scalar‘𝑊))) → {〈∅, 𝑘〉, 〈{∅},
(0g‘(Scalar‘𝑊))〉}:{∅, {∅}}–1-1-onto→{𝑘, (0g‘(Scalar‘𝑊))})) |
33 | 28, 29, 30, 31, 32 | mp4an 684 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((∅
≠ {∅} ∧ 𝑘 ≠
(0g‘(Scalar‘𝑊))) → {〈∅, 𝑘〉, 〈{∅},
(0g‘(Scalar‘𝑊))〉}:{∅, {∅}}–1-1-onto→{𝑘, (0g‘(Scalar‘𝑊))}) |
34 | 26, 27, 33 | sylancr 581 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) → {〈∅, 𝑘〉, 〈{∅},
(0g‘(Scalar‘𝑊))〉}:{∅, {∅}}–1-1-onto→{𝑘, (0g‘(Scalar‘𝑊))}) |
35 | | f1of1 6381 |
. . . . . . . . . . . . . . . . . 18
⊢
({〈∅, 𝑘〉, 〈{∅},
(0g‘(Scalar‘𝑊))〉}:{∅, {∅}}–1-1-onto→{𝑘, (0g‘(Scalar‘𝑊))} → {〈∅, 𝑘〉, 〈{∅},
(0g‘(Scalar‘𝑊))〉}:{∅, {∅}}–1-1→{𝑘, (0g‘(Scalar‘𝑊))}) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) → {〈∅, 𝑘〉, 〈{∅},
(0g‘(Scalar‘𝑊))〉}:{∅, {∅}}–1-1→{𝑘, (0g‘(Scalar‘𝑊))}) |
37 | | eldifi 3961 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) → 𝑘 ∈ (Base‘(Scalar‘𝑊))) |
38 | 21 | lmodfgrp 19235 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑊 ∈ LMod →
(Scalar‘𝑊) ∈
Grp) |
39 | | eqid 2825 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
40 | | eqid 2825 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) |
41 | 39, 40 | grpidcl 17811 |
. . . . . . . . . . . . . . . . . . 19
⊢
((Scalar‘𝑊)
∈ Grp → (0g‘(Scalar‘𝑊)) ∈ (Base‘(Scalar‘𝑊))) |
42 | 19, 38, 41 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑊 ∈ LVec →
(0g‘(Scalar‘𝑊)) ∈ (Base‘(Scalar‘𝑊))) |
43 | | prssi 4572 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈
(Base‘(Scalar‘𝑊)) ∧
(0g‘(Scalar‘𝑊)) ∈ (Base‘(Scalar‘𝑊))) → {𝑘, (0g‘(Scalar‘𝑊))} ⊆
(Base‘(Scalar‘𝑊))) |
44 | 37, 42, 43 | syl2anr 590 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ LVec ∧ 𝑘 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → {𝑘, (0g‘(Scalar‘𝑊))} ⊆
(Base‘(Scalar‘𝑊))) |
45 | | f1ss 6347 |
. . . . . . . . . . . . . . . . 17
⊢
(({〈∅, 𝑘〉, 〈{∅},
(0g‘(Scalar‘𝑊))〉}:{∅, {∅}}–1-1→{𝑘, (0g‘(Scalar‘𝑊))} ∧ {𝑘, (0g‘(Scalar‘𝑊))} ⊆
(Base‘(Scalar‘𝑊))) → {〈∅, 𝑘〉, 〈{∅},
(0g‘(Scalar‘𝑊))〉}:{∅, {∅}}–1-1→(Base‘(Scalar‘𝑊))) |
46 | 36, 44, 45 | syl2an2 677 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LVec ∧ 𝑘 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → {〈∅, 𝑘〉, 〈{∅},
(0g‘(Scalar‘𝑊))〉}:{∅, {∅}}–1-1→(Base‘(Scalar‘𝑊))) |
47 | | fvex 6450 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘(Scalar‘𝑊)) ∈ V |
48 | 47 | f1dom 8250 |
. . . . . . . . . . . . . . . 16
⊢
({〈∅, 𝑘〉, 〈{∅},
(0g‘(Scalar‘𝑊))〉}:{∅, {∅}}–1-1→(Base‘(Scalar‘𝑊)) → {∅, {∅}}
≼ (Base‘(Scalar‘𝑊))) |
49 | 46, 48 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ LVec ∧ 𝑘 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → {∅, {∅}} ≼
(Base‘(Scalar‘𝑊))) |
50 | 25, 49 | syl5eqbr 4910 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ LVec ∧ 𝑘 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → 2o ≼
(Base‘(Scalar‘𝑊))) |
51 | 50 | ad2ant2rl 755 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → 2o ≼
(Base‘(Scalar‘𝑊))) |
52 | 39 | isnzr2 19631 |
. . . . . . . . . . . . 13
⊢
((Scalar‘𝑊)
∈ NzRing ↔ ((Scalar‘𝑊) ∈ Ring ∧ 2o ≼
(Base‘(Scalar‘𝑊)))) |
53 | 24, 51, 52 | sylanbrc 578 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → (Scalar‘𝑊) ∈
NzRing) |
54 | | simplr 785 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → 𝐹 ∈ (LIndS‘𝑊)) |
55 | | simprl 787 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → 𝑥 ∈ 𝐹) |
56 | | eqid 2825 |
. . . . . . . . . . . . 13
⊢
(LSpan‘𝑊) =
(LSpan‘𝑊) |
57 | 56, 21 | lindsind2 20532 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ LMod ∧
(Scalar‘𝑊) ∈
NzRing) ∧ 𝐹 ∈
(LIndS‘𝑊) ∧ 𝑥 ∈ 𝐹) → ¬ 𝑥 ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥}))) |
58 | 20, 53, 54, 55, 57 | syl211anc 1499 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → ¬ 𝑥 ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥}))) |
59 | 58 | 3adantl3 1213 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → ¬ 𝑥 ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥}))) |
60 | 59 | adantr 474 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → ¬ 𝑥 ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥}))) |
61 | 18, 60 | eldifd 3809 |
. . . . . . . 8
⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → 𝑥 ∈ (((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ∖ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥})))) |
62 | | eqid 2825 |
. . . . . . . . 9
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) |
63 | 1, 62, 56 | lspsolv 19510 |
. . . . . . . 8
⊢ ((𝑊 ∈ LVec ∧ ((𝐹 ∖ {𝑥}) ⊆ (Base‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊) ∧ 𝑥 ∈ (((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ∖ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥}))))) → 𝑋 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥}))) |
64 | 12, 15, 17, 61, 63 | syl13anc 1495 |
. . . . . . 7
⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → 𝑋 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥}))) |
65 | 64 | ex 403 |
. . . . . 6
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) → 𝑋 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))) |
66 | | eldif 3808 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) ↔ (𝑋 ∈ (Base‘𝑊) ∧ ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))) |
67 | | snssi 4559 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑋 ∈ 𝐹 → {𝑋} ⊆ 𝐹) |
68 | 1, 56 | lspss 19350 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑊 ∈ LMod ∧ 𝐹 ⊆ (Base‘𝑊) ∧ {𝑋} ⊆ 𝐹) → ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹)) |
69 | 19, 2, 67, 68 | syl3an 1203 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ 𝐹) → ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹)) |
70 | 69 | ad4ant124 1219 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑋 ∈ 𝐹) → ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹)) |
71 | 1, 56 | lspsnid 19359 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ (Base‘𝑊)) → 𝑋 ∈ ((LSpan‘𝑊)‘{𝑋})) |
72 | 19, 71 | sylan 575 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) → 𝑋 ∈ ((LSpan‘𝑊)‘{𝑋})) |
73 | 72 | ad4ant13 757 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑋 ∈ 𝐹) → 𝑋 ∈ ((LSpan‘𝑊)‘{𝑋})) |
74 | 70, 73 | sseldd 3828 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑋 ∈ 𝐹) → 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)) |
75 | 74 | ex 403 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝑋 ∈ 𝐹 → 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))) |
76 | 75 | con3d 150 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) → (¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹) → ¬ 𝑋 ∈ 𝐹)) |
77 | 76 | expimpd 447 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) → ((𝑋 ∈ (Base‘𝑊) ∧ ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)) → ¬ 𝑋 ∈ 𝐹)) |
78 | 77 | 3impia 1149 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ (𝑋 ∈ (Base‘𝑊) ∧ ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))) → ¬ 𝑋 ∈ 𝐹) |
79 | 66, 78 | syl3an3b 1528 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ¬ 𝑋 ∈ 𝐹) |
80 | | eleq1 2894 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑋 = 𝑥 → (𝑋 ∈ 𝐹 ↔ 𝑥 ∈ 𝐹)) |
81 | 80 | notbid 310 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑋 = 𝑥 → (¬ 𝑋 ∈ 𝐹 ↔ ¬ 𝑥 ∈ 𝐹)) |
82 | 79, 81 | syl5ibcom 237 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝑋 = 𝑥 → ¬ 𝑥 ∈ 𝐹)) |
83 | 82 | necon2ad 3014 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝑥 ∈ 𝐹 → 𝑋 ≠ 𝑥)) |
84 | 83 | imp 397 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → 𝑋 ≠ 𝑥) |
85 | | disjsn2 4468 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ≠ 𝑥 → ({𝑋} ∩ {𝑥}) = ∅) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → ({𝑋} ∩ {𝑥}) = ∅) |
87 | | disj3 4247 |
. . . . . . . . . . . . 13
⊢ (({𝑋} ∩ {𝑥}) = ∅ ↔ {𝑋} = ({𝑋} ∖ {𝑥})) |
88 | 86, 87 | sylib 210 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → {𝑋} = ({𝑋} ∖ {𝑥})) |
89 | 88 | uneq2d 3996 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → ((𝐹 ∖ {𝑥}) ∪ {𝑋}) = ((𝐹 ∖ {𝑥}) ∪ ({𝑋} ∖ {𝑥}))) |
90 | | difundir 4112 |
. . . . . . . . . . 11
⊢ ((𝐹 ∪ {𝑋}) ∖ {𝑥}) = ((𝐹 ∖ {𝑥}) ∪ ({𝑋} ∖ {𝑥})) |
91 | 89, 90 | syl6eqr 2879 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → ((𝐹 ∖ {𝑥}) ∪ {𝑋}) = ((𝐹 ∪ {𝑋}) ∖ {𝑥})) |
92 | 91 | fveq2d 6441 |
. . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) = ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))) |
93 | 92 | eleq2d 2892 |
. . . . . . . 8
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ↔ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))) |
94 | 93 | adantrr 708 |
. . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ↔ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))) |
95 | | simpl 476 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LVec ∧ 𝑘 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → 𝑊 ∈ LVec) |
96 | | eldifsn 4538 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ↔ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠
(0g‘(Scalar‘𝑊)))) |
97 | 96 | biimpi 208 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) → (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠
(0g‘(Scalar‘𝑊)))) |
98 | 97 | adantl 475 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LVec ∧ 𝑘 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠
(0g‘(Scalar‘𝑊)))) |
99 | 2 | sselda 3827 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (LIndS‘𝑊) ∧ 𝑥 ∈ 𝐹) → 𝑥 ∈ (Base‘𝑊)) |
100 | | eqid 2825 |
. . . . . . . . . . . . . 14
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
101 | 1, 21, 100, 39, 40, 56 | lspsnvs 19480 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LVec ∧ (𝑘 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠
(0g‘(Scalar‘𝑊))) ∧ 𝑥 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑥)}) = ((LSpan‘𝑊)‘{𝑥})) |
102 | 95, 98, 99, 101 | syl2an3an 1549 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ LVec ∧ 𝑘 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) ∧ (𝐹 ∈ (LIndS‘𝑊) ∧ 𝑥 ∈ 𝐹)) → ((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑥)}) = ((LSpan‘𝑊)‘{𝑥})) |
103 | 102 | an42s 651 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → ((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑥)}) = ((LSpan‘𝑊)‘{𝑥})) |
104 | 103 | sseq1d 3857 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → (((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑥)}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{𝑥}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))) |
105 | 104 | 3adantl3 1213 |
. . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → (((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑥)}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{𝑥}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))) |
106 | 19 | 3ad2ant1 1167 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → 𝑊 ∈ LMod) |
107 | 106 | adantr 474 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)))) → 𝑊 ∈ LMod) |
108 | | snssi 4559 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ (Base‘𝑊) → {𝑋} ⊆ (Base‘𝑊)) |
109 | 2, 108, 6 | syl2an 589 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊)) |
110 | 109 | ssdifssd 3977 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → ((𝐹 ∪ {𝑋}) ∖ {𝑥}) ⊆ (Base‘𝑊)) |
111 | 1, 62, 56 | lspcl 19342 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ LMod ∧ ((𝐹 ∪ {𝑋}) ∖ {𝑥}) ⊆ (Base‘𝑊)) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊)) |
112 | 19, 110, 111 | syl2an 589 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LVec ∧ (𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊))) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊)) |
113 | 112 | 3impb 1147 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊)) |
114 | 113 | adantr 474 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)))) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊)) |
115 | 19 | anim1i 608 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ LVec ∧ 𝑘 ∈
(Base‘(Scalar‘𝑊))) → (𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)))) |
116 | 1, 21, 100, 39 | lmodvscl 19243 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑘( ·𝑠
‘𝑊)𝑥) ∈ (Base‘𝑊)) |
117 | 116 | 3expa 1151 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ LMod ∧ 𝑘 ∈
(Base‘(Scalar‘𝑊))) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑘( ·𝑠
‘𝑊)𝑥) ∈ (Base‘𝑊)) |
118 | 115, 99, 117 | syl2an 589 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ LVec ∧ 𝑘 ∈
(Base‘(Scalar‘𝑊))) ∧ (𝐹 ∈ (LIndS‘𝑊) ∧ 𝑥 ∈ 𝐹)) → (𝑘( ·𝑠
‘𝑊)𝑥) ∈ (Base‘𝑊)) |
119 | 118 | an42s 651 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)))) → (𝑘( ·𝑠
‘𝑊)𝑥) ∈ (Base‘𝑊)) |
120 | 119 | 3adantl3 1213 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)))) → (𝑘( ·𝑠
‘𝑊)𝑥) ∈ (Base‘𝑊)) |
121 | 1, 62, 56, 107, 114, 120 | lspsnel5 19361 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)))) → ((𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑥)}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))) |
122 | 37, 121 | sylanr2 673 |
. . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → ((𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑥)}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))) |
123 | 106 | adantr 474 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑥 ∈ 𝐹) → 𝑊 ∈ LMod) |
124 | 113 | adantr 474 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑥 ∈ 𝐹) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊)) |
125 | 99 | 3ad2antl2 1241 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑥 ∈ 𝐹) → 𝑥 ∈ (Base‘𝑊)) |
126 | 1, 62, 56, 123, 124, 125 | lspsnel5 19361 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑥 ∈ 𝐹) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{𝑥}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))) |
127 | 126 | adantrr 708 |
. . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{𝑥}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))) |
128 | 105, 122,
127 | 3bitr4rd 304 |
. . . . . . . 8
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))) |
129 | 3, 128 | syl3anl3 1540 |
. . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))) |
130 | 94, 129 | bitrd 271 |
. . . . . 6
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ↔ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))) |
131 | | difsnid 4561 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐹 → ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = 𝐹) |
132 | 131 | fveq2d 6441 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐹 → ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((LSpan‘𝑊)‘𝐹)) |
133 | 132 | eleq2d 2892 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐹 → (𝑋 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) ↔ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))) |
134 | 133 | ad2antrl 719 |
. . . . . 6
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → (𝑋 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) ↔ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))) |
135 | 65, 130, 134 | 3imtr3d 285 |
. . . . 5
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → ((𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) → 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))) |
136 | 11, 135 | mtod 190 |
. . . 4
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))) |
137 | 136 | ralrimivva 3180 |
. . 3
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))) |
138 | 10 | adantr 474 |
. . . . . 6
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)) |
139 | | difsn 4549 |
. . . . . . . . . . 11
⊢ (¬
𝑋 ∈ 𝐹 → (𝐹 ∖ {𝑋}) = 𝐹) |
140 | 79, 139 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∖ {𝑋}) = 𝐹) |
141 | 140 | fveq2d 6441 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})) = ((LSpan‘𝑊)‘𝐹)) |
142 | 141 | eleq2d 2892 |
. . . . . . . 8
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ((𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})) ↔ (𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹))) |
143 | 142 | adantr 474 |
. . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → ((𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})) ↔ (𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹))) |
144 | 1, 21, 100, 39, 40, 56 | lspsnvs 19480 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ LVec ∧ (𝑘 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠
(0g‘(Scalar‘𝑊))) ∧ 𝑋 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑋)}) = ((LSpan‘𝑊)‘{𝑋})) |
145 | 144 | 3expa 1151 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ LVec ∧ (𝑘 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠
(0g‘(Scalar‘𝑊)))) ∧ 𝑋 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑋)}) = ((LSpan‘𝑊)‘{𝑋})) |
146 | 145 | an32s 642 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠
(0g‘(Scalar‘𝑊)))) → ((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑋)}) = ((LSpan‘𝑊)‘{𝑋})) |
147 | 96, 146 | sylan2b 587 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → ((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑋)}) = ((LSpan‘𝑊)‘{𝑋})) |
148 | 147 | sseq1d 3857 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → (((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑋)}) ⊆ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹))) |
149 | 148 | 3adantl2 1212 |
. . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → (((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑋)}) ⊆ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹))) |
150 | 106 | adantr 474 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → 𝑊 ∈ LMod) |
151 | 1, 62, 56 | lspcl 19342 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ LMod ∧ 𝐹 ⊆ (Base‘𝑊)) → ((LSpan‘𝑊)‘𝐹) ∈ (LSubSp‘𝑊)) |
152 | 19, 2, 151 | syl2an 589 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) → ((LSpan‘𝑊)‘𝐹) ∈ (LSubSp‘𝑊)) |
153 | 152 | 3adant3 1166 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘𝐹) ∈ (LSubSp‘𝑊)) |
154 | 153 | adantr 474 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → ((LSpan‘𝑊)‘𝐹) ∈ (LSubSp‘𝑊)) |
155 | 1, 21, 100, 39 | lmodvscl 19243 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝑘( ·𝑠
‘𝑊)𝑋) ∈ (Base‘𝑊)) |
156 | 155 | 3expa 1151 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ LMod ∧ 𝑘 ∈
(Base‘(Scalar‘𝑊))) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝑘( ·𝑠
‘𝑊)𝑋) ∈ (Base‘𝑊)) |
157 | 156 | an32s 642 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑘( ·𝑠
‘𝑊)𝑋) ∈ (Base‘𝑊)) |
158 | 19, 157 | sylanl1 670 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑘( ·𝑠
‘𝑊)𝑋) ∈ (Base‘𝑊)) |
159 | 158 | 3adantl2 1212 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑘( ·𝑠
‘𝑊)𝑋) ∈ (Base‘𝑊)) |
160 | 1, 62, 56, 150, 154, 159 | lspsnel5 19361 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → ((𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑋)}) ⊆ ((LSpan‘𝑊)‘𝐹))) |
161 | 37, 160 | sylan2 586 |
. . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → ((𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{(𝑘( ·𝑠
‘𝑊)𝑋)}) ⊆ ((LSpan‘𝑊)‘𝐹))) |
162 | | simp3 1172 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → 𝑋 ∈ (Base‘𝑊)) |
163 | 1, 62, 56, 106, 153, 162 | lspsnel5 19361 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝑋 ∈ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹))) |
164 | 163 | adantr 474 |
. . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → (𝑋 ∈ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹))) |
165 | 149, 161,
164 | 3bitr4d 303 |
. . . . . . . 8
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → ((𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹) ↔ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))) |
166 | 3, 165 | syl3anl3 1540 |
. . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → ((𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹) ↔ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))) |
167 | 143, 166 | bitrd 271 |
. . . . . 6
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → ((𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})) ↔ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))) |
168 | 138, 167 | mtbird 317 |
. . . . 5
⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → ¬ (𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋}))) |
169 | 168 | ralrimiva 3175 |
. . . 4
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋}))) |
170 | | oveq2 6918 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝑘( ·𝑠
‘𝑊)𝑥) = (𝑘( ·𝑠
‘𝑊)𝑋)) |
171 | | sneq 4409 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑋 → {𝑥} = {𝑋}) |
172 | 171 | difeq2d 3957 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → ((𝐹 ∪ {𝑋}) ∖ {𝑥}) = ((𝐹 ∪ {𝑋}) ∖ {𝑋})) |
173 | | difun2 4273 |
. . . . . . . . . . 11
⊢ ((𝐹 ∪ {𝑋}) ∖ {𝑋}) = (𝐹 ∖ {𝑋}) |
174 | 172, 173 | syl6eq 2877 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → ((𝐹 ∪ {𝑋}) ∖ {𝑥}) = (𝐹 ∖ {𝑋})) |
175 | 174 | fveq2d 6441 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) = ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋}))) |
176 | 170, 175 | eleq12d 2900 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → ((𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ (𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})))) |
177 | 176 | notbid 310 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ¬ (𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})))) |
178 | 177 | ralbidv 3195 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})))) |
179 | 178 | ralsng 4440 |
. . . . 5
⊢ (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) → (∀𝑥 ∈ {𝑋}∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})))) |
180 | 179 | 3ad2ant3 1169 |
. . . 4
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (∀𝑥 ∈ {𝑋}∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})))) |
181 | 169, 180 | mpbird 249 |
. . 3
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ∀𝑥 ∈ {𝑋}∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))) |
182 | | ralunb 4023 |
. . 3
⊢
(∀𝑥 ∈
(𝐹 ∪ {𝑋})∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ (∀𝑥 ∈ 𝐹 ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∧ ∀𝑥 ∈ {𝑋}∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))) |
183 | 137, 181,
182 | sylanbrc 578 |
. 2
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ∀𝑥 ∈ (𝐹 ∪ {𝑋})∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))) |
184 | 1, 100, 56, 21, 39, 40 | islinds2 20526 |
. . 3
⊢ (𝑊 ∈ LVec → ((𝐹 ∪ {𝑋}) ∈ (LIndS‘𝑊) ↔ ((𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊) ∧ ∀𝑥 ∈ (𝐹 ∪ {𝑋})∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))) |
185 | 184 | 3ad2ant1 1167 |
. 2
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ((𝐹 ∪ {𝑋}) ∈ (LIndS‘𝑊) ↔ ((𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊) ∧ ∀𝑥 ∈ (𝐹 ∪ {𝑋})∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))) |
186 | 8, 183, 185 | mpbir2and 704 |
1
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∪ {𝑋}) ∈ (LIndS‘𝑊)) |