# Metamath Proof Explorer

## Theorem dochexmidlem5

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}$
dochexmidlem5.pp ${⊢}{\phi }\to {p}\in {A}$
dochexmidlem5.z
dochexmidlem5.m
dochexmidlem5.xn
dochexmidlem5.pl
Assertion dochexmidlem5

### 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 dochexmidlem5.pp ${⊢}{\phi }\to {p}\in {A}$
12 dochexmidlem5.z
13 dochexmidlem5.m
14 dochexmidlem5.xn
15 dochexmidlem5.pl
16 1 3 9 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
18 4 5 lssss ${⊢}{X}\in {S}\to {X}\subseteq {V}$
19 10 18 syl ${⊢}{\phi }\to {X}\subseteq {V}$
20 1 3 4 5 2 dochlss
21 9 19 20 syl2anc
22 5 8 16 11 lsatlssel ${⊢}{\phi }\to {p}\in {S}$
23 5 7 lsmcl
24 16 10 22 23 syl3anc
25 13 24 eqeltrid ${⊢}{\phi }\to {M}\in {S}$
26 5 lssincl
27 16 21 25 26 syl3anc
29 simpr
30 5 12 8 17 28 29 lssatomic
31 30 ex