# Metamath Proof Explorer

## Theorem mapdindp3

Description: Vector independence lemma. (Contributed by NM, 29-Apr-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 mapdindp3

### 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 lveclmod ${⊢}{W}\in \mathrm{LVec}\to {W}\in \mathrm{LMod}$
14 5 13 syl ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
15 9 eldifad ${⊢}{\phi }\to {w}\in {V}$
16 7 eldifad ${⊢}{\phi }\to {Y}\in {V}$
18 14 15 16 17 syl3anc
19 1 3 4 5 6 16 15 11 12 lspindp1 ${⊢}{\phi }\to \left({N}\left(\left\{{w}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)\wedge ¬{X}\in {N}\left(\left\{{w},{Y}\right\}\right)\right)$
20 19 simprd ${⊢}{\phi }\to ¬{X}\in {N}\left(\left\{{w},{Y}\right\}\right)$
21 18 20 ssneldd
22 6 eldifad ${⊢}{\phi }\to {X}\in {V}$
23 1 4 lspsnid ${⊢}\left({W}\in \mathrm{LMod}\wedge {X}\in {V}\right)\to {X}\in {N}\left(\left\{{X}\right\}\right)$
24 14 22 23 syl2anc ${⊢}{\phi }\to {X}\in {N}\left(\left\{{X}\right\}\right)$
25 eleq2
26 24 25 syl5ibcom
27 26 necon3bd
28 21 27 mpd