# Metamath Proof Explorer

## Theorem mapdindp4

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 mapdindp4

### 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}$
17 1 2 lmodvacl
18 14 15 16 17 syl3anc
19 6 eldifad ${⊢}{\phi }\to {X}\in {V}$
20 1 4 5 15 19 16 12 lspindpi ${⊢}{\phi }\to \left({N}\left(\left\{{w}\right\}\right)\ne {N}\left(\left\{{X}\right\}\right)\wedge {N}\left(\left\{{w}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)\right)$
21 20 simprd ${⊢}{\phi }\to {N}\left(\left\{{w}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)$
22 21 necomd ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)\ne {N}\left(\left\{{w}\right\}\right)$
23 1 2 3 4 5 16 9 22 lspindp3
24 1 2 lmodcom
25 14 15 16 24 syl3anc
26 25 sneqd
27 26 fveq2d
28 23 27 neeqtrrd
29 10 28 eqnetrrd
30 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)$
31 30 simprd ${⊢}{\phi }\to ¬{X}\in {N}\left(\left\{{w},{Y}\right\}\right)$
32 eqid ${⊢}\mathrm{LSSum}\left({W}\right)=\mathrm{LSSum}\left({W}\right)$
33 8 eldifad ${⊢}{\phi }\to {Z}\in {V}$
34 1 4 32 14 33 18 lsmpr
35 1 2 lmodcom
36 14 16 15 35 syl3anc
37 36 preq2d
38 37 fveq2d
39 1 2 4 14 16 15 lspprabs
40 1 4 32 14 16 18 lsmpr
41 38 39 40 3eqtr3rd
42 10 oveq1d
43 prcom ${⊢}\left\{{Y},{w}\right\}=\left\{{w},{Y}\right\}$
44 43 fveq2i ${⊢}{N}\left(\left\{{Y},{w}\right\}\right)={N}\left(\left\{{w},{Y}\right\}\right)$
45 44 a1i ${⊢}{\phi }\to {N}\left(\left\{{Y},{w}\right\}\right)={N}\left(\left\{{w},{Y}\right\}\right)$
46 41 42 45 3eqtr3d
47 34 46 eqtrd
48 31 47 neleqtrrd
49 1 3 4 5 8 18 19 29 48 lspindp1
50 49 simprd