cm0

Description: The zero Hilbert lattice element commutes with every element. (Contributed by NM, 16-Jun-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	cm0	$⊢ A \in C_{ℋ} \to 0_{ℋ} 𝐶_{ℋ} A$

Step	Hyp	Ref	Expression
1		h0elch	$⊢ 0_{ℋ} \in C_{ℋ}$
2	1	choccli	$⊢ ⊥ (0_{ℋ}) \in C_{ℋ}$
3		chjcl	$⊢ (⊥ (0_{ℋ}) \in C_{ℋ} \land A \in C_{ℋ}) \to ⊥ (0_{ℋ}) \lor_{ℋ} A \in C_{ℋ}$
4	2 3	mpan	$⊢ A \in C_{ℋ} \to ⊥ (0_{ℋ}) \lor_{ℋ} A \in C_{ℋ}$
5		chm0	$⊢ ⊥ (0_{ℋ}) \lor_{ℋ} A \in C_{ℋ} \to (⊥ (0_{ℋ}) \lor_{ℋ} A) \cap 0_{ℋ} = 0_{ℋ}$
6	4 5	syl	$⊢ A \in C_{ℋ} \to (⊥ (0_{ℋ}) \lor_{ℋ} A) \cap 0_{ℋ} = 0_{ℋ}$
7		chm0	$⊢ A \in C_{ℋ} \to A \cap 0_{ℋ} = 0_{ℋ}$
8	6 7	eqtr4d	$⊢ A \in C_{ℋ} \to (⊥ (0_{ℋ}) \lor_{ℋ} A) \cap 0_{ℋ} = A \cap 0_{ℋ}$
9		incom	$⊢ 0_{ℋ} \cap (⊥ (0_{ℋ}) \lor_{ℋ} A) = (⊥ (0_{ℋ}) \lor_{ℋ} A) \cap 0_{ℋ}$
10		incom	$⊢ 0_{ℋ} \cap A = A \cap 0_{ℋ}$
11	8 9 10	3eqtr4g	$⊢ A \in C_{ℋ} \to 0_{ℋ} \cap (⊥ (0_{ℋ}) \lor_{ℋ} A) = 0_{ℋ} \cap A$
12		cmbr3	$⊢ (0_{ℋ} \in C_{ℋ} \land A \in C_{ℋ}) \to (0_{ℋ} 𝐶_{ℋ} A \leftrightarrow 0_{ℋ} \cap (⊥ (0_{ℋ}) \lor_{ℋ} A) = 0_{ℋ} \cap A)$
13	1 12	mpan	$⊢ A \in C_{ℋ} \to (0_{ℋ} 𝐶_{ℋ} A \leftrightarrow 0_{ℋ} \cap (⊥ (0_{ℋ}) \lor_{ℋ} A) = 0_{ℋ} \cap A)$
14	11 13	mpbird	$⊢ A \in C_{ℋ} \to 0_{ℋ} 𝐶_{ℋ} A$

Metamath Proof Explorer