Metamath Proof Explorer

Theorem dihord4

Description: The isomorphism H for a lattice K is order-preserving in the region not under co-atom W . TODO: reformat ( q e. A /\ -. q .<_ W ) to eliminate adant*. (Contributed by NM, 6-Mar-2014)

Ref Expression
Hypotheses dihord3.b 
|- B = ( Base ` K )
dihord3.l 
|- .<_ = ( le ` K )
dihord3.h 
|- H = ( LHyp ` K )
dihord3.i 
|- I = ( ( DIsoH ` K ) ` W )
Assertion dihord4 
|- ( ( ( 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 dihord3.b 
 |-  B = ( Base ` K )
2 dihord3.l 
 |-  .<_ = ( le ` K )
3 dihord3.h 
 |-  H = ( LHyp ` K )
4 dihord3.i 
 |-  I = ( ( DIsoH ` K ) ` W )
5 eqid 
 |-  ( join ` K ) = ( join ` K )
6 eqid 
 |-  ( meet ` K ) = ( meet ` K )
7 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
8 1 2 5 6 7 3 lhpmcvr2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> E. q e. ( Atoms ` K ) ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) )
9 8 3adant3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) -> E. q e. ( Atoms ` K ) ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) )
10 1 2 5 6 7 3 lhpmcvr2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Y e. B /\ -. Y .<_ W ) ) -> E. r e. ( Atoms ` K ) ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) )
11 10 3adant2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) -> E. r e. ( Atoms ` K ) ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) )
12 reeanv 
 |-  ( E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) <-> ( E. q e. ( Atoms ` K ) ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ E. r e. ( Atoms ` K ) ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) )
13 9 11 12 sylanbrc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) -> E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) )
14 simp11 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) -> ( K e. HL /\ W e. H ) )
15 simp12 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) -> ( X e. B /\ -. X .<_ W ) )
16 simp2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) -> q e. ( Atoms ` K ) )
17 simp3ll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) -> -. q .<_ W )
18 16 17 jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) -> ( q e. ( Atoms ` K ) /\ -. q .<_ W ) )
19 simp3lr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) -> ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X )
20 eqid 
 |-  ( ( DIsoB ` K ) ` W ) = ( ( DIsoB ` K ) ` W )
21 eqid 
 |-  ( ( DIsoC ` K ) ` W ) = ( ( DIsoC ` K ) ` W )
22 eqid 
 |-  ( ( DVecH ` K ) ` W ) = ( ( DVecH ` K ) ` W )
23 eqid 
 |-  ( LSSum ` ( ( DVecH ` K ) ` W ) ) = ( LSSum ` ( ( DVecH ` K ) ` W ) )
24 1 2 5 6 7 3 4 20 21 22 23 dihvalcq 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. ( Atoms ` K ) /\ -. q .<_ W ) /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) ) -> ( I ` X ) = ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( X ( meet ` K ) W ) ) ) )
25 14 15 18 19 24 syl112anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) -> ( I ` X ) = ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( X ( meet ` K ) W ) ) ) )
26 simp13 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) -> ( Y e. B /\ -. Y .<_ W ) )
27 simp2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) -> r e. ( Atoms ` K ) )
28 simp3rl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) -> -. r .<_ W )
29 27 28 jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) -> ( r e. ( Atoms ` K ) /\ -. r .<_ W ) )
30 simp3rr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) -> ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y )
31 1 2 5 6 7 3 4 20 21 22 23 dihvalcq 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Y e. B /\ -. Y .<_ W ) /\ ( ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) -> ( I ` Y ) = ( ( ( ( DIsoC ` K ) ` W ) ` r ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) ) )
32 14 26 29 30 31 syl112anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) -> ( I ` Y ) = ( ( ( ( DIsoC ` K ) ` W ) ` r ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) ) )
33 25 32 sseq12d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) -> ( ( I ` X ) C_ ( I ` Y ) <-> ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( X ( meet ` K ) W ) ) ) C_ ( ( ( ( DIsoC ` K ) ` W ) ` r ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) ) ) )
34 simpl11 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) /\ ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( X ( meet ` K ) W ) ) ) C_ ( ( ( ( DIsoC ` K ) ` W ) ` r ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) ) ) -> ( K e. HL /\ W e. H ) )
35 simpl2l 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) /\ ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( X ( meet ` K ) W ) ) ) C_ ( ( ( ( DIsoC ` K ) ` W ) ` r ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) ) ) -> q e. ( Atoms ` K ) )
36 17 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) /\ ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( X ( meet ` K ) W ) ) ) C_ ( ( ( ( DIsoC ` K ) ` W ) ` r ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) ) ) -> -. q .<_ W )
37 35 36 jca 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) /\ ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( X ( meet ` K ) W ) ) ) C_ ( ( ( ( DIsoC ` K ) ` W ) ` r ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) ) ) -> ( q e. ( Atoms ` K ) /\ -. q .<_ W ) )
38 simpl2r 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) /\ ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( X ( meet ` K ) W ) ) ) C_ ( ( ( ( DIsoC ` K ) ` W ) ` r ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) ) ) -> r e. ( Atoms ` K ) )
39 28 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) /\ ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( X ( meet ` K ) W ) ) ) C_ ( ( ( ( DIsoC ` K ) ` W ) ` r ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) ) ) -> -. r .<_ W )
40 38 39 jca 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) /\ ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( X ( meet ` K ) W ) ) ) C_ ( ( ( ( DIsoC ` K ) ` W ) ` r ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) ) ) -> ( r e. ( Atoms ` K ) /\ -. r .<_ W ) )
41 simp12l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) -> X e. B )
42 41 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) /\ ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( X ( meet ` K ) W ) ) ) C_ ( ( ( ( DIsoC ` K ) ` W ) ` r ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) ) ) -> X e. B )
43 simp13l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) -> Y e. B )
44 43 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) /\ ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( X ( meet ` K ) W ) ) ) C_ ( ( ( ( DIsoC ` K ) ` W ) ` r ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) ) ) -> Y e. B )
45 19 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) /\ ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( X ( meet ` K ) W ) ) ) C_ ( ( ( ( DIsoC ` K ) ` W ) ` r ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) ) ) -> ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X )
46 30 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) /\ ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( X ( meet ` K ) W ) ) ) C_ ( ( ( ( DIsoC ` K ) ` W ) ` r ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) ) ) -> ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y )
47 simpr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) /\ ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( X ( meet ` K ) W ) ) ) C_ ( ( ( ( DIsoC ` K ) ` W ) ` r ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) ) ) -> ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( X ( meet ` K ) W ) ) ) C_ ( ( ( ( DIsoC ` K ) ` W ) ` r ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) ) )
48 1 2 5 6 7 3 20 21 22 23 dihord2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( q e. ( Atoms ` K ) /\ -. q .<_ W ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) ) /\ ( X e. B /\ Y e. B ) /\ ( ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y /\ ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( X ( meet ` K ) W ) ) ) C_ ( ( ( ( DIsoC ` K ) ` W ) ` r ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) ) ) ) -> X .<_ Y )
49 34 37 40 42 44 45 46 47 48 syl323anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) /\ ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( X ( meet ` K ) W ) ) ) C_ ( ( ( ( DIsoC ` K ) ` W ) ` r ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) ) ) -> X .<_ Y )
50 simpl11 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) /\ X .<_ Y ) -> ( K e. HL /\ W e. H ) )
51 simpl2l 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) /\ X .<_ Y ) -> q e. ( Atoms ` K ) )
52 17 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) /\ X .<_ Y ) -> -. q .<_ W )
53 51 52 jca 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) /\ X .<_ Y ) -> ( q e. ( Atoms ` K ) /\ -. q .<_ W ) )
54 simpl2r 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) /\ X .<_ Y ) -> r e. ( Atoms ` K ) )
55 28 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) /\ X .<_ Y ) -> -. r .<_ W )
56 54 55 jca 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) /\ X .<_ Y ) -> ( r e. ( Atoms ` K ) /\ -. r .<_ W ) )
57 41 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) /\ X .<_ Y ) -> X e. B )
58 43 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) /\ X .<_ Y ) -> Y e. B )
59 19 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) /\ X .<_ Y ) -> ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X )
60 30 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) /\ X .<_ Y ) -> ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y )
61 simpr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) /\ X .<_ Y ) -> X .<_ Y )
62 1 2 5 6 7 3 20 21 22 23 dihord1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( q e. ( Atoms ` K ) /\ -. q .<_ W ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) ) /\ ( X e. B /\ Y e. B ) /\ ( ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y /\ X .<_ Y ) ) -> ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( X ( meet ` K ) W ) ) ) C_ ( ( ( ( DIsoC ` K ) ` W ) ` r ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) ) )
63 50 53 56 57 58 59 60 61 62 syl323anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) /\ X .<_ Y ) -> ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( X ( meet ` K ) W ) ) ) C_ ( ( ( ( DIsoC ` K ) ` W ) ` r ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) ) )
64 49 63 impbida 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) -> ( ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( X ( meet ` K ) W ) ) ) C_ ( ( ( ( DIsoC ` K ) ` W ) ` r ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) ) <-> X .<_ Y ) )
65 33 64 bitrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) ) -> ( ( I ` X ) C_ ( I ` Y ) <-> X .<_ Y ) )
66 65 3exp 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) -> ( ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) -> ( ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) -> ( ( I ` X ) C_ ( I ` Y ) <-> X .<_ Y ) ) ) )
67 66 rexlimdvv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) -> ( E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) /\ ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) -> ( ( I ` X ) C_ ( I ` Y ) <-> X .<_ Y ) ) )
68 13 67 mpd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) -> ( ( I ` X ) C_ ( I ` Y ) <-> X .<_ Y ) )