# Metamath Proof Explorer

## Theorem dihord1

Description: Part of proof after Lemma N of Crawley p. 122. Forward ordering property. TODO: change ( Q .\/ ( X ./\ W ) ) = X to Q .<_ X using lhpmcvr3 , here and all theorems below. (Contributed by NM, 2-Mar-2014)

Ref Expression
Hypotheses dihjust.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
dihjust.l
dihjust.j
dihjust.m
dihjust.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
dihjust.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dihjust.i ${⊢}{I}=\mathrm{DIsoB}\left({K}\right)\left({W}\right)$
dihjust.J ${⊢}{J}=\mathrm{DIsoC}\left({K}\right)\left({W}\right)$
dihjust.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dihjust.s
Assertion dihord1

### Proof

Step Hyp Ref Expression
1 dihjust.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 dihjust.l
3 dihjust.j
4 dihjust.m
5 dihjust.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
6 dihjust.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
7 dihjust.i ${⊢}{I}=\mathrm{DIsoB}\left({K}\right)\left({W}\right)$
8 dihjust.J ${⊢}{J}=\mathrm{DIsoC}\left({K}\right)\left({W}\right)$
9 dihjust.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
10 dihjust.s
11 simp11
12 simp13
13 simp12
14 simp11l
15 14 hllatd
16 simp2r
17 simp11r
18 1 6 lhpbase ${⊢}{W}\in {H}\to {W}\in {B}$
19 17 18 syl
20 1 4 latmcl
21 15 16 19 20 syl3anc
22 1 2 4 latmle2
23 15 16 19 22 syl3anc
24 21 23 jca
25 simp12l
26 1 5 atbase ${⊢}{Q}\in {A}\to {Q}\in {B}$
27 25 26 syl
28 simp2l
29 1 4 latmcl
30 15 28 19 29 syl3anc
31 1 3 latjcl
32 15 27 30 31 syl3anc
33 1 2 3 latlej1
34 15 27 30 33 syl3anc
35 simp31
36 simp33
37 35 36 eqbrtrd
38 1 2 15 27 32 16 34 37 lattrd
39 simp32
40 38 39 breqtrrd
41 1 2 3 5 6 9 10 7 8 cdlemn5
42 11 12 13 24 40 41 syl131anc
43 1 2 4 latmlem1
44 15 28 16 19 43 syl13anc
45 36 44 mpd
46 1 2 4 latmle2
47 15 28 19 46 syl3anc
48 1 2 6 7 dibord
49 11 30 47 21 23 48 syl122anc
50 45 49 mpbird
51 6 9 11 dvhlmod
52 eqid ${⊢}\mathrm{LSubSp}\left({U}\right)=\mathrm{LSubSp}\left({U}\right)$
53 52 lsssssubg ${⊢}{U}\in \mathrm{LMod}\to \mathrm{LSubSp}\left({U}\right)\subseteq \mathrm{SubGrp}\left({U}\right)$
54 51 53 syl
55 2 5 6 9 8 52 diclss
56 11 12 55 syl2anc
57 54 56 sseldd
58 1 2 6 9 7 52 diblss
59 11 21 23 58 syl12anc
60 54 59 sseldd
61 10 lsmub2
62 57 60 61 syl2anc
63 50 62 sstrd
64 2 5 6 9 8 52 diclss
65 11 13 64 syl2anc
66 54 65 sseldd
67 1 2 6 9 7 52 diblss
68 11 30 47 67 syl12anc
69 54 68 sseldd
70 52 10 lsmcl
71 51 56 59 70 syl3anc
72 54 71 sseldd
73 10 lsmlub
74 66 69 72 73 syl3anc
75 42 63 74 mpbi2and