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

Theorem ltrnat 37158
Description: The lattice translation of an atom is also an atom. TODO: See if this can shorten some ltrnel 37157 uses. (Contributed by NM, 25-May-2012.)
Hypotheses
Ref Expression
ltrnel.l = (le‘𝐾)
ltrnel.a 𝐴 = (Atoms‘𝐾)
ltrnel.h 𝐻 = (LHyp‘𝐾)
ltrnel.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
Assertion
Ref Expression
ltrnat (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃𝐴) → (𝐹𝑃) ∈ 𝐴)

Proof of Theorem ltrnat
StepHypRef Expression
1 simp3 1130 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃𝐴) → 𝑃𝐴)
2 eqid 2821 . . . 4 (Base‘𝐾) = (Base‘𝐾)
3 ltrnel.a . . . 4 𝐴 = (Atoms‘𝐾)
42, 3atbase 36307 . . 3 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
5 ltrnel.h . . . 4 𝐻 = (LHyp‘𝐾)
6 ltrnel.t . . . 4 𝑇 = ((LTrn‘𝐾)‘𝑊)
72, 3, 5, 6ltrnatb 37155 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃 ∈ (Base‘𝐾)) → (𝑃𝐴 ↔ (𝐹𝑃) ∈ 𝐴))
84, 7syl3an3 1157 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃𝐴) → (𝑃𝐴 ↔ (𝐹𝑃) ∈ 𝐴))
91, 8mpbid 233 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃𝐴) → (𝐹𝑃) ∈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1079   = wceq 1528  wcel 2105  cfv 6349  Basecbs 16473  lecple 16562  Atomscatm 36281  HLchlt 36368  LHypclh 37002  LTrncltrn 37119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-map 8398  df-plt 17558  df-glb 17575  df-p0 17639  df-oposet 36194  df-ol 36196  df-oml 36197  df-covers 36284  df-ats 36285  df-hlat 36369  df-lhyp 37006  df-laut 37007  df-ldil 37122  df-ltrn 37123
This theorem is referenced by:  ltrncoat  37162  trlcnv  37183  trljat2  37185  trlat  37187  trlval3  37205  trlval4  37206  cdlemc3  37211  cdlemc5  37213  cdlemg2kq  37620  cdlemg9a  37650  cdlemg9  37652  cdlemg10bALTN  37654  cdlemg10c  37657  cdlemg10a  37658  cdlemg10  37659  cdlemg12a  37661  cdlemg12c  37663  cdlemg13a  37669  cdlemg17a  37679  cdlemg17g  37685  cdlemg18a  37696  cdlemg18b  37697  cdlemg18c  37698  trlcoabs2N  37740  trlcolem  37744  cdlemg42  37747  cdlemi  37838  cdlemk3  37851  cdlemk4  37852  cdlemk6  37855  cdlemk9  37857  cdlemk9bN  37858  cdlemk10  37861  cdlemksat  37864  cdlemk7  37866  cdlemk12  37868  cdlemkole  37871  cdlemk14  37872  cdlemk15  37873  cdlemk17  37876  cdlemk5u  37879  cdlemk6u  37880  cdlemkuat  37884  cdlemk7u  37888  cdlemk12u  37890  cdlemk37  37932  cdlemk39  37934  cdlemkfid1N  37939  cdlemk47  37967  cdlemk48  37968  cdlemk50  37970  cdlemk51  37971  cdlemk52  37972  cdlemm10N  38136
  Copyright terms: Public domain W3C validator