# Metamath Proof Explorer

## Theorem lspprcl

Description: The span of a pair is a subspace (frequently used special case of lspcl ). (Contributed by NM, 11-Apr-2015)

Ref Expression
Hypotheses lspval.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
lspval.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
lspval.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
lspprcl.w ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
lspprcl.x ${⊢}{\phi }\to {X}\in {V}$
lspprcl.y ${⊢}{\phi }\to {Y}\in {V}$
Assertion lspprcl ${⊢}{\phi }\to {N}\left(\left\{{X},{Y}\right\}\right)\in {S}$

### Proof

Step Hyp Ref Expression
1 lspval.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 lspval.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
3 lspval.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
4 lspprcl.w ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
5 lspprcl.x ${⊢}{\phi }\to {X}\in {V}$
6 lspprcl.y ${⊢}{\phi }\to {Y}\in {V}$
7 5 6 prssd ${⊢}{\phi }\to \left\{{X},{Y}\right\}\subseteq {V}$
8 1 2 3 lspcl ${⊢}\left({W}\in \mathrm{LMod}\wedge \left\{{X},{Y}\right\}\subseteq {V}\right)\to {N}\left(\left\{{X},{Y}\right\}\right)\in {S}$
9 4 7 8 syl2anc ${⊢}{\phi }\to {N}\left(\left\{{X},{Y}\right\}\right)\in {S}$