# Metamath Proof Explorer

## Theorem lbspss

Description: No proper subset of a basis spans the space. (Contributed by Mario Carneiro, 25-Jun-2014)

Ref Expression
Hypotheses lbsind2.j ${⊢}{J}=\mathrm{LBasis}\left({W}\right)$
lbsind2.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
lbsind2.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
lbsind2.o
lbsind2.z
lbspss.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
Assertion lbspss

### Proof

Step Hyp Ref Expression
1 lbsind2.j ${⊢}{J}=\mathrm{LBasis}\left({W}\right)$
2 lbsind2.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
3 lbsind2.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
4 lbsind2.o
5 lbsind2.z
6 lbspss.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
7 pssnel ${⊢}{C}\subset {B}\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge ¬{x}\in {C}\right)$
9 simpl2
10 6 1 lbsss ${⊢}{B}\in {J}\to {B}\subseteq {V}$
11 9 10 syl
12 simprl
13 11 12 sseldd
14 simpl1l
15 11 ssdifssd
16 simpl3
17 16 pssssd
18 17 sseld
19 simprr
20 eleq1w ${⊢}{y}={x}\to \left({y}\in {C}↔{x}\in {C}\right)$
21 20 notbid ${⊢}{y}={x}\to \left(¬{y}\in {C}↔¬{x}\in {C}\right)$
22 19 21 syl5ibrcom
25 eldifsn ${⊢}{y}\in \left({B}\setminus \left\{{x}\right\}\right)↔\left({y}\in {B}\wedge {y}\ne {x}\right)$
28 6 2 lspss ${⊢}\left({W}\in \mathrm{LMod}\wedge {B}\setminus \left\{{x}\right\}\subseteq {V}\wedge {C}\subseteq {B}\setminus \left\{{x}\right\}\right)\to {N}\left({C}\right)\subseteq {N}\left({B}\setminus \left\{{x}\right\}\right)$
34 nelne1 ${⊢}\left({x}\in {V}\wedge ¬{x}\in {N}\left({C}\right)\right)\to {V}\ne {N}\left({C}\right)$