# Metamath Proof Explorer

## Theorem mapdindp2

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 mapdindp2

### 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 preq2
14 13 fveq2d
15 lveclmod ${⊢}{W}\in \mathrm{LVec}\to {W}\in \mathrm{LMod}$
16 5 15 syl ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
17 6 eldifad ${⊢}{\phi }\to {X}\in {V}$
18 1 3 4 16 17 lsppr0
19 14 18 sylan9eqr
20 7 eldifad ${⊢}{\phi }\to {Y}\in {V}$
21 prssi ${⊢}\left({X}\in {V}\wedge {Y}\in {V}\right)\to \left\{{X},{Y}\right\}\subseteq {V}$
22 17 20 21 syl2anc ${⊢}{\phi }\to \left\{{X},{Y}\right\}\subseteq {V}$
23 snsspr1 ${⊢}\left\{{X}\right\}\subseteq \left\{{X},{Y}\right\}$
24 23 a1i ${⊢}{\phi }\to \left\{{X}\right\}\subseteq \left\{{X},{Y}\right\}$
25 1 4 lspss ${⊢}\left({W}\in \mathrm{LMod}\wedge \left\{{X},{Y}\right\}\subseteq {V}\wedge \left\{{X}\right\}\subseteq \left\{{X},{Y}\right\}\right)\to {N}\left(\left\{{X}\right\}\right)\subseteq {N}\left(\left\{{X},{Y}\right\}\right)$
26 16 22 24 25 syl3anc ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\subseteq {N}\left(\left\{{X},{Y}\right\}\right)$
28 19 27 eqsstrd
30 28 29 ssneldd
39 simpr
40 1 2 3 4 32 33 34 35 36 37 38 31 39 mapdindp0
41 40 oveq2d
42 eqid ${⊢}\mathrm{LSSum}\left({W}\right)=\mathrm{LSSum}\left({W}\right)$
43 8 eldifad ${⊢}{\phi }\to {Z}\in {V}$
44 1 2 lmodvacl
45 16 20 43 44 syl3anc
46 1 4 42 16 17 45 lsmpr
48 1 4 42 16 17 20 lsmpr ${⊢}{\phi }\to {N}\left(\left\{{X},{Y}\right\}\right)={N}\left(\left\{{X}\right\}\right)\mathrm{LSSum}\left({W}\right){N}\left(\left\{{Y}\right\}\right)$