HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  ela Structured version   Visualization version   GIF version

Theorem ela 28383
Description: Atoms in a Hilbert lattice are the elements that cover the zero subspace. Definition of atom in [Kalmbach] p. 15. (Contributed by NM, 9-Jun-2004.) (New usage is discouraged.)
Assertion
Ref Expression
ela (𝐴 ∈ HAtoms ↔ (𝐴C ∧ 0 𝐴))

Proof of Theorem ela
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 breq2 4576 . 2 (𝑥 = 𝐴 → (0 𝑥 ↔ 0 𝐴))
2 df-at 28382 . 2 HAtoms = {𝑥C ∣ 0 𝑥}
31, 2elrab2 3327 1 (𝐴 ∈ HAtoms ↔ (𝐴C ∧ 0 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wb 194  wa 382  wcel 1975   class class class wbr 4572   C cch 26971  0c0h 26977   ccv 27006  HAtomscat 27007
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2227  ax-ext 2584
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2591  df-cleq 2597  df-clel 2600  df-nfc 2734  df-rab 2899  df-v 3169  df-dif 3537  df-un 3539  df-in 3541  df-ss 3548  df-nul 3869  df-if 4031  df-sn 4120  df-pr 4122  df-op 4126  df-br 4573  df-at 28382
This theorem is referenced by:  elat2  28384  elatcv0  28385  atcv0  28386
  Copyright terms: Public domain W3C validator