Metamath Proof Explorer

Theorem dihord5apre

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

Ref Expression
Hypotheses dihord5apre.b 
|- B = ( Base ` K )
dihord5apre.l 
|- .<_ = ( le ` K )
dihord5apre.h 
|- H = ( LHyp ` K )
dihord5apre.j 
|- .\/ = ( join ` K )
dihord5apre.m 
|- ./\ = ( meet ` K )
dihord5apre.a 
|- A = ( Atoms ` K )
dihord5apre.u 
|- U = ( ( DVecH ` K ) ` W )
dihord5apre.s 
|- .(+) = ( LSSum ` U )
dihord5apre.i 
|- I = ( ( DIsoH ` K ) ` W )
Assertion dihord5apre 
|- ( ( ( ( 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 dihord5apre.b 
 |-  B = ( Base ` K )
2 dihord5apre.l 
 |-  .<_ = ( le ` K )
3 dihord5apre.h 
 |-  H = ( LHyp ` K )
4 dihord5apre.j 
 |-  .\/ = ( join ` K )
5 dihord5apre.m 
 |-  ./\ = ( meet ` K )
6 dihord5apre.a 
 |-  A = ( Atoms ` K )
7 dihord5apre.u 
 |-  U = ( ( DVecH ` K ) ` W )
8 dihord5apre.s 
 |-  .(+) = ( LSSum ` U )
9 dihord5apre.i 
 |-  I = ( ( DIsoH ` K ) ` W )
10 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) ) -> ( K e. HL /\ W e. H ) )
11 simpl3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) ) -> ( Y e. B /\ -. Y .<_ W ) )
12 1 2 4 5 6 3 lhpmcvr2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Y e. B /\ -. Y .<_ W ) ) -> E. r e. A ( -. r .<_ W /\ ( r .\/ ( Y ./\ W ) ) = Y ) )
13 10 11 12 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) ) -> E. r e. A ( -. r .<_ W /\ ( r .\/ ( Y ./\ W ) ) = Y ) )
14 simp11l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> K e. HL )
15 14 hllatd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> K e. Lat )
16 simp12l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> X e. B )
17 simp3ll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> r e. A )
18 1 6 atbase 
 |-  ( r e. A -> r e. B )
19 17 18 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> r e. B )
20 1 4 latjcl 
 |-  ( ( K e. Lat /\ r e. B /\ X e. B ) -> ( r .\/ X ) e. B )
21 15 19 16 20 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( r .\/ X ) e. B )
22 simp13l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> Y e. B )
23 1 2 4 latlej2 
 |-  ( ( K e. Lat /\ r e. B /\ X e. B ) -> X .<_ ( r .\/ X ) )
24 15 19 16 23 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> X .<_ ( r .\/ X ) )
25 simp11 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( K e. HL /\ W e. H ) )
26 simp3lr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> -. r .<_ W )
27 1 2 4 latlej1 
 |-  ( ( K e. Lat /\ r e. B /\ X e. B ) -> r .<_ ( r .\/ X ) )
28 15 19 16 27 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> r .<_ ( r .\/ X ) )
29 simp11r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> W e. H )
30 1 3 lhpbase 
 |-  ( W e. H -> W e. B )
31 29 30 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> W e. B )
32 1 2 lattr 
 |-  ( ( K e. Lat /\ ( r e. B /\ ( r .\/ X ) e. B /\ W e. B ) ) -> ( ( r .<_ ( r .\/ X ) /\ ( r .\/ X ) .<_ W ) -> r .<_ W ) )
33 15 19 21 31 32 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( ( r .<_ ( r .\/ X ) /\ ( r .\/ X ) .<_ W ) -> r .<_ W ) )
34 28 33 mpand 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( ( r .\/ X ) .<_ W -> r .<_ W ) )
35 26 34 mtod 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> -. ( r .\/ X ) .<_ W )
36 simp3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( r e. A /\ -. r .<_ W ) )
37 simp12 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( X e. B /\ X .<_ W ) )
38 1 2 4 5 6 3 lhple 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( r e. A /\ -. r .<_ W ) /\ ( X e. B /\ X .<_ W ) ) -> ( ( r .\/ X ) ./\ W ) = X )
39 25 36 37 38 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( ( r .\/ X ) ./\ W ) = X )
40 39 oveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( r .\/ ( ( r .\/ X ) ./\ W ) ) = ( r .\/ X ) )
41 eqid 
 |-  ( ( DIsoB ` K ) ` W ) = ( ( DIsoB ` K ) ` W )
42 eqid 
 |-  ( ( DIsoC ` K ) ` W ) = ( ( DIsoC ` K ) ` W )
43 1 2 4 5 6 3 9 41 42 7 8 dihvalcq 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( r .\/ X ) e. B /\ -. ( r .\/ X ) .<_ W ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( ( r .\/ X ) ./\ W ) ) = ( r .\/ X ) ) ) -> ( I ` ( r .\/ X ) ) = ( ( ( ( DIsoC ` K ) ` W ) ` r ) .(+) ( ( ( DIsoB ` K ) ` W ) ` ( ( r .\/ X ) ./\ W ) ) ) )
44 25 21 35 36 40 43 syl122anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( I ` ( r .\/ X ) ) = ( ( ( ( DIsoC ` K ) ` W ) ` r ) .(+) ( ( ( DIsoB ` K ) ` W ) ` ( ( r .\/ X ) ./\ W ) ) ) )
45 3 7 25 dvhlmod 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> U e. LMod )
46 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
47 46 lsssssubg 
 |-  ( U e. LMod -> ( LSubSp ` U ) C_ ( SubGrp ` U ) )
