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 = Base W
lspval.s S = LSubSp W
lspval.n N = LSpan W
lspprcl.w φ W LMod
lspprcl.x φ X V
lspprcl.y φ Y V
Assertion lspprcl φ N X Y S


Step Hyp Ref Expression
1 lspval.v V = Base W
2 lspval.s S = LSubSp W
3 lspval.n N = LSpan W
4 lspprcl.w φ W LMod
5 lspprcl.x φ X V
6 lspprcl.y φ Y V
7 5 6 prssd φ X Y V
8 1 2 3 lspcl W LMod X Y V N X Y S
9 4 7 8 syl2anc φ N X Y S