# Metamath Proof Explorer

## Theorem mapdh6hN

Description: Lemmma for mapdh6N . Part (6) of Baer p. 48 line 2. (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
mapdh6d.xn ${⊢}{\phi }\to ¬{X}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
mapdh6d.yz ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)={N}\left(\left\{{Z}\right\}\right)$
mapdh6d.y
mapdh6d.z
mapdh6d.w
mapdh6d.wn ${⊢}{\phi }\to ¬{w}\in {N}\left(\left\{{X},{Y}\right\}\right)$
Assertion mapdh6hN

### 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 mapdh6d.xn ${⊢}{\phi }\to ¬{X}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
21 mapdh6d.yz ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)={N}\left(\left\{{Z}\right\}\right)$
22 mapdh6d.y
23 mapdh6d.z
24 mapdh6d.w
25 mapdh6d.wn ${⊢}{\phi }\to ¬{w}\in {N}\left(\left\{{X},{Y}\right\}\right)$
26 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 mapdh6gN
27 3 10 14 lcdlmod ${⊢}{\phi }\to {C}\in \mathrm{LMod}$
28 24 eldifad ${⊢}{\phi }\to {w}\in {V}$
29 3 5 14 dvhlvec ${⊢}{\phi }\to {U}\in \mathrm{LVec}$
30 17 eldifad ${⊢}{\phi }\to {X}\in {V}$
31 22 eldifad ${⊢}{\phi }\to {Y}\in {V}$
32 6 9 29 28 30 31 25 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)$
33 32 simpld ${⊢}{\phi }\to {N}\left(\left\{{w}\right\}\right)\ne {N}\left(\left\{{X}\right\}\right)$
34 33 necomd ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{w}\right\}\right)$
35 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 28 34 mapdhcl ${⊢}{\phi }\to {I}\left(⟨{X},{F},{w}⟩\right)\in {D}$
36 23 eldifad ${⊢}{\phi }\to {Z}\in {V}$
37 6 9 29 30 31 36 20 lspindpi ${⊢}{\phi }\to \left({N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)\wedge {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)\right)$
38 37 simpld ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)$
39 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 31 38 mapdhcl ${⊢}{\phi }\to {I}\left(⟨{X},{F},{Y}⟩\right)\in {D}$
40 37 simprd ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)$
41 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 36 40 mapdhcl ${⊢}{\phi }\to {I}\left(⟨{X},{F},{Z}⟩\right)\in {D}$
42 11 19 lmodass
43 27 35 39 41 42 syl13anc
44 26 43 eqtrd
45 3 5 14 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
46 6 18 lmodvacl
47 45 31 36 46 syl3anc
48 6 18 8 9 29 17 22 23 24 21 38 25 mapdindp1
49 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 47 48 mapdhcl
50 11 19 lmodvacl
51 27 39 41 50 syl3anc
52 11 19 lmodlcan
53 27 49 51 35 52 syl13anc
54 44 53 mpbid