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

Theorem ltrnel 37155
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‘𝐾)
ltrnel.a 𝐴 = (Atoms‘𝐾)
ltrnel.h 𝐻 = (LHyp‘𝐾)
ltrnel.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
Assertion
Ref Expression
ltrnel (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝐹𝑃) ∈ 𝐴 ∧ ¬ (𝐹𝑃) 𝑊))

Proof of Theorem ltrnel
StepHypRef Expression
1 simp3l 1193 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑃𝐴)
2 eqid 2818 . . . . . 6 (Base‘𝐾) = (Base‘𝐾)
3 ltrnel.a . . . . . 6 𝐴 = (Atoms‘𝐾)
42, 3atbase 36305 . . . . 5 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
54adantr 481 . . . 4 ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) → 𝑃 ∈ (Base‘𝐾))
6 ltrnel.h . . . . 5 𝐻 = (LHyp‘𝐾)
7 ltrnel.t . . . . 5 𝑇 = ((LTrn‘𝐾)‘𝑊)
82, 3, 6, 7ltrnatb 37153 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃 ∈ (Base‘𝐾)) → (𝑃𝐴 ↔ (𝐹𝑃) ∈ 𝐴))
95, 8syl3an3 1157 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃𝐴 ↔ (𝐹𝑃) ∈ 𝐴))
101, 9mpbid 233 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝐹𝑃) ∈ 𝐴)
11 simp3r 1194 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ¬ 𝑃 𝑊)
12 simp1 1128 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
13 simp2 1129 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐹𝑇)
141, 4syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑃 ∈ (Base‘𝐾))
15 simp1r 1190 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑊𝐻)
162, 6lhpbase 37014 . . . . . 6 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
1715, 16syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑊 ∈ (Base‘𝐾))
18 ltrnel.l . . . . . 6 = (le‘𝐾)
192, 18, 6, 7ltrnle 37145 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → (𝑃 𝑊 ↔ (𝐹𝑃) (𝐹𝑊)))
2012, 13, 14, 17, 19syl112anc 1366 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 𝑊 ↔ (𝐹𝑃) (𝐹𝑊)))
21 simp1l 1189 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐾 ∈ HL)
2221hllatd 36380 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐾 ∈ Lat)
232, 18latref 17651 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝑊 ∈ (Base‘𝐾)) → 𝑊 𝑊)
2422, 17, 23syl2anc 584 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑊 𝑊)
252, 18, 6, 7ltrnval1 37150 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑊 ∈ (Base‘𝐾) ∧ 𝑊 𝑊)) → (𝐹𝑊) = 𝑊)
2612, 13, 17, 24, 25syl112anc 1366 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝐹𝑊) = 𝑊)
2726breq2d 5069 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝐹𝑃) (𝐹𝑊) ↔ (𝐹𝑃) 𝑊))
2820, 27bitrd 280 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 𝑊 ↔ (𝐹𝑃) 𝑊))
2911, 28mtbid 325 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ¬ (𝐹𝑃) 𝑊)
3010, 29jca 512 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝐹𝑃) ∈ 𝐴 ∧ ¬ (𝐹𝑃) 𝑊))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1079   = wceq 1528  wcel 2105   class class class wbr 5057  cfv 6348  Basecbs 16471  lecple 16560  Latclat 17643  Atomscatm 36279  HLchlt 36366  LHypclh 37000  LTrncltrn 37117
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 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  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 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-map 8397  df-proset 17526  df-poset 17544  df-plt 17556  df-glb 17573  df-p0 17637  df-lat 17644  df-oposet 36192  df-ol 36194  df-oml 36195  df-covers 36282  df-ats 36283  df-atl 36314  df-cvlat 36338  df-hlat 36367  df-lhyp 37004  df-laut 37005  df-ldil 37120  df-ltrn 37121
This theorem is referenced by:  ltrncoelN  37159  ltrnmw  37167  trlcnv  37181  trljat2  37183  cdlemc3  37209  cdlemc5  37211  cdlemd9  37222  cdlemeiota  37601  cdlemg1cex  37604  cdlemg2l  37619  cdlemg2m  37620  cdlemg7fvbwN  37623  cdlemg4a  37624  cdlemg4b1  37625  cdlemg4b2  37626  cdlemg4d  37629  cdlemg4e  37630  cdlemg4  37633  cdlemg6e  37638  cdlemg7fvN  37640  cdlemg8b  37644  cdlemg8c  37645  cdlemg10bALTN  37652  cdlemg10a  37656  cdlemg12d  37662  cdlemg13a  37667  cdlemg13  37668  cdlemg14f  37669  cdlemg17b  37678  cdlemg17f  37682  cdlemg17i  37685  trlcoabs  37737  trlcoabs2N  37738  trlcolem  37742  cdlemg43  37746  cdlemg44b  37748  cdlemi2  37835  cdlemi  37836  cdlemk2  37848  cdlemk3  37849  cdlemk4  37850  cdlemk8  37854  cdlemk9  37855  cdlemk9bN  37856  cdlemki  37857  cdlemksv2  37863  cdlemk12  37866  cdlemkoatnle  37867  cdlemk12u  37888  cdlemkfid1N  37937  cdlemk47  37965  dia2dimlem1  38080  dia2dimlem2  38081  dia2dimlem3  38082  dia2dimlem6  38085  cdlemm10N  38134  dih1dimatlem0  38344  dih1dimatlem  38345
  Copyright terms: Public domain W3C validator