This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( Base ` K )
dihord6apre.l 
|- .<_ = ( le ` K )
dihord6apre.a 
|- A = ( Atoms ` K )
dihord6apre.h 
|- H = ( LHyp ` K )
dihord6apre.p 
|- P = ( ( oc ` K ) ` W )
dihord6apre.o 
|- O = ( h e. T |-> ( _I |` B ) )
dihord6apre.t 
|- T = ( ( LTrn ` K ) ` W )
dihord6apre.e 
|- E = ( ( TEndo ` K ) ` W )
dihord6apre.i 
|- I = ( ( DIsoH ` K ) ` W )
dihord6apre.u 
|- U = ( ( DVecH ` K ) ` W )
dihord6apre.s 
|- .(+) = ( LSSum ` U )
dihord6apre.g 
|- G = ( iota_ h e. T ( h ` P ) = q )
Assertion dihord6apre 
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) ) -> X .<_ Y )

Proof

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