# Metamath Proof Explorer

## Theorem hdmap1l6a

Description: Lemma for hdmap1l6 . Part (6) in Baer p. 47, case 1. (Contributed by NM, 23-Apr-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)$
hdmap1l6e.y
hdmap1l6e.z
hdmap1l6e.xn ${⊢}{\phi }\to ¬{X}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
hdmap1l6.yz ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)$
hdmap1l6.fg ${⊢}{\phi }\to {I}\left(⟨{X},{F},{Y}⟩\right)={G}$
hdmap1l6.fe ${⊢}{\phi }\to {I}\left(⟨{X},{F},{Z}⟩\right)={E}$
Assertion hdmap1l6a

### 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 hdmap1l6e.y
21 hdmap1l6e.z
22 hdmap1l6e.xn ${⊢}{\phi }\to ¬{X}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
23 hdmap1l6.yz ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)$
24 hdmap1l6.fg ${⊢}{\phi }\to {I}\left(⟨{X},{F},{Y}⟩\right)={G}$
25 hdmap1l6.fe ${⊢}{\phi }\to {I}\left(⟨{X},{F},{Z}⟩\right)={E}$
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 hdmap1l6lem2
27 24 25 oveq12d
28 27 sneqd
29 28 fveq2d
30 26 29 eqtr4d
31 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 hdmap1l6lem1
32 27 oveq2d
33 32 sneqd
34 33 fveq2d
35 31 34 eqtr4d
36 1 2 16 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
37 20 eldifad ${⊢}{\phi }\to {Y}\in {V}$
38 21 eldifad ${⊢}{\phi }\to {Z}\in {V}$
39 3 4 lmodvacl
40 36 37 38 39 syl3anc
41 3 4 6 7 36 37 38 23 lmodindp1
42 eldifsn
43 40 41 42 sylanbrc
44 1 8 16 lcdlmod ${⊢}{\phi }\to {C}\in \mathrm{LMod}$
45 1 2 16 dvhlvec ${⊢}{\phi }\to {U}\in \mathrm{LVec}$
46 18 eldifad ${⊢}{\phi }\to {X}\in {V}$
47 3 6 7 45 37 21 46 23 22 lspindp2 ${⊢}{\phi }\to \left({N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)\wedge ¬{Z}\in {N}\left(\left\{{X},{Y}\right\}\right)\right)$
48 47 simpld ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)$
49 1 2 3 6 7 8 9 13 14 15 16 17 19 48 18 37 hdmap1cl ${⊢}{\phi }\to {I}\left(⟨{X},{F},{Y}⟩\right)\in {D}$
50 3 6 7 45 20 38 46 23 22 lspindp1 ${⊢}{\phi }\to \left({N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)\wedge ¬{Y}\in {N}\left(\left\{{X},{Z}\right\}\right)\right)$
51 50 simpld ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)$
52 1 2 3 6 7 8 9 13 14 15 16 17 19 51 18 38 hdmap1cl ${⊢}{\phi }\to {I}\left(⟨{X},{F},{Z}⟩\right)\in {D}$
53 9 10 lmodvacl
54 44 49 52 53 syl3anc
55 eqid ${⊢}\mathrm{LSubSp}\left({U}\right)=\mathrm{LSubSp}\left({U}\right)$
56 3 55 7 36 37 38 lspprcl ${⊢}{\phi }\to {N}\left(\left\{{Y},{Z}\right\}\right)\in \mathrm{LSubSp}\left({U}\right)$
57 3 4 7 36 37 38 lspprvacl
58 55 7 36 56 57 lspsnel5a
59 3 55 7 36 56 46 lspsnel5 ${⊢}{\phi }\to \left({X}\in {N}\left(\left\{{Y},{Z}\right\}\right)↔{N}\left(\left\{{X}\right\}\right)\subseteq {N}\left(\left\{{Y},{Z}\right\}\right)\right)$
60 22 59 mtbid ${⊢}{\phi }\to ¬{N}\left(\left\{{X}\right\}\right)\subseteq {N}\left(\left\{{Y},{Z}\right\}\right)$
61 nssne2
62 58 60 61 syl2anc
63 62 necomd
64 1 2 3 5 6 7 8 9 11 13 14 15 16 18 17 43 54 63 19 hdmap1eq
65 30 35 64 mpbir2and