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 1033 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  P  e.  A )
2 eqid 2422 . . . . . 6  |-  ( Base `  K )  =  (
Base `  K )
3 ltrnel.a . . . . . 6  |-  A  =  ( Atoms `  K )
42, 3atbase 32774 . . . . 5  |-  ( P  e.  A  ->  P  e.  ( Base `  K
) )
54adantr 466 . . . 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 1299 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( P  e.  A  <->  ( F `  P )  e.  A
) )
101, 9mpbid 213 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( F `  P )  e.  A
)
11 simp3r 1034 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  -.  P  .<_  W )
12 simp1 1005 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( K  e.  HL  /\  W  e.  H ) )
13 simp2 1006 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  F  e.  T )
141, 4syl 17 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  P  e.  ( Base `  K )
)
15 simp1r 1030 . . . . . 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 17 . . . . 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 1268 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( P  .<_  W  <->  ( F `  P )  .<_  ( F `
 W ) ) )
21 simp1l 1029 . . . . . . . 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 17 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  K  e.  Lat )
242, 18latref 16287 . . . . . . 7  |-  ( ( K  e.  Lat  /\  W  e.  ( Base `  K ) )  ->  W  .<_  W )
2523, 17, 24syl2anc 665 . . . . . 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 1268 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( F `  W )  =  W )
2827breq2d 4432 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( ( F `  P )  .<_  ( F `  W
)  <->  ( F `  P )  .<_  W ) )
2920, 28bitrd 256 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( P  .<_  W  <->  ( F `  P )  .<_  W ) )
3011, 29mtbid 301 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  -.  ( F `  P )  .<_  W )
3110, 30jca 534 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 187    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1868   class class class wbr 4420   ` cfv 5598   Basecbs 15109   lecple 15185   Latclat 16279   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 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4765  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-f1 5603  df-fo 5604  df-f1o 5605  df-fv 5606  df-riota 6264  df-ov 6305  df-oprab 6306  df-mpt2 6307  df-map 7479  df-preset 16161  df-poset 16179  df-plt 16192  df-glb 16209  df-p0 16273  df-lat 16280  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  ltrnmw  33635  trlcnv  33650  trljat2  33652  cdlemc3  33678  cdlemc5  33680  cdlemd9  33691  cdlemeiota  34071  cdlemg1cex  34074  cdlemg2l  34089  cdlemg2m  34090  cdlemg7fvbwN  34093  cdlemg4a  34094  cdlemg4b1  34095  cdlemg4b2  34096  cdlemg4d  34099  cdlemg4e  34100  cdlemg4  34103  cdlemg6e  34108  cdlemg7fvN  34110  cdlemg8b  34114  cdlemg8c  34115  cdlemg10bALTN  34122  cdlemg10a  34126  cdlemg12d  34132  cdlemg13a  34137  cdlemg13  34138  cdlemg14f  34139  cdlemg17b  34148  cdlemg17f  34152  cdlemg17i  34155  trlcoabs  34207  trlcoabs2N  34208  trlcolem  34212  cdlemg43  34216  cdlemg44b  34218  cdlemi2  34305  cdlemi  34306  cdlemk2  34318  cdlemk3  34319  cdlemk4  34320  cdlemk8  34324  cdlemk9  34325  cdlemk9bN  34326  cdlemki  34327  cdlemksv2  34333  cdlemk12  34336  cdlemkoatnle  34337  cdlemk12u  34358  cdlemkfid1N  34407  cdlemk47  34435  dia2dimlem1  34551  dia2dimlem2  34552  dia2dimlem3  34553  dia2dimlem6  34556  cdlemm10N  34605  dih1dimatlem0  34815  dih1dimatlem  34816
  Copyright terms: Public domain W3C validator