# Metamath Proof Explorer

## Theorem lsatspn0

Description: The span of a vector is an atom iff the vector is nonzero. (Contributed by NM, 4-Feb-2015)

Ref Expression
Hypotheses lsatspn0.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
lsatspn0.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
lsatspn0.o
lsatspn0.a ${⊢}{A}=\mathrm{LSAtoms}\left({W}\right)$
isateln0.w ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
isateln0.x ${⊢}{\phi }\to {X}\in {V}$
Assertion lsatspn0

### Proof

Step Hyp Ref Expression
1 lsatspn0.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 lsatspn0.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
3 lsatspn0.o
4 lsatspn0.a ${⊢}{A}=\mathrm{LSAtoms}\left({W}\right)$
5 isateln0.w ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
6 isateln0.x ${⊢}{\phi }\to {X}\in {V}$
7 5 adantr ${⊢}\left({\phi }\wedge {N}\left(\left\{{X}\right\}\right)\in {A}\right)\to {W}\in \mathrm{LMod}$
8 simpr ${⊢}\left({\phi }\wedge {N}\left(\left\{{X}\right\}\right)\in {A}\right)\to {N}\left(\left\{{X}\right\}\right)\in {A}$
9 3 4 7 8 lsatn0
10 sneq
11 10 fveq2d