Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dihord5apre Structured version   Unicode version

Theorem dihord5apre 34742
Description: Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.)
Hypotheses
Ref Expression
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
Ref Expression
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 of Theorem dihord5apre
Dummy variable  r is distinct from all other variables.
StepHypRef Expression
1 simpl1 1008 . . 3  |-  ( ( ( ( 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 ) )
2 simpl3 1010 . . 3  |-  ( ( ( ( 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 ) )
3 dihord5apre.b . . . 4  |-  B  =  ( Base `  K
)
4 dihord5apre.l . . . 4  |-  .<_  =  ( le `  K )
5 dihord5apre.j . . . 4  |-  .\/  =  ( join `  K )
6 dihord5apre.m . . . 4  |-  ./\  =  ( meet `  K )
7 dihord5apre.a . . . 4  |-  A  =  ( Atoms `  K )
8 dihord5apre.h . . . 4  |-  H  =  ( LHyp `  K
)
93, 4, 5, 6, 7, 8lhpmcvr2 33501 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( Y  e.  B  /\  -.  Y  .<_  W ) )  ->  E. r  e.  A  ( -.  r  .<_  W  /\  ( r  .\/  ( Y  ./\  W ) )  =  Y ) )
101, 2, 9syl2anc 665 . 2  |-  ( ( ( ( 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 ) )
11 simp11l 1116 . . . . . . . 8  |-  ( ( ( ( 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 )
12 hllat 32841 . . . . . . . 8  |-  ( K  e.  HL  ->  K  e.  Lat )
1311, 12syl 17 . . . . . . 7  |-  ( ( ( ( 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 )
14 simp12l 1118 . . . . . . 7  |-  ( ( ( ( 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 )
15 simp3ll 1076 . . . . . . . . 9  |-  ( ( ( ( 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 )
163, 7atbase 32767 . . . . . . . . 9  |-  ( r  e.  A  ->  r  e.  B )
1715, 16syl 17 . . . . . . . 8  |-  ( ( ( ( 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 )
183, 5latjcl 16235 . . . . . . . 8  |-  ( ( K  e.  Lat  /\  r  e.  B  /\  X  e.  B )  ->  ( r  .\/  X
)  e.  B )
1913, 17, 14, 18syl3anc 1264 . . . . . . 7  |-  ( ( ( ( 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
)
20 simp13l 1120 . . . . . . 7  |-  ( ( ( ( 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 )
213, 4, 5latlej2 16245 . . . . . . . 8  |-  ( ( K  e.  Lat  /\  r  e.  B  /\  X  e.  B )  ->  X  .<_  ( r  .\/  X ) )
2213, 17, 14, 21syl3anc 1264 . . . . . . 7  |-  ( ( ( ( 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 ) )
23 simp11 1035 . . . . . . . . . 10  |-  ( ( ( ( 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 ) )
24 simp3lr 1077 . . . . . . . . . . 11  |-  ( ( ( ( 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 )
253, 4, 5latlej1 16244 . . . . . . . . . . . . 13  |-  ( ( K  e.  Lat  /\  r  e.  B  /\  X  e.  B )  ->  r  .<_  ( r  .\/  X ) )
2613, 17, 14, 25syl3anc 1264 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) )
27 simp11r 1117 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
283, 8lhpbase 33475 . . . . . . . . . . . . . 14  |-  ( W  e.  H  ->  W  e.  B )
2927, 28syl 17 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )
303, 4lattr 16240 . . . . . . . . . . . . 13  |-  ( ( K  e.  Lat  /\  ( r  e.  B  /\  ( r  .\/  X
)  e.  B  /\  W  e.  B )
)  ->  ( (
r  .<_  ( r  .\/  X )  /\  ( r 
.\/  X )  .<_  W )  ->  r  .<_  W ) )
3113, 17, 19, 29, 30syl13anc 1266 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) )
3226, 31mpand 679 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) )
3324, 32mtod 180 . . . . . . . . . 10  |-  ( ( ( ( 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 )
34 simp3l 1033 . . . . . . . . . 10  |-  ( ( ( ( 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 ) )
35 simp12 1036 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) )
363, 4, 5, 6, 7, 8lhple 33519 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( r  e.  A  /\  -.  r  .<_  W )  /\  ( X  e.  B  /\  X  .<_  W ) )  ->  ( ( r 
.\/  X )  ./\  W )  =  X )
3723, 34, 35, 36syl3anc 1264 . . . . . . . . . . 11  |-  ( ( ( ( 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 )
3837oveq2d 6260 . . . . . . . . . 10  |-  ( ( ( ( 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 ) )
39 dihord5apre.i . . . . . . . . . . 11  |-  I  =  ( ( DIsoH `  K
) `  W )
40 eqid 2423 . . . . . . . . . . 11  |-  ( (
DIsoB `  K ) `  W )  =  ( ( DIsoB `  K ) `  W )
41 eqid 2423 . . . . . . . . . . 11  |-  ( (
DIsoC `  K ) `  W )  =  ( ( DIsoC `  K ) `  W )
42 dihord5apre.u . . . . . . . . . . 11  |-  U  =  ( ( DVecH `  K
) `  W )
43 dihord5apre.s . . . . . . . . . . 11  |-  .(+)  =  (
LSSum `  U )
443, 4, 5, 6, 7, 8, 39, 40, 41, 42, 43dihvalcq 34716 . . . . . . . . . 10  |-  ( ( ( 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 ) ) ) )
4523, 19, 33, 34, 38, 44syl122anc 1273 . . . . . . . . 9  |-  ( ( ( ( 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 ) ) ) )
468, 42, 23dvhlmod 34590 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
47 eqid 2423 . . . . . . . . . . . . . . 15  |-  ( LSubSp `  U )  =  (
LSubSp `  U )
4847lsssssubg 18119 . . . . . . . . . . . . . 14  |-  ( U  e.  LMod  ->  ( LSubSp `  U )  C_  (SubGrp `  U ) )
4946, 48syl 17 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 ) )
504, 7, 8, 42, 41, 47diclss 34673 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( r  e.  A  /\  -.  r  .<_  W ) )  -> 
( ( ( DIsoC `  K ) `  W
) `  r )  e.  ( LSubSp `  U )
)
5123, 34, 50syl2anc 665 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 ) )
5249, 51sseldd 3403 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) )
533, 6latmcl 16236 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  Lat  /\  Y  e.  B  /\  W  e.  B )  ->  ( Y  ./\  W
)  e.  B )
5413, 20, 29, 53syl3anc 1264 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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
)
553, 4, 6latmle2 16261 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  Lat  /\  Y  e.  B  /\  W  e.  B )  ->  ( Y  ./\  W
)  .<_  W )
5613, 20, 29, 55syl3anc 1264 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
573, 4, 8, 42, 40, 47diblss 34650 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( Y 
./\  W )  e.  B  /\  ( Y 
./\  W )  .<_  W ) )  -> 
( ( ( DIsoB `  K ) `  W
) `  ( Y  ./\ 
W ) )  e.  ( LSubSp `  U )
)
5823, 54, 56, 57syl12anc 1262 . . . . . . . . . . . . 13  |-  ( ( ( ( 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
) )
5949, 58sseldd 3403 . . . . . . . . . . . 12  |-  ( ( ( ( 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
) )
6043lsmub1 17246 . . . . . . . . . . . 12  |-  ( ( ( ( ( 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 ) ) ) )
6152, 59, 60syl2anc 665 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) ) ) )
62 simp13 1037 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) )
63 simp3r 1034 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )
643, 4, 5, 6, 7, 8, 39, 40, 41, 42, 43dihvalcq 34716 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) ) )
6523, 62, 34, 63, 64syl112anc 1268 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) ) ) )
6661, 65sseqtr4d 3439 . . . . . . . . . 10  |-  ( ( ( ( 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 ) )
6737fveq2d 5824 . . . . . . . . . . . 12  |-  ( ( ( ( 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
) )
683, 4, 8, 39, 40dihvalb 34717 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W ) )  ->  (
I `  X )  =  ( ( (
DIsoB `  K ) `  W ) `  X
) )
6923, 35, 68syl2anc 665 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) )
7067, 69eqtr4d 2460 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) )
71 simp2 1006 . . . . . . . . . . 11  |-  ( ( ( ( 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 )
)
7270, 71eqsstrd 3436 . . . . . . . . . 10  |-  ( ( ( ( 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 ) )
733, 6latmcl 16236 . . . . . . . . . . . . . 14  |-  ( ( K  e.  Lat  /\  ( r  .\/  X
)  e.  B  /\  W  e.  B )  ->  ( ( r  .\/  X )  ./\  W )  e.  B )
7413, 19, 29, 73syl3anc 1264 . . . . . . . . . . . . 13  |-  ( ( ( ( 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
)
753, 4, 6latmle2 16261 . . . . . . . . . . . . . 14  |-  ( ( K  e.  Lat  /\  ( r  .\/  X
)  e.  B  /\  W  e.  B )  ->  ( ( r  .\/  X )  ./\  W )  .<_  W )
7613, 19, 29, 75syl3anc 1264 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )
773, 4, 8, 42, 40, 47diblss 34650 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( ( r  .\/  X ) 
./\  W )  e.  B  /\  ( ( r  .\/  X ) 
./\  W )  .<_  W ) )  -> 
( ( ( DIsoB `  K ) `  W
) `  ( (
r  .\/  X )  ./\  W ) )  e.  ( LSubSp `  U )
)
7823, 74, 76, 77syl12anc 1262 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) )
7949, 78sseldd 3403 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) )
803, 8, 39, 42, 47dihlss 34730 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  Y  e.  B
)  ->  ( I `  Y )  e.  (
LSubSp `  U ) )
8123, 20, 80syl2anc 665 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) )
8249, 81sseldd 3403 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) )
8343lsmlub 17253 . . . . . . . . . . 11  |-  ( ( ( ( ( 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 )
) )
8452, 79, 82, 83syl3anc 1264 . . . . . . . . . 10  |-  ( ( ( ( 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 )
) )
8566, 72, 84mpbi2and 929 . . . . . . . . 9  |-  ( ( ( ( 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 )
)
8645, 85eqsstrd 3436 . . . . . . . 8  |-  ( ( ( ( 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 )
)
873, 4, 8, 39dihord4 34738 . . . . . . . . 9  |-  ( ( ( 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 )
)
8823, 19, 33, 62, 87syl121anc 1269 . . . . . . . 8  |-  ( ( ( ( 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 )
)
8986, 88mpbid 213 . . . . . . 7  |-  ( ( ( ( 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 )
903, 4, 13, 14, 19, 20, 22, 89lattrd 16242 . . . . . 6  |-  ( ( ( ( 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 )
91903expia 1207 . . . . 5  |-  ( ( ( ( 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 ) )
9291exp4c 611 . . . 4  |-  ( ( ( ( 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 ) ) ) )
9392imp4a 592 . . 3  |-  ( ( ( ( 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 ) ) )
9493rexlimdv 2849 . 2  |-  ( ( ( ( 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 ) )
9510, 94mpd 15 1  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  -.  Y  .<_  W ) )  /\  ( I `
 X )  C_  ( I `  Y
) )  ->  X  .<_  Y )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1872   E.wrex 2710    C_ wss 3374   class class class wbr 4361   ` cfv 5539  (class class class)co 6244   Basecbs 15059   lecple 15135   joincjn 16127   meetcmee 16128   Latclat 16229  SubGrpcsubg 16749   LSSumclsm 17224   LModclmod 18029   LSubSpclss 18093   Atomscatm 32741   HLchlt 32828   LHypclh 33461   DVecHcdvh 34558   DIsoBcdib 34618   DIsoCcdic 34652   DIsoHcdih 34708
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-rep 4474  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-cnex 9541  ax-resscn 9542  ax-1cn 9543  ax-icn 9544  ax-addcl 9545  ax-addrcl 9546  ax-mulcl 9547  ax-mulrcl 9548  ax-mulcom 9549  ax-addass 9550  ax-mulass 9551  ax-distr 9552  ax-i2m1 9553  ax-1ne0 9554  ax-1rid 9555  ax-rnegex 9556  ax-rrecex 9557  ax-cnre 9558  ax-pre-lttri 9559  ax-pre-lttrn 9560  ax-pre-ltadd 9561  ax-pre-mulgt0 9562  ax-riotaBAD 32437
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-pss 3390  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4158  df-int 4194  df-iun 4239  df-iin 4240  df-br 4362  df-opab 4421  df-mpt 4422  df-tr 4457  df-eprel 4702  df-id 4706  df-po 4712  df-so 4713  df-fr 4750  df-we 4752  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-pred 5337  df-ord 5383  df-on 5384  df-lim 5385  df-suc 5386  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-riota 6206  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-om 6646  df-1st 6746  df-2nd 6747  df-tpos 6923  df-undef 6970  df-wrecs 6978  df-recs 7040  df-rdg 7078  df-1o 7132  df-oadd 7136  df-er 7313  df-map 7424  df-en 7520  df-dom 7521  df-sdom 7522  df-fin 7523  df-pnf 9623  df-mnf 9624  df-xr 9625  df-ltxr 9626  df-le 9627  df-sub 9808  df-neg 9809  df-nn 10556  df-2 10614  df-3 10615  df-4 10616  df-5 10617  df-6 10618  df-n0 10816  df-z 10884  df-uz 11106  df-fz 11731  df-struct 15061  df-ndx 15062  df-slot 15063  df-base 15064  df-sets 15065  df-ress 15066  df-plusg 15141  df-mulr 15142  df-sca 15144  df-vsca 15145  df-0g 15278  df-preset 16111  df-poset 16129  df-plt 16142  df-lub 16158  df-glb 16159  df-join 16160  df-meet 16161  df-p0 16223  df-p1 16224  df-lat 16230  df-clat 16292  df-mgm 16426  df-sgrp 16465  df-mnd 16475  df-submnd 16521  df-grp 16611  df-minusg 16612  df-sbg 16613  df-subg 16752  df-cntz 16909  df-lsm 17226  df-cmn 17370  df-abl 17371  df-mgp 17662  df-ur 17674  df-ring 17720  df-oppr 17789  df-dvdsr 17807  df-unit 17808  df-invr 17838  df-dvr 17849  df-drng 17915  df-lmod 18031  df-lss 18094  df-lsp 18133  df-lvec 18264  df-oposet 32654  df-ol 32656  df-oml 32657  df-covers 32744  df-ats 32745  df-atl 32776  df-cvlat 32800  df-hlat 32829  df-llines 32975  df-lplanes 32976  df-lvols 32977  df-lines 32978  df-psubsp 32980  df-pmap 32981  df-padd 33273  df-lhyp 33465  df-laut 33466  df-ldil 33581  df-ltrn 33582  df-trl 33637  df-tendo 34234  df-edring 34236  df-disoa 34509  df-dvech 34559  df-dib 34619  df-dic 34653  df-dih 34709
This theorem is referenced by:  dihord5a  34743
  Copyright terms: Public domain W3C validator