chm0

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

		Ref	Expression
	Assertion	chm0	$⊢ A \in C_{ℋ} \to A \cap 0_{ℋ} = 0_{ℋ}$

Step	Hyp	Ref	Expression
1		ineq1	$⊢ A = if (A \in C_{ℋ}, A, 0_{ℋ}) \to A \cap 0_{ℋ} = if (A \in C_{ℋ}, A, 0_{ℋ}) \cap 0_{ℋ}$
2	1	eqeq1d	$⊢ A = if (A \in C_{ℋ}, A, 0_{ℋ}) \to (A \cap 0_{ℋ} = 0_{ℋ} \leftrightarrow if (A \in C_{ℋ}, A, 0_{ℋ}) \cap 0_{ℋ} = 0_{ℋ})$
3		h0elch	$⊢ 0_{ℋ} \in C_{ℋ}$
4	3	elimel	$⊢ if (A \in C_{ℋ}, A, 0_{ℋ}) \in C_{ℋ}$
5	4	chm0i	$⊢ if (A \in C_{ℋ}, A, 0_{ℋ}) \cap 0_{ℋ} = 0_{ℋ}$
6	2 5	dedth	$⊢ A \in C_{ℋ} \to A \cap 0_{ℋ} = 0_{ℋ}$

Metamath Proof Explorer