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

Theorem lhple 37357
 Description: Property of a lattice element under a co-atom. (Contributed by NM, 28-Feb-2014.)
Hypotheses
Ref Expression
lhple.b 𝐵 = (Base‘𝐾)
lhple.l = (le‘𝐾)
lhple.j = (join‘𝐾)
lhple.m = (meet‘𝐾)
lhple.a 𝐴 = (Atoms‘𝐾)
lhple.h 𝐻 = (LHyp‘𝐾)
Assertion
Ref Expression
lhple (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑋𝐵𝑋 𝑊)) → ((𝑃 𝑋) 𝑊) = 𝑋)

Proof of Theorem lhple
StepHypRef Expression
1 simp1l 1194 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑋𝐵𝑋 𝑊)) → 𝐾 ∈ HL)
21hllatd 36679 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑋𝐵𝑋 𝑊)) → 𝐾 ∈ Lat)
3 simp2l 1196 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑋𝐵𝑋 𝑊)) → 𝑃𝐴)
4 lhple.b . . . . . 6 𝐵 = (Base‘𝐾)
5 lhple.a . . . . . 6 𝐴 = (Atoms‘𝐾)
64, 5atbase 36604 . . . . 5 (𝑃𝐴𝑃𝐵)
73, 6syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑋𝐵𝑋 𝑊)) → 𝑃𝐵)
8 simp3l 1198 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑋𝐵𝑋 𝑊)) → 𝑋𝐵)
9 lhple.j . . . . 5 = (join‘𝐾)
104, 9latjcom 17664 . . . 4 ((𝐾 ∈ Lat ∧ 𝑃𝐵𝑋𝐵) → (𝑃 𝑋) = (𝑋 𝑃))
112, 7, 8, 10syl3anc 1368 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑋𝐵𝑋 𝑊)) → (𝑃 𝑋) = (𝑋 𝑃))
1211oveq1d 7151 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑋𝐵𝑋 𝑊)) → ((𝑃 𝑋) 𝑊) = ((𝑋 𝑃) 𝑊))
13 simp1 1133 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑋𝐵𝑋 𝑊)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
14 simp3r 1199 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑋𝐵𝑋 𝑊)) → 𝑋 𝑊)
15 lhple.l . . . 4 = (le‘𝐾)
16 lhple.m . . . 4 = (meet‘𝐾)
17 lhple.h . . . 4 𝐻 = (LHyp‘𝐾)
184, 15, 9, 16, 17lhpmod6i1 37354 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑃𝐵) ∧ 𝑋 𝑊) → (𝑋 (𝑃 𝑊)) = ((𝑋 𝑃) 𝑊))
1913, 8, 7, 14, 18syl121anc 1372 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑋𝐵𝑋 𝑊)) → (𝑋 (𝑃 𝑊)) = ((𝑋 𝑃) 𝑊))
20 eqid 2798 . . . . . 6 (0.‘𝐾) = (0.‘𝐾)
2115, 16, 20, 5, 17lhpmat 37345 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 𝑊) = (0.‘𝐾))
22213adant3 1129 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑋𝐵𝑋 𝑊)) → (𝑃 𝑊) = (0.‘𝐾))
2322oveq2d 7152 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑋𝐵𝑋 𝑊)) → (𝑋 (𝑃 𝑊)) = (𝑋 (0.‘𝐾)))
24 hlol 36676 . . . . 5 (𝐾 ∈ HL → 𝐾 ∈ OL)
251, 24syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑋𝐵𝑋 𝑊)) → 𝐾 ∈ OL)
264, 9, 20olj01 36540 . . . 4 ((𝐾 ∈ OL ∧ 𝑋𝐵) → (𝑋 (0.‘𝐾)) = 𝑋)
2725, 8, 26syl2anc 587 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑋𝐵𝑋 𝑊)) → (𝑋 (0.‘𝐾)) = 𝑋)
2823, 27eqtrd 2833 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑋𝐵𝑋 𝑊)) → (𝑋 (𝑃 𝑊)) = 𝑋)
2912, 19, 283eqtr2d 2839 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑋𝐵𝑋 𝑊)) → ((𝑃 𝑋) 𝑊) = 𝑋)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   class class class wbr 5031  ‘cfv 6325  (class class class)co 7136  Basecbs 16478  lecple 16567  joincjn 17549  meetcmee 17550  0.cp0 17642  Latclat 17650  OLcol 36489  Atomscatm 36578  HLchlt 36665  LHypclh 37299 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7444 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-iun 4884  df-iin 4885  df-br 5032  df-opab 5094  df-mpt 5112  df-id 5426  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-f1 6330  df-fo 6331  df-f1o 6332  df-fv 6333  df-riota 7094  df-ov 7139  df-oprab 7140  df-mpo 7141  df-1st 7674  df-2nd 7675  df-proset 17533  df-poset 17551  df-plt 17563  df-lub 17579  df-glb 17580  df-join 17581  df-meet 17582  df-p0 17644  df-p1 17645  df-lat 17651  df-clat 17713  df-oposet 36491  df-ol 36493  df-oml 36494  df-covers 36581  df-ats 36582  df-atl 36613  df-cvlat 36637  df-hlat 36666  df-psubsp 36818  df-pmap 36819  df-padd 37111  df-lhyp 37303 This theorem is referenced by:  lhpat4N  37359  cdlemn2  38510  dihord5apre  38577
 Copyright terms: Public domain W3C validator