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 )