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

Theorem cdlemk12u 30212
Description: Part of proof of Lemma K of [Crawley] p. 118. Line 18, p. 119, showing Eq. 4 (line 10, p. 119) for the sigma1 ( U) case. (Contributed by NM, 4-Jul-2013.)
Hypotheses
Ref Expression
cdlemk1.b  |-  B  =  ( Base `  K
)
cdlemk1.l  |-  .<_  =  ( le `  K )
cdlemk1.j  |-  .\/  =  ( join `  K )
cdlemk1.m  |-  ./\  =  ( meet `  K )
cdlemk1.a  |-  A  =  ( Atoms `  K )
cdlemk1.h  |-  H  =  ( LHyp `  K
)
cdlemk1.t  |-  T  =  ( ( LTrn `  K
) `  W )
cdlemk1.r  |-  R  =  ( ( trL `  K
) `  W )
cdlemk1.s  |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T
( i `  P
)  =  ( ( P  .\/  ( R `
 f ) ) 
./\  ( ( N `
 P )  .\/  ( R `  ( f  o.  `' F ) ) ) ) ) )
cdlemk1.o  |-  O  =  ( S `  D
)
cdlemk1.u  |-  U  =  ( e  e.  T  |->  ( iota_ j  e.  T
( j `  P
)  =  ( ( P  .\/  ( R `
 e ) ) 
./\  ( ( O `
 P )  .\/  ( R `  ( e  o.  `' D ) ) ) ) ) )
Assertion
Ref Expression
cdlemk12u  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  (
( U `  G
) `  P )  =  ( ( P 
.\/  ( G `  P ) )  ./\  ( ( ( U `
 X ) `  P )  .\/  ( R `  ( X  o.  `' G ) ) ) ) )
Distinct variable groups:    f, i,  ./\    .<_ , i    .\/ , f, i    A, i    D, f, i    f, F, i    i, H    i, K    f, N, i    P, f, i    R, f, i    T, f, i    f, W, i    ./\ , e    .\/ , e    D, e, j    e, G, j   
e, O    P, e    R, e    T, e    e, W    ./\ , j    .<_ , j    .\/ , j    A, j    D, j    j, F   
j, H    j, K    j, N    j, O    P, j    R, j    T, j   
j, W    e, F    e, X, j
Allowed substitution hints:    A( e, f)    B( e, f, i, j)    S( e, f, i, j)    U( e, f, i, j)    G( f, i)    H( e, f)    K( e, f)    .<_ ( e, f)    N( e)    O( f, i)    X( f, i)

Proof of Theorem cdlemk12u
StepHypRef Expression
1 simp11l 1071 . 2  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  K  e.  HL )
2 simp22l 1079 . 2  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  P  e.  A )
3 simp11 990 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( K  e.  HL  /\  W  e.  H ) )
4 simp212 1099 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  G  e.  T )
5 cdlemk1.l . . . 4  |-  .<_  =  ( le `  K )
6 cdlemk1.a . . . 4  |-  A  =  ( Atoms `  K )
7 cdlemk1.h . . . 4  |-  H  =  ( LHyp `  K
)
8 cdlemk1.t . . . 4  |-  T  =  ( ( LTrn `  K
) `  W )
95, 6, 7, 8ltrnat 29480 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  G  e.  T  /\  P  e.  A
)  ->  ( G `  P )  e.  A
)
103, 4, 2, 9syl3anc 1187 . 2  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( G `  P )  e.  A )
11 simp23 995 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( R `  F )  =  ( R `  N ) )
12 simp213 1100 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  X  e.  T )
13 simp12 991 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  F  e.  T )
14 simp13 992 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  D  e.  T )
15 simp211 1098 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  N  e.  T )
16 simp331 1113 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( R `  D )  =/=  ( R `  F
) )
17 simp333 1115 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( R `  X )  =/=  ( R `  D
) )
1817necomd 2502 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( R `  D )  =/=  ( R `  X
) )
1916, 18jca 520 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  (
( R `  D
)  =/=  ( R `
 F )  /\  ( R `  D )  =/=  ( R `  X ) ) )
20 simp311 1107 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  F  =/=  (  _I  |`  B ) )
21 simp32l 1085 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  X  =/=  (  _I  |`  B ) )
22 simp312 1108 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  D  =/=  (  _I  |`  B ) )
2320, 21, 223jca 1137 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( F  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B ) ) )
24 simp22 994 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( P  e.  A  /\  -.  P  .<_  W ) )
25 cdlemk1.b . . . 4  |-  B  =  ( Base `  K
)
26 cdlemk1.j . . . 4  |-  .\/  =  ( join `  K )
27 cdlemk1.m . . . 4  |-  ./\  =  ( meet `  K )
28 cdlemk1.r . . . 4  |-  R  =  ( ( trL `  K
) `  W )
29 cdlemk1.s . . . 4  |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T
( i `  P
)  =  ( ( P  .\/  ( R `
 f ) ) 
./\  ( ( N `
 P )  .\/  ( R `  ( f  o.  `' F ) ) ) ) ) )
30 cdlemk1.o . . . 4  |-  O  =  ( S `  D
)
31 cdlemk1.u . . . 4  |-  U  =  ( e  e.  T  |->  ( iota_ j  e.  T
( j `  P
)  =  ( ( P  .\/  ( R `
 e ) ) 
./\  ( ( O `
 P )  .\/  ( R `  ( e  o.  `' D ) ) ) ) ) )
3225, 5, 26, 27, 6, 7, 8, 28, 29, 30, 31cdlemkuat 30206 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N )  /\  X  e.  T )  /\  ( F  e.  T  /\  D  e.  T  /\  N  e.  T )  /\  ( ( ( R `
 D )  =/=  ( R `  F
)  /\  ( R `  D )  =/=  ( R `  X )
)  /\  ( F  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B ) )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) )  ->  ( ( U `  X ) `  P )  e.  A
)
333, 11, 12, 13, 14, 15, 19, 23, 24, 32syl333anc 1219 . 2  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  (
( U `  X
) `  P )  e.  A )
34 simp32r 1086 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( R `  G )  =/=  ( R `  X
) )
3534necomd 2502 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( R `  X )  =/=  ( R `  G
) )
366, 7, 8, 28trlcocnvat 30064 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  T  /\  G  e.  T )  /\  ( R `  X )  =/=  ( R `  G
) )  ->  ( R `  ( X  o.  `' G ) )  e.  A )
373, 12, 4, 35, 36syl121anc 1192 . 2  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( R `  ( X  o.  `' G ) )  e.  A )
38 simp332 1114 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( R `  G )  =/=  ( R `  D
) )
3938necomd 2502 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( R `  D )  =/=  ( R `  G
) )
4016, 39jca 520 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  (
( R `  D
)  =/=  ( R `
 F )  /\  ( R `  D )  =/=  ( R `  G ) ) )
