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

Theorem ltrnel 33623
Description: The lattice translation of an atom not under the fiducial co-atom is also an atom not under the fiducial co-atom. Remark below Lemma B in [Crawley] p. 112. (Contributed by NM, 22-May-2012.)
Hypotheses
Ref Expression
ltrnel.l  |-  .<_  =  ( le `  K )
ltrnel.a  |-  A  =  ( Atoms `  K )
ltrnel.h  |-  H  =  ( LHyp `  K
)
ltrnel.t  |-  T  =  ( ( LTrn `  K
) `  W )
Assertion
Ref Expression
ltrnel  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( ( F `  P )  e.  A  /\  -.  ( F `  P )  .<_  W ) )

Proof of Theorem ltrnel
StepHypRef Expression
1 simp3l 1016 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  P  e.  A )
2 eqid 2438 . . . . . 6  |-  ( Base `  K )  =  (
Base `  K )
3 ltrnel.a . . . . . 6  |-  A  =  ( Atoms `  K )
42, 3atbase 32774 . . . . 5  |-  ( P  e.  A  ->  P  e.  ( Base `  K
) )
54adantr 465 . . . 4  |-  ( ( P  e.  A  /\  -.  P  .<_  W )  ->  P  e.  (
Base `  K )
)
6 ltrnel.h . . . . 5  |-  H  =  ( LHyp `  K
)
7 ltrnel.t . . . . 5  |-  T  =  ( ( LTrn `  K
) `  W )
82, 3, 6, 7ltrnatb 33621 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  P  e.  ( Base `  K ) )  ->  ( P  e.  A  <->  ( F `  P )  e.  A
) )
95, 8syl3an3 1253 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( P  e.  A  <->  ( F `  P )  e.  A
) )
101, 9mpbid 210 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( F `  P )  e.  A
)
11 simp3r 1017 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  -.  P  .<_  W )
12 simp1 988 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( K  e.  HL  /\  W  e.  H ) )
13 simp2 989 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  F  e.  T )
141, 4syl 16 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  P  e.  ( Base `  K )
)
15 simp1r 1013 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  W  e.  H )
162, 6lhpbase 33482 . . . . . 6  |-  ( W  e.  H  ->  W  e.  ( Base `  K
) )
1715, 16syl 16 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  W  e.  ( Base `  K )
)
18 ltrnel.l . . . . . 6  |-  .<_  =  ( le `  K )
192, 18, 6, 7ltrnle 33613 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  (
Base `  K )  /\  W  e.  ( Base `  K ) ) )  ->  ( P  .<_  W  <->  ( F `  P )  .<_  ( F `
 W ) ) )
2012, 13, 14, 17, 19syl112anc 1222 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( P  .<_  W  <->  ( F `  P )  .<_  ( F `
 W ) ) )
21 simp1l 1012 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  K  e.  HL )
22 hllat 32848 . . . . . . . 8  |-  ( K  e.  HL  ->  K  e.  Lat )
2321, 22syl 16 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  K  e.  Lat )
242, 18latref 15215 . . . . . . 7  |-  ( ( K  e.  Lat  /\  W  e.  ( Base `  K ) )  ->  W  .<_  W )
2523, 17, 24syl2anc 661 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  W  .<_  W )
262, 18, 6, 7ltrnval1 33618 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( W  e.  (
Base `  K )  /\  W  .<_  W ) )  ->  ( F `  W )  =  W )
2712, 13, 17, 25, 26syl112anc 1222 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( F `  W )  =  W )
2827breq2d 4299 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( ( F `  P )  .<_  ( F `  W
)  <->  ( F `  P )  .<_  W ) )
2920, 28bitrd 253 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( P  .<_  W  <->  ( F `  P )  .<_  W ) )
3011, 29mtbid 300 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  -.  ( F `  P )  .<_  W )
3110, 30jca 532 1  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( ( F `  P )  e.  A  /\  -.  ( F `  P )  .<_  W ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965    = wceq 1369    e. wcel 1756   class class class wbr 4287   ` cfv 5413   Basecbs 14166   lecple 14237   Latclat 15207   Atomscatm 32748   HLchlt 32835   LHypclh 33468   LTrncltrn 33585
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 2419  ax-rep 4398  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367
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 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-reu 2717  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-map 7208  df-poset 15108  df-plt 15120  df-glb 15137  df-p0 15201  df-lat 15208  df-oposet 32661  df-ol 32663  df-oml 32664  df-covers 32751  df-ats 32752  df-atl 32783  df-cvlat 32807  df-hlat 32836  df-lhyp 33472  df-laut 33473  df-ldil 33588  df-ltrn 33589
This theorem is referenced by:  ltrncoelN  33627  trlcnv  33649  trljat2  33651  cdlemc3  33677  cdlemc5  33679  cdlemd9  33690  cdlemeiota  34069  cdlemg1cex  34072  cdlemg2l  34087  cdlemg2m  34088  cdlemg7fvbwN  34091  cdlemg4a  34092  cdlemg4b1  34093  cdlemg4b2  34094  cdlemg4d  34097  cdlemg4e  34098  cdlemg4  34101  cdlemg6e  34106  cdlemg7fvN  34108  cdlemg8b  34112  cdlemg8c  34113  cdlemg10bALTN  34120  cdlemg10a  34124  cdlemg12d  34130  cdlemg13a  34135  cdlemg13  34136  cdlemg14f  34137  cdlemg17b  34146  cdlemg17f  34150  cdlemg17i  34153  trlcoabs  34205  trlcoabs2N  34206  trlcolem  34210  cdlemg43  34214  cdlemg44b  34216  cdlemi2  34303  cdlemi  34304  cdlemk2  34316  cdlemk3  34317  cdlemk4  34318  cdlemk8  34322  cdlemk9  34323  cdlemk9bN  34324  cdlemki  34325  cdlemksv2  34331  cdlemk12  34334  cdlemkoatnle  34335  cdlemk12u  34356  cdlemkfid1N  34405  cdlemk47  34433  dia2dimlem1  34549  dia2dimlem2  34550  dia2dimlem3  34551  dia2dimlem6  34554  cdlemm10N  34603  dih1dimatlem0  34813  dih1dimatlem  34814
  Copyright terms: Public domain W3C validator