Metamath Proof Explorer

Theorem lsatdim

Description: A line, spanned by a nonzero singleton, has dimension 1. (Contributed by Thierry Arnoux, 20-May-2023)

Ref Expression
Hypotheses lbslsat.v ⊢ V = Base W
lbslsat.n ⊢ N = LSpan ⁡ W
lbslsat.z ⊢ 0 ˙ = 0 W
lbslsat.y ⊢ Y = W ↾ 𝑠 N ⁡ X
Assertion lsatdim ⊢ W ∈ LVec ∧ X ∈ V ∧ X ≠ 0 ˙ → dim ⁡ Y = 1

Proof

Step Hyp Ref Expression
1 lbslsat.v ⊢ V = Base W
2 lbslsat.n ⊢ N = LSpan ⁡ W
3 lbslsat.z ⊢ 0 ˙ = 0 W
4 lbslsat.y ⊢ Y = W ↾ 𝑠 N ⁡ X
5 simp1 ⊢ W ∈ LVec ∧ X ∈ V ∧ X ≠ 0 ˙ → W ∈ LVec
6 lveclmod ⊢ W ∈ LVec → W ∈ LMod
7 5 6 syl ⊢ W ∈ LVec ∧ X ∈ V ∧ X ≠ 0 ˙ → W ∈ LMod
8 simp2 ⊢ W ∈ LVec ∧ X ∈ V ∧ X ≠ 0 ˙ → X ∈ V
9 8 snssd ⊢ W ∈ LVec ∧ X ∈ V ∧ X ≠ 0 ˙ → X ⊆ V
10 eqid ⊢ LSubSp ⁡ W = LSubSp ⁡ W
11 1 10 2 lspcl ⊢ W ∈ LMod ∧ X ⊆ V → N ⁡ X ∈ LSubSp ⁡ W
12 7 9 11 syl2anc ⊢ W ∈ LVec ∧ X ∈ V ∧ X ≠ 0 ˙ → N ⁡ X ∈ LSubSp ⁡ W
13 4 10 lsslvec ⊢ W ∈ LVec ∧ N ⁡ X ∈ LSubSp ⁡ W → Y ∈ LVec
14 5 12 13 syl2anc ⊢ W ∈ LVec ∧ X ∈ V ∧ X ≠ 0 ˙ → Y ∈ LVec
15 1 2 3 4 lbslsat ⊢ W ∈ LVec ∧ X ∈ V ∧ X ≠ 0 ˙ → X ∈ LBasis ⁡ Y
16 eqid ⊢ LBasis ⁡ Y = LBasis ⁡ Y
17 16 dimval ⊢ Y ∈ LVec ∧ X ∈ LBasis ⁡ Y → dim ⁡ Y = X
18 14 15 17 syl2anc ⊢ W ∈ LVec ∧ X ∈ V ∧ X ≠ 0 ˙ → dim ⁡ Y = X
19 hashsng ⊢ X ∈ V → X = 1
20 8 19 syl ⊢ W ∈ LVec ∧ X ∈ V ∧ X ≠ 0 ˙ → X = 1
21 18 20 eqtrd ⊢ W ∈ LVec ∧ X ∈ V ∧ X ≠ 0 ˙ → dim ⁡ Y = 1