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

Theorem ltrnatb 40139
Description: The lattice translation of an atom is an atom. (Contributed by NM, 20-May-2012.)
Hypotheses
Ref Expression
ltrnatb.b 𝐵 = (Base‘𝐾)
ltrnatb.a 𝐴 = (Atoms‘𝐾)
ltrnatb.h 𝐻 = (LHyp‘𝐾)
ltrnatb.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
Assertion
Ref Expression
ltrnatb (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃𝐵) → (𝑃𝐴 ↔ (𝐹𝑃) ∈ 𝐴))

Proof of Theorem ltrnatb
StepHypRef Expression
1 simp3 1139 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃𝐵) → 𝑃𝐵)
2 ltrnatb.b . . . . 5 𝐵 = (Base‘𝐾)
3 ltrnatb.h . . . . 5 𝐻 = (LHyp‘𝐾)
4 ltrnatb.t . . . . 5 𝑇 = ((LTrn‘𝐾)‘𝑊)
52, 3, 4ltrncl 40127 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃𝐵) → (𝐹𝑃) ∈ 𝐵)
61, 52thd 265 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃𝐵) → (𝑃𝐵 ↔ (𝐹𝑃) ∈ 𝐵))
7 simp1 1137 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃𝐵) → (𝐾 ∈ HL ∧ 𝑊𝐻))
8 simp2 1138 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃𝐵) → 𝐹𝑇)
9 simp1l 1198 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃𝐵) → 𝐾 ∈ HL)
10 hlop 39363 . . . . . 6 (𝐾 ∈ HL → 𝐾 ∈ OP)
11 eqid 2737 . . . . . . 7 (0.‘𝐾) = (0.‘𝐾)
122, 11op0cl 39185 . . . . . 6 (𝐾 ∈ OP → (0.‘𝐾) ∈ 𝐵)
139, 10, 123syl 18 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃𝐵) → (0.‘𝐾) ∈ 𝐵)
14 eqid 2737 . . . . . 6 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
152, 14, 3, 4ltrncvr 40135 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ ((0.‘𝐾) ∈ 𝐵𝑃𝐵)) → ((0.‘𝐾)( ⋖ ‘𝐾)𝑃 ↔ (𝐹‘(0.‘𝐾))( ⋖ ‘𝐾)(𝐹𝑃)))
167, 8, 13, 1, 15syl112anc 1376 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃𝐵) → ((0.‘𝐾)( ⋖ ‘𝐾)𝑃 ↔ (𝐹‘(0.‘𝐾))( ⋖ ‘𝐾)(𝐹𝑃)))
179, 10syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃𝐵) → 𝐾 ∈ OP)
18 simp1r 1199 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃𝐵) → 𝑊𝐻)
192, 3lhpbase 40000 . . . . . . . 8 (𝑊𝐻𝑊𝐵)
2018, 19syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃𝐵) → 𝑊𝐵)
21 eqid 2737 . . . . . . . 8 (le‘𝐾) = (le‘𝐾)
222, 21, 11op0le 39187 . . . . . . 7 ((𝐾 ∈ OP ∧ 𝑊𝐵) → (0.‘𝐾)(le‘𝐾)𝑊)
2317, 20, 22syl2anc 584 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃𝐵) → (0.‘𝐾)(le‘𝐾)𝑊)
242, 21, 3, 4ltrnval1 40136 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ ((0.‘𝐾) ∈ 𝐵 ∧ (0.‘𝐾)(le‘𝐾)𝑊)) → (𝐹‘(0.‘𝐾)) = (0.‘𝐾))
257, 8, 13, 23, 24syl112anc 1376 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃𝐵) → (𝐹‘(0.‘𝐾)) = (0.‘𝐾))
2625breq1d 5153 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃𝐵) → ((𝐹‘(0.‘𝐾))( ⋖ ‘𝐾)(𝐹𝑃) ↔ (0.‘𝐾)( ⋖ ‘𝐾)(𝐹𝑃)))
2716, 26bitrd 279 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃𝐵) → ((0.‘𝐾)( ⋖ ‘𝐾)𝑃 ↔ (0.‘𝐾)( ⋖ ‘𝐾)(𝐹𝑃)))
286, 27anbi12d 632 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃𝐵) → ((𝑃𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑃) ↔ ((𝐹𝑃) ∈ 𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)(𝐹𝑃))))
29 ltrnatb.a . . . 4 𝐴 = (Atoms‘𝐾)
302, 11, 14, 29isat 39287 . . 3 (𝐾 ∈ HL → (𝑃𝐴 ↔ (𝑃𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑃)))
319, 30syl 17 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃𝐵) → (𝑃𝐴 ↔ (𝑃𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑃)))
322, 11, 14, 29isat 39287 . . 3 (𝐾 ∈ HL → ((𝐹𝑃) ∈ 𝐴 ↔ ((𝐹𝑃) ∈ 𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)(𝐹𝑃))))
339, 32syl 17 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃𝐵) → ((𝐹𝑃) ∈ 𝐴 ↔ ((𝐹𝑃) ∈ 𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)(𝐹𝑃))))
3428, 31, 333bitr4d 311 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃𝐵) → (𝑃𝐴 ↔ (𝐹𝑃) ∈ 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wcel 2108   class class class wbr 5143  cfv 6561  Basecbs 17247  lecple 17304  0.cp0 18468  OPcops 39173  ccvr 39263  Atomscatm 39264  HLchlt 39351  LHypclh 39986  LTrncltrn 40103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-map 8868  df-plt 18375  df-glb 18392  df-p0 18470  df-oposet 39177  df-ol 39179  df-oml 39180  df-covers 39267  df-ats 39268  df-hlat 39352  df-lhyp 39990  df-laut 39991  df-ldil 40106  df-ltrn 40107
This theorem is referenced by:  ltrncnvatb  40140  ltrnel  40141  ltrnat  40142
  Copyright terms: Public domain W3C validator