41 simp313 1109 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  G  =/=  (  _I  |`  B ) )
4220, 41, 223jca 1137 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B ) ) )
4325, 5, 26, 27, 6, 7, 8, 28, 29, 30, 31cdlemkuat 30206 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N )  /\  G  e.  T )  /\  ( F  e.  T  /\  D  e.  T  /\  N  e.  T )  /\  ( ( ( R `
 D )  =/=  ( R `  F
)  /\  ( R `  D )  =/=  ( R `  G )
)  /\  ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B ) )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) )  ->  ( ( U `  G ) `  P )  e.  A
)
443, 11, 4, 13, 14, 15, 40, 42, 24, 43syl333anc 1219 . 2  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  (
( U `  G
) `  P )  e.  A )
4525, 5, 26, 27, 6, 7, 8, 28, 29, 30, 31cdlemkuv2 30207 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N )  /\  G  e.  T )  /\  ( F  e.  T  /\  D  e.  T  /\  N  e.  T )  /\  ( ( ( R `
 D )  =/=  ( R `  F
)  /\  ( R `  D )  =/=  ( R `  G )
)  /\  ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B ) )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) )  ->  ( ( U `  G ) `  P )  =  ( ( P  .\/  ( R `  G )
)  ./\  ( ( O `  P )  .\/  ( R `  ( G  o.  `' D
) ) ) ) )
463, 11, 4, 13, 14, 15, 40, 42, 24, 45syl333anc 1219 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  (
( U `  G
) `  P )  =  ( ( P 
.\/  ( R `  G ) )  ./\  ( ( O `  P )  .\/  ( R `  ( G  o.  `' D ) ) ) ) )
47 hllat 28704 . . . . . 6  |-  ( K  e.  HL  ->  K  e.  Lat )
481, 47syl 17 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  K  e.  Lat )
4925, 6, 7, 8, 28trlnidat 29513 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  G  e.  T  /\  G  =/=  (  _I  |`  B ) )  ->  ( R `  G )  e.  A
)
503, 4, 41, 49syl3anc 1187 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( R `  G )  e.  A )
5125, 26, 6hlatjcl 28707 . . . . . 6  |-  ( ( K  e.  HL  /\  P  e.  A  /\  ( R `  G )  e.  A )  -> 
( P  .\/  ( R `  G )
)  e.  B )
521, 2, 50, 51syl3anc 1187 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( P  .\/  ( R `  G ) )  e.  B )
53 simp1 960 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  (
( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T
) )
5415, 24, 113jca 1137 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) ) )
5525, 5, 26, 27, 6, 7, 8, 28, 29, 30cdlemkoatnle 30191 . . . . . . . 8  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  ( R `  D )  =/=  ( R `  F ) ) )  ->  ( ( O `
 P )  e.  A  /\  -.  ( O `  P )  .<_  W ) )
5655simpld 447 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  ( R `  D )  =/=  ( R `  F ) ) )  ->  ( O `  P )  e.  A
)
5753, 54, 20, 22, 16, 56syl113anc 1199 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( O `  P )  e.  A )
586, 7, 8, 28trlcocnvat 30064 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( G  e.  T  /\  D  e.  T )  /\  ( R `  G )  =/=  ( R `  D
) )  ->  ( R `  ( G  o.  `' D ) )  e.  A )
593, 4, 14, 38, 58syl121anc 1192 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( R `  ( G  o.  `' D ) )  e.  A )
6025, 26, 6hlatjcl 28707 . . . . . 6  |-  ( ( K  e.  HL  /\  ( O `  P )  e.  A  /\  ( R `  ( G  o.  `' D ) )  e.  A )  ->  (
( O `  P
)  .\/  ( R `  ( G  o.  `' D ) ) )  e.  B )
611, 57, 59, 60syl3anc 1187 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  (
( O `  P
)  .\/  ( R `  ( G  o.  `' D ) ) )  e.  B )
6225, 5, 27latmle1 14130 . . . . 5  |-  ( ( K  e.  Lat  /\  ( P  .\/  ( R `
 G ) )  e.  B  /\  (
( O `  P
)  .\/  ( R `  ( G  o.  `' D ) ) )  e.  B )  -> 
( ( P  .\/  ( R `  G ) )  ./\  ( ( O `  P )  .\/  ( R `  ( G  o.  `' D
) ) ) ) 
.<_  ( P  .\/  ( R `  G )
) )
6348, 52, 61, 62syl3anc 1187 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  (
( P  .\/  ( R `  G )
)  ./\  ( ( O `  P )  .\/  ( R `  ( G  o.  `' D
) ) ) ) 
.<_  ( P  .\/  ( R `  G )
) )
6446, 63eqbrtrd 4003 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  (
( U `  G
) `  P )  .<_  ( P  .\/  ( R `  G )
) )
655, 26, 6, 7, 8, 28trljat1 29506 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  G  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( P  .\/  ( R `  G
) )  =  ( P  .\/  ( G `
 P ) ) )
663, 4, 24, 65syl3anc 1187 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( P  .\/  ( R `  G ) )  =  ( P  .\/  ( G `  P )
) )
6764, 66breqtrd 4007 . 2  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  (
( U `  G
) `  P )  .<_  ( P  .\/  ( G `  P )
) )
68 simp2 961 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) ) )
69 simp31 996 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) ) )
70 simp33 998 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  (
( R `  D
)  =/=  ( R `
 F )  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X )  =/=  ( R `  D
) ) )
71 eqid 2256 . . . 4  |-  ( ( ( G `  P
)  .\/  ( X `  P ) )  ./\  ( ( R `  ( G  o.  `' D ) )  .\/  ( R `  ( X  o.  `' D ) ) ) )  =  ( ( ( G `
 P )  .\/  ( X `  P ) )  ./\  ( ( R `  ( G  o.  `' D ) )  .\/  ( R `  ( X  o.  `' D ) ) ) )
7225, 5, 26, 27, 6, 7, 8, 28, 29, 30, 31, 71cdlemk11u 30211 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  X  =/=  (  _I  |`  B )  /\  ( ( R `
 D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  (
( U `  G
) `  P )  .<_  ( ( ( U `
 X ) `  P )  .\/  ( R `  ( X  o.  `' G ) ) ) )
7353, 68, 69, 21, 70, 72syl113anc 1199 . 2  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  (
( U `  G
) `  P )  .<_  ( ( ( U `
 X ) `  P )  .\/  ( R `  ( X  o.  `' G ) ) ) )
745, 26, 6hlatlej2 28716 . . . . 5  |-  ( ( K  e.  HL  /\  P  e.  A  /\  ( R `  G )  e.  A )  -> 
( R `  G
)  .<_  ( P  .\/  ( R `  G ) ) )
751, 2, 50, 74syl3anc 1187 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( R `  G )  .<_  ( P  .\/  ( R `  G )
) )
7675, 66breqtrd 4007 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( R `  G )  .<_  ( P  .\/  ( G `  P )
) )
7725, 5, 26, 27, 6, 7, 8, 28, 29, 30, 31cdlemkuel 30205 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( R `  F )  =  ( R `  N )  /\  X  e.  T )  /\  ( F  e.  T  /\  D  e.  T  /\  N  e.  T )  /\  ( ( ( R `
 D )  =/=  ( R `  F
)  /\  ( R `  D )  =/=  ( R `  X )
)  /\  ( F  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B ) )  /\  ( P  e.  A  /\  -.  P  .<_  W ) ) )  ->  ( U `  X )  e.  T
)
783, 11, 12, 13, 14, 15, 19, 23, 24, 77syl333anc 1219 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( U `  X )  e.  T )
795, 6, 7, 8ltrnel 29479 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( U `  X )  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( (
( U `  X
) `  P )  e.  A  /\  -.  (
( U `  X
) `  P )  .<_  W ) )
803, 78, 24, 79syl3anc 1187 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  (
( ( U `  X ) `  P
)  e.  A  /\  -.  ( ( U `  X ) `  P
)  .<_  W ) )
817, 8ltrncnv 29486 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  G  e.  T
)  ->  `' G  e.  T )
823, 4, 81syl2anc 645 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  `' G  e.  T )
837, 8, 28trlcnv 29505 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  G  e.  T
)  ->  ( R `  `' G )  =  ( R `  G ) )
843, 4, 83syl2anc 645 . . . . . . . 8  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( R `  `' G
)  =  ( R `
 G ) )
8584, 34eqnetrd 2437 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( R `  `' G
)  =/=  ( R `
 X ) )
