# Metamath Proof Explorer

## Theorem mapdh6iN

Description: Lemmma for mapdh6N . Eliminate auxiliary vector w . (Contributed by NM, 1-May-2015) (New usage is discouraged.)

Ref Expression
Hypotheses mapdh.q ${⊢}{Q}={0}_{{C}}$
mapdh.i
mapdh.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
mapdh.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
mapdh.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
mapdh.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
mapdh.s
mapdhc.o
mapdh.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
mapdh.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
mapdh.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
mapdh.r ${⊢}{R}={-}_{{C}}$
mapdh.j ${⊢}{J}=\mathrm{LSpan}\left({C}\right)$
mapdh.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
mapdhc.f ${⊢}{\phi }\to {F}\in {D}$
mapdh.mn ${⊢}{\phi }\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={J}\left(\left\{{F}\right\}\right)$
mapdhcl.x
mapdh.p
mapdh.a
mapdh6i.xn ${⊢}{\phi }\to ¬{X}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
mapdh6i.y
mapdh6i.z
mapdh6i.yz ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)={N}\left(\left\{{Z}\right\}\right)$
Assertion mapdh6iN

### Proof

Step Hyp Ref Expression
1 mapdh.q ${⊢}{Q}={0}_{{C}}$
2 mapdh.i
3 mapdh.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
4 mapdh.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
5 mapdh.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
6 mapdh.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
7 mapdh.s
8 mapdhc.o
9 mapdh.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
10 mapdh.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
11 mapdh.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
12 mapdh.r ${⊢}{R}={-}_{{C}}$
13 mapdh.j ${⊢}{J}=\mathrm{LSpan}\left({C}\right)$
14 mapdh.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
15 mapdhc.f ${⊢}{\phi }\to {F}\in {D}$
16 mapdh.mn ${⊢}{\phi }\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={J}\left(\left\{{F}\right\}\right)$
17 mapdhcl.x
18 mapdh.p
19 mapdh.a
20 mapdh6i.xn ${⊢}{\phi }\to ¬{X}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
21 mapdh6i.y
22 mapdh6i.z
23 mapdh6i.yz ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)={N}\left(\left\{{Z}\right\}\right)$
24 17 eldifad ${⊢}{\phi }\to {X}\in {V}$
25 21 eldifad ${⊢}{\phi }\to {Y}\in {V}$
26 3 5 6 9 14 24 25 dvh3dim ${⊢}{\phi }\to \exists {w}\in {V}\phantom{\rule{.4em}{0ex}}¬{w}\in {N}\left(\left\{{X},{Y}\right\}\right)$
27 14 3ad2ant1 ${⊢}\left({\phi }\wedge {w}\in {V}\wedge ¬{w}\in {N}\left(\left\{{X},{Y}\right\}\right)\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
28 15 3ad2ant1 ${⊢}\left({\phi }\wedge {w}\in {V}\wedge ¬{w}\in {N}\left(\left\{{X},{Y}\right\}\right)\right)\to {F}\in {D}$
29 16 3ad2ant1 ${⊢}\left({\phi }\wedge {w}\in {V}\wedge ¬{w}\in {N}\left(\left\{{X},{Y}\right\}\right)\right)\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={J}\left(\left\{{F}\right\}\right)$
31 20 3ad2ant1 ${⊢}\left({\phi }\wedge {w}\in {V}\wedge ¬{w}\in {N}\left(\left\{{X},{Y}\right\}\right)\right)\to ¬{X}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
32 23 3ad2ant1 ${⊢}\left({\phi }\wedge {w}\in {V}\wedge ¬{w}\in {N}\left(\left\{{X},{Y}\right\}\right)\right)\to {N}\left(\left\{{Y}\right\}\right)={N}\left(\left\{{Z}\right\}\right)$
35 eqid ${⊢}\mathrm{LSubSp}\left({U}\right)=\mathrm{LSubSp}\left({U}\right)$
36 3 5 14 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
37 36 3ad2ant1 ${⊢}\left({\phi }\wedge {w}\in {V}\wedge ¬{w}\in {N}\left(\left\{{X},{Y}\right\}\right)\right)\to {U}\in \mathrm{LMod}$
38 6 35 9 36 24 25 lspprcl ${⊢}{\phi }\to {N}\left(\left\{{X},{Y}\right\}\right)\in \mathrm{LSubSp}\left({U}\right)$
39 38 3ad2ant1 ${⊢}\left({\phi }\wedge {w}\in {V}\wedge ¬{w}\in {N}\left(\left\{{X},{Y}\right\}\right)\right)\to {N}\left(\left\{{X},{Y}\right\}\right)\in \mathrm{LSubSp}\left({U}\right)$
40 simp2 ${⊢}\left({\phi }\wedge {w}\in {V}\wedge ¬{w}\in {N}\left(\left\{{X},{Y}\right\}\right)\right)\to {w}\in {V}$
41 simp3 ${⊢}\left({\phi }\wedge {w}\in {V}\wedge ¬{w}\in {N}\left(\left\{{X},{Y}\right\}\right)\right)\to ¬{w}\in {N}\left(\left\{{X},{Y}\right\}\right)$