Theorem chm0

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

	Ref	Expression
Assertion	chm0	|- ( A e. CH -> ( A i^i 0H ) = 0H )

Proof

Step	Hyp	Ref	Expression
1		ineq1	|- ( A = if ( A e. CH , A , 0H ) -> ( A i^i 0H ) = ( if ( A e. CH , A , 0H ) i^i 0H ) )
2	1	eqeq1d	|- ( A = if ( A e. CH , A , 0H ) -> ( ( A i^i 0H ) = 0H <-> ( if ( A e. CH , A , 0H ) i^i 0H ) = 0H ) )
3		h0elch	|- 0H e. CH
4	3	elimel	|- if ( A e. CH , A , 0H ) e. CH
5	4	chm0i	|- ( if ( A e. CH , A , 0H ) i^i 0H ) = 0H
6	2 5	dedth	|- ( A e. CH -> ( A i^i 0H ) = 0H )