8625, 7, 8, 28trlcone 30068 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( `' G  e.  T  /\  X  e.  T )  /\  (
( R `  `' G )  =/=  ( R `  X )  /\  X  =/=  (  _I  |`  B ) ) )  ->  ( R `  `' G )  =/=  ( R `  ( `' G  o.  X )
) )
873, 82, 12, 85, 21, 86syl122anc 1196 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( R `  `' G
)  =/=  ( R `
 ( `' G  o.  X ) ) )
8887necomd 2502 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( R `  ( `' G  o.  X )
)  =/=  ( R `
 `' G ) )
897, 8ltrncom 30078 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  `' G  e.  T  /\  X  e.  T )  ->  ( `' G  o.  X
)  =  ( X  o.  `' G ) )
903, 82, 12, 89syl3anc 1187 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( `' G  o.  X
)  =  ( X  o.  `' G ) )
9190fveq2d 5448 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( R `  ( `' G  o.  X )
)  =  ( R `
 ( X  o.  `' G ) ) )
9288, 91, 843netr3d 2445 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( R `  ( X  o.  `' G ) )  =/=  ( R `  G
) )
937, 8ltrnco 30059 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  T  /\  `' G  e.  T
)  ->  ( X  o.  `' G )  e.  T
)
943, 12, 82, 93syl3anc 1187 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( X  o.  `' G
)  e.  T )
955, 7, 8, 28trlle 29524 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  o.  `' G )  e.  T
)  ->  ( R `  ( X  o.  `' G ) )  .<_  W )
963, 94, 95syl2anc 645 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( R `  ( X  o.  `' G ) )  .<_  W )
975, 7, 8, 28trlle 29524 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  G  e.  T
)  ->  ( R `  G )  .<_  W )
983, 4, 97syl2anc 645 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( R `  G )  .<_  W )
995, 26, 6, 7lhp2atnle 29373 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
( ( U `  X ) `  P
)  e.  A  /\  -.  ( ( U `  X ) `  P
)  .<_  W )  /\  ( R `  ( X  o.  `' G ) )  =/=  ( R `
 G ) )  /\  ( ( R `
 ( X  o.  `' G ) )  e.  A  /\  ( R `
 ( X  o.  `' G ) )  .<_  W )  /\  (
( R `  G
)  e.  A  /\  ( R `  G ) 
.<_  W ) )  ->  -.  ( R `  G
)  .<_  ( ( ( U `  X ) `
 P )  .\/  ( R `  ( X  o.  `' G ) ) ) )
1003, 80, 92, 37, 96, 50, 98, 99syl322anc 1215 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  -.  ( R `  G ) 
.<_  ( ( ( U `
 X ) `  P )  .\/  ( R `  ( X  o.  `' G ) ) ) )
101 nbrne1 4000 . . 3  |-  ( ( ( R `  G
)  .<_  ( P  .\/  ( G `  P ) )  /\  -.  ( R `  G )  .<_  ( ( ( U `
 X ) `  P )  .\/  ( R `  ( X  o.  `' G ) ) ) )  ->  ( P  .\/  ( G `  P
) )  =/=  (
( ( U `  X ) `  P
)  .\/  ( R `  ( X  o.  `' G ) ) ) )
10276, 100, 101syl2anc 645 . 2  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  ( P  .\/  ( G `  P ) )  =/=  ( ( ( U `
 X ) `  P )  .\/  ( R `  ( X  o.  `' G ) ) ) )
1035, 26, 27, 62atm 28867 . 2  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  ( G `  P )  e.  A )  /\  ( ( ( U `
 X ) `  P )  e.  A  /\  ( R `  ( X  o.  `' G
) )  e.  A  /\  ( ( U `  G ) `  P
)  e.  A )  /\  ( ( ( U `  G ) `
 P )  .<_  ( P  .\/  ( G `
 P ) )  /\  ( ( U `
 G ) `  P )  .<_  ( ( ( U `  X
) `  P )  .\/  ( R `  ( X  o.  `' G
) ) )  /\  ( P  .\/  ( G `
 P ) )  =/=  ( ( ( U `  X ) `
 P )  .\/  ( R `  ( X  o.  `' G ) ) ) ) )  ->  ( ( U `
 G ) `  P )  =  ( ( P  .\/  ( G `  P )
)  ./\  ( (
( U `  X
) `  P )  .\/  ( R `  ( X  o.  `' G
) ) ) ) )
1041, 2, 10, 33, 37, 44, 67, 73, 102, 103syl333anc 1219 1  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  D  e.  T )  /\  (
( N  e.  T  /\  G  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  D  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B ) )  /\  ( X  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  X )
)  /\  ( ( R `  D )  =/=  ( R `  F
)  /\  ( R `  G )  =/=  ( R `  D )  /\  ( R `  X
)  =/=  ( R `
 D ) ) ) )  ->  (
( U `  G
) `  P )  =  ( ( P 
.\/  ( G `  P ) )  ./\  ( ( ( U `
 X ) `  P )  .\/  ( R `  ( X  o.  `' G ) ) ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    /\ wa 360    /\ w3a 939    = wceq 1619    e. wcel 1621    =/= wne 2419   class class class wbr 3983    e. cmpt 4037    _I cid 4262   `'ccnv 4646    |` cres 4649    o. ccom 4651   ` cfv 4659  (class class class)co 5778   iota_crio 6249   Basecbs 13096   lecple 13163   joincjn 14026   meetcmee 14027   Latclat 14099   Atomscatm 28604   HLchlt 28691   LHypclh 29324   LTrncltrn 29441   trLctrl 29498
This theorem is referenced by:  cdlemk12u-2N  30230  cdlemk22  30233
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-rep 4091  ax-sep 4101  ax-nul 4109  ax-pow 4146  ax-pr 4172  ax-un 4470
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-nel 2422  df-ral 2521  df-rex 2522  df-reu 2523  df-rmo 2524  df-rab 2525  df-v 2759  df-sbc 2953  df-csb 3043  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-nul 3417  df-if 3526  df-pw 3587  df-sn 3606  df-pr 3607  df-op 3609  df-uni 3788  df-iun 3867  df-iin 3868  df-br 3984  df-opab 4038  df-mpt 4039  df-id 4267  df-xp 4661  df-rel 4662  df-cnv 4663  df-co 4664  df-dm 4665  df-rn 4666  df-res 4667  df-ima 4668  df-fun 4669  df-fn 4670  df-f 4671  df-f1 4672  df-fo 4673  df-f1o 4674  df-fv 4675  df-ov 5781  df-oprab 5782  df-mpt2 5783  df-1st 6042  df-2nd 6043  df-iota 6211  df-undef 6250  df-riota 6258  df-map 6728  df-poset 14028  df-plt 14040  df-lub 14056  df-glb 14057  df-join 14058  df-meet 14059  df-p0 14093  df-p1 14094  df-lat 14100  df-clat 14162  df-oposet 28517  df-ol 28519  df-oml 28520  df-covers 28607  df-ats 28608  df-atl 28639  df-cvlat 28663  df-hlat 28692  df-llines 28838  df-lplanes 28839  df-lvols 28840  df-lines 28841  df-psubsp 28843  df-pmap 28844  df-padd 29136  df-lhyp 29328  df-laut 29329  df-ldil 29444  df-ltrn 29445  df-trl 29499
  Copyright terms: Public domain W3C validator