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

Theorem lhpelim 33704
Description: Eliminate an atom not under a lattice hyperplane. TODO: Look at proofs using lhpmat 33697 to see if this can be used to shorten them. (Contributed by NM, 27-Apr-2013.)
Hypotheses
Ref Expression
lhpelim.b  |-  B  =  ( Base `  K
)
lhpelim.l  |-  .<_  =  ( le `  K )
lhpelim.j  |-  .\/  =  ( join `  K )
lhpelim.m  |-  ./\  =  ( meet `  K )
lhpelim.a  |-  A  =  ( Atoms `  K )
lhpelim.h  |-  H  =  ( LHyp `  K
)
Assertion
Ref Expression
lhpelim  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  X  e.  B )  ->  (
( P  .\/  ( X  ./\  W ) ) 
./\  W )  =  ( X  ./\  W
) )

Proof of Theorem lhpelim
StepHypRef Expression
1 lhpelim.l . . . . 5  |-  .<_  =  ( le `  K )
2 lhpelim.m . . . . 5  |-  ./\  =  ( meet `  K )
3 eqid 2443 . . . . 5  |-  ( 0.
`  K )  =  ( 0. `  K
)
4 lhpelim.a . . . . 5  |-  A  =  ( Atoms `  K )
5 lhpelim.h . . . . 5  |-  H  =  ( LHyp `  K
)
61, 2, 3, 4, 5lhpmat 33697 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  -> 
( P  ./\  W
)  =  ( 0.
`  K ) )
763adant3 1008 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  X  e.  B )  ->  ( P  ./\  W )  =  ( 0. `  K
) )
87oveq1d 6125 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  X  e.  B )  ->  (
( P  ./\  W
)  .\/  ( X  ./\ 
W ) )  =  ( ( 0. `  K )  .\/  ( X  ./\  W ) ) )
9 simp1l 1012 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  X  e.  B )  ->  K  e.  HL )
10 simp2l 1014 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  X  e.  B )  ->  P  e.  A )
11 hllat 33031 . . . . 5  |-  ( K  e.  HL  ->  K  e.  Lat )
129, 11syl 16 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  X  e.  B )  ->  K  e.  Lat )
13 simp3 990 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  X  e.  B )  ->  X  e.  B )
14 simp1r 1013 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  X  e.  B )  ->  W  e.  H )
15 lhpelim.b . . . . . 6  |-  B  =  ( Base `  K
)
1615, 5lhpbase 33665 . . . . 5  |-  ( W  e.  H  ->  W  e.  B )
1714, 16syl 16 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  X  e.  B )  ->  W  e.  B )
1815, 2latmcl 15241 . . . 4  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  W  e.  B )  ->  ( X  ./\  W
)  e.  B )
1912, 13, 17, 18syl3anc 1218 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  X  e.  B )  ->  ( X  ./\  W )  e.  B )
2015, 1, 2latmle2 15266 . . . 4  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  W  e.  B )  ->  ( X  ./\  W
)  .<_  W )
2112, 13, 17, 20syl3anc 1218 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  X  e.  B )  ->  ( X  ./\  W )  .<_  W )
22 lhpelim.j . . . 4  |-  .\/  =  ( join `  K )
2315, 1, 22, 2, 4atmod4i2 33534 . . 3  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  ( X  ./\  W
)  e.  B  /\  W  e.  B )  /\  ( X  ./\  W
)  .<_  W )  -> 
( ( P  ./\  W )  .\/  ( X 
./\  W ) )  =  ( ( P 
.\/  ( X  ./\  W ) )  ./\  W
) )
249, 10, 19, 17, 21, 23syl131anc 1231 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  X  e.  B )  ->  (
( P  ./\  W
)  .\/  ( X  ./\ 
W ) )  =  ( ( P  .\/  ( X  ./\  W ) )  ./\  W )
)
25 hlol 33029 . . . 4  |-  ( K  e.  HL  ->  K  e.  OL )
269, 25syl 16 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  X  e.  B )  ->  K  e.  OL )
2715, 22, 3olj02 32894 . . 3  |-  ( ( K  e.  OL  /\  ( X  ./\  W )  e.  B )  -> 
( ( 0. `  K )  .\/  ( X  ./\  W ) )  =  ( X  ./\  W ) )
2826, 19, 27syl2anc 661 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  X  e.  B )  ->  (
( 0. `  K
)  .\/  ( X  ./\ 
W ) )  =  ( X  ./\  W
) )
298, 24, 283eqtr3d 2483 1  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  X  e.  B )  ->  (
( P  .\/  ( X  ./\  W ) ) 
./\  W )  =  ( X  ./\  W
) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    /\ w3a 965    = wceq 1369    e. wcel 1756   class class class wbr 4311   ` cfv 5437  (class class class)co 6110   Basecbs 14193   lecple 14264   joincjn 15133   meetcmee 15134   0.cp0 15226   Latclat 15234   OLcol 32842   Atomscatm 32931   HLchlt 33018   LHypclh 33651
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 4422  ax-sep 4432  ax-nul 4440  ax-pow 4489  ax-pr 4550  ax-un 6391
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  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-ral 2739  df-rex 2740  df-reu 2741  df-rab 2743  df-v 2993  df-sbc 3206  df-csb 3308  df-dif 3350  df-un 3352  df-in 3354  df-ss 3361  df-nul 3657  df-if 3811  df-pw 3881  df-sn 3897  df-pr 3899  df-op 3903  df-uni 4111  df-iun 4192  df-iin 4193  df-br 4312  df-opab 4370  df-mpt 4371  df-id 4655  df-xp 4865  df-rel 4866  df-cnv 4867  df-co 4868  df-dm 4869  df-rn 4870  df-res 4871  df-ima 4872  df-iota 5400  df-fun 5439  df-fn 5440  df-f 5441  df-f1 5442  df-fo 5443  df-f1o 5444  df-fv 5445  df-riota 6071  df-ov 6113  df-oprab 6114  df-mpt2 6115  df-1st 6596  df-2nd 6597  df-poset 15135  df-plt 15147  df-lub 15163  df-glb 15164  df-join 15165  df-meet 15166  df-p0 15228  df-lat 15235  df-clat 15297  df-oposet 32844  df-ol 32846  df-oml 32847  df-covers 32934  df-ats 32935  df-atl 32966  df-cvlat 32990  df-hlat 33019  df-psubsp 33170  df-pmap 33171  df-padd 33463  df-lhyp 33655
This theorem is referenced by:  cdleme48b  34170  cdlemg7fvN  34291
  Copyright terms: Public domain W3C validator