Step | Hyp | Ref
| Expression |
1 | | simp1 1135 |
. 2
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → 𝑊 ∈ LVec) |
2 | | snssi 4741 |
. . 3
⊢ (𝑋 ∈ 𝐵 → {𝑋} ⊆ 𝐵) |
3 | 2 | 3ad2ant2 1133 |
. 2
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → {𝑋} ⊆ 𝐵) |
4 | | simpr 485 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → 𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) |
5 | | eldifsni 4723 |
. . . . . . . . . 10
⊢ (𝑦 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) → 𝑦 ≠
(0g‘(Scalar‘𝑊))) |
6 | 4, 5 | syl 17 |
. . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → 𝑦 ≠
(0g‘(Scalar‘𝑊))) |
7 | 6 | neneqd 2948 |
. . . . . . . 8
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → ¬ 𝑦 = (0g‘(Scalar‘𝑊))) |
8 | | simpl3 1192 |
. . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → 𝑋 ≠ 0 ) |
9 | 8 | neneqd 2948 |
. . . . . . . 8
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → ¬ 𝑋 = 0 ) |
10 | | ioran 981 |
. . . . . . . 8
⊢ (¬
(𝑦 =
(0g‘(Scalar‘𝑊)) ∨ 𝑋 = 0 ) ↔ (¬ 𝑦 =
(0g‘(Scalar‘𝑊)) ∧ ¬ 𝑋 = 0 )) |
11 | 7, 9, 10 | sylanbrc 583 |
. . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → ¬ (𝑦 = (0g‘(Scalar‘𝑊)) ∨ 𝑋 = 0 )) |
12 | | lindssn.1 |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑊) |
13 | | eqid 2738 |
. . . . . . . . 9
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
14 | | eqid 2738 |
. . . . . . . . 9
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
15 | | eqid 2738 |
. . . . . . . . 9
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
16 | | eqid 2738 |
. . . . . . . . 9
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) |
17 | | lindssn.2 |
. . . . . . . . 9
⊢ 0 =
(0g‘𝑊) |
18 | 1 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → 𝑊 ∈ LVec) |
19 | 4 | eldifad 3899 |
. . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → 𝑦 ∈ (Base‘(Scalar‘𝑊))) |
20 | | simpl2 1191 |
. . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → 𝑋 ∈ 𝐵) |
21 | 12, 13, 14, 15, 16, 17, 18, 19, 20 | lvecvs0or 20370 |
. . . . . . . 8
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → ((𝑦( ·𝑠
‘𝑊)𝑋) = 0 ↔ (𝑦 = (0g‘(Scalar‘𝑊)) ∨ 𝑋 = 0 ))) |
22 | 21 | necon3abid 2980 |
. . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → ((𝑦( ·𝑠
‘𝑊)𝑋) ≠ 0 ↔ ¬ (𝑦 =
(0g‘(Scalar‘𝑊)) ∨ 𝑋 = 0 ))) |
23 | 11, 22 | mpbird 256 |
. . . . . 6
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → (𝑦( ·𝑠
‘𝑊)𝑋) ≠ 0 ) |
24 | | nelsn 4601 |
. . . . . 6
⊢ ((𝑦(
·𝑠 ‘𝑊)𝑋) ≠ 0 → ¬ (𝑦(
·𝑠 ‘𝑊)𝑋) ∈ { 0 }) |
25 | 23, 24 | syl 17 |
. . . . 5
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → ¬ (𝑦( ·𝑠
‘𝑊)𝑋) ∈ { 0 }) |
26 | | difid 4304 |
. . . . . . . 8
⊢ ({𝑋} ∖ {𝑋}) = ∅ |
27 | 26 | a1i 11 |
. . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → ({𝑋} ∖ {𝑋}) = ∅) |
28 | 27 | fveq2d 6778 |
. . . . . 6
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → ((LSpan‘𝑊)‘({𝑋} ∖ {𝑋})) = ((LSpan‘𝑊)‘∅)) |
29 | | lveclmod 20368 |
. . . . . . . 8
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
30 | | eqid 2738 |
. . . . . . . . 9
⊢
(LSpan‘𝑊) =
(LSpan‘𝑊) |
31 | 17, 30 | lsp0 20271 |
. . . . . . . 8
⊢ (𝑊 ∈ LMod →
((LSpan‘𝑊)‘∅) = { 0 }) |
32 | 1, 29, 31 | 3syl 18 |
. . . . . . 7
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) →
((LSpan‘𝑊)‘∅) = { 0 }) |
33 | 32 | adantr 481 |
. . . . . 6
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → ((LSpan‘𝑊)‘∅) = { 0 }) |
34 | 28, 33 | eqtrd 2778 |
. . . . 5
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → ((LSpan‘𝑊)‘({𝑋} ∖ {𝑋})) = { 0 }) |
35 | 25, 34 | neleqtrrd 2861 |
. . . 4
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) → ¬ (𝑦( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘({𝑋} ∖ {𝑋}))) |
36 | 35 | ralrimiva 3103 |
. . 3
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ∀𝑦 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑦( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘({𝑋} ∖ {𝑋}))) |
37 | | oveq2 7283 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝑦( ·𝑠
‘𝑊)𝑥) = (𝑦( ·𝑠
‘𝑊)𝑋)) |
38 | | sneq 4571 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → {𝑥} = {𝑋}) |
39 | 38 | difeq2d 4057 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → ({𝑋} ∖ {𝑥}) = ({𝑋} ∖ {𝑋})) |
40 | 39 | fveq2d 6778 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → ((LSpan‘𝑊)‘({𝑋} ∖ {𝑥})) = ((LSpan‘𝑊)‘({𝑋} ∖ {𝑋}))) |
41 | 37, 40 | eleq12d 2833 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → ((𝑦( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘({𝑋} ∖ {𝑥})) ↔ (𝑦( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘({𝑋} ∖ {𝑋})))) |
42 | 41 | notbid 318 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (¬ (𝑦( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘({𝑋} ∖ {𝑥})) ↔ ¬ (𝑦( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘({𝑋} ∖ {𝑋})))) |
43 | 42 | ralbidv 3112 |
. . . . 5
⊢ (𝑥 = 𝑋 → (∀𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑦( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘({𝑋} ∖ {𝑥})) ↔ ∀𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑦( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘({𝑋} ∖ {𝑋})))) |
44 | 43 | ralsng 4609 |
. . . 4
⊢ (𝑋 ∈ 𝐵 → (∀𝑥 ∈ {𝑋}∀𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑦( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘({𝑋} ∖ {𝑥})) ↔ ∀𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑦( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘({𝑋} ∖ {𝑋})))) |
45 | 44 | 3ad2ant2 1133 |
. . 3
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (∀𝑥 ∈ {𝑋}∀𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑦( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘({𝑋} ∖ {𝑥})) ↔ ∀𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑦( ·𝑠
‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘({𝑋} ∖ {𝑋})))) |
46 | 36, 45 | mpbird 256 |
. 2
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ∀𝑥 ∈ {𝑋}∀𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑦( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘({𝑋} ∖ {𝑥}))) |
47 | 12, 13, 30, 14, 15, 16 | islinds2 21020 |
. . 3
⊢ (𝑊 ∈ LVec → ({𝑋} ∈ (LIndS‘𝑊) ↔ ({𝑋} ⊆ 𝐵 ∧ ∀𝑥 ∈ {𝑋}∀𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑦( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘({𝑋} ∖ {𝑥}))))) |
48 | 47 | biimpar 478 |
. 2
⊢ ((𝑊 ∈ LVec ∧ ({𝑋} ⊆ 𝐵 ∧ ∀𝑥 ∈ {𝑋}∀𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑦( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘({𝑋} ∖ {𝑥})))) → {𝑋} ∈ (LIndS‘𝑊)) |
49 | 1, 3, 46, 48 | syl12anc 834 |
1
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → {𝑋} ∈ (LIndS‘𝑊)) |