# Metamath Proof Explorer

## Theorem hdmap1l6e

Description: Lemmma for hdmap1l6 . Part (6) in Baer p. 47 line 38. (Contributed by NM, 1-May-2015)

Ref Expression
Hypotheses hdmap1l6.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
hdmap1l6.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
hdmap1l6.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
hdmap1l6.p
hdmap1l6.s
hdmap1l6c.o
hdmap1l6.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
hdmap1l6.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
hdmap1l6.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
hdmap1l6.a
hdmap1l6.r ${⊢}{R}={-}_{{C}}$
hdmap1l6.q ${⊢}{Q}={0}_{{C}}$
hdmap1l6.l ${⊢}{L}=\mathrm{LSpan}\left({C}\right)$
hdmap1l6.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
hdmap1l6.i ${⊢}{I}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)$
hdmap1l6.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
hdmap1l6.f ${⊢}{\phi }\to {F}\in {D}$
hdmap1l6cl.x
hdmap1l6.mn ${⊢}{\phi }\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={L}\left(\left\{{F}\right\}\right)$
hdmap1l6d.xn ${⊢}{\phi }\to ¬{X}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
hdmap1l6d.yz ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)={N}\left(\left\{{Z}\right\}\right)$
hdmap1l6d.y
hdmap1l6d.z
hdmap1l6d.w
hdmap1l6d.wn ${⊢}{\phi }\to ¬{w}\in {N}\left(\left\{{X},{Y}\right\}\right)$
Assertion hdmap1l6e

### Proof

Step Hyp Ref Expression
1 hdmap1l6.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 hdmap1l6.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 hdmap1l6.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
4 hdmap1l6.p
5 hdmap1l6.s
6 hdmap1l6c.o
7 hdmap1l6.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
8 hdmap1l6.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
9 hdmap1l6.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
10 hdmap1l6.a
11 hdmap1l6.r ${⊢}{R}={-}_{{C}}$
12 hdmap1l6.q ${⊢}{Q}={0}_{{C}}$
13 hdmap1l6.l ${⊢}{L}=\mathrm{LSpan}\left({C}\right)$
14 hdmap1l6.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
15 hdmap1l6.i ${⊢}{I}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)$
16 hdmap1l6.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
17 hdmap1l6.f ${⊢}{\phi }\to {F}\in {D}$
18 hdmap1l6cl.x
19 hdmap1l6.mn ${⊢}{\phi }\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={L}\left(\left\{{F}\right\}\right)$
20 hdmap1l6d.xn ${⊢}{\phi }\to ¬{X}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
21 hdmap1l6d.yz ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)={N}\left(\left\{{Z}\right\}\right)$
22 hdmap1l6d.y
23 hdmap1l6d.z
24 hdmap1l6d.w
25 hdmap1l6d.wn ${⊢}{\phi }\to ¬{w}\in {N}\left(\left\{{X},{Y}\right\}\right)$
26 1 2 16 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
27 24 eldifad ${⊢}{\phi }\to {w}\in {V}$
28 22 eldifad ${⊢}{\phi }\to {Y}\in {V}$
29 3 4 lmodvacl
30 26 27 28 29 syl3anc
31 1 2 16 dvhlvec ${⊢}{\phi }\to {U}\in \mathrm{LVec}$
32 18 eldifad ${⊢}{\phi }\to {X}\in {V}$
33 3 7 31 27 32 28 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)$
34 33 simprd ${⊢}{\phi }\to {N}\left(\left\{{w}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)$
35 3 4 6 7 26 27 28 34 lmodindp1
36 eldifsn
37 30 35 36 sylanbrc
38 23 eldifad ${⊢}{\phi }\to {Z}\in {V}$
39 3 7 31 32 28 38 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)$
40 39 simpld ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)$
41 3 4 6 7 31 18 22 23 24 21 40 25 mapdindp3
42 3 4 6 7 31 18 22 23 24 21 40 25 mapdindp4
43 3 6 7 31 18 30 38 41 42 lspindp1
44 43 simprd
45 prcom
46 45 fveq2i
47 46 eleq2i
48 44 47 sylnibr
49 3 7 31 38 32 30 42 lspindpi
50 49 simprd
51 50 necomd
52 eqidd
53 eqidd ${⊢}{\phi }\to {I}\left(⟨{X},{F},{Z}⟩\right)={I}\left(⟨{X},{F},{Z}⟩\right)$
54 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 37 23 48 51 52 53 hdmap1l6a