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

Theorem cdlemm10N 34782
Description: The image of the map  G is the entire one-dimensional subspace  ( I `  V ). Remark after Lemma M of [Crawley] p. 121 line 23. (Contributed by NM, 24-Nov-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
cdlemm10.l  |-  .<_  =  ( le `  K )
cdlemm10.j  |-  .\/  =  ( join `  K )
cdlemm10.a  |-  A  =  ( Atoms `  K )
cdlemm10.h  |-  H  =  ( LHyp `  K
)
cdlemm10.t  |-  T  =  ( ( LTrn `  K
) `  W )
cdlemm10.r  |-  R  =  ( ( trL `  K
) `  W )
cdlemm10.i  |-  I  =  ( ( DIsoA `  K
) `  W )
cdlemm10.c  |-  C  =  { r  e.  A  |  ( r  .<_  ( P  .\/  V )  /\  -.  r  .<_  W ) }
cdlemm10.f  |-  F  =  ( iota_ f  e.  T  ( f `  P
)  =  s )
cdlemm10.g  |-  G  =  ( q  e.  C  |->  ( iota_ f  e.  T  ( f `  P
)  =  q ) )
Assertion
Ref Expression
cdlemm10N  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  ->  ran  G  =  ( I `  V
) )
Distinct variable groups:    f, r,
s,  .<_    .\/ , r    A, f,
r, s    s, q, C    G, s    f, H, s    f, K, s   
f, q, P, r, s    R, f, s    T, f, q, s    f, V, r, s    f, W, r, s
Allowed substitution hints:    A( q)    C( f, r)    R( r, q)    T( r)    F( f, s, r, q)    G( f, r, q)    H( r, q)    I( f, s, r, q)    .\/ ( f, s, q)    K( r, q)    .<_ ( q)    V( q)    W( q)

Proof of Theorem cdlemm10N
Dummy variable  g is distinct from all other variables.
StepHypRef Expression
1 riotaex 6071 . . . . 5  |-  ( iota_ f  e.  T  ( f `
 P )  =  q )  e.  _V
2 cdlemm10.g . . . . 5  |-  G  =  ( q  e.  C  |->  ( iota_ f  e.  T  ( f `  P
)  =  q ) )
31, 2fnmpti 5554 . . . 4  |-  G  Fn  C
4 fvelrnb 5754 . . . 4  |-  ( G  Fn  C  ->  (
g  e.  ran  G  <->  E. s  e.  C  ( G `  s )  =  g ) )
53, 4ax-mp 5 . . 3  |-  ( g  e.  ran  G  <->  E. s  e.  C  ( G `  s )  =  g )
6 eqeq2 2452 . . . . . . . . . . . 12  |-  ( q  =  s  ->  (
( f `  P
)  =  q  <->  ( f `  P )  =  s ) )
76riotabidv 6069 . . . . . . . . . . 11  |-  ( q  =  s  ->  ( iota_ f  e.  T  ( f `  P )  =  q )  =  ( iota_ f  e.  T  ( f `  P
)  =  s ) )
8 riotaex 6071 . . . . . . . . . . 11  |-  ( iota_ f  e.  T  ( f `
 P )  =  s )  e.  _V
97, 2, 8fvmpt 5789 . . . . . . . . . 10  |-  ( s  e.  C  ->  ( G `  s )  =  ( iota_ f  e.  T  ( f `  P )  =  s ) )
10 cdlemm10.f . . . . . . . . . 10  |-  F  =  ( iota_ f  e.  T  ( f `  P
)  =  s )
119, 10syl6eqr 2493 . . . . . . . . 9  |-  ( s  e.  C  ->  ( G `  s )  =  F )
1211adantl 466 . . . . . . . 8  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  s  e.  C )  ->  ( G `  s )  =  F )
1312eqeq1d 2451 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  s  e.  C )  ->  (
( G `  s
)  =  g  <->  F  =  g ) )
1413rexbidva 2747 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  ->  ( E. s  e.  C  ( G `  s )  =  g  <->  E. s  e.  C  F  =  g )
)
15 simpl1 991 . . . . . . . . . . 11  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
g  e.  T  /\  ( R `  g ) 
.<_  V ) )  -> 
( K  e.  HL  /\  W  e.  H ) )
16 simprl 755 . . . . . . . . . . 11  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
g  e.  T  /\  ( R `  g ) 
.<_  V ) )  -> 
g  e.  T )
17 simpl2l 1041 . . . . . . . . . . 11  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
g  e.  T  /\  ( R `  g ) 
.<_  V ) )  ->  P  e.  A )
18 cdlemm10.l . . . . . . . . . . . 12  |-  .<_  =  ( le `  K )
19 cdlemm10.a . . . . . . . . . . . 12  |-  A  =  ( Atoms `  K )
20 cdlemm10.h . . . . . . . . . . . 12  |-  H  =  ( LHyp `  K
)
21 cdlemm10.t . . . . . . . . . . . 12  |-  T  =  ( ( LTrn `  K
) `  W )
2218, 19, 20, 21ltrnat 33803 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  g  e.  T  /\  P  e.  A
)  ->  ( g `  P )  e.  A
)
2315, 16, 17, 22syl3anc 1218 . . . . . . . . . 10  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
g  e.  T  /\  ( R `  g ) 
.<_  V ) )  -> 
( g `  P
)  e.  A )
24 eqid 2443 . . . . . . . . . . . 12  |-  ( Base `  K )  =  (
Base `  K )
25 simpl1l 1039 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
g  e.  T  /\  ( R `  g ) 
.<_  V ) )  ->  K  e.  HL )
26 hllat 33027 . . . . . . . . . . . . 13  |-  ( K  e.  HL  ->  K  e.  Lat )
2725, 26syl 16 . . . . . . . . . . . 12  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
g  e.  T  /\  ( R `  g ) 
.<_  V ) )  ->  K  e.  Lat )
2824, 19atbase 32953 . . . . . . . . . . . . . 14  |-  ( P  e.  A  ->  P  e.  ( Base `  K
) )
2917, 28syl 16 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
g  e.  T  /\  ( R `  g ) 
.<_  V ) )  ->  P  e.  ( Base `  K ) )
3024, 20, 21ltrncl 33788 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  g  e.  T  /\  P  e.  ( Base `  K ) )  ->  ( g `  P )  e.  (
Base `  K )
)
3115, 16, 29, 30syl3anc 1218 . . . . . . . . . . . 12  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
g  e.  T  /\  ( R `  g ) 
.<_  V ) )  -> 
( g `  P
)  e.  ( Base `  K ) )
32 cdlemm10.j . . . . . . . . . . . . . 14  |-  .\/  =  ( join `  K )
3324, 32latjcl 15236 . . . . . . . . . . . . 13  |-  ( ( K  e.  Lat  /\  P  e.  ( Base `  K )  /\  (
g `  P )  e.  ( Base `  K
) )  ->  ( P  .\/  ( g `  P ) )  e.  ( Base `  K
) )
3427, 29, 31, 33syl3anc 1218 . . . . . . . . . . . 12  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
g  e.  T  /\  ( R `  g ) 
.<_  V ) )  -> 
( P  .\/  (
g `  P )
)  e.  ( Base `  K ) )
35 simpl3l 1043 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
g  e.  T  /\  ( R `  g ) 
.<_  V ) )  ->  V  e.  A )
3624, 32, 19hlatjcl 33030 . . . . . . . . . . . . 13  |-  ( ( K  e.  HL  /\  P  e.  A  /\  V  e.  A )  ->  ( P  .\/  V
)  e.  ( Base `  K ) )
3725, 17, 35, 36syl3anc 1218 . . . . . . . . . . . 12  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
g  e.  T  /\  ( R `  g ) 
.<_  V ) )  -> 
( P  .\/  V
)  e.  ( Base `  K ) )
3824, 18, 32latlej2 15246 . . . . . . . . . . . . 13  |-  ( ( K  e.  Lat  /\  P  e.  ( Base `  K )  /\  (
g `  P )  e.  ( Base `  K
) )  ->  (
g `  P )  .<_  ( P  .\/  (
g `  P )
) )
3927, 29, 31, 38syl3anc 1218 . . . . . . . . . . . 12  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
g  e.  T  /\  ( R `  g ) 
.<_  V ) )  -> 
( g `  P
)  .<_  ( P  .\/  ( g `  P
) ) )
40 simpl2 992 . . . . . . . . . . . . . 14  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
g  e.  T  /\  ( R `  g ) 
.<_  V ) )  -> 
( P  e.  A  /\  -.  P  .<_  W ) )
41 cdlemm10.r . . . . . . . . . . . . . . 15  |-  R  =  ( ( trL `  K
) `  W )
4218, 32, 19, 20, 21, 41trljat1 33829 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  g  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( P  .\/  ( R `  g
) )  =  ( P  .\/  ( g `
 P ) ) )
