# Metamath Proof Explorer

## Theorem dochexmidlem6

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

### 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 dochexmidlem6.pp ${⊢}{\phi }\to {p}\in {A}$
12 dochexmidlem6.z
13 dochexmidlem6.m
14 dochexmidlem6.xn
15 dochexmidlem6.c
16 dochexmidlem6.pl
17 1 2 3 4 5 6 7 8 9 10 11 12 13 14 16 dochexmidlem5
18 17 fveq2d
19 1 3 2 4 12 doch0
20 9 19 syl
21 18 20 eqtrd
22 21 ineq1d
23 eqid ${⊢}\mathrm{DIsoH}\left({K}\right)\left({W}\right)=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
24 4 5 lssss ${⊢}{X}\in {S}\to {X}\subseteq {V}$
25 10 24 syl ${⊢}{\phi }\to {X}\subseteq {V}$
26 1 3 4 2 dochssv
27 9 25 26 syl2anc
28 1 23 3 4 2 dochcl
29 9 27 28 syl2anc
30 15 29 eqeltrrd ${⊢}{\phi }\to {X}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
31 1 23 3 7 8 9 30 11 dihsmatrn
32 13 31 eqeltrid ${⊢}{\phi }\to {M}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
33 1 3 23 5 dihrnlss ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {M}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)\right)\to {M}\in {S}$
34 9 32 33 syl2anc ${⊢}{\phi }\to {M}\in {S}$
35 1 3 9 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
36 5 8 35 11 lsatlssel ${⊢}{\phi }\to {p}\in {S}$
37 5 7 lsmcl
38 35 10 36 37 syl3anc
39 4 5 lssss
40 38 39 syl
41 13 40 eqsstrid ${⊢}{\phi }\to {M}\subseteq {V}$
42 1 23 3 4 2 9 41 dochoccl
43 32 42 mpbid
44 5 lsssssubg ${⊢}{U}\in \mathrm{LMod}\to {S}\subseteq \mathrm{SubGrp}\left({U}\right)$
45 35 44 syl ${⊢}{\phi }\to {S}\subseteq \mathrm{SubGrp}\left({U}\right)$
46 45 10 sseldd ${⊢}{\phi }\to {X}\in \mathrm{SubGrp}\left({U}\right)$
47 45 36 sseldd ${⊢}{\phi }\to {p}\in \mathrm{SubGrp}\left({U}\right)$
48 7 lsmub1
49 46 47 48 syl2anc
50 49 13 sseqtrrdi ${⊢}{\phi }\to {X}\subseteq {M}$
51 1 3 5 2 9 10 34 43 50 dihoml4
52 sseqin2 ${⊢}{M}\subseteq {V}↔{V}\cap {M}={M}$
53 41 52 sylib ${⊢}{\phi }\to {V}\cap {M}={M}$
54 22 51 53 3eqtr3rd
55 54 15 eqtrd ${⊢}{\phi }\to {M}={X}$