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 34081
Description: An element covered by an atom must be zero. (atcveq0 29056 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 2621 . . . . . . . 8 (le‘𝐾) = (le‘𝐾)
3 atcvreq0.z . . . . . . . 8 0 = (0.‘𝐾)
41, 2, 3atl0le 34071 . . . . . . 7 ((𝐾 ∈ AtLat ∧ 𝑋𝐵) → 0 (le‘𝐾)𝑋)
543adant3 1079 . . . . . 6 ((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) → 0 (le‘𝐾)𝑋)
65adantr 481 . . . . 5 (((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶𝑃) → 0 (le‘𝐾)𝑋)
7 atcvreq0.a . . . . . . 7 𝐴 = (Atoms‘𝐾)
81, 7atbase 34056 . . . . . 6 (𝑃𝐴𝑃𝐵)
9 eqid 2621 . . . . . . 7 (lt‘𝐾) = (lt‘𝐾)
10 atcvreq0.c . . . . . . 7 𝐶 = ( ⋖ ‘𝐾)
111, 9, 10cvrlt 34037 . . . . . 6 (((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐵) ∧ 𝑋𝐶𝑃) → 𝑋(lt‘𝐾)𝑃)
128, 11syl3anl3 1373 . . . . 5 (((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶𝑃) → 𝑋(lt‘𝐾)𝑃)
13 atlpos 34068 . . . . . . . 8 (𝐾 ∈ AtLat → 𝐾 ∈ Poset)
14133ad2ant1 1080 . . . . . . 7 ((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) → 𝐾 ∈ Poset)
1514adantr 481 . . . . . 6 (((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶𝑃) → 𝐾 ∈ Poset)
161, 3atl0cl 34070 . . . . . . . 8 (𝐾 ∈ AtLat → 0𝐵)
17163ad2ant1 1080 . . . . . . 7 ((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) → 0𝐵)
1817adantr 481 . . . . . 6 (((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶𝑃) → 0𝐵)
1983ad2ant3 1082 . . . . . . 7 ((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) → 𝑃𝐵)
2019adantr 481 . . . . . 6 (((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶𝑃) → 𝑃𝐵)
21 simpl2 1063 . . . . . 6 (((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶𝑃) → 𝑋𝐵)
223, 10, 7atcvr0 34055 . . . . . . . 8 ((𝐾 ∈ AtLat ∧ 𝑃𝐴) → 0 𝐶𝑃)
23223adant2 1078 . . . . . . 7 ((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) → 0 𝐶𝑃)
2423adantr 481 . . . . . 6 (((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶𝑃) → 0 𝐶𝑃)
251, 2, 9, 10cvrnbtwn3 34043 . . . . . 6 ((𝐾 ∈ Poset ∧ ( 0𝐵𝑃𝐵𝑋𝐵) ∧ 0 𝐶𝑃) → (( 0 (le‘𝐾)𝑋𝑋(lt‘𝐾)𝑃) ↔ 0 = 𝑋))
2615, 18, 20, 21, 24, 25syl131anc 1336 . . . . 5 (((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶𝑃) → (( 0 (le‘𝐾)𝑋𝑋(lt‘𝐾)𝑃) ↔ 0 = 𝑋))
276, 12, 26mpbi2and 955 . . . 4 (((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶𝑃) → 0 = 𝑋)
2827eqcomd 2627 . . 3 (((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) ∧ 𝑋𝐶𝑃) → 𝑋 = 0 )
2928ex 450 . 2 ((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) → (𝑋𝐶𝑃𝑋 = 0 ))
30 breq1 4616 . . 3 (𝑋 = 0 → (𝑋𝐶𝑃0 𝐶𝑃))
3123, 30syl5ibrcom 237 . 2 ((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) → (𝑋 = 0𝑋𝐶𝑃))
3229, 31impbid 202 1 ((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴) → (𝑋𝐶𝑃𝑋 = 0 ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987   class class class wbr 4613  cfv 5847  Basecbs 15781  lecple 15869  Posetcpo 16861  ltcplt 16862  0.cp0 16958  ccvr 34029  Atomscatm 34030  AtLatcal 34031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-preset 16849  df-poset 16867  df-plt 16879  df-glb 16896  df-p0 16960  df-lat 16967  df-covers 34033  df-ats 34034  df-atl 34065
This theorem is referenced by:  atncvrN  34082  atcvrj0  34194  1cvrjat  34241
  Copyright terms: Public domain W3C validator