48 45 47 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( LSubSp ` U ) C_ ( SubGrp ` U ) )
49 2 6 3 7 42 46 diclss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( r e. A /\ -. r .<_ W ) ) -> ( ( ( DIsoC ` K ) ` W ) ` r ) e. ( LSubSp ` U ) )
50 25 36 49 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( ( ( DIsoC ` K ) ` W ) ` r ) e. ( LSubSp ` U ) )
51 48 50 sseldd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( ( ( DIsoC ` K ) ` W ) ` r ) e. ( SubGrp ` U ) )
52 1 5 latmcl 
 |-  ( ( K e. Lat /\ Y e. B /\ W e. B ) -> ( Y ./\ W ) e. B )
53 15 22 31 52 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( Y ./\ W ) e. B )
54 1 2 5 latmle2 
 |-  ( ( K e. Lat /\ Y e. B /\ W e. B ) -> ( Y ./\ W ) .<_ W )
55 15 22 31 54 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( Y ./\ W ) .<_ W )
56 1 2 3 7 41 46 diblss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Y ./\ W ) e. B /\ ( Y ./\ W ) .<_ W ) ) -> ( ( ( DIsoB ` K ) ` W ) ` ( Y ./\ W ) ) e. ( LSubSp ` U ) )
57 25 53 55 56 syl12anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( ( ( DIsoB ` K ) ` W ) ` ( Y ./\ W ) ) e. ( LSubSp ` U ) )
58 48 57 sseldd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( ( ( DIsoB ` K ) ` W ) ` ( Y ./\ W ) ) e. ( SubGrp ` U ) )
59 8 lsmub1 
 |-  ( ( ( ( ( DIsoC ` K ) ` W ) ` r ) e. ( SubGrp ` U ) /\ ( ( ( DIsoB ` K ) ` W ) ` ( Y ./\ W ) ) e. ( SubGrp ` U ) ) -> ( ( ( DIsoC ` K ) ` W ) ` r ) C_ ( ( ( ( DIsoC ` K ) ` W ) ` r ) .(+) ( ( ( DIsoB ` K ) ` W ) ` ( Y ./\ W ) ) ) )
60 51 58 59 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( ( ( DIsoC ` K ) ` W ) ` r ) C_ ( ( ( ( DIsoC ` K ) ` W ) ` r ) .(+) ( ( ( DIsoB ` K ) ` W ) ` ( Y ./\ W ) ) ) )
61 simp13 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( Y e. B /\ -. Y .<_ W ) )
62 simp3r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( r .\/ ( Y ./\ W ) ) = Y )
63 1 2 4 5 6 3 9 41 42 7 8 dihvalcq 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Y e. B /\ -. Y .<_ W ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( I ` Y ) = ( ( ( ( DIsoC ` K ) ` W ) ` r ) .(+) ( ( ( DIsoB ` K ) ` W ) ` ( Y ./\ W ) ) ) )
64 25 61 36 62 63 syl112anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( I ` Y ) = ( ( ( ( DIsoC ` K ) ` W ) ` r ) .(+) ( ( ( DIsoB ` K ) ` W ) ` ( Y ./\ W ) ) ) )
65 60 64 sseqtrrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( ( ( DIsoC ` K ) ` W ) ` r ) C_ ( I ` Y ) )
66 39 fveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( ( ( DIsoB ` K ) ` W ) ` ( ( r .\/ X ) ./\ W ) ) = ( ( ( DIsoB ` K ) ` W ) ` X ) )
67 1 2 3 9 41 dihvalb 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) = ( ( ( DIsoB ` K ) ` W ) ` X ) )
68 25 37 67 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( I ` X ) = ( ( ( DIsoB ` K ) ` W ) ` X ) )
69 66 68 eqtr4d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( ( ( DIsoB ` K ) ` W ) ` ( ( r .\/ X ) ./\ W ) ) = ( I ` X ) )
70 simp2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( I ` X ) C_ ( I ` Y ) )
71 69 70 eqsstrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( ( ( DIsoB ` K ) ` W ) ` ( ( r .\/ X ) ./\ W ) ) C_ ( I ` Y ) )
72 1 5 latmcl 
 |-  ( ( K e. Lat /\ ( r .\/ X ) e. B /\ W e. B ) -> ( ( r .\/ X ) ./\ W ) e. B )
73 15 21 31 72 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( ( r .\/ X ) ./\ W ) e. B )
74 1 2 5 latmle2 
 |-  ( ( K e. Lat /\ ( r .\/ X ) e. B /\ W e. B ) -> ( ( r .\/ X ) ./\ W ) .<_ W )
75 15 21 31 74 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( ( r .\/ X ) ./\ W ) .<_ W )
76 1 2 3 7 41 46 diblss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( ( r .\/ X ) ./\ W ) e. B /\ ( ( r .\/ X ) ./\ W ) .<_ W ) ) -> ( ( ( DIsoB ` K ) ` W ) ` ( ( r .\/ X ) ./\ W ) ) e. ( LSubSp ` U ) )
77 25 73 75 76 syl12anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( ( ( DIsoB ` K ) ` W ) ` ( ( r .\/ X ) ./\ W ) ) e. ( LSubSp ` U ) )
78 48 77 sseldd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( ( ( DIsoB ` K ) ` W ) ` ( ( r .\/ X ) ./\ W ) ) e. ( SubGrp ` U ) )
79 1 3 9 7 46 dihlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y e. B ) -> ( I ` Y ) e. ( LSubSp ` U ) )
80 25 22 79 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( I ` Y ) e. ( LSubSp ` U ) )
81 48 80 sseldd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( I ` Y ) e. ( SubGrp ` U ) )
82 8 lsmlub 
 |-  ( ( ( ( ( DIsoC ` K ) ` W ) ` r ) e. ( SubGrp ` U ) /\ ( ( ( DIsoB ` K ) ` W ) ` ( ( r .\/ X ) ./\ W ) ) e. ( SubGrp ` U ) /\ ( I ` Y ) e. ( SubGrp ` U ) ) -> ( ( ( ( ( DIsoC ` K ) ` W ) ` r ) C_ ( I ` Y ) /\ ( ( ( DIsoB ` K ) ` W ) ` ( ( r .\/ X ) ./\ W ) ) C_ ( I ` Y ) ) <-> ( ( ( ( DIsoC ` K ) ` W ) ` r ) .(+) ( ( ( DIsoB ` K ) ` W ) ` ( ( r .\/ X ) ./\ W ) ) ) C_ ( I ` Y ) ) )
