Metamath Proof Explorer

Theorem lspsnvsi

Description: Span of a scalar product of a singleton. (Contributed by NM, 23-Apr-2014) (Proof shortened by Mario Carneiro, 4-Sep-2014)

Ref Expression
Hypotheses lspsn.f 
|- F = ( Scalar ` W )
lspsn.k 
|- K = ( Base ` F )
lspsn.v 
|- V = ( Base ` W )
lspsn.t 
|- .x. = ( .s ` W )
lspsn.n 
|- N = ( LSpan ` W )
Assertion lspsnvsi 
|- ( ( W e. LMod /\ R e. K /\ X e. V ) -> ( N ` { ( R .x. X ) } ) C_ ( N ` { X } ) )

Proof

Step Hyp Ref Expression
1 lspsn.f 
 |-  F = ( Scalar ` W )
2 lspsn.k 
 |-  K = ( Base ` F )
3 lspsn.v 
 |-  V = ( Base ` W )
4 lspsn.t 
 |-  .x. = ( .s ` W )
5 lspsn.n 
 |-  N = ( LSpan ` W )
6 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
7 simp1 
 |-  ( ( W e. LMod /\ R e. K /\ X e. V ) -> W e. LMod )
8 simp3 
 |-  ( ( W e. LMod /\ R e. K /\ X e. V ) -> X e. V )
9 8 snssd 
 |-  ( ( W e. LMod /\ R e. K /\ X e. V ) -> { X } C_ V )
10 3 6 5 lspcl 
 |-  ( ( W e. LMod /\ { X } C_ V ) -> ( N ` { X } ) e. ( LSubSp ` W ) )
11 7 9 10 syl2anc 
 |-  ( ( W e. LMod /\ R e. K /\ X e. V ) -> ( N ` { X } ) e. ( LSubSp ` W ) )
12 simp2 
 |-  ( ( W e. LMod /\ R e. K /\ X e. V ) -> R e. K )
13 3 4 1 2 5 7 12 8 lspsneli 
 |-  ( ( W e. LMod /\ R e. K /\ X e. V ) -> ( R .x. X ) e. ( N ` { X } ) )
14 6 5 7 11 13 lspsnel5a 
 |-  ( ( W e. LMod /\ R e. K /\ X e. V ) -> ( N ` { ( R .x. X ) } ) C_ ( N ` { X } ) )