4315, 16, 40, 42syl3anc 1218 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
g  e.  T  /\  ( R `  g ) 
.<_  V ) )  -> 
( P  .\/  ( R `  g )
)  =  ( P 
.\/  ( g `  P ) ) )
44 simprr 756 . . . . . . . . . . . . . 14  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
g  e.  T  /\  ( R `  g ) 
.<_  V ) )  -> 
( R `  g
)  .<_  V )
4524, 20, 21, 41trlcl 33827 . . . . . . . . . . . . . . . 16  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  g  e.  T
)  ->  ( R `  g )  e.  (
Base `  K )
)
4615, 16, 45syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
g  e.  T  /\  ( R `  g ) 
.<_  V ) )  -> 
( R `  g
)  e.  ( Base `  K ) )
4724, 19atbase 32953 . . . . . . . . . . . . . . . 16  |-  ( V  e.  A  ->  V  e.  ( Base `  K
) )
4835, 47syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
g  e.  T  /\  ( R `  g ) 
.<_  V ) )  ->  V  e.  ( Base `  K ) )
4924, 18, 32latjlej2 15251 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  Lat  /\  ( ( R `  g )  e.  (
Base `  K )  /\  V  e.  ( Base `  K )  /\  P  e.  ( Base `  K ) ) )  ->  ( ( R `
 g )  .<_  V  ->  ( P  .\/  ( R `  g ) )  .<_  ( P  .\/  V ) ) )
5027, 46, 48, 29, 49syl13anc 1220 . . . . . . . . . . . . . 14  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
g  e.  T  /\  ( R `  g ) 
.<_  V ) )  -> 
( ( R `  g )  .<_  V  -> 
( P  .\/  ( R `  g )
)  .<_  ( P  .\/  V ) ) )
5144, 50mpd 15 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
g  e.  T  /\  ( R `  g ) 
.<_  V ) )  -> 
( P  .\/  ( R `  g )
)  .<_  ( P  .\/  V ) )
5243, 51eqbrtrrd 4329 . . . . . . . . . . . 12  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
g  e.  T  /\  ( R `  g ) 
.<_  V ) )  -> 
( P  .\/  (
g `  P )
)  .<_  ( P  .\/  V ) )
5324, 18, 27, 31, 34, 37, 39, 52lattrd 15243 . . . . . . . . . . 11  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
g  e.  T  /\  ( R `  g ) 
.<_  V ) )  -> 
( g `  P
)  .<_  ( P  .\/  V ) )
5418, 19, 20, 21ltrnel 33802 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  g  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( (
g `  P )  e.  A  /\  -.  (
g `  P )  .<_  W ) )
5554simprd 463 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  g  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  -.  (
g `  P )  .<_  W )
5615, 16, 40, 55syl3anc 1218 . . . . . . . . . . 11  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
g  e.  T  /\  ( R `  g ) 
.<_  V ) )  ->  -.  ( g `  P
)  .<_  W )
5753, 56jca 532 . . . . . . . . . 10  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
g  e.  T  /\  ( R `  g ) 
.<_  V ) )  -> 
( ( g `  P )  .<_  ( P 
.\/  V )  /\  -.  ( g `  P
)  .<_  W ) )
58 breq1 4310 . . . . . . . . . . . 12  |-  ( r  =  ( g `  P )  ->  (
r  .<_  ( P  .\/  V )  <->  ( g `  P )  .<_  ( P 
.\/  V ) ) )
59 breq1 4310 . . . . . . . . . . . . 13  |-  ( r  =  ( g `  P )  ->  (
r  .<_  W  <->  ( g `  P )  .<_  W ) )
6059notbid 294 . . . . . . . . . . . 12  |-  ( r  =  ( g `  P )  ->  ( -.  r  .<_  W  <->  -.  (
g `  P )  .<_  W ) )
6158, 60anbi12d 710 . . . . . . . . . . 11  |-  ( r  =  ( g `  P )  ->  (
( r  .<_  ( P 
.\/  V )  /\  -.  r  .<_  W )  <-> 
( ( g `  P )  .<_  ( P 
.\/  V )  /\  -.  ( g `  P
)  .<_  W ) ) )
62 cdlemm10.c . . . . . . . . . . 11  |-  C  =  { r  e.  A  |  ( r  .<_  ( P  .\/  V )  /\  -.  r  .<_  W ) }
6361, 62elrab2 3134 . . . . . . . . . 10  |-  ( ( g `  P )  e.  C  <->  ( (
g `  P )  e.  A  /\  (
( g `  P
)  .<_  ( P  .\/  V )  /\  -.  (
g `  P )  .<_  W ) ) )
6423, 57, 63sylanbrc 664 . . . . . . . . 9  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
g  e.  T  /\  ( R `  g ) 
.<_  V ) )  -> 
( g `  P
)  e.  C )
6518, 19, 20, 21cdlemeiota 34248 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  g  e.  T )  ->  g  =  ( iota_ f  e.  T  ( f `  P )  =  ( g `  P ) ) )
6615, 40, 16, 65syl3anc 1218 . . . . . . . . . 10  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
g  e.  T  /\  ( R `  g ) 
.<_  V ) )  -> 
g  =  ( iota_ f  e.  T  ( f `
 P )  =  ( g `  P
) ) )
6766eqcomd 2448 . . . . . . . . 9  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
g  e.  T  /\  ( R `  g ) 
.<_  V ) )  -> 
( iota_ f  e.  T  ( f `  P
)  =  ( g `
 P ) )  =  g )
68 eqeq2 2452 . . . . . . . . . . . . 13  |-  ( s  =  ( g `  P )  ->  (
( f `  P
)  =  s  <->  ( f `  P )  =  ( g `  P ) ) )
6968riotabidv 6069 . . . . . . . . . . . 12  |-  ( s  =  ( g `  P )  ->  ( iota_ f  e.  T  ( f `  P )  =  s )  =  ( iota_ f  e.  T  ( f `  P
)  =  ( g `
 P ) ) )
7010, 69syl5eq 2487 . . . . . . . . . . 11  |-  ( s  =  ( g `  P )  ->  F  =  ( iota_ f  e.  T  ( f `  P )  =  ( g `  P ) ) )
7170eqeq1d 2451 . . . . . . . . . 10  |-  ( s  =  ( g `  P )  ->  ( F  =  g  <->  ( iota_ f  e.  T  ( f `
 P )  =  ( g `  P
) )  =  g ) )
7271rspcev 3088 . . . . . . . . 9  |-  ( ( ( g `  P
)  e.  C  /\  ( iota_ f  e.  T  ( f `  P
)  =  ( g `
 P ) )  =  g )  ->  E. s  e.  C  F  =  g )
