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

Theorem cdlemk7 33848
Description: Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 119. (Contributed by NM, 27-Jun-2013.)
Hypotheses
Ref Expression
cdlemk.b  |-  B  =  ( Base `  K
)
cdlemk.l  |-  .<_  =  ( le `  K )
cdlemk.j  |-  .\/  =  ( join `  K )
cdlemk.a  |-  A  =  ( Atoms `  K )
cdlemk.h  |-  H  =  ( LHyp `  K
)
cdlemk.t  |-  T  =  ( ( LTrn `  K
) `  W )
cdlemk.r  |-  R  =  ( ( trL `  K
) `  W )
cdlemk.m  |-  ./\  =  ( meet `  K )
cdlemk.s  |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T  ( i `  P
)  =  ( ( P  .\/  ( R `
 f ) ) 
./\  ( ( N `
 P )  .\/  ( R `  ( f  o.  `' F ) ) ) ) ) )
cdlemk.v  |-  V  =  ( ( ( G `
 P )  .\/  ( X `  P ) )  ./\  ( ( R `  ( G  o.  `' F ) )  .\/  ( R `  ( X  o.  `' F ) ) ) )
Assertion
Ref Expression
cdlemk7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  (
( S `  G
) `  P )  .<_  ( ( ( S `
 X ) `  P )  .\/  V
) )
Distinct variable groups:    ./\ , f    .\/ , f    f, F, i    f, G, i    f, N    P, f    R, f    T, f   
f, W    ./\ , i    .<_ , i    .\/ , i    A, i    i, F   
i, H    i, K    i, N    P, i    R, i    T, i    i, W    f, X, i
Allowed substitution hints:    A( f)    B( f, i)    S( f, i)    H( f)    K( f)    .<_ ( f)    V( f, i)

Proof of Theorem cdlemk7
StepHypRef Expression
1 simp1 997 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  (
( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
) )
2 simp2 998 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) ) )
3 simp311 1144 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  F  =/=  (  _I  |`  B ) )
4 simp312 1145 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  G  =/=  (  _I  |`  B ) )
5 simp32 1034 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  ( R `  G )  =/=  ( R `  F
) )
6 simp33 1035 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  ( R `  X )  =/=  ( R `  F
) )
75, 6jca 530 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  (
( R `  G
)  =/=  ( R `
 F )  /\  ( R `  X )  =/=  ( R `  F ) ) )
8 cdlemk.b . . . 4  |-  B  =  ( Base `  K
)
9 cdlemk.l . . . 4  |-  .<_  =  ( le `  K )
10 cdlemk.j . . . 4  |-  .\/  =  ( join `  K )
11 cdlemk.a . . . 4  |-  A  =  ( Atoms `  K )
12 cdlemk.h . . . 4  |-  H  =  ( LHyp `  K
)
13 cdlemk.t . . . 4  |-  T  =  ( ( LTrn `  K
) `  W )
14 cdlemk.r . . . 4  |-  R  =  ( ( trL `  K
) `  W )
15 cdlemk.m . . . 4  |-  ./\  =  ( meet `  K )
168, 9, 10, 11, 12, 13, 14, 15cdlemk6 33837 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  ( ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) ) )  -> 
( ( P  .\/  ( G `  P ) )  ./\  ( ( N `  P )  .\/  ( R `  ( G  o.  `' F
) ) ) ) 
.<_  ( ( ( ( G `  P ) 
.\/  ( X `  P ) )  ./\  ( ( R `  ( G  o.  `' F ) )  .\/  ( R `  ( X  o.  `' F ) ) ) )  .\/  ( ( ( X `
 P )  .\/  P )  ./\  ( ( R `  ( X  o.  `' F ) )  .\/  ( N `  P ) ) ) ) )
171, 2, 3, 4, 7, 16syl113anc 1242 . 2  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  (
( P  .\/  ( G `  P )
)  ./\  ( ( N `  P )  .\/  ( R `  ( G  o.  `' F
) ) ) ) 
.<_  ( ( ( ( G `  P ) 
.\/  ( X `  P ) )  ./\  ( ( R `  ( G  o.  `' F ) )  .\/  ( R `  ( X  o.  `' F ) ) ) )  .\/  ( ( ( X `
 P )  .\/  P )  ./\  ( ( R `  ( X  o.  `' F ) )  .\/  ( N `  P ) ) ) ) )
18 simp21l 1114 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  N  e.  T )
19 simp22 1031 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  ( P  e.  A  /\  -.  P  .<_  W ) )
20 simp23 1032 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  ( R `  F )  =  ( R `  N ) )
2118, 19, 203jca 1177 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) ) )
22 cdlemk.s . . . . 5  |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T  ( i `  P
)  =  ( ( P  .\/  ( R `
 f ) ) 
./\  ( ( N `
 P )  .\/  ( R `  ( f  o.  `' F ) ) ) ) ) )
238, 9, 10, 11, 12, 13, 14, 15, 22cdlemksv2 33847 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  ( R `  G )  =/=  ( R `  F ) ) )  ->  ( ( S `
 G ) `  P )  =  ( ( P  .\/  ( R `  G )
)  ./\  ( ( N `  P )  .\/  ( R `  ( G  o.  `' F
) ) ) ) )
241, 21, 3, 4, 5, 23syl113anc 1242 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  (
( S `  G
) `  P )  =  ( ( P 
.\/  ( R `  G ) )  ./\  ( ( N `  P )  .\/  ( R `  ( G  o.  `' F ) ) ) ) )
25 simp11 1027 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  ( K  e.  HL  /\  W  e.  H ) )
26 simp13 1029 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  G  e.  T )
279, 10, 11, 12, 13, 14trljat1 33165 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  G  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( P  .\/  ( R `  G
) )  =  ( P  .\/  ( G `
 P ) ) )
2825, 26, 19, 27syl3anc 1230 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  ( P  .\/  ( R `  G ) )  =  ( P  .\/  ( G `  P )
) )
2928oveq1d 6249 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  (
( P  .\/  ( R `  G )
)  ./\  ( ( N `  P )  .\/  ( R `  ( G  o.  `' F
) ) ) )  =  ( ( P 
.\/  ( G `  P ) )  ./\  ( ( N `  P )  .\/  ( R `  ( G  o.  `' F ) ) ) ) )
3024, 29eqtrd 2443 . 2  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  (
( S `  G
) `  P )  =  ( ( P 
.\/  ( G `  P ) )  ./\  ( ( N `  P )  .\/  ( R `  ( G  o.  `' F ) ) ) ) )
31 simp11l 1108 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  K  e.  HL )
32 hllat 32362 . . . . 5  |-  ( K  e.  HL  ->  K  e.  Lat )
3331, 32syl 17 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  K  e.  Lat )
34 simp12 1028 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  F  e.  T )
35 simp21r 1115 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  X  e.  T )
3625, 34, 353jca 1177 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  (
( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  X  e.  T
) )
37 simp313 1146 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  X  =/=  (  _I  |`  B ) )
388, 9, 10, 11, 12, 13, 14, 15, 22cdlemksat 33846 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  X  e.  T )  /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( F  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B )  /\  ( R `  X )  =/=  ( R `  F ) ) )  ->  ( ( S `
 X ) `  P )  e.  A
)
3936, 21, 3, 37, 6, 38syl113anc 1242 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  (
( S `  X
) `  P )  e.  A )
408, 11atbase 32288 . . . . 5  |-  ( ( ( S `  X
) `  P )  e.  A  ->  ( ( S `  X ) `
 P )  e.  B )
4139, 40syl 17 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  (
( S `  X
) `  P )  e.  B )
42 simp11r 1109 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  W  e.  H )
43 simp22l 1116 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  P  e.  A )
44 cdlemk.v . . . . . 6  |-  V  =  ( ( ( G `
 P )  .\/  ( X `  P ) )  ./\  ( ( R `  ( G  o.  `' F ) )  .\/  ( R `  ( X  o.  `' F ) ) ) )
458, 9, 10, 11, 12, 13, 14, 15, 44cdlemkvcl 33842 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  G  e.  T  /\  X  e.  T )  /\  P  e.  A )  ->  V  e.  B )
4631, 42, 34, 26, 35, 43, 45syl231anc 1250 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  V  e.  B )
478, 10latjcom 15905 . . . 4  |-  ( ( K  e.  Lat  /\  ( ( S `  X ) `  P
)  e.  B  /\  V  e.  B )  ->  ( ( ( S `
 X ) `  P )  .\/  V
)  =  ( V 
.\/  ( ( S `
 X ) `  P ) ) )
4833, 41, 46, 47syl3anc 1230 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  (
( ( S `  X ) `  P
)  .\/  V )  =  ( V  .\/  ( ( S `  X ) `  P
) ) )
4944a1i 11 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  V  =  ( ( ( G `  P ) 
.\/  ( X `  P ) )  ./\  ( ( R `  ( G  o.  `' F ) )  .\/  ( R `  ( X  o.  `' F ) ) ) ) )
508, 9, 10, 11, 12, 13, 14, 15, 22cdlemksv2 33847 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  X  e.  T )  /\  ( N  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( F  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B )  /\  ( R `  X )  =/=  ( R `  F ) ) )  ->  ( ( S `
 X ) `  P )  =  ( ( P  .\/  ( R `  X )
)  ./\  ( ( N `  P )  .\/  ( R `  ( X  o.  `' F
) ) ) ) )
5136, 21, 3, 37, 6, 50syl113anc 1242 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  (
( S `  X
) `  P )  =  ( ( P 
.\/  ( R `  X ) )  ./\  ( ( N `  P )  .\/  ( R `  ( X  o.  `' F ) ) ) ) )
529, 10, 11, 12, 13, 14trljat1 33165 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( P  .\/  ( R `  X
) )  =  ( P  .\/  ( X `
 P ) ) )
5325, 35, 19, 52syl3anc 1230 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  ( P  .\/  ( R `  X ) )  =  ( P  .\/  ( X `  P )
) )
549, 11, 12, 13ltrnat 33138 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  T  /\  P  e.  A
)  ->  ( X `  P )  e.  A
)
5525, 35, 43, 54syl3anc 1230 . . . . . . . 8  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  ( X `  P )  e.  A )
5610, 11hlatjcom 32366 . . . . . . . 8  |-  ( ( K  e.  HL  /\  ( X `  P )  e.  A  /\  P  e.  A )  ->  (
( X `  P
)  .\/  P )  =  ( P  .\/  ( X `  P ) ) )
5731, 55, 43, 56syl3anc 1230 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  (
( X `  P
)  .\/  P )  =  ( P  .\/  ( X `  P ) ) )
5853, 57eqtr4d 2446 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  ( P  .\/  ( R `  X ) )  =  ( ( X `  P )  .\/  P
) )
599, 11, 12, 13ltrnat 33138 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  N  e.  T  /\  P  e.  A
)  ->  ( N `  P )  e.  A
)
6025, 18, 43, 59syl3anc 1230 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  ( N `  P )  e.  A )
6135, 34jca 530 . . . . . . . 8  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  ( X  e.  T  /\  F  e.  T )
)
6211, 12, 13, 14trlcocnvat 33724 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  T  /\  F  e.  T )  /\  ( R `  X )  =/=  ( R `  F
) )  ->  ( R `  ( X  o.  `' F ) )  e.  A )
6325, 61, 6, 62syl3anc 1230 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  ( R `  ( X  o.  `' F ) )  e.  A )
6410, 11hlatjcom 32366 . . . . . . 7  |-  ( ( K  e.  HL  /\  ( N `  P )  e.  A  /\  ( R `  ( X  o.  `' F ) )  e.  A )  ->  (
( N `  P
)  .\/  ( R `  ( X  o.  `' F ) ) )  =  ( ( R `
 ( X  o.  `' F ) )  .\/  ( N `  P ) ) )
6531, 60, 63, 64syl3anc 1230 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  (
( N `  P
)  .\/  ( R `  ( X  o.  `' F ) ) )  =  ( ( R `
 ( X  o.  `' F ) )  .\/  ( N `  P ) ) )
6658, 65oveq12d 6252 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  (
( P  .\/  ( R `  X )
)  ./\  ( ( N `  P )  .\/  ( R `  ( X  o.  `' F
) ) ) )  =  ( ( ( X `  P ) 
.\/  P )  ./\  ( ( R `  ( X  o.  `' F ) )  .\/  ( N `  P ) ) ) )
6751, 66eqtrd 2443 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  (
( S `  X
) `  P )  =  ( ( ( X `  P ) 
.\/  P )  ./\  ( ( R `  ( X  o.  `' F ) )  .\/  ( N `  P ) ) ) )
6849, 67oveq12d 6252 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  ( V  .\/  ( ( S `
 X ) `  P ) )  =  ( ( ( ( G `  P ) 
.\/  ( X `  P ) )  ./\  ( ( R `  ( G  o.  `' F ) )  .\/  ( R `  ( X  o.  `' F ) ) ) )  .\/  ( ( ( X `
 P )  .\/  P )  ./\  ( ( R `  ( X  o.  `' F ) )  .\/  ( N `  P ) ) ) ) )
6948, 68eqtrd 2443 . 2  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  (
( ( S `  X ) `  P
)  .\/  V )  =  ( ( ( ( G `  P
)  .\/  ( X `  P ) )  ./\  ( ( R `  ( G  o.  `' F ) )  .\/  ( R `  ( X  o.  `' F ) ) ) )  .\/  ( ( ( X `
 P )  .\/  P )  ./\  ( ( R `  ( X  o.  `' F ) )  .\/  ( N `  P ) ) ) ) )
7017, 30, 693brtr4d 4424 1  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
( N  e.  T  /\  X  e.  T
)  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( R `  F )  =  ( R `  N ) )  /\  ( ( F  =/=  (  _I  |`  B )  /\  G  =/=  (  _I  |`  B )  /\  X  =/=  (  _I  |`  B ) )  /\  ( R `
 G )  =/=  ( R `  F
)  /\  ( R `  X )  =/=  ( R `  F )
) )  ->  (
( S `  G
) `  P )  .<_  ( ( ( S `
 X ) `  P )  .\/  V
) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 367    /\ w3a 974    = wceq 1405    e. wcel 1842    =/= wne 2598   class class class wbr 4394    |-> cmpt 4452    _I cid 4732   `'ccnv 4941    |` cres 4944    o. ccom 4946   ` cfv 5525   iota_crio 6195  (class class class)co 6234   Basecbs 14733   lecple 14808   joincjn 15789   meetcmee 15790   Latclat 15891   Atomscatm 32262   HLchlt 32349   LHypclh 32982   LTrncltrn 33099   trLctrl 33157
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4506  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6530  ax-riotaBAD 31958
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2758  df-rex 2759  df-reu 2760  df-rmo 2761  df-rab 2762  df-v 3060  df-sbc 3277  df-csb 3373  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-iun 4272  df-iin 4273  df-br 4395  df-opab 4453  df-mpt 4454  df-id 4737  df-xp 4948  df-rel 4949  df-cnv 4950  df-co 4951  df-dm 4952  df-rn 4953  df-res 4954  df-ima 4955  df-iota 5489  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-riota 6196  df-ov 6237  df-oprab 6238  df-mpt2 6239  df-1st 6738  df-2nd 6739  df-undef 6959  df-map 7379  df-preset 15773  df-poset 15791  df-plt 15804  df-lub 15820  df-glb 15821  df-join 15822  df-meet 15823  df-p0 15885  df-p1 15886  df-lat 15892  df-clat 15954  df-oposet 32175  df-ol 32177  df-oml 32178  df-covers 32265  df-ats 32266  df-atl 32297  df-cvlat 32321  df-hlat 32350  df-llines 32496  df-lplanes 32497  df-lvols 32498  df-lines 32499  df-psubsp 32501  df-pmap 32502  df-padd 32794  df-lhyp 32986  df-laut 32987  df-ldil 33102  df-ltrn 33103  df-trl 33158
This theorem is referenced by:  cdlemk11  33849
  Copyright terms: Public domain W3C validator