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

Theorem dihglbcpreN 34914
Description: Isomorphism H of a lattice glb when the glb is not under the fiducial hyperplane  W. (Contributed by NM, 20-Mar-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
dihglbc.b  |-  B  =  ( Base `  K
)
dihglbc.g  |-  G  =  ( glb `  K
)
dihglbc.h  |-  H  =  ( LHyp `  K
)
dihglbc.i  |-  I  =  ( ( DIsoH `  K
) `  W )
dihglbc.l  |-  .<_  =  ( le `  K )
dihglbcpre.j  |-  .\/  =  ( join `  K )
dihglbcpre.m  |-  ./\  =  ( meet `  K )
dihglbcpre.a  |-  A  =  ( Atoms `  K )
dihglbcpre.p  |-  P  =  ( ( oc `  K ) `  W
)
dihglbcpre.t  |-  T  =  ( ( LTrn `  K
) `  W )
dihglbcpre.r  |-  R  =  ( ( trL `  K
) `  W )
dihglbcpre.e  |-  E  =  ( ( TEndo `  K
) `  W )
dihglbcpre.f  |-  F  =  ( iota_ g  e.  T  ( g `  P
)  =  q )
Assertion
Ref Expression
dihglbcpreN  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S
)  .<_  W )  -> 
( I `  ( G `  S )
)  =  |^|_ x  e.  S  ( I `  x ) )
Distinct variable groups:    x, q,  ./\    g, q, x,  .<_    x,  .\/    A, g, q, x    B, q, x    x, E    x, F    G, q, x    g, H, q, x    I, q   
g, K, q, x    P, g    x, R    S, q, x    T, g, x   
g, W, q, x
Allowed substitution hints:    B( g)    P( x, q)    R( g, q)    S( g)    T( q)    E( g, q)    F( g, q)    G( g)    I( x, g)    .\/ ( g, q)    ./\ ( g)

Proof of Theorem dihglbcpreN
Dummy variables  f 
s are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dihglbc.h . . . 4  |-  H  =  ( LHyp `  K
)
2 dihglbc.i . . . 4  |-  I  =  ( ( DIsoH `  K
) `  W )
31, 2dihvalrel 34893 . . 3  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  Rel  ( I `  ( G `  S ) ) )
433ad2ant1 1035 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S
)  .<_  W )  ->  Rel  ( I `  ( G `  S )
) )
5 simp2r 1041 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S
)  .<_  W )  ->  S  =/=  (/) )
6 n0 3753 . . . . . 6  |-  ( S  =/=  (/)  <->  E. x  x  e.  S )
75, 6sylib 201 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S
)  .<_  W )  ->  E. x  x  e.  S )
8 simpr 467 . . . . . . . 8  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  x  e.  S )  ->  x  e.  S )
9 simpl1 1017 . . . . . . . . 9  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  x  e.  S )  ->  ( K  e.  HL  /\  W  e.  H ) )
101, 2dihvalrel 34893 . . . . . . . . 9  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  Rel  ( I `  x ) )
119, 10syl 17 . . . . . . . 8  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  x  e.  S )  ->  Rel  ( I `  x
) )
128, 11jca 539 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  x  e.  S )  ->  (
x  e.  S  /\  Rel  ( I `  x
) ) )
1312ex 440 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S
)  .<_  W )  -> 
( x  e.  S  ->  ( x  e.  S  /\  Rel  ( I `  x ) ) ) )
1413eximdv 1775 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S
)  .<_  W )  -> 
( E. x  x  e.  S  ->  E. x
( x  e.  S  /\  Rel  ( I `  x ) ) ) )
157, 14mpd 15 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S
)  .<_  W )  ->  E. x ( x  e.  S  /\  Rel  (
I `  x )
) )
16 df-rex 2755 . . . 4  |-  ( E. x  e.  S  Rel  ( I `  x
)  <->  E. x ( x  e.  S  /\  Rel  ( I `  x
) ) )
1715, 16sylibr 217 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S
)  .<_  W )  ->  E. x  e.  S  Rel  ( I `  x
) )
18 reliin 4977 . . 3  |-  ( E. x  e.  S  Rel  ( I `  x
)  ->  Rel  |^|_ x  e.  S  ( I `  x ) )
1917, 18syl 17 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S
)  .<_  W )  ->  Rel  |^|_ x  e.  S  ( I `  x
) )
20 id 22 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S
)  .<_  W )  -> 
( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W ) )
21 simp1 1014 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S
)  .<_  W )  -> 
( K  e.  HL  /\  W  e.  H ) )
22 simp1l 1038 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S
)  .<_  W )  ->  K  e.  HL )
23 hlclat 32970 . . . . . . 7  |-  ( K  e.  HL  ->  K  e.  CLat )
2422, 23syl 17 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S
)  .<_  W )  ->  K  e.  CLat )
25 simp2l 1040 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S
)  .<_  W )  ->  S  C_  B )
26 dihglbc.b . . . . . . 7  |-  B  =  ( Base `  K
)
27 dihglbc.g . . . . . . 7  |-  G  =  ( glb `  K
)
2826, 27clatglbcl 16415 . . . . . 6  |-  ( ( K  e.  CLat  /\  S  C_  B )  ->  ( G `  S )  e.  B )
2924, 25, 28syl2anc 671 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S
)  .<_  W )  -> 
( G `  S
)  e.  B )
30 simp3 1016 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S
)  .<_  W )  ->  -.  ( G `  S
)  .<_  W )
31 dihglbc.l . . . . . 6  |-  .<_  =  ( le `  K )
32 dihglbcpre.j . . . . . 6  |-  .\/  =  ( join `  K )
33 dihglbcpre.m . . . . . 6  |-  ./\  =  ( meet `  K )
34 dihglbcpre.a . . . . . 6  |-  A  =  ( Atoms `  K )
3526, 31, 32, 33, 34, 1lhpmcvr2 33635 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( G `
 S )  e.  B  /\  -.  ( G `  S )  .<_  W ) )  ->  E. q  e.  A  ( -.  q  .<_  W  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) ) )
3621, 29, 30, 35syl12anc 1274 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S
)  .<_  W )  ->  E. q  e.  A  ( -.  q  .<_  W  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) ) )
37 simpl1 1017 . . . . . . . . 9  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) ) )  ->  ( K  e.  HL  /\  W  e.  H ) )
3829adantr 471 . . . . . . . . 9  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) ) )  ->  ( G `  S )  e.  B )
39 simpl3 1019 . . . . . . . . 9  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) ) )  ->  -.  ( G `  S ) 
.<_  W )
40 simpr 467 . . . . . . . . 9  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) ) )  ->  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) ) )
41 dihglbcpre.p . . . . . . . . . 10  |-  P  =  ( ( oc `  K ) `  W
)
42 dihglbcpre.t . . . . . . . . . 10  |-  T  =  ( ( LTrn `  K
) `  W )
43 dihglbcpre.r . . . . . . . . . 10  |-  R  =  ( ( trL `  K
) `  W )
44 dihglbcpre.e . . . . . . . . . 10  |-  E  =  ( ( TEndo `  K
) `  W )
45 dihglbcpre.f . . . . . . . . . 10  |-  F  =  ( iota_ g  e.  T  ( g `  P
)  =  q )
46 vex 3060 . . . . . . . . . 10  |-  f  e. 
_V
47 vex 3060 . . . . . . . . . 10  |-  s  e. 
_V
4826, 31, 32, 33, 34, 1, 41, 42, 43, 44, 2, 45, 46, 47dihopelvalc 34863 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( G `
 S )  e.  B  /\  -.  ( G `  S )  .<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) ) )  ->  ( <. f ,  s >.  e.  ( I `  ( G `  S )
)  <->  ( ( f  e.  T  /\  s  e.  E )  /\  ( R `  ( f  o.  `' ( s `  F ) ) ) 
.<_  ( G `  S
) ) ) )
4937, 38, 39, 40, 48syl121anc 1281 . . . . . . . 8  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) ) )  ->  ( <. f ,  s >.  e.  ( I `  ( G `  S )
)  <->  ( ( f  e.  T  /\  s  e.  E )  /\  ( R `  ( f  o.  `' ( s `  F ) ) ) 
.<_  ( G `  S
) ) ) )
50 simpl2r 1068 . . . . . . . . . . 11  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) ) )  ->  S  =/=  (/) )
51 r19.28zv 3876 . . . . . . . . . . 11  |-  ( S  =/=  (/)  ->  ( A. x  e.  S  (
( f  e.  T  /\  s  e.  E
)  /\  ( R `  ( f  o.  `' ( s `  F
) ) )  .<_  x )  <->  ( (
f  e.  T  /\  s  e.  E )  /\  A. x  e.  S  ( R `  ( f  o.  `' ( s `
 F ) ) )  .<_  x )
) )
5250, 51syl 17 . . . . . . . . . 10  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) ) )  ->  ( A. x  e.  S  ( ( f  e.  T  /\  s  e.  E )  /\  ( R `  ( f  o.  `' ( s `  F ) ) ) 
.<_  x )  <->  ( (
f  e.  T  /\  s  e.  E )  /\  A. x  e.  S  ( R `  ( f  o.  `' ( s `
 F ) ) )  .<_  x )
) )
53 simp11 1044 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  ( K  e.  HL  /\  W  e.  H ) )
54 simp12l 1127 . . . . . . . . . . . . . 14  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  S  C_  B )
55 simp3 1016 . . . . . . . . . . . . . 14  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  x  e.  S )
5654, 55sseldd 3445 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  x  e.  B )
57 simp13 1046 . . . . . . . . . . . . . 14  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  -.  ( G `  S ) 
.<_  W )
58 simp11l 1125 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  K  e.  HL )
5958, 23syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  K  e.  CLat )
6026, 31, 27clatglble 16426 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  CLat  /\  S  C_  B  /\  x  e.  S )  ->  ( G `  S )  .<_  x )
6159, 54, 55, 60syl3anc 1276 . . . . . . . . . . . . . . 15  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  ( G `  S )  .<_  x )
62 hllat 32975 . . . . . . . . . . . . . . . . 17  |-  ( K  e.  HL  ->  K  e.  Lat )
6358, 62syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  K  e.  Lat )
64293ad2ant1 1035 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  ( G `  S )  e.  B )
65 simp11r 1126 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  W  e.  H )
6626, 1lhpbase 33609 . . . . . . . . . . . . . . . . 17  |-  ( W  e.  H  ->  W  e.  B )
6765, 66syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  W  e.  B )
6826, 31lattr 16357 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  Lat  /\  ( ( G `  S )  e.  B  /\  x  e.  B  /\  W  e.  B
) )  ->  (
( ( G `  S )  .<_  x  /\  x  .<_  W )  -> 
( G `  S
)  .<_  W ) )
6963, 64, 56, 67, 68syl13anc 1278 . . . . . . . . . . . . . . 15  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  (
( ( G `  S )  .<_  x  /\  x  .<_  W )  -> 
( G `  S
)  .<_  W ) )
7061, 69mpand 686 . . . . . . . . . . . . . 14  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  (
x  .<_  W  ->  ( G `  S )  .<_  W ) )
7157, 70mtod 182 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  -.  x  .<_  W )
72 simp2l 1040 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  (
q  e.  A  /\  -.  q  .<_  W ) )
73 simp2ll 1081 . . . . . . . . . . . . . . 15  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  q  e.  A )
7426, 34atbase 32901 . . . . . . . . . . . . . . . . 17  |-  ( q  e.  A  ->  q  e.  B )
7573, 74syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  q  e.  B )
7626, 33latmcl 16353 . . . . . . . . . . . . . . . . . . 19  |-  ( ( K  e.  Lat  /\  ( G `  S )  e.  B  /\  W  e.  B )  ->  (
( G `  S
)  ./\  W )  e.  B )
7763, 64, 67, 76syl3anc 1276 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  (
( G `  S
)  ./\  W )  e.  B )
7826, 31, 32latlej1 16361 . . . . . . . . . . . . . . . . . 18  |-  ( ( K  e.  Lat  /\  q  e.  B  /\  ( ( G `  S )  ./\  W
)  e.  B )  ->  q  .<_  ( q 
.\/  ( ( G `
 S )  ./\  W ) ) )
7963, 75, 77, 78syl3anc 1276 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  q  .<_  ( q  .\/  (
( G `  S
)  ./\  W )
) )
80 simp2r 1041 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  (
q  .\/  ( ( G `  S )  ./\  W ) )  =  ( G `  S
) )
8179, 80breqtrd 4443 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  q  .<_  ( G `  S
) )
8226, 31, 63, 75, 64, 56, 81, 61lattrd 16359 . . . . . . . . . . . . . . 15  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  q  .<_  x )
8326, 31, 32, 33, 34atmod3i1 33475 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  HL  /\  ( q  e.  A  /\  x  e.  B  /\  W  e.  B
)  /\  q  .<_  x )  ->  ( q  .\/  ( x  ./\  W
) )  =  ( x  ./\  ( q  .\/  W ) ) )
8458, 73, 56, 67, 82, 83syl131anc 1289 . . . . . . . . . . . . . 14  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  (
q  .\/  ( x  ./\ 
W ) )  =  ( x  ./\  (
q  .\/  W )
) )
85 eqid 2462 . . . . . . . . . . . . . . . . 17  |-  ( 1.
`  K )  =  ( 1. `  K
)
8631, 32, 85, 34, 1lhpjat2 33632 . . . . . . . . . . . . . . . 16  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( q  e.  A  /\  -.  q  .<_  W ) )  -> 
( q  .\/  W
)  =  ( 1.
`  K ) )
8753, 72, 86syl2anc 671 . . . . . . . . . . . . . . 15  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  (
q  .\/  W )  =  ( 1. `  K ) )
8887oveq2d 6336 . . . . . . . . . . . . . 14  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  (
x  ./\  ( q  .\/  W ) )  =  ( x  ./\  ( 1. `  K ) ) )
89 hlol 32973 . . . . . . . . . . . . . . . 16  |-  ( K  e.  HL  ->  K  e.  OL )
9058, 89syl 17 . . . . . . . . . . . . . . 15  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  K  e.  OL )
9126, 33, 85olm11 32839 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  OL  /\  x  e.  B )  ->  ( x  ./\  ( 1. `  K ) )  =  x )
9290, 56, 91syl2anc 671 . . . . . . . . . . . . . 14  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  (
x  ./\  ( 1. `  K ) )  =  x )
9384, 88, 923eqtrd 2500 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  (
q  .\/  ( x  ./\ 
W ) )  =  x )
9426, 31, 32, 33, 34, 1, 41, 42, 43, 44, 2, 45, 46, 47dihopelvalc 34863 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( x  e.  B  /\  -.  x  .<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( x  ./\  W ) )  =  x ) )  ->  ( <. f ,  s >.  e.  ( I `  x )  <-> 
( ( f  e.  T  /\  s  e.  E )  /\  ( R `  ( f  o.  `' ( s `  F ) ) ) 
.<_  x ) ) )
9553, 56, 71, 72, 93, 94syl122anc 1285 . . . . . . . . . . . 12  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  x  e.  S )  ->  ( <. f ,  s >.  e.  ( I `  x
)  <->  ( ( f  e.  T  /\  s  e.  E )  /\  ( R `  ( f  o.  `' ( s `  F ) ) ) 
.<_  x ) ) )
96953expa 1215 . . . . . . . . . . 11  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) ) )  /\  x  e.  S )  ->  ( <. f ,  s >.  e.  ( I `  x
)  <->  ( ( f  e.  T  /\  s  e.  E )  /\  ( R `  ( f  o.  `' ( s `  F ) ) ) 
.<_  x ) ) )
9796ralbidva 2836 . . . . . . . . . 10  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) ) )  ->  ( A. x  e.  S  <. f ,  s >.  e.  ( I `  x
)  <->  A. x  e.  S  ( ( f  e.  T  /\  s  e.  E )  /\  ( R `  ( f  o.  `' ( s `  F ) ) ) 
.<_  x ) ) )
98 simp11l 1125 . . . . . . . . . . . . . 14  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  ( f  e.  T  /\  s  e.  E ) )  ->  K  e.  HL )
9998, 23syl 17 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  ( f  e.  T  /\  s  e.  E ) )  ->  K  e.  CLat )
100 simp11 1044 . . . . . . . . . . . . . 14  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  ( f  e.  T  /\  s  e.  E ) )  -> 
( K  e.  HL  /\  W  e.  H ) )
101 simp3l 1042 . . . . . . . . . . . . . . 15  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  ( f  e.  T  /\  s  e.  E ) )  -> 
f  e.  T )
102 simp3r 1043 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  ( f  e.  T  /\  s  e.  E ) )  -> 
s  e.  E )
10331, 34, 1, 41lhpocnel2 33630 . . . . . . . . . . . . . . . . . . 19  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( P  e.  A  /\  -.  P  .<_  W ) )
104100, 103syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  ( f  e.  T  /\  s  e.  E ) )  -> 
( P  e.  A  /\  -.  P  .<_  W ) )
105 simp2l 1040 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  ( f  e.  T  /\  s  e.  E ) )  -> 
( q  e.  A  /\  -.  q  .<_  W ) )
10631, 34, 1, 42, 45ltrniotacl 34192 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  (
q  e.  A  /\  -.  q  .<_  W ) )  ->  F  e.  T )
107100, 104, 105, 106syl3anc 1276 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  ( f  e.  T  /\  s  e.  E ) )  ->  F  e.  T )
1081, 42, 44tendocl 34380 . . . . . . . . . . . . . . . . 17  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  s  e.  E  /\  F  e.  T
)  ->  ( s `  F )  e.  T
)
109100, 102, 107, 108syl3anc 1276 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  ( f  e.  T  /\  s  e.  E ) )  -> 
( s `  F
)  e.  T )
1101, 42ltrncnv 33757 . . . . . . . . . . . . . . . 16  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s `  F )  e.  T
)  ->  `' (
s `  F )  e.  T )
111100, 109, 110syl2anc 671 . . . . . . . . . . . . . . 15  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  ( f  e.  T  /\  s  e.  E ) )  ->  `' ( s `  F )  e.  T
)
1121, 42ltrnco 34332 . . . . . . . . . . . . . . 15  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  f  e.  T  /\  `' ( s `  F )  e.  T
)  ->  ( f  o.  `' ( s `  F ) )  e.  T )
113100, 101, 111, 112syl3anc 1276 . . . . . . . . . . . . . 14  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  ( f  e.  T  /\  s  e.  E ) )  -> 
( f  o.  `' ( s `  F
) )  e.  T
)
11426, 1, 42, 43trlcl 33776 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( f  o.  `' ( s `  F ) )  e.  T )  ->  ( R `  ( f  o.  `' ( s `  F ) ) )  e.  B )
115100, 113, 114syl2anc 671 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  ( f  e.  T  /\  s  e.  E ) )  -> 
( R `  (
f  o.  `' ( s `  F ) ) )  e.  B
)
116 simp12l 1127 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  ( f  e.  T  /\  s  e.  E ) )  ->  S  C_  B )
11726, 31, 27clatleglb 16427 . . . . . . . . . . . . 13  |-  ( ( K  e.  CLat  /\  ( R `  ( f  o.  `' ( s `  F ) ) )  e.  B  /\  S  C_  B )  ->  (
( R `  (
f  o.  `' ( s `  F ) ) )  .<_  ( G `
 S )  <->  A. x  e.  S  ( R `  ( f  o.  `' ( s `  F
) ) )  .<_  x ) )
11899, 115, 116, 117syl3anc 1276 . . . . . . . . . . . 12  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) )  /\  ( f  e.  T  /\  s  e.  E ) )  -> 
( ( R `  ( f  o.  `' ( s `  F
) ) )  .<_  ( G `  S )  <->  A. x  e.  S  ( R `  ( f  o.  `' ( s `
 F ) ) )  .<_  x )
)
1191183expa 1215 . . . . . . . . . . 11  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) ) )  /\  (
f  e.  T  /\  s  e.  E )
)  ->  ( ( R `  ( f  o.  `' ( s `  F ) ) ) 
.<_  ( G `  S
)  <->  A. x  e.  S  ( R `  ( f  o.  `' ( s `
 F ) ) )  .<_  x )
)
120119pm5.32da 651 . . . . . . . . . 10  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) ) )  ->  (
( ( f  e.  T  /\  s  e.  E )  /\  ( R `  ( f  o.  `' ( s `  F ) ) ) 
.<_  ( G `  S
) )  <->  ( (
f  e.  T  /\  s  e.  E )  /\  A. x  e.  S  ( R `  ( f  o.  `' ( s `
 F ) ) )  .<_  x )
) )
12152, 97, 1203bitr4rd 294 . . . . . . . . 9  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) ) )  ->  (
( ( f  e.  T  /\  s  e.  E )  /\  ( R `  ( f  o.  `' ( s `  F ) ) ) 
.<_  ( G `  S
) )  <->  A. x  e.  S  <. f ,  s >.  e.  (
I `  x )
) )
122 opex 4681 . . . . . . . . . 10  |-  <. f ,  s >.  e.  _V
123 eliin 4298 . . . . . . . . . 10  |-  ( <.
f ,  s >.  e.  _V  ->  ( <. f ,  s >.  e.  |^|_ x  e.  S  ( I `
 x )  <->  A. x  e.  S  <. f ,  s >.  e.  (
I `  x )
) )
124122, 123ax-mp 5 . . . . . . . . 9  |-  ( <.
f ,  s >.  e.  |^|_ x  e.  S  ( I `  x
)  <->  A. x  e.  S  <. f ,  s >.  e.  ( I `  x
) )
125121, 124syl6bbr 271 . . . . . . . 8  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) ) )  ->  (
( ( f  e.  T  /\  s  e.  E )  /\  ( R `  ( f  o.  `' ( s `  F ) ) ) 
.<_  ( G `  S
) )  <->  <. f ,  s >.  e.  |^|_ x  e.  S  ( I `  x ) ) )
12649, 125bitrd 261 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S ) 
.<_  W )  /\  (
( q  e.  A  /\  -.  q  .<_  W )  /\  ( q  .\/  ( ( G `  S )  ./\  W
) )  =  ( G `  S ) ) )  ->  ( <. f ,  s >.  e.  ( I `  ( G `  S )
)  <->  <. f ,  s
>.  e.  |^|_ x  e.  S  ( I `  x
) ) )
127126exp44 622 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S
)  .<_  W )  -> 
( q  e.  A  ->  ( -.  q  .<_  W  ->  ( ( q 
.\/  ( ( G `
 S )  ./\  W ) )  =  ( G `  S )  ->  ( <. f ,  s >.  e.  ( I `  ( G `
 S ) )  <->  <. f ,  s >.  e.  |^|_ x  e.  S  ( I `  x
) ) ) ) ) )
128127imp4a 598 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S
)  .<_  W )  -> 
( q  e.  A  ->  ( ( -.  q  .<_  W  /\  ( q 
.\/  ( ( G `
 S )  ./\  W ) )  =  ( G `  S ) )  ->  ( <. f ,  s >.  e.  ( I `  ( G `
 S ) )  <->  <. f ,  s >.  e.  |^|_ x  e.  S  ( I `  x
) ) ) ) )
129128rexlimdv 2889 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S
)  .<_  W )  -> 
( E. q  e.  A  ( -.  q  .<_  W  /\  ( q 
.\/  ( ( G `
 S )  ./\  W ) )  =  ( G `  S ) )  ->  ( <. f ,  s >.  e.  ( I `  ( G `
 S ) )  <->  <. f ,  s >.  e.  |^|_ x  e.  S  ( I `  x
) ) ) )
13036, 129mpd 15 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S
)  .<_  W )  -> 
( <. f ,  s
>.  e.  ( I `  ( G `  S ) )  <->  <. f ,  s
>.  e.  |^|_ x  e.  S  ( I `  x
) ) )
131130eqrelrdv2 4956 . 2  |-  ( ( ( Rel  ( I `
 ( G `  S ) )  /\  Rel  |^|_ x  e.  S  ( I `  x
) )  /\  (
( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S
)  .<_  W ) )  ->  ( I `  ( G `  S ) )  =  |^|_ x  e.  S  ( I `  x ) )
1324, 19, 20, 131syl21anc 1275 1  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S  C_  B  /\  S  =/=  (/) )  /\  -.  ( G `  S
)  .<_  W )  -> 
( I `  ( G `  S )
)  =  |^|_ x  e.  S  ( I `  x ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    /\ wa 375    /\ w3a 991    = wceq 1455   E.wex 1674    e. wcel 1898    =/= wne 2633   A.wral 2749   E.wrex 2750   _Vcvv 3057    C_ wss 3416   (/)c0 3743   <.cop 3986   |^|_ciin 4293   class class class wbr 4418   `'ccnv 4855    o. ccom 4860   Rel wrel 4861   ` cfv 5605   iota_crio 6281  (class class class)co 6320   Basecbs 15176   lecple 15252   occoc 15253   glbcglb 16243   joincjn 16244   meetcmee 16245   1.cp1 16339   Latclat 16346   CLatccla 16408   OLcol 32786   Atomscatm 32875   HLchlt 32962   LHypclh 33595   LTrncltrn 33712   trLctrl 33770   TEndoctendo 34365   DIsoHcdih 34842
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4531  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-cnex 9626  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-mulcom 9634  ax-addass 9635  ax-mulass 9636  ax-distr 9637  ax-i2m1 9638  ax-1ne0 9639  ax-1rid 9640  ax-rnegex 9641  ax-rrecex 9642  ax-cnre 9643  ax-pre-lttri 9644  ax-pre-lttrn 9645  ax-pre-ltadd 9646  ax-pre-mulgt0 9647  ax-riotaBAD 32571
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-fal 1461  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-iin 4295  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-om 6725  df-1st 6825  df-2nd 6826  df-tpos 7004  df-undef 7051  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-1o 7213  df-oadd 7217  df-er 7394  df-map 7505  df-en 7601  df-dom 7602  df-sdom 7603  df-fin 7604  df-pnf 9708  df-mnf 9709  df-xr 9710  df-ltxr 9711  df-le 9712  df-sub 9893  df-neg 9894  df-nn 10643  df-2 10701  df-3 10702  df-4 10703  df-5 10704  df-6 10705  df-n0 10904  df-z 10972  df-uz 11194  df-fz 11820  df-struct 15178  df-ndx 15179  df-slot 15180  df-base 15181  df-sets 15182  df-ress 15183  df-plusg 15258  df-mulr 15259  df-sca 15261  df-vsca 15262  df-0g 15395  df-preset 16228  df-poset 16246  df-plt 16259  df-lub 16275  df-glb 16276  df-join 16277  df-meet 16278  df-p0 16340  df-p1 16341  df-lat 16347  df-clat 16409  df-mgm 16543  df-sgrp 16582  df-mnd 16592  df-submnd 16638  df-grp 16728  df-minusg 16729  df-sbg 16730  df-subg 16869  df-cntz 17026  df-lsm 17343  df-cmn 17487  df-abl 17488  df-mgp 17779  df-ur 17791  df-ring 17837  df-oppr 17906  df-dvdsr 17924  df-unit 17925  df-invr 17955  df-dvr 17966  df-drng 18032  df-lmod 18148  df-lss 18211  df-lsp 18250  df-lvec 18381  df-oposet 32788  df-ol 32790  df-oml 32791  df-covers 32878  df-ats 32879  df-atl 32910  df-cvlat 32934  df-hlat 32963  df-llines 33109  df-lplanes 33110  df-lvols 33111  df-lines 33112  df-psubsp 33114  df-pmap 33115  df-padd 33407  df-lhyp 33599  df-laut 33600  df-ldil 33715  df-ltrn 33716  df-trl 33771  df-tendo 34368  df-edring 34370  df-disoa 34643  df-dvech 34693  df-dib 34753  df-dic 34787  df-dih 34843
This theorem is referenced by:  dihglbcN  34915
  Copyright terms: Public domain W3C validator