This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
lbslsat.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lbslsat.z ⊢ 0 = ( 0g ‘ 𝑊 )
lbslsat.y ⊢ 𝑌 = ( 𝑊 ↾s ( 𝑁 ‘ { 𝑋 } ) )
Assertion lsatdim ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ( dim ‘ 𝑌 ) = 1 )

Proof

Step Hyp Ref Expression
1 lbslsat.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lbslsat.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3 lbslsat.z ⊢ 0 = ( 0g ‘ 𝑊 )
4 lbslsat.y ⊢ 𝑌 = ( 𝑊 ↾s ( 𝑁 ‘ { 𝑋 } ) )
5 simp1 ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → 𝑊 ∈ LVec )
6 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
7 5 6 syl ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → 𝑊 ∈ LMod )
8 simp2 ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ 𝑉 )
9 8 snssd ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → { 𝑋 } ⊆ 𝑉 )
10 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
11 1 10 2 lspcl ⊢ ( ( 𝑊 ∈ LMod ∧ { 𝑋 } ⊆ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
12 7 9 11 syl2anc ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
13 4 10 lsslvec ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) ) → 𝑌 ∈ LVec )
14 5 12 13 syl2anc ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → 𝑌 ∈ LVec )
15 1 2 3 4 lbslsat ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → { 𝑋 } ∈ ( LBasis ‘ 𝑌 ) )
16 eqid ⊢ ( LBasis ‘ 𝑌 ) = ( LBasis ‘ 𝑌 )
17 16 dimval ⊢ ( ( 𝑌 ∈ LVec ∧ { 𝑋 } ∈ ( LBasis ‘ 𝑌 ) ) → ( dim ‘ 𝑌 ) = ( ♯ ‘ { 𝑋 } ) )
18 14 15 17 syl2anc ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ( dim ‘ 𝑌 ) = ( ♯ ‘ { 𝑋 } ) )
19 hashsng ⊢ ( 𝑋 ∈ 𝑉 → ( ♯ ‘ { 𝑋 } ) = 1 )
20 8 19 syl ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ( ♯ ‘ { 𝑋 } ) = 1 )
21 18 20 eqtrd ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ( dim ‘ 𝑌 ) = 1 )