This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem chjidm

Description: Idempotent law for Hilbert lattice join. (Contributed by NM, 26-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Assertion	chjidm	$⊢ A \in C_{ℋ} \to A \lor_{ℋ} A = A$

Step	Hyp	Ref	Expression
1		inidm	$⊢ A \cap A = A$
2	1	oveq2i	$⊢ A \lor_{ℋ} (A \cap A) = A \lor_{ℋ} A$
3		chabs1	$⊢ (A \in C_{ℋ} \land A \in C_{ℋ}) \to A \lor_{ℋ} (A \cap A) = A$
4	3	anidms	$⊢ A \in C_{ℋ} \to A \lor_{ℋ} (A \cap A) = A$
5	2 4	eqtr3id	$⊢ A \in C_{ℋ} \to A \lor_{ℋ} A = A$