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. = ( 0g ` W )
lbslsat.y 
|- Y = ( W |`s ( N ` { X } ) )
Assertion lsatdim 
|- ( ( W e. LVec /\ X e. 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. = ( 0g ` W )
4 lbslsat.y 
 |-  Y = ( W |`s ( N ` { X } ) )
5 simp1 
 |-  ( ( W e. LVec /\ X e. V /\ X =/= .0. ) -> W e. LVec )
6 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
7 5 6 syl 
 |-  ( ( W e. LVec /\ X e. V /\ X =/= .0. ) -> W e. LMod )
8 simp2 
 |-  ( ( W e. LVec /\ X e. V /\ X =/= .0. ) -> X e. V )
9 8 snssd 
 |-  ( ( W e. LVec /\ X e. V /\ X =/= .0. ) -> { X } C_ V )
10 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
11 1 10 2 lspcl 
 |-  ( ( W e. LMod /\ { X } C_ V ) -> ( N ` { X } ) e. ( LSubSp ` W ) )
12 7 9 11 syl2anc 
 |-  ( ( W e. LVec /\ X e. V /\ X =/= .0. ) -> ( N ` { X } ) e. ( LSubSp ` W ) )
13 4 10 lsslvec 
 |-  ( ( W e. LVec /\ ( N ` { X } ) e. ( LSubSp ` W ) ) -> Y e. LVec )
14 5 12 13 syl2anc 
 |-  ( ( W e. LVec /\ X e. V /\ X =/= .0. ) -> Y e. LVec )
15 1 2 3 4 lbslsat 
 |-  ( ( W e. LVec /\ X e. V /\ X =/= .0. ) -> { X } e. ( LBasis ` Y ) )
16 eqid 
 |-  ( LBasis ` Y ) = ( LBasis ` Y )
17 16 dimval 
 |-  ( ( Y e. LVec /\ { X } e. ( LBasis ` Y ) ) -> ( dim ` Y ) = ( # ` { X } ) )
18 14 15 17 syl2anc 
 |-  ( ( W e. LVec /\ X e. V /\ X =/= .0. ) -> ( dim ` Y ) = ( # ` { X } ) )
19 hashsng 
 |-  ( X e. V -> ( # ` { X } ) = 1 )
20 8 19 syl 
 |-  ( ( W e. LVec /\ X e. V /\ X =/= .0. ) -> ( # ` { X } ) = 1 )
21 18 20 eqtrd 
 |-  ( ( W e. LVec /\ X e. V /\ X =/= .0. ) -> ( dim ` Y ) = 1 )