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 โŠข ๐น = ( Scalar โ€˜ ๐‘Š )
lspsn.k โŠข ๐พ = ( Base โ€˜ ๐น )
lspsn.v โŠข ๐‘‰ = ( Base โ€˜ ๐‘Š )
lspsn.t โŠข ยท = ( ยท๐‘  โ€˜ ๐‘Š )
lspsn.n โŠข ๐‘ = ( LSpan โ€˜ ๐‘Š )
Assertion lspsnvsi ( ( ๐‘Š โˆˆ LMod โˆง ๐‘… โˆˆ ๐พ โˆง ๐‘‹ โˆˆ ๐‘‰ ) โ†’ ( ๐‘ โ€˜ { ( ๐‘… ยท ๐‘‹ ) } ) โŠ† ( ๐‘ โ€˜ { ๐‘‹ } ) )

Proof

Step Hyp Ref Expression
1 lspsn.f โŠข ๐น = ( Scalar โ€˜ ๐‘Š )
2 lspsn.k โŠข ๐พ = ( Base โ€˜ ๐น )
3 lspsn.v โŠข ๐‘‰ = ( Base โ€˜ ๐‘Š )
4 lspsn.t โŠข ยท = ( ยท๐‘  โ€˜ ๐‘Š )
5 lspsn.n โŠข ๐‘ = ( LSpan โ€˜ ๐‘Š )
6 eqid โŠข ( LSubSp โ€˜ ๐‘Š ) = ( LSubSp โ€˜ ๐‘Š )
7 simp1 โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘… โˆˆ ๐พ โˆง ๐‘‹ โˆˆ ๐‘‰ ) โ†’ ๐‘Š โˆˆ LMod )
8 simp3 โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘… โˆˆ ๐พ โˆง ๐‘‹ โˆˆ ๐‘‰ ) โ†’ ๐‘‹ โˆˆ ๐‘‰ )
9 8 snssd โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘… โˆˆ ๐พ โˆง ๐‘‹ โˆˆ ๐‘‰ ) โ†’ { ๐‘‹ } โŠ† ๐‘‰ )
10 3 6 5 lspcl โŠข ( ( ๐‘Š โˆˆ LMod โˆง { ๐‘‹ } โŠ† ๐‘‰ ) โ†’ ( ๐‘ โ€˜ { ๐‘‹ } ) โˆˆ ( LSubSp โ€˜ ๐‘Š ) )
11 7 9 10 syl2anc โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘… โˆˆ ๐พ โˆง ๐‘‹ โˆˆ ๐‘‰ ) โ†’ ( ๐‘ โ€˜ { ๐‘‹ } ) โˆˆ ( LSubSp โ€˜ ๐‘Š ) )
12 simp2 โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘… โˆˆ ๐พ โˆง ๐‘‹ โˆˆ ๐‘‰ ) โ†’ ๐‘… โˆˆ ๐พ )
13 3 4 1 2 5 7 12 8 lspsneli โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘… โˆˆ ๐พ โˆง ๐‘‹ โˆˆ ๐‘‰ ) โ†’ ( ๐‘… ยท ๐‘‹ ) โˆˆ ( ๐‘ โ€˜ { ๐‘‹ } ) )
14 6 5 7 11 13 lspsnel5a โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘… โˆˆ ๐พ โˆง ๐‘‹ โˆˆ ๐‘‰ ) โ†’ ( ๐‘ โ€˜ { ( ๐‘… ยท ๐‘‹ ) } ) โŠ† ( ๐‘ โ€˜ { ๐‘‹ } ) )