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 35920
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 1241 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑃𝐴)
2 eqid 2752 . . . . . 6 (Base‘𝐾) = (Base‘𝐾)
3 ltrnel.a . . . . . 6 𝐴 = (Atoms‘𝐾)
42, 3atbase 35071 . . . . 5 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
54adantr 472 . . . 4 ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) → 𝑃 ∈ (Base‘𝐾))
6 ltrnel.h . . . . 5 𝐻 = (LHyp‘𝐾)
7 ltrnel.t . . . . 5 𝑇 = ((LTrn‘𝐾)‘𝑊)
82, 3, 6, 7ltrnatb 35918 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃 ∈ (Base‘𝐾)) → (𝑃𝐴 ↔ (𝐹𝑃) ∈ 𝐴))
95, 8syl3an3 1168 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃𝐴 ↔ (𝐹𝑃) ∈ 𝐴))
101, 9mpbid 222 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝐹𝑃) ∈ 𝐴)
11 simp3r 1242 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ¬ 𝑃 𝑊)
12 simp1 1130 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
13 simp2 1131 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐹𝑇)
141, 4syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑃 ∈ (Base‘𝐾))
15 simp1r 1238 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑊𝐻)
162, 6lhpbase 35779 . . . . . 6 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
1715, 16syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑊 ∈ (Base‘𝐾))
18 ltrnel.l . . . . . 6 = (le‘𝐾)
192, 18, 6, 7ltrnle 35910 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → (𝑃 𝑊 ↔ (𝐹𝑃) (𝐹𝑊)))
2012, 13, 14, 17, 19syl112anc 1477 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 𝑊 ↔ (𝐹𝑃) (𝐹𝑊)))
21 simp1l 1237 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐾 ∈ HL)
22 hllat 35145 . . . . . . . 8 (𝐾 ∈ HL → 𝐾 ∈ Lat)
2321, 22syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐾 ∈ Lat)
242, 18latref 17246 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝑊 ∈ (Base‘𝐾)) → 𝑊 𝑊)
2523, 17, 24syl2anc 696 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑊 𝑊)
262, 18, 6, 7ltrnval1 35915 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑊 ∈ (Base‘𝐾) ∧ 𝑊 𝑊)) → (𝐹𝑊) = 𝑊)
2712, 13, 17, 25, 26syl112anc 1477 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝐹𝑊) = 𝑊)
2827breq2d 4808 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝐹𝑃) (𝐹𝑊) ↔ (𝐹𝑃) 𝑊))
2920, 28bitrd 268 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 𝑊 ↔ (𝐹𝑃) 𝑊))
3011, 29mtbid 313 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ¬ (𝐹𝑃) 𝑊)
3110, 30jca 555 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝐹𝑃) ∈ 𝐴 ∧ ¬ (𝐹𝑃) 𝑊))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1072   = wceq 1624  wcel 2131   class class class wbr 4796  cfv 6041  Basecbs 16051  lecple 16142  Latclat 17238  Atomscatm 35045  HLchlt 35132  LHypclh 35765  LTrncltrn 35882
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-rep 4915  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-ral 3047  df-rex 3048  df-reu 3049  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-iun 4666  df-br 4797  df-opab 4857  df-mpt 4874  df-id 5166  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-f1 6046  df-fo 6047  df-f1o 6048  df-fv 6049  df-riota 6766  df-ov 6808  df-oprab 6809  df-mpt2 6810  df-map 8017  df-preset 17121  df-poset 17139  df-plt 17151  df-glb 17168  df-p0 17232  df-lat 17239  df-oposet 34958  df-ol 34960  df-oml 34961  df-covers 35048  df-ats 35049  df-atl 35080  df-cvlat 35104  df-hlat 35133  df-lhyp 35769  df-laut 35770  df-ldil 35885  df-ltrn 35886
This theorem is referenced by:  ltrncoelN  35924  ltrnmw  35932  trlcnv  35947  trljat2  35949  cdlemc3  35975  cdlemc5  35977  cdlemd9  35988  cdlemeiota  36367  cdlemg1cex  36370  cdlemg2l  36385  cdlemg2m  36386  cdlemg7fvbwN  36389  cdlemg4a  36390  cdlemg4b1  36391  cdlemg4b2  36392  cdlemg4d  36395  cdlemg4e  36396  cdlemg4  36399  cdlemg6e  36404  cdlemg7fvN  36406  cdlemg8b  36410  cdlemg8c  36411  cdlemg10bALTN  36418  cdlemg10a  36422  cdlemg12d  36428  cdlemg13a  36433  cdlemg13  36434  cdlemg14f  36435  cdlemg17b  36444  cdlemg17f  36448  cdlemg17i  36451  trlcoabs  36503  trlcoabs2N  36504  trlcolem  36508  cdlemg43  36512  cdlemg44b  36514  cdlemi2  36601  cdlemi  36602  cdlemk2  36614  cdlemk3  36615  cdlemk4  36616  cdlemk8  36620  cdlemk9  36621  cdlemk9bN  36622  cdlemki  36623  cdlemksv2  36629  cdlemk12  36632  cdlemkoatnle  36633  cdlemk12u  36654  cdlemkfid1N  36703  cdlemk47  36731  dia2dimlem1  36847  dia2dimlem2  36848  dia2dimlem3  36849  dia2dimlem6  36852  cdlemm10N  36901  dih1dimatlem0  37111  dih1dimatlem  37112
  Copyright terms: Public domain W3C validator