This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hatomic

Description: A Hilbert lattice is atomic, i.e. any nonzero element is greater than or equal to some atom. Remark in Kalmbach p. 140. Also Definition 3.4-2 in MegPav2000 p. 2345 (PDF p. 8). (Contributed by NM, 24-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion hatomic 
|- ( ( A e. CH /\ A =/= 0H ) -> E. x e. HAtoms x C_ A )

Proof

Step Hyp Ref Expression
1 neeq1 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( A =/= 0H <-> if ( A e. CH , A , 0H ) =/= 0H ) )
2 sseq2 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( x C_ A <-> x C_ if ( A e. CH , A , 0H ) ) )
3 2 rexbidv 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( E. x e. HAtoms x C_ A <-> E. x e. HAtoms x C_ if ( A e. CH , A , 0H ) ) )
4 1 3 imbi12d 
 |-  ( A = if ( A e. CH , A , 0H ) -> ( ( A =/= 0H -> E. x e. HAtoms x C_ A ) <-> ( if ( A e. CH , A , 0H ) =/= 0H -> E. x e. HAtoms x C_ if ( A e. CH , A , 0H ) ) ) )
5 h0elch 
 |-  0H e. CH
6 5 elimel 
 |-  if ( A e. CH , A , 0H ) e. CH
7 6 hatomici 
 |-  ( if ( A e. CH , A , 0H ) =/= 0H -> E. x e. HAtoms x C_ if ( A e. CH , A , 0H ) )
8 4 7 dedth 
 |-  ( A e. CH -> ( A =/= 0H -> E. x e. HAtoms x C_ A ) )
9 8 imp 
 |-  ( ( A e. CH /\ A =/= 0H ) -> E. x e. HAtoms x C_ A )