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

Metamath Proof Explorer

Theorem hlatjidm

Description: Idempotence of join operation. Frequently-used special case of latjcom for atoms. (Contributed by NM, 15-Jul-2012)

	Ref	Expression
Hypotheses	hlatjcom.j	$⊢ \underset{˙}{\lor} = join (K)$
	hlatjcom.a	$⊢ A = Atoms (K)$
Assertion	hlatjidm	$⊢ (K \in HL \land X \in A) \to X \underset{˙}{\lor} X = X$

Step	Hyp	Ref	Expression
1		hlatjcom.j	$⊢ \underset{˙}{\lor} = join (K)$
2		hlatjcom.a	$⊢ A = Atoms (K)$
3		hllat	$⊢ K \in HL \to K \in Lat$
4		eqid	$⊢ {Base}_{K} = {Base}_{K}$
5	4 2	atbase	$⊢ X \in A \to X \in {Base}_{K}$
6	4 1	latjidm	$⊢ (K \in Lat \land X \in {Base}_{K}) \to X \underset{˙}{\lor} X = X$
7	3 5 6	syl2an	$⊢ (K \in HL \land X \in A) \to X \underset{˙}{\lor} X = X$