# Metamath Proof Explorer

## Theorem lspsnss2

Description: Comparable spans of singletons must have proportional vectors. See lspsneq for equal span version. (Contributed by NM, 7-Jun-2015)

Ref Expression
Hypotheses lspsnss2.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
lspsnss2.s ${⊢}{S}=\mathrm{Scalar}\left({W}\right)$
lspsnss2.k ${⊢}{K}={\mathrm{Base}}_{{S}}$
lspsnss2.t
lspsnss2.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
lspsnss2.w ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
lspsnss2.x ${⊢}{\phi }\to {X}\in {V}$
lspsnss2.y ${⊢}{\phi }\to {Y}\in {V}$
Assertion lspsnss2

### Proof

Step Hyp Ref Expression
1 lspsnss2.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 lspsnss2.s ${⊢}{S}=\mathrm{Scalar}\left({W}\right)$
3 lspsnss2.k ${⊢}{K}={\mathrm{Base}}_{{S}}$
4 lspsnss2.t
5 lspsnss2.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
6 lspsnss2.w ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
7 lspsnss2.x ${⊢}{\phi }\to {X}\in {V}$
8 lspsnss2.y ${⊢}{\phi }\to {Y}\in {V}$
9 eqid ${⊢}\mathrm{LSubSp}\left({W}\right)=\mathrm{LSubSp}\left({W}\right)$
10 1 9 5 lspsncl ${⊢}\left({W}\in \mathrm{LMod}\wedge {Y}\in {V}\right)\to {N}\left(\left\{{Y}\right\}\right)\in \mathrm{LSubSp}\left({W}\right)$
11 6 8 10 syl2anc ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)\in \mathrm{LSubSp}\left({W}\right)$
12 1 9 5 6 11 7 lspsnel5 ${⊢}{\phi }\to \left({X}\in {N}\left(\left\{{Y}\right\}\right)↔{N}\left(\left\{{X}\right\}\right)\subseteq {N}\left(\left\{{Y}\right\}\right)\right)$
13 2 3 1 4 5 lspsnel
14 6 8 13 syl2anc
15 12 14 bitr3d