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 = ( Base ` K )
dihjust.l 
|- .<_ = ( le ` K )
dihjust.j 
|- .\/ = ( join ` K )
dihjust.m 
|- ./\ = ( meet ` K )
dihjust.a 
|- A = ( Atoms ` K )
dihjust.h 
|- H = ( LHyp ` K )
dihjust.i 
|- I = ( ( DIsoB ` K ) ` W )
dihjust.J 
|- J = ( ( DIsoC ` K ) ` W )
dihjust.u 
|- U = ( ( DVecH ` K ) ` W )
dihjust.s 
|- .(+) = ( LSSum ` U )
Assertion dihord1 
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( X e. B /\ Y e. B ) /\ ( ( Q .\/ ( X ./\ W ) ) = X /\ ( R .\/ ( Y ./\ W ) ) = Y /\ X .<_ Y ) ) -> ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` R ) .(+) ( I ` ( Y ./\ W ) ) ) )

Proof

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