# Metamath Proof Explorer

## Theorem lsppr0

Description: The span of a vector paired with zero equals the span of the singleton of the vector. (Contributed by NM, 29-Aug-2014)

Ref Expression
Hypotheses lsppr0.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
lsppr0.z
lsppr0.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
lsppr0.w ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
lsppr0.x ${⊢}{\phi }\to {X}\in {V}$
Assertion lsppr0

### Proof

Step Hyp Ref Expression
1 lsppr0.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 lsppr0.z
3 lsppr0.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
4 lsppr0.w ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
5 lsppr0.x ${⊢}{\phi }\to {X}\in {V}$
6 eqid ${⊢}\mathrm{LSSum}\left({W}\right)=\mathrm{LSSum}\left({W}\right)$
7 1 2 lmod0vcl
8 4 7 syl
9 1 3 6 4 5 8 lsmpr
10 2 3 lspsn0
11 4 10 syl
12 11 oveq2d
13 1 3 lspsnsubg ${⊢}\left({W}\in \mathrm{LMod}\wedge {X}\in {V}\right)\to {N}\left(\left\{{X}\right\}\right)\in \mathrm{SubGrp}\left({W}\right)$
14 4 5 13 syl2anc ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\in \mathrm{SubGrp}\left({W}\right)$
15 2 6 lsm01
16 14 15 syl
17 9 12 16 3eqtrd