Metamath Proof Explorer

Theorem dochexmidlem4

Description: Lemma for dochexmid . (Contributed by NM, 15-Jan-2015)

Ref Expression
Hypotheses dochexmidlem1.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dochexmidlem1.o
dochexmidlem1.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dochexmidlem1.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
dochexmidlem1.s ${⊢}{S}=\mathrm{LSubSp}\left({U}\right)$
dochexmidlem1.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
dochexmidlem1.p
dochexmidlem1.a ${⊢}{A}=\mathrm{LSAtoms}\left({U}\right)$
dochexmidlem1.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
dochexmidlem1.x ${⊢}{\phi }\to {X}\in {S}$
dochexmidlem4.pp ${⊢}{\phi }\to {p}\in {A}$
dochexmidlem4.qq ${⊢}{\phi }\to {q}\in {A}$
dochexmidlem4.z
dochexmidlem4.m
dochexmidlem4.xn
dochexmidlem4.pl
Assertion dochexmidlem4

Proof

Step Hyp Ref Expression
1 dochexmidlem1.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 dochexmidlem1.o
3 dochexmidlem1.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
4 dochexmidlem1.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
5 dochexmidlem1.s ${⊢}{S}=\mathrm{LSubSp}\left({U}\right)$
6 dochexmidlem1.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
7 dochexmidlem1.p
8 dochexmidlem1.a ${⊢}{A}=\mathrm{LSAtoms}\left({U}\right)$
9 dochexmidlem1.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
10 dochexmidlem1.x ${⊢}{\phi }\to {X}\in {S}$
11 dochexmidlem4.pp ${⊢}{\phi }\to {p}\in {A}$
12 dochexmidlem4.qq ${⊢}{\phi }\to {q}\in {A}$
13 dochexmidlem4.z
14 dochexmidlem4.m
15 dochexmidlem4.xn
16 dochexmidlem4.pl
17 1 3 9 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
18 5 8 17 11 lsatlssel ${⊢}{\phi }\to {p}\in {S}$
19 inss2
20 16 19 sstrdi ${⊢}{\phi }\to {q}\subseteq {M}$
21 20 14 sseqtrdi
22 13 5 7 8 17 10 18 12 15 21 lsmsat