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

Theorem atcvreq0 35928
Description: An element covered by an atom must be zero. (atcveq0 29922 analog.) (Contributed by NM, 4-Nov-2011.)
Hypotheses
Ref Expression
atcvreq0.b 𝐵 = (Base‘𝐾)
atcvreq0.l = (le‘𝐾)
atcvreq0.z 0 = (0.‘𝐾)
atcvreq0.c 𝐶 = ( ⋖ ‘𝐾)
atcvreq0.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
atcvreq0 ((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) → (𝑋𝐶𝑃𝑋 = 0 ))

Proof of Theorem atcvreq0
StepHypRef Expression
1 atcvreq0.b . . . . . . . 8 𝐵 = (Base‘𝐾)
2 eqid 2773 . . . . . . . 8 (le‘𝐾) = (le‘𝐾)
3 atcvreq0.z . . . . . . . 8 0 = (0.‘𝐾)
41, 2, 3atl0le 35918 . . . . . . 7 ((𝐾 ∈ AtLat ∧ 𝑋𝐵) → 0 (le‘𝐾)𝑋)
543adant3 1113 . . . . . 6 ((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) → 0 (le‘𝐾)𝑋)
65adantr 473 . . . . 5 (((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶𝑃) → 0 (le‘𝐾)𝑋)
7 atcvreq0.a . . . . . . 7 𝐴 = (Atoms‘𝐾)
81, 7atbase 35903 . . . . . 6 (𝑃𝐴𝑃𝐵)
9 eqid 2773 . . . . . . 7 (lt‘𝐾) = (lt‘𝐾)
10 atcvreq0.c . . . . . . 7 𝐶 = ( ⋖ ‘𝐾)
111, 9, 10cvrlt 35884 . . . . . 6 (((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐵) ∧ 𝑋𝐶𝑃) → 𝑋(lt‘𝐾)𝑃)
128, 11syl3anl3 1395 . . . . 5 (((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶𝑃) → 𝑋(lt‘𝐾)𝑃)
13 atlpos 35915 . . . . . . . 8 (𝐾 ∈ AtLat → 𝐾 ∈ Poset)
14133ad2ant1 1114 . . . . . . 7 ((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) → 𝐾 ∈ Poset)
1514adantr 473 . . . . . 6 (((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶𝑃) → 𝐾 ∈ Poset)
161, 3atl0cl 35917 . . . . . . . 8 (𝐾 ∈ AtLat → 0𝐵)
17163ad2ant1 1114 . . . . . . 7 ((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) → 0𝐵)
1817adantr 473 . . . . . 6 (((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶𝑃) → 0𝐵)
1983ad2ant3 1116 . . . . . . 7 ((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) → 𝑃𝐵)
2019adantr 473 . . . . . 6 (((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶𝑃) → 𝑃𝐵)
21 simpl2 1173 . . . . . 6 (((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶𝑃) → 𝑋𝐵)
223, 10, 7atcvr0 35902 . . . . . . . 8 ((𝐾 ∈ AtLat ∧ 𝑃𝐴) → 0 𝐶𝑃)
23223adant2 1112 . . . . . . 7 ((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) → 0 𝐶𝑃)
2423adantr 473 . . . . . 6 (((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶𝑃) → 0 𝐶𝑃)
251, 2, 9, 10cvrnbtwn3 35890 . . . . . 6 ((𝐾 ∈ Poset ∧ ( 0𝐵𝑃𝐵𝑋𝐵) ∧ 0 𝐶𝑃) → (( 0 (le‘𝐾)𝑋𝑋(lt‘𝐾)𝑃) ↔ 0 = 𝑋))
2615, 18, 20, 21, 24, 25syl131anc 1364 . . . . 5 (((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶𝑃) → (( 0 (le‘𝐾)𝑋𝑋(lt‘𝐾)𝑃) ↔ 0 = 𝑋))
276, 12, 26mpbi2and 700 . . . 4 (((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶𝑃) → 0 = 𝑋)
2827eqcomd 2779 . . 3 (((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶𝑃) → 𝑋 = 0 )
2928ex 405 . 2 ((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) → (𝑋𝐶𝑃𝑋 = 0 ))
30 breq1 4929 . . 3 (𝑋 = 0 → (𝑋𝐶𝑃0 𝐶𝑃))
3123, 30syl5ibrcom 239 . 2 ((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) → (𝑋 = 0𝑋𝐶𝑃))
3229, 31impbid 204 1 ((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) → (𝑋𝐶𝑃𝑋 = 0 ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387  w3a 1069   = wceq 1508  wcel 2051   class class class wbr 4926  cfv 6186  Basecbs 16338  lecple 16427  Posetcpo 17421  ltcplt 17422  0.cp0 17518  ccvr 35876  Atomscatm 35877  AtLatcal 35878
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-rep 5046  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-ral 3088  df-rex 3089  df-reu 3090  df-rab 3092  df-v 3412  df-sbc 3677  df-csb 3782  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-op 4443  df-uni 4710  df-iun 4791  df-br 4927  df-opab 4989  df-mpt 5006  df-id 5309  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-riota 6936  df-proset 17409  df-poset 17427  df-plt 17439  df-glb 17456  df-p0 17520  df-lat 17527  df-covers 35880  df-ats 35881  df-atl 35912
This theorem is referenced by:  atncvrN  35929  atcvrj0  36042  1cvrjat  36089
  Copyright terms: Public domain W3C validator