| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | lveclmod 21105 | . . . . 5
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) | 
| 2 |  | snssi 4808 | . . . . 5
⊢ (𝑋 ∈ 𝑉 → {𝑋} ⊆ 𝑉) | 
| 3 |  | lbslsat.v | . . . . . 6
⊢ 𝑉 = (Base‘𝑊) | 
| 4 |  | eqid 2737 | . . . . . 6
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) | 
| 5 |  | lbslsat.n | . . . . . 6
⊢ 𝑁 = (LSpan‘𝑊) | 
| 6 | 3, 4, 5 | lspcl 20974 | . . . . 5
⊢ ((𝑊 ∈ LMod ∧ {𝑋} ⊆ 𝑉) → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑊)) | 
| 7 | 1, 2, 6 | syl2an 596 | . . . 4
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑊)) | 
| 8 |  | lbslsat.y | . . . . 5
⊢ 𝑌 = (𝑊 ↾s (𝑁‘{𝑋})) | 
| 9 | 8, 4 | lsslvec 21108 | . . . 4
⊢ ((𝑊 ∈ LVec ∧ (𝑁‘{𝑋}) ∈ (LSubSp‘𝑊)) → 𝑌 ∈ LVec) | 
| 10 | 7, 9 | syldan 591 | . . 3
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → 𝑌 ∈ LVec) | 
| 11 | 10 | 3adant3 1133 | . 2
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → 𝑌 ∈ LVec) | 
| 12 | 3, 5 | lspssid 20983 | . . . . 5
⊢ ((𝑊 ∈ LMod ∧ {𝑋} ⊆ 𝑉) → {𝑋} ⊆ (𝑁‘{𝑋})) | 
| 13 | 1, 2, 12 | syl2an 596 | . . . 4
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → {𝑋} ⊆ (𝑁‘{𝑋})) | 
| 14 | 3, 5 | lspssv 20981 | . . . . . 6
⊢ ((𝑊 ∈ LMod ∧ {𝑋} ⊆ 𝑉) → (𝑁‘{𝑋}) ⊆ 𝑉) | 
| 15 | 1, 2, 14 | syl2an 596 | . . . . 5
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ⊆ 𝑉) | 
| 16 | 8, 3 | ressbas2 17283 | . . . . 5
⊢ ((𝑁‘{𝑋}) ⊆ 𝑉 → (𝑁‘{𝑋}) = (Base‘𝑌)) | 
| 17 | 15, 16 | syl 17 | . . . 4
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) = (Base‘𝑌)) | 
| 18 | 13, 17 | sseqtrd 4020 | . . 3
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → {𝑋} ⊆ (Base‘𝑌)) | 
| 19 | 18 | 3adant3 1133 | . 2
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → {𝑋} ⊆ (Base‘𝑌)) | 
| 20 | 1 | adantr 480 | . . . . 5
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → 𝑊 ∈ LMod) | 
| 21 |  | eqid 2737 | . . . . . 6
⊢
(LSpan‘𝑌) =
(LSpan‘𝑌) | 
| 22 | 8, 5, 21, 4 | lsslsp 21013 | . . . . 5
⊢ ((𝑊 ∈ LMod ∧ (𝑁‘{𝑋}) ∈ (LSubSp‘𝑊) ∧ {𝑋} ⊆ (𝑁‘{𝑋})) → ((LSpan‘𝑌)‘{𝑋}) = (𝑁‘{𝑋})) | 
| 23 | 20, 7, 13, 22 | syl3anc 1373 | . . . 4
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → ((LSpan‘𝑌)‘{𝑋}) = (𝑁‘{𝑋})) | 
| 24 | 23 | 3adant3 1133 | . . 3
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) →
((LSpan‘𝑌)‘{𝑋}) = (𝑁‘{𝑋})) | 
| 25 | 17 | 3adant3 1133 | . . 3
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → (𝑁‘{𝑋}) = (Base‘𝑌)) | 
| 26 | 24, 25 | eqtrd 2777 | . 2
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) →
((LSpan‘𝑌)‘{𝑋}) = (Base‘𝑌)) | 
| 27 |  | difid 4376 | . . . . . . . . . . . . 13
⊢ ({𝑋} ∖ {𝑋}) = ∅ | 
| 28 | 27 | fveq2i 6909 | . . . . . . . . . . . 12
⊢
((LSpan‘𝑌)‘({𝑋} ∖ {𝑋})) = ((LSpan‘𝑌)‘∅) | 
| 29 | 28 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋})) = ((LSpan‘𝑌)‘∅)) | 
| 30 | 29 | eleq2d 2827 | . . . . . . . . . 10
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → (𝑋 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋})) ↔ 𝑋 ∈ ((LSpan‘𝑌)‘∅))) | 
| 31 | 30 | biimpa 476 | . . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋}))) → 𝑋 ∈ ((LSpan‘𝑌)‘∅)) | 
| 32 |  | lveclmod 21105 | . . . . . . . . . . 11
⊢ (𝑌 ∈ LVec → 𝑌 ∈ LMod) | 
| 33 |  | eqid 2737 | . . . . . . . . . . . 12
⊢
(0g‘𝑌) = (0g‘𝑌) | 
| 34 | 33, 21 | lsp0 21007 | . . . . . . . . . . 11
⊢ (𝑌 ∈ LMod →
((LSpan‘𝑌)‘∅) =
{(0g‘𝑌)}) | 
| 35 | 10, 32, 34 | 3syl 18 | . . . . . . . . . 10
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → ((LSpan‘𝑌)‘∅) =
{(0g‘𝑌)}) | 
| 36 | 35 | adantr 480 | . . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋}))) → ((LSpan‘𝑌)‘∅) =
{(0g‘𝑌)}) | 
| 37 | 31, 36 | eleqtrd 2843 | . . . . . . . 8
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋}))) → 𝑋 ∈ {(0g‘𝑌)}) | 
| 38 |  | elsni 4643 | . . . . . . . 8
⊢ (𝑋 ∈
{(0g‘𝑌)}
→ 𝑋 =
(0g‘𝑌)) | 
| 39 | 37, 38 | syl 17 | . . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋}))) → 𝑋 = (0g‘𝑌)) | 
| 40 |  | lmodgrp 20865 | . . . . . . . . . 10
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) | 
| 41 |  | grpmnd 18958 | . . . . . . . . . 10
⊢ (𝑊 ∈ Grp → 𝑊 ∈ Mnd) | 
| 42 | 20, 40, 41 | 3syl 18 | . . . . . . . . 9
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → 𝑊 ∈ Mnd) | 
| 43 |  | lbslsat.z | . . . . . . . . . . 11
⊢  0 =
(0g‘𝑊) | 
| 44 | 43, 3, 5 | 0ellsp 33397 | . . . . . . . . . 10
⊢ ((𝑊 ∈ LMod ∧ {𝑋} ⊆ 𝑉) → 0 ∈ (𝑁‘{𝑋})) | 
| 45 | 1, 2, 44 | syl2an 596 | . . . . . . . . 9
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → 0 ∈ (𝑁‘{𝑋})) | 
| 46 | 8, 3, 43 | ress0g 18775 | . . . . . . . . 9
⊢ ((𝑊 ∈ Mnd ∧ 0 ∈ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑋}) ⊆ 𝑉) → 0 =
(0g‘𝑌)) | 
| 47 | 42, 45, 15, 46 | syl3anc 1373 | . . . . . . . 8
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → 0 =
(0g‘𝑌)) | 
| 48 | 47 | adantr 480 | . . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋}))) → 0 =
(0g‘𝑌)) | 
| 49 | 39, 48 | eqtr4d 2780 | . . . . . 6
⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋}))) → 𝑋 = 0 ) | 
| 50 | 49 | ex 412 | . . . . 5
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → (𝑋 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋})) → 𝑋 = 0 )) | 
| 51 | 50 | necon3ad 2953 | . . . 4
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉) → (𝑋 ≠ 0 → ¬ 𝑋 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋})))) | 
| 52 | 51 | 3impia 1118 | . . 3
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ¬ 𝑋 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋}))) | 
| 53 |  | id 22 | . . . . . . 7
⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋) | 
| 54 |  | sneq 4636 | . . . . . . . . 9
⊢ (𝑥 = 𝑋 → {𝑥} = {𝑋}) | 
| 55 | 54 | difeq2d 4126 | . . . . . . . 8
⊢ (𝑥 = 𝑋 → ({𝑋} ∖ {𝑥}) = ({𝑋} ∖ {𝑋})) | 
| 56 | 55 | fveq2d 6910 | . . . . . . 7
⊢ (𝑥 = 𝑋 → ((LSpan‘𝑌)‘({𝑋} ∖ {𝑥})) = ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋}))) | 
| 57 | 53, 56 | eleq12d 2835 | . . . . . 6
⊢ (𝑥 = 𝑋 → (𝑥 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑥})) ↔ 𝑋 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋})))) | 
| 58 | 57 | notbid 318 | . . . . 5
⊢ (𝑥 = 𝑋 → (¬ 𝑥 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑥})) ↔ ¬ 𝑋 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋})))) | 
| 59 | 58 | ralsng 4675 | . . . 4
⊢ (𝑋 ∈ 𝑉 → (∀𝑥 ∈ {𝑋} ¬ 𝑥 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑥})) ↔ ¬ 𝑋 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋})))) | 
| 60 | 59 | 3ad2ant2 1135 | . . 3
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → (∀𝑥 ∈ {𝑋} ¬ 𝑥 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑥})) ↔ ¬ 𝑋 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑋})))) | 
| 61 | 52, 60 | mpbird 257 | . 2
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ∀𝑥 ∈ {𝑋} ¬ 𝑥 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑥}))) | 
| 62 |  | eqid 2737 | . . . 4
⊢
(Base‘𝑌) =
(Base‘𝑌) | 
| 63 |  | eqid 2737 | . . . 4
⊢
(LBasis‘𝑌) =
(LBasis‘𝑌) | 
| 64 | 62, 63, 21 | islbs2 21156 | . . 3
⊢ (𝑌 ∈ LVec → ({𝑋} ∈ (LBasis‘𝑌) ↔ ({𝑋} ⊆ (Base‘𝑌) ∧ ((LSpan‘𝑌)‘{𝑋}) = (Base‘𝑌) ∧ ∀𝑥 ∈ {𝑋} ¬ 𝑥 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑥}))))) | 
| 65 | 64 | biimpar 477 | . 2
⊢ ((𝑌 ∈ LVec ∧ ({𝑋} ⊆ (Base‘𝑌) ∧ ((LSpan‘𝑌)‘{𝑋}) = (Base‘𝑌) ∧ ∀𝑥 ∈ {𝑋} ¬ 𝑥 ∈ ((LSpan‘𝑌)‘({𝑋} ∖ {𝑥})))) → {𝑋} ∈ (LBasis‘𝑌)) | 
| 66 | 11, 19, 26, 61, 65 | syl13anc 1374 | 1
⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → {𝑋} ∈ (LBasis‘𝑌)) |