Step | Hyp | Ref
| Expression |
1 | | lveclmod 20175 |
. . . . . 6
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
2 | 1 | adantr 484 |
. . . . 5
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → 𝑊 ∈ LMod) |
3 | | snssi 4737 |
. . . . . 6
⊢ (𝑋 ∈ 𝑉 → {𝑋} ⊆ 𝑉) |
4 | 3 | adantl 485 |
. . . . 5
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → {𝑋} ⊆ 𝑉) |
5 | | lbslsat.v |
. . . . . 6
⊢ 𝑉 = (Base‘𝑊) |
6 | | eqid 2739 |
. . . . . 6
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) |
7 | | lbslsat.n |
. . . . . 6
⊢ 𝑁 = (LSpan‘𝑊) |
8 | 5, 6, 7 | lspcl 20045 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ {𝑋} ⊆ 𝑉) → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑊)) |
9 | 2, 4, 8 | syl2anc 587 |
. . . 4
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑊)) |
10 | | lbslsat.y |
. . . . 5
⊢ 𝑌 = (𝑊 ↾s (𝑁‘{𝑋})) |
11 | 10, 6 | lsslvec 20176 |
. . . 4
⊢ ((𝑊 ∈ LVec ∧ (𝑁‘{𝑋}) ∈ (LSubSp‘𝑊)) → 𝑌 ∈ LVec) |
12 | 9, 11 | syldan 594 |
. . 3
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → 𝑌 ∈ LVec) |
13 | 12 | 3adant3 1134 |
. 2
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → 𝑌 ∈ LVec) |
14 | 5, 7 | lspssid 20054 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ {𝑋} ⊆ 𝑉) → {𝑋} ⊆ (𝑁‘{𝑋})) |
15 | 2, 4, 14 | syl2anc 587 |
. . . 4
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → {𝑋} ⊆ (𝑁‘{𝑋})) |
16 | 5, 7 | lspssv 20052 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ {𝑋} ⊆ 𝑉) → (𝑁‘{𝑋}) ⊆ 𝑉) |
17 | 2, 4, 16 | syl2anc 587 |
. . . . 5
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ⊆ 𝑉) |
18 | 10, 5 | ressbas2 16823 |
. . . . 5
⊢ ((𝑁‘{𝑋}) ⊆ 𝑉 → (𝑁‘{𝑋}) = (Base‘𝑌)) |
19 | 17, 18 | syl 17 |
. . . 4
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) = (Base‘𝑌)) |
20 | 15, 19 | sseqtrd 3957 |
. . 3
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → {𝑋} ⊆ (Base‘𝑌)) |
21 | 20 | 3adant3 1134 |
. 2
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → {𝑋} ⊆ (Base‘𝑌)) |
22 | 2 | 3adant3 1134 |
. . . 4
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → 𝑊 ∈ LMod) |
23 | 9 | 3adant3 1134 |
. . . 4
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑊)) |
24 | 15 | 3adant3 1134 |
. . . 4
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → {𝑋} ⊆ (𝑁‘{𝑋})) |
25 | | eqid 2739 |
. . . . 5
⊢
(LSpan‘𝑌) =
(LSpan‘𝑌) |
26 | 10, 7, 25, 6 | lsslsp 20084 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ (𝑁‘{𝑋}) ∈ (LSubSp‘𝑊) ∧ {𝑋} ⊆ (𝑁‘{𝑋})) → (𝑁‘{𝑋}) = ((LSpan‘𝑌)‘{𝑋})) |
27 | 22, 23, 24, 26 | syl3anc 1373 |
. . 3
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → (𝑁‘{𝑋}) = ((LSpan‘𝑌)‘{𝑋})) |
28 | 19 | 3adant3 1134 |
. . 3
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → (𝑁‘{𝑋}) = (Base‘𝑌)) |
29 | 27, 28 | eqtr3d 2781 |
. 2
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) →
((LSpan‘𝑌)‘{𝑋}) = (Base‘𝑌)) |
30 | | difid 4301 |
. . . . . . . . . . . . 13
⊢ ({𝑋} ∖ {𝑋}) = ∅ |
31 | 30 | fveq2i 6741 |
. . . . . . . . . . . 12
⊢
((LSpan‘𝑌)‘({𝑋} ∖ {𝑋})) = ((LSpan‘𝑌)‘∅) |
32 | 31 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋})) = ((LSpan‘𝑌)‘∅)) |
33 | 32 | eleq2d 2825 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → (𝑋 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋})) ↔ 𝑋 ∈ ((LSpan‘𝑌)‘∅))) |
34 | 33 | biimpa 480 |
. . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋}))) → 𝑋 ∈ ((LSpan‘𝑌)‘∅)) |
35 | | lveclmod 20175 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ LVec → 𝑌 ∈ LMod) |
36 | | eqid 2739 |
. . . . . . . . . . . 12
⊢
(0g‘𝑌) = (0g‘𝑌) |
37 | 36, 25 | lsp0 20078 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ LMod →
((LSpan‘𝑌)‘∅) =
{(0g‘𝑌)}) |
38 | 12, 35, 37 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → ((LSpan‘𝑌)‘∅) =
{(0g‘𝑌)}) |
39 | 38 | adantr 484 |
. . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋}))) → ((LSpan‘𝑌)‘∅) =
{(0g‘𝑌)}) |
40 | 34, 39 | eleqtrd 2842 |
. . . . . . . 8
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋}))) → 𝑋 ∈ {(0g‘𝑌)}) |
41 | | elsni 4574 |
. . . . . . . 8
⊢ (𝑋 ∈
{(0g‘𝑌)}
→ 𝑋 =
(0g‘𝑌)) |
42 | 40, 41 | syl 17 |
. . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋}))) → 𝑋 = (0g‘𝑌)) |
43 | | lmodgrp 19938 |
. . . . . . . . . 10
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) |
44 | | grpmnd 18404 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Grp → 𝑊 ∈ Mnd) |
45 | 2, 43, 44 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → 𝑊 ∈ Mnd) |
46 | | lbslsat.z |
. . . . . . . . . . 11
⊢ 0 =
(0g‘𝑊) |
47 | 46, 5, 7 | 0ellsp 31310 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ LMod ∧ {𝑋} ⊆ 𝑉) → 0 ∈ (𝑁‘{𝑋})) |
48 | 2, 4, 47 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → 0 ∈ (𝑁‘{𝑋})) |
49 | 10, 5, 46 | ress0g 18233 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Mnd ∧ 0 ∈ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑋}) ⊆ 𝑉) → 0 =
(0g‘𝑌)) |
50 | 45, 48, 17, 49 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → 0 =
(0g‘𝑌)) |
51 | 50 | adantr 484 |
. . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋}))) → 0 =
(0g‘𝑌)) |
52 | 42, 51 | eqtr4d 2782 |
. . . . . 6
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋}))) → 𝑋 = 0 ) |
53 | 52 | ex 416 |
. . . . 5
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → (𝑋 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋})) → 𝑋 = 0 )) |
54 | 53 | necon3ad 2956 |
. . . 4
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → (𝑋 ≠ 0 → ¬ 𝑋 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋})))) |
55 | 54 | 3impia 1119 |
. . 3
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ¬ 𝑋 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋}))) |
56 | | id 22 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋) |
57 | | sneq 4567 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → {𝑥} = {𝑋}) |
58 | 57 | difeq2d 4053 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → ({𝑋} ∖ {𝑥}) = ({𝑋} ∖ {𝑋})) |
59 | 58 | fveq2d 6742 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → ((LSpan‘𝑌)‘({𝑋} ∖ {𝑥})) = ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋}))) |
60 | 56, 59 | eleq12d 2834 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (𝑥 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑥})) ↔ 𝑋 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋})))) |
61 | 60 | notbid 321 |
. . . . 5
⊢ (𝑥 = 𝑋 → (¬ 𝑥 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑥})) ↔ ¬ 𝑋 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋})))) |
62 | 61 | ralsng 4605 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → (∀𝑥 ∈ {𝑋} ¬ 𝑥 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑥})) ↔ ¬ 𝑋 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋})))) |
63 | 62 | 3ad2ant2 1136 |
. . 3
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → (∀𝑥 ∈ {𝑋} ¬ 𝑥 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑥})) ↔ ¬ 𝑋 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋})))) |
64 | 55, 63 | mpbird 260 |
. 2
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ∀𝑥 ∈ {𝑋} ¬ 𝑥 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑥}))) |
65 | | eqid 2739 |
. . . 4
⊢
(Base‘𝑌) =
(Base‘𝑌) |
66 | | eqid 2739 |
. . . 4
⊢
(LBasis‘𝑌) =
(LBasis‘𝑌) |
67 | 65, 66, 25 | islbs2 20223 |
. . 3
⊢ (𝑌 ∈ LVec → ({𝑋} ∈ (LBasis‘𝑌) ↔ ({𝑋} ⊆ (Base‘𝑌) ∧ ((LSpan‘𝑌)‘{𝑋}) = (Base‘𝑌) ∧ ∀𝑥 ∈ {𝑋} ¬ 𝑥 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑥}))))) |
68 | 67 | biimpar 481 |
. 2
⊢ ((𝑌 ∈ LVec ∧ ({𝑋} ⊆ (Base‘𝑌) ∧ ((LSpan‘𝑌)‘{𝑋}) = (Base‘𝑌) ∧ ∀𝑥 ∈ {𝑋} ¬ 𝑥 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑥})))) → {𝑋} ∈ (LBasis‘𝑌)) |
69 | 13, 21, 29, 64, 68 | syl13anc 1374 |
1
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → {𝑋} ∈ (LBasis‘𝑌)) |