latjidm

Description: Lattice join is idempotent. Analogue of unidm . (Contributed by NM, 8-Oct-2011)

	Ref	Expression
Hypotheses	latjidm.b	$⊢ B = {Base}_{K}$
	latjidm.j	$⊢ \underset{˙}{\lor} = join (K)$
Assertion	latjidm	$⊢ (K \in Lat \land X \in B) \to X \underset{˙}{\lor} X = X$

Step	Hyp	Ref	Expression
1		latjidm.b	$⊢ B = {Base}_{K}$
2		latjidm.j	$⊢ \underset{˙}{\lor} = join (K)$
3		eqid	$⊢ \leq_{K} = \leq_{K}$
4		simpl	$⊢ (K \in Lat \land X \in B) \to K \in Lat$
5	1 2	latjcl	$⊢ (K \in Lat \land X \in B \land X \in B) \to X \underset{˙}{\lor} X \in B$
6	5	3anidm23	$⊢ (K \in Lat \land X \in B) \to X \underset{˙}{\lor} X \in B$
7		simpr	$⊢ (K \in Lat \land X \in B) \to X \in B$
8	1 3	latref	$⊢ (K \in Lat \land X \in B) \to X \leq_{K} X$
9	1 3 2	latjle12	$⊢ (K \in Lat \land (X \in B \land X \in B \land X \in B)) \to ((X \leq_{K} X \land X \leq_{K} X) \leftrightarrow (X \underset{˙}{\lor} X) \leq_{K} X)$
10	4 7 7 7 9	syl13anc	$⊢ (K \in Lat \land X \in B) \to ((X \leq_{K} X \land X \leq_{K} X) \leftrightarrow (X \underset{˙}{\lor} X) \leq_{K} X)$
11	8 8 10	mpbi2and	$⊢ (K \in Lat \land X \in B) \to (X \underset{˙}{\lor} X) \leq_{K} X$
12	1 3 2	latlej1	$⊢ (K \in Lat \land X \in B \land X \in B) \to X \leq_{K} (X \underset{˙}{\lor} X)$
13	12	3anidm23	$⊢ (K \in Lat \land X \in B) \to X \leq_{K} (X \underset{˙}{\lor} X)$
14	1 3 4 6 7 11 13	latasymd	$⊢ (K \in Lat \land X \in B) \to X \underset{˙}{\lor} X = X$

Metamath Proof Explorer