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 ( ( 𝐴 ∈ Cℋ ∧ 𝐴 ≠ 0ℋ ) → ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ 𝐴 )

Proof

Step Hyp Ref Expression
1 neeq1 ⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( 𝐴 ≠ 0ℋ ↔ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ≠ 0ℋ ) )
2 sseq2 ⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( 𝑥 ⊆ 𝐴 ↔ 𝑥 ⊆ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ) )
3 2 rexbidv ⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ 𝐴 ↔ ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ) )
4 1 3 imbi12d ⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( ( 𝐴 ≠ 0ℋ → ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ 𝐴 ) ↔ ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ≠ 0ℋ → ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ) ) )
5 h0elch ⊢ 0ℋ ∈ Cℋ
6 5 elimel ⊢ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ∈ Cℋ
7 6 hatomici ⊢ ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ≠ 0ℋ → ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) )
8 4 7 dedth ⊢ ( 𝐴 ∈ Cℋ → ( 𝐴 ≠ 0ℋ → ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ 𝐴 ) )
9 8 imp ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐴 ≠ 0ℋ ) → ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ 𝐴 )