# Metamath Proof Explorer

## Theorem mapdindp1

Description: Vector independence lemma. (Contributed by NM, 1-May-2015)

Ref Expression
Hypotheses mapdindp1.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
mapdindp1.p
mapdindp1.o
mapdindp1.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
mapdindp1.w ${⊢}{\phi }\to {W}\in \mathrm{LVec}$
mapdindp1.x
mapdindp1.y
mapdindp1.z
mapdindp1.W
mapdindp1.e ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)={N}\left(\left\{{Z}\right\}\right)$
mapdindp1.ne ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)$
mapdindp1.f ${⊢}{\phi }\to ¬{w}\in {N}\left(\left\{{X},{Y}\right\}\right)$
Assertion mapdindp1

### Proof

Step Hyp Ref Expression
1 mapdindp1.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 mapdindp1.p
3 mapdindp1.o
4 mapdindp1.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
5 mapdindp1.w ${⊢}{\phi }\to {W}\in \mathrm{LVec}$
6 mapdindp1.x
7 mapdindp1.y
8 mapdindp1.z
9 mapdindp1.W
10 mapdindp1.e ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)={N}\left(\left\{{Z}\right\}\right)$
11 mapdindp1.ne ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)$
12 mapdindp1.f ${⊢}{\phi }\to ¬{w}\in {N}\left(\left\{{X},{Y}\right\}\right)$
13 eldifsni
14 6 13 syl
15 lveclmod ${⊢}{W}\in \mathrm{LVec}\to {W}\in \mathrm{LMod}$
16 5 15 syl ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
17 3 4 lspsn0
18 16 17 syl
19 18 eqeq2d
20 6 eldifad ${⊢}{\phi }\to {X}\in {V}$
21 1 3 4 lspsneq0
22 16 20 21 syl2anc
23 19 22 bitrd
24 23 necon3bid
25 14 24 mpbird
27 sneq
28 27 fveq2d