Theorem chm0

Description: Meet with Hilbert lattice zero. (Contributed by NM, 14-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	chm0	⊢ ( 𝐴 ∈ Cℋ → ( 𝐴 ∩ 0ℋ ) = 0ℋ )

Proof

Step	Hyp	Ref	Expression
1		ineq1	⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( 𝐴 ∩ 0ℋ ) = ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ∩ 0ℋ ) )
2	1	eqeq1d	⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( ( 𝐴 ∩ 0ℋ ) = 0ℋ ↔ ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ∩ 0ℋ ) = 0ℋ ) )
3		h0elch	⊢ 0ℋ ∈ Cℋ
4	3	elimel	⊢ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ∈ Cℋ
5	4	chm0i	⊢ ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ∩ 0ℋ ) = 0ℋ
6	2 5	dedth	⊢ ( 𝐴 ∈ Cℋ → ( 𝐴 ∩ 0ℋ ) = 0ℋ )