# Metamath Proof Explorer

## Theorem dihord6apre

Description: Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014)

Ref Expression
Hypotheses dihord6apre.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
dihord6apre.l
dihord6apre.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
dihord6apre.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dihord6apre.p ${⊢}{P}=\mathrm{oc}\left({K}\right)\left({W}\right)$
dihord6apre.o ${⊢}{O}=\left({h}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)$
dihord6apre.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
dihord6apre.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
dihord6apre.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
dihord6apre.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dihord6apre.s
dihord6apre.g ${⊢}{G}=\left(\iota {h}\in {T}|{h}\left({P}\right)={q}\right)$
Assertion dihord6apre

### Proof

Step Hyp Ref Expression
1 dihord6apre.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 dihord6apre.l
3 dihord6apre.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
4 dihord6apre.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
5 dihord6apre.p ${⊢}{P}=\mathrm{oc}\left({K}\right)\left({W}\right)$
6 dihord6apre.o ${⊢}{O}=\left({h}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)$
7 dihord6apre.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
8 dihord6apre.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
9 dihord6apre.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
10 dihord6apre.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
11 dihord6apre.s
12 dihord6apre.g ${⊢}{G}=\left(\iota {h}\in {T}|{h}\left({P}\right)={q}\right)$
13 1 4 7 8 6 tendo1ne0 ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {\mathrm{I}↾}_{{T}}\ne {O}$
15 14 neneqd
16 eqid ${⊢}\mathrm{join}\left({K}\right)=\mathrm{join}\left({K}\right)$
17 eqid ${⊢}\mathrm{meet}\left({K}\right)=\mathrm{meet}\left({K}\right)$
18 1 2 16 17 3 4 lhpmcvr2
20 simpl1
21 simpl2
22 simpr
23 eqid ${⊢}\mathrm{DIsoB}\left({K}\right)\left({W}\right)=\mathrm{DIsoB}\left({K}\right)\left({W}\right)$
24 eqid ${⊢}\mathrm{DIsoC}\left({K}\right)\left({W}\right)=\mathrm{DIsoC}\left({K}\right)\left({W}\right)$
25 1 2 16 17 3 4 9 23 24 10 11 dihvalcq
26 20 21 22 25 syl3anc
27 simpl3
28 1 2 4 9 23 dihvalb
29 20 27 28 syl2anc
30 26 29 sseq12d
31 4 10 20 dvhlmod
32 eqid ${⊢}\mathrm{LSubSp}\left({U}\right)=\mathrm{LSubSp}\left({U}\right)$
33 32 lsssssubg ${⊢}{U}\in \mathrm{LMod}\to \mathrm{LSubSp}\left({U}\right)\subseteq \mathrm{SubGrp}\left({U}\right)$
34 31 33 syl
35 simprl
36 2 3 4 10 24 32 diclss
37 20 35 36 syl2anc
38 34 37 sseldd
39 simpl1l
40 39 hllatd
41 simpl2l
42 simpl1r
43 1 4 lhpbase ${⊢}{W}\in {H}\to {W}\in {B}$
44 42 43 syl
45 1 17 latmcl ${⊢}\left({K}\in \mathrm{Lat}\wedge {X}\in {B}\wedge {W}\in {B}\right)\to {X}\mathrm{meet}\left({K}\right){W}\in {B}$
46 40 41 44 45 syl3anc
47 1 2 17 latmle2
48 40 41 44 47 syl3anc
49 1 2 4 10 23 32 diblss
50 20 46 48 49 syl12anc
51 34 50 sseldd
52 11 lsmub1
53 38 51 52 syl2anc
54 sstr
55 eqidd
56 4 7 8 tendoidcl ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {\mathrm{I}↾}_{{T}}\in {E}$
57 20 56 syl
58 fvex ${⊢}\left({\mathrm{I}↾}_{{T}}\right)\left({G}\right)\in \mathrm{V}$
59 7 fvexi ${⊢}{T}\in \mathrm{V}$
60 resiexg ${⊢}{T}\in \mathrm{V}\to {\mathrm{I}↾}_{{T}}\in \mathrm{V}$
61 59 60 ax-mp ${⊢}{\mathrm{I}↾}_{{T}}\in \mathrm{V}$
62 2 3 4 5 7 8 24 12 58 61 dicopelval2
63 20 35 62 syl2anc
64 55 57 63 mpbir2and
65 ssel2 ${⊢}\left(\mathrm{DIsoC}\left({K}\right)\left({W}\right)\left({q}\right)\subseteq \mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({Y}\right)\wedge ⟨\left({\mathrm{I}↾}_{{T}}\right)\left({G}\right),{\mathrm{I}↾}_{{T}}⟩\in \mathrm{DIsoC}\left({K}\right)\left({W}\right)\left({q}\right)\right)\to ⟨\left({\mathrm{I}↾}_{{T}}\right)\left({G}\right),{\mathrm{I}↾}_{{T}}⟩\in \mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({Y}\right)$
66 eqid ${⊢}\mathrm{DIsoA}\left({K}\right)\left({W}\right)=\mathrm{DIsoA}\left({K}\right)\left({W}\right)$
67 1 2 4 7 6 66 23 dibopelval2
68 20 27 67 syl2anc
69 simpr ${⊢}\left(\left({\mathrm{I}↾}_{{T}}\right)\left({G}\right)\in \mathrm{DIsoA}\left({K}\right)\left({W}\right)\left({Y}\right)\wedge {\mathrm{I}↾}_{{T}}={O}\right)\to {\mathrm{I}↾}_{{T}}={O}$
70 68 69 syl6bi
71 65 70 syl5
72 64 71 mpan2d
73 54 72 syl5
74 53 73 mpand
75 30 74 sylbid
76 75 exp44
77 76 imp4a
78 77 rexlimdv
79 19 78 mpd
80 15 79 mtod
81 80 pm2.21d
82 81 imp