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

Theorem ltrnel 33775
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 1058 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  P  e.  A )
2 eqid 2471 . . . . . 6  |-  ( Base `  K )  =  (
Base `  K )
3 ltrnel.a . . . . . 6  |-  A  =  ( Atoms `  K )
42, 3atbase 32926 . . . . 5  |-  ( P  e.  A  ->  P  e.  ( Base `  K
) )
54adantr 472 . . . 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 33773 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  P  e.  ( Base `  K ) )  ->  ( P  e.  A  <->  ( F `  P )  e.  A
) )
95, 8syl3an3 1327 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( P  e.  A  <->  ( F `  P )  e.  A
) )
101, 9mpbid 215 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( F `  P )  e.  A
)
11 simp3r 1059 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  -.  P  .<_  W )
12 simp1 1030 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( K  e.  HL  /\  W  e.  H ) )
13 simp2 1031 . . . . 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 1055 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  W  e.  H )
162, 6lhpbase 33634 . . . . . 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 33765 . . . . 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 1296 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( P  .<_  W  <->  ( F `  P )  .<_  ( F `
 W ) ) )
21 simp1l 1054 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  K  e.  HL )
22 hllat 33000 . . . . . . . 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 16377 . . . . . . 7  |-  ( ( K  e.  Lat  /\  W  e.  ( Base `  K ) )  ->  W  .<_  W )
2523, 17, 24syl2anc 673 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  W  .<_  W )
262, 18, 6, 7ltrnval1 33770 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( W  e.  (
Base `  K )  /\  W  .<_  W ) )  ->  ( F `  W )  =  W )
2712, 13, 17, 25, 26syl112anc 1296 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( F `  W )  =  W )
2827breq2d 4407 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( ( F `  P )  .<_  ( F `  W
)  <->  ( F `  P )  .<_  W ) )
2920, 28bitrd 261 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( P  .<_  W  <->  ( F `  P )  .<_  W ) )
3011, 29mtbid 307 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  -.  ( F `  P )  .<_  W )
3110, 30jca 541 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 189    /\ wa 376    /\ w3a 1007    = wceq 1452    e. wcel 1904   class class class wbr 4395   ` cfv 5589   Basecbs 15199   lecple 15275   Latclat 16369   Atomscatm 32900   HLchlt 32987   LHypclh 33620   LTrncltrn 33737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-reu 2763  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-map 7492  df-preset 16251  df-poset 16269  df-plt 16282  df-glb 16299  df-p0 16363  df-lat 16370  df-oposet 32813  df-ol 32815  df-oml 32816  df-covers 32903  df-ats 32904  df-atl 32935  df-cvlat 32959  df-hlat 32988  df-lhyp 33624  df-laut 33625  df-ldil 33740  df-ltrn 33741
This theorem is referenced by:  ltrncoelN  33779  ltrnmw  33787  trlcnv  33802  trljat2  33804  cdlemc3  33830  cdlemc5  33832  cdlemd9  33843  cdlemeiota  34223  cdlemg1cex  34226  cdlemg2l  34241  cdlemg2m  34242  cdlemg7fvbwN  34245  cdlemg4a  34246  cdlemg4b1  34247  cdlemg4b2  34248  cdlemg4d  34251  cdlemg4e  34252  cdlemg4  34255  cdlemg6e  34260  cdlemg7fvN  34262  cdlemg8b  34266  cdlemg8c  34267  cdlemg10bALTN  34274  cdlemg10a  34278  cdlemg12d  34284  cdlemg13a  34289  cdlemg13  34290  cdlemg14f  34291  cdlemg17b  34300  cdlemg17f  34304  cdlemg17i  34307  trlcoabs  34359  trlcoabs2N  34360  trlcolem  34364  cdlemg43  34368  cdlemg44b  34370  cdlemi2  34457  cdlemi  34458  cdlemk2  34470  cdlemk3  34471  cdlemk4  34472  cdlemk8  34476  cdlemk9  34477  cdlemk9bN  34478  cdlemki  34479  cdlemksv2  34485  cdlemk12  34488  cdlemkoatnle  34489  cdlemk12u  34510  cdlemkfid1N  34559  cdlemk47  34587  dia2dimlem1  34703  dia2dimlem2  34704  dia2dimlem3  34705  dia2dimlem6  34708  cdlemm10N  34757  dih1dimatlem0  34967  dih1dimatlem  34968
  Copyright terms: Public domain W3C validator