83 51 78 81 82 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( ( ( ( ( DIsoC ` K ) ` W ) ` r ) C_ ( I ` Y ) /\ ( ( ( DIsoB ` K ) ` W ) ` ( ( r .\/ X ) ./\ W ) ) C_ ( I ` Y ) ) <-> ( ( ( ( DIsoC ` K ) ` W ) ` r ) .(+) ( ( ( DIsoB ` K ) ` W ) ` ( ( r .\/ X ) ./\ W ) ) ) C_ ( I ` Y ) ) )
84 65 71 83 mpbi2and 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( ( ( ( DIsoC ` K ) ` W ) ` r ) .(+) ( ( ( DIsoB ` K ) ` W ) ` ( ( r .\/ X ) ./\ W ) ) ) C_ ( I ` Y ) )
85 44 84 eqsstrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( I ` ( r .\/ X ) ) C_ ( I ` Y ) )
86 1 2 3 9 dihord4 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( r .\/ X ) e. B /\ -. ( r .\/ X ) .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) -> ( ( I ` ( r .\/ X ) ) C_ ( I ` Y ) <-> ( r .\/ X ) .<_ Y ) )
87 25 21 35 61 86 syl121anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( ( I ` ( r .\/ X ) ) C_ ( I ` Y ) <-> ( r .\/ X ) .<_ Y ) )
88 85 87 mpbid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> ( r .\/ X ) .<_ Y )
89 1 2 15 16 21 22 24 88 lattrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) /\ ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) ) -> X .<_ Y )
90 89 3expia 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) ) -> ( ( ( r e. A /\ -. r .<_ W ) /\ ( r .\/ ( Y ./\ W ) ) = Y ) -> X .<_ Y ) )
91 90 exp4c 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) ) -> ( r e. A -> ( -. r .<_ W -> ( ( r .\/ ( Y ./\ W ) ) = Y -> X .<_ Y ) ) ) )
92 91 imp4a 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) ) -> ( r e. A -> ( ( -. r .<_ W /\ ( r .\/ ( Y ./\ W ) ) = Y ) -> X .<_ Y ) ) )
93 92 rexlimdv 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) ) -> ( E. r e. A ( -. r .<_ W /\ ( r .\/ ( Y ./\ W ) ) = Y ) -> X .<_ Y ) )
94 13 93 mpd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) ) -> X .<_ Y )