7364, 67, 72syl2anc 661 . . . . . . . 8  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
g  e.  T  /\  ( R `  g ) 
.<_  V ) )  ->  E. s  e.  C  F  =  g )
7473ex 434 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  ->  ( ( g  e.  T  /\  ( R `  g )  .<_  V )  ->  E. s  e.  C  F  =  g ) )
75 breq1 4310 . . . . . . . . . . . . 13  |-  ( r  =  s  ->  (
r  .<_  ( P  .\/  V )  <->  s  .<_  ( P 
.\/  V ) ) )
76 breq1 4310 . . . . . . . . . . . . . 14  |-  ( r  =  s  ->  (
r  .<_  W  <->  s  .<_  W ) )
7776notbid 294 . . . . . . . . . . . . 13  |-  ( r  =  s  ->  ( -.  r  .<_  W  <->  -.  s  .<_  W ) )
7875, 77anbi12d 710 . . . . . . . . . . . 12  |-  ( r  =  s  ->  (
( r  .<_  ( P 
.\/  V )  /\  -.  r  .<_  W )  <-> 
( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) ) )
7978, 62elrab2 3134 . . . . . . . . . . 11  |-  ( s  e.  C  <->  ( s  e.  A  /\  (
s  .<_  ( P  .\/  V )  /\  -.  s  .<_  W ) ) )
80 simpl1 991 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) ) )  ->  ( K  e.  HL  /\  W  e.  H ) )
81 simpl2l 1041 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) ) )  ->  P  e.  A )
82 simpl2r 1042 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) ) )  ->  -.  P  .<_  W )
83 simprl 755 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) ) )  ->  s  e.  A )
84 simprrr 764 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) ) )  ->  -.  s  .<_  W )
8518, 19, 20, 21, 10ltrniotacl 34242 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  (
s  e.  A  /\  -.  s  .<_  W ) )  ->  F  e.  T )
8618, 19, 20, 21, 10ltrniotaval 34244 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  (
s  e.  A  /\  -.  s  .<_  W ) )  ->  ( F `  P )  =  s )
8785, 86jca 532 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  (
s  e.  A  /\  -.  s  .<_  W ) )  ->  ( F  e.  T  /\  ( F `  P )  =  s ) )
8880, 81, 82, 83, 84, 87syl122anc 1227 . . . . . . . . . . . 12  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) ) )  ->  ( F  e.  T  /\  ( F `  P )  =  s ) )
89 simp3l 1016 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) )  /\  ( F  e.  T  /\  ( F `  P )  =  s ) )  ->  F  e.  T
)
90 simp11 1018 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) )  /\  ( F  e.  T  /\  ( F `  P )  =  s ) )  ->  ( K  e.  HL  /\  W  e.  H ) )
91 simp12 1019 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) )  /\  ( F  e.  T  /\  ( F `  P )  =  s ) )  ->  ( P  e.  A  /\  -.  P  .<_  W ) )
92 eqid 2443 . . . . . . . . . . . . . . . . 17  |-  ( meet `  K )  =  (
meet `  K )
9318, 32, 92, 19, 20, 21, 41trlval2 33826 . . . . . . . . . . . . . . . 16  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( R `  F )  =  ( ( P  .\/  ( F `  P )
) ( meet `  K
) W ) )
9490, 89, 91, 93syl3anc 1218 . . . . . . . . . . . . . . 15  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) )  /\  ( F  e.  T  /\  ( F `  P )  =  s ) )  ->  ( R `  F )  =  ( ( P  .\/  ( F `  P )
) ( meet `  K
) W ) )
95 simp3r 1017 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) )  /\  ( F  e.  T  /\  ( F `  P )  =  s ) )  ->  ( F `  P )  =  s )
9695oveq2d 6122 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) )  /\  ( F  e.  T  /\  ( F `  P )  =  s ) )  ->  ( P  .\/  ( F `  P ) )  =  ( P 
.\/  s ) )
9796oveq1d 6121 . . . . . . . . . . . . . . 15  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) )  /\  ( F  e.  T  /\  ( F `  P )  =  s ) )  ->  ( ( P 
.\/  ( F `  P ) ) (
meet `  K ) W )  =  ( ( P  .\/  s
) ( meet `  K
) W ) )
9894, 97eqtrd 2475 . . . . . . . . . . . . . 14  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) )  /\  ( F  e.  T  /\  ( F `  P )  =  s ) )  ->  ( R `  F )  =  ( ( P  .\/  s
) ( meet `  K
) W ) )
99 simpl1l 1039 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) ) )  ->  K  e.  HL )
100 simpl3l 1043 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) ) )  ->  V  e.  A )
10118, 32, 19hlatlej1 33038 . . . . . . . . . . . . . . . . . . 19  |-  ( ( K  e.  HL  /\  P  e.  A  /\  V  e.  A )  ->  P  .<_  ( P  .\/  V ) )
10299, 81, 100, 101syl3anc 1218 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) ) )  ->  P  .<_  ( P  .\/  V
) )
103 simprrl 763 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) ) )  ->  s  .<_  ( P  .\/  V
) )
10499, 26syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) ) )  ->  K  e.  Lat )
10581, 28syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) ) )  ->  P  e.  ( Base `  K
) )
10624, 19atbase 32953 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  e.  A  ->  s  e.  ( Base `  K
) )
107106ad2antrl 727 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) ) )  ->  s  e.  ( Base `  K
) )
10899, 81, 100, 36syl3anc 1218 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) ) )  ->  ( P  .\/  V )  e.  ( Base `  K
) )
10924, 18, 32latjle12 15247 . . . . . . . . . . . . . . . . . . 19  |-  ( ( K  e.  Lat  /\  ( P  e.  ( Base `  K )  /\  s  e.  ( Base `  K )  /\  ( P  .\/  V )  e.  ( Base `  K
) ) )  -> 
( ( P  .<_  ( P  .\/  V )  /\  s  .<_  ( P 
.\/  V ) )  <-> 
( P  .\/  s
)  .<_  ( P  .\/  V ) ) )
110104, 105, 107, 108, 109syl13anc 1220 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) ) )  ->  (
( P  .<_  ( P 
.\/  V )  /\  s  .<_  ( P  .\/  V ) )  <->  ( P  .\/  s )  .<_  ( P 
.\/  V ) ) )
111102, 103, 110mpbi2and 912 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) ) )  ->  ( P  .\/  s )  .<_  ( P  .\/  V ) )
11224, 32, 19hlatjcl 33030 . . . . . . . . . . . . . . . . . . 19  |-  ( ( K  e.  HL  /\  P  e.  A  /\  s  e.  A )  ->  ( P  .\/  s
)  e.  ( Base `  K ) )
11399, 81, 83, 112syl3anc 1218 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) ) )  ->  ( P  .\/  s )  e.  ( Base `  K
) )
114 simpl1r 1040 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) ) )  ->  W  e.  H )
11524, 20lhpbase 33661 . . . . . . . . . . . . . . . . . . 19  |-  ( W  e.  H  ->  W  e.  ( Base `  K
) )
116114, 115syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) ) )  ->  W  e.  ( Base `  K
) )
11724, 18, 92latmlem1 15266 . . . . . . . . . . . . . . . . . 18  |-  ( ( K  e.  Lat  /\  ( ( P  .\/  s )  e.  (
Base `  K )  /\  ( P  .\/  V
)  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) ) )  -> 
( ( P  .\/  s )  .<_  ( P 
.\/  V )  -> 
( ( P  .\/  s ) ( meet `  K ) W ) 
.<_  ( ( P  .\/  V ) ( meet `  K
) W ) ) )
118104, 113, 108, 116, 117syl13anc 1220 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) ) )  ->  (
( P  .\/  s
)  .<_  ( P  .\/  V )  ->  ( ( P  .\/  s ) (
meet `  K ) W )  .<_  ( ( P  .\/  V ) ( meet `  K
) W ) ) )
119111, 118mpd 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) ) )  ->  (
( P  .\/  s
) ( meet `  K
) W )  .<_  ( ( P  .\/  V ) ( meet `  K
) W ) )
12018, 32, 92, 19, 20lhpat4N 33707 . . . . . . . . . . . . . . . . 17  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  ->  ( ( P 
.\/  V ) (
meet `  K ) W )  =  V )
121120adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) ) )  ->  (
( P  .\/  V
) ( meet `  K
) W )  =  V )
122119, 121breqtrd 4331 . . . . . . . . . . . . . . 15  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) ) )  ->  (
( P  .\/  s
) ( meet `  K
) W )  .<_  V )
1231223adant3 1008 . . . . . . . . . . . . . 14  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) )  /\  ( F  e.  T  /\  ( F `  P )  =  s ) )  ->  ( ( P 
.\/  s ) (
meet `  K ) W )  .<_  V )
12498, 123eqbrtrd 4327 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) )  /\  ( F  e.  T  /\  ( F `  P )  =  s ) )  ->  ( R `  F )  .<_  V )
12589, 124jca 532 . . . . . . . . . . . 12  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) )  /\  ( F  e.  T  /\  ( F `  P )  =  s ) )  ->  ( F  e.  T  /\  ( R `
 F )  .<_  V ) )
12688, 125mpd3an3 1315 . . . . . . . . . . 11  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  (
s  e.  A  /\  ( s  .<_  ( P 
.\/  V )  /\  -.  s  .<_  W ) ) )  ->  ( F  e.  T  /\  ( R `  F ) 
.<_  V ) )
12779, 126sylan2b 475 . . . . . . . . . 10  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  s  e.  C )  ->  ( F  e.  T  /\  ( R `  F ) 
.<_  V ) )
128127ex 434 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  ->  ( s  e.  C  ->  ( F  e.  T  /\  ( R `  F )  .<_  V ) ) )
129 eleq1 2503 . . . . . . . . . . 11  |-  ( F  =  g  ->  ( F  e.  T  <->  g  e.  T ) )
130 fveq2 5706 . . . . . . . . . . . 12  |-  ( F  =  g  ->  ( R `  F )  =  ( R `  g ) )
131130breq1d 4317 . . . . . . . . . . 11  |-  ( F  =  g  ->  (
( R `  F
)  .<_  V  <->  ( R `  g )  .<_  V ) )
132129, 131anbi12d 710 . . . . . . . . . 10  |-  ( F  =  g  ->  (
( F  e.  T  /\  ( R `  F
)  .<_  V )  <->  ( g  e.  T  /\  ( R `  g )  .<_  V ) ) )
133132biimpcd 224 . . . . . . . . 9  |-  ( ( F  e.  T  /\  ( R `  F ) 
.<_  V )  ->  ( F  =  g  ->  ( g  e.  T  /\  ( R `  g ) 
.<_  V ) ) )
134128, 133syl6 33 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  ->  ( s  e.  C  ->  ( F  =  g  ->  ( g  e.  T  /\  ( R `  g )  .<_  V ) ) ) )
135134rexlimdv 2855 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  ->  ( E. s  e.  C  F  =  g  ->  ( g  e.  T  /\  ( R `
 g )  .<_  V ) ) )
13674, 135impbid 191 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  ->  ( ( g  e.  T  /\  ( R `  g )  .<_  V )  <->  E. s  e.  C  F  =  g ) )
13714, 136bitr4d 256 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  ->  ( E. s  e.  C  ( G `  s )  =  g  <-> 
( g  e.  T  /\  ( R `  g
)  .<_  V ) ) )
138 fveq2 5706 . . . . . . 7  |-  ( f  =  g  ->  ( R `  f )  =  ( R `  g ) )
139138breq1d 4317 . . . . . 6  |-  ( f  =  g  ->  (
( R `  f
)  .<_  V  <->  ( R `  g )  .<_  V ) )
140139elrab 3132 . . . . 5  |-  ( g  e.  { f  e.  T  |  ( R `
 f )  .<_  V }  <->  ( g  e.  T  /\  ( R `
 g )  .<_  V ) )
141137, 140syl6bbr 263 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  ->  ( E. s  e.  C  ( G `  s )  =  g  <-> 
g  e.  { f  e.  T  |  ( R `  f ) 
.<_  V } ) )
142 simp1l 1012 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  ->  K  e.  HL )
143 simp1r 1013 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  ->  W  e.  H
)
144 simp3l 1016 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  ->  V  e.  A
)
145144, 47syl 16 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  ->  V  e.  (
Base `  K )
)
146 simp3r 1017 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  ->  V  .<_  W )
147 cdlemm10.i . . . . . . 7  |-  I  =  ( ( DIsoA `  K
) `  W )
14824, 18, 20, 21, 41, 147diaval 34696 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( V  e.  ( Base `  K
)  /\  V  .<_  W ) )  ->  (
I `  V )  =  { f  e.  T  |  ( R `  f )  .<_  V }
)
149142, 143, 145, 146, 148syl22anc 1219 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  ->  ( I `  V )  =  {
f  e.  T  | 
( R `  f
)  .<_  V } )
150149eleq2d 2510 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  ->  ( g  e.  ( I `  V
)  <->  g  e.  {
f  e.  T  | 
( R `  f
)  .<_  V } ) )
151141, 150bitr4d 256 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  ->  ( E. s  e.  C  ( G `  s )  =  g  <-> 
g  e.  ( I `
 V ) ) )
1525, 151syl5bb 257 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  ->  ( g  e. 
ran  G  <->  g  e.  ( I `  V ) ) )
153152eqrdv 2441 1  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( V  e.  A  /\  V  .<_  W ) )  ->  ran  G  =  ( I `  V
) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965    = wceq 1369    e. wcel 1756   E.wrex 2731   {crab 2734   class class class wbr 4307    e. cmpt 4365   ran crn 4856    Fn wfn 5428   ` cfv 5433   iota_crio 6066  (class class class)co 6106   Basecbs 14189   lecple 14260   joincjn 15129   meetcmee 15130   Latclat 15230   Atomscatm 32927   HLchlt 33014   LHypclh 33647   LTrncltrn 33764   trLctrl 33821   DIsoAcdia 34692
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4418  ax-sep 4428  ax-nul 4436  ax-pow 4485  ax-pr 4546  ax-un 6387  ax-riotaBAD 32623
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-nel 2623  df-ral 2735  df-rex 2736  df-reu 2737  df-rmo 2738  df-rab 2739  df-v 2989  df-sbc 3202  df-csb 3304  df-dif 3346  df-un 3348  df-in 3350  df-ss 3357  df-nul 3653  df-if 3807  df-pw 3877  df-sn 3893  df-pr 3895  df-op 3899  df-uni 4107  df-iun 4188  df-iin 4189  df-br 4308  df-opab 4366  df-mpt 4367  df-id 4651  df-xp 4861  df-rel 4862  df-cnv 4863  df-co 4864  df-dm 4865  df-rn 4866  df-res 4867  df-ima 4868  df-iota 5396  df-fun 5435  df-fn 5436  df-f 5437  df-f1 5438  df-fo 5439  df-f1o 5440  df-fv 5441  df-riota 6067  df-ov 6109  df-oprab 6110  df-mpt2 6111  df-1st 6592  df-2nd 6593  df-undef 6807  df-map 7231  df-poset 15131  df-plt 15143  df-lub 15159  df-glb 15160  df-join 15161  df-meet 15162  df-p0 15224  df-p1 15225  df-lat 15231  df-clat 15293  df-oposet 32840  df-ol 32842  df-oml 32843  df-covers 32930  df-ats 32931  df-atl 32962  df-cvlat 32986  df-hlat 33015  df-llines 33161  df-lplanes 33162  df-lvols 33163  df-lines 33164  df-psubsp 33166  df-pmap 33167  df-padd 33459  df-lhyp 33651  df-laut 33652  df-ldil 33767  df-ltrn 33768  df-trl 33822  df-disoa 34693
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator