latabs2

Description: Lattice absorption law. From definition of lattice in Kalmbach p. 14. ( chabs2 analog.) (Contributed by NM, 8-Nov-2011)

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

Step	Hyp	Ref	Expression
1		latabs1.b	$⊢ B = {Base}_{K}$
2		latabs1.j	$⊢ \underset{˙}{\lor} = join (K)$
3		latabs1.m	$⊢ \underset{˙}{\land} = meet (K)$
4		eqid	$⊢ \leq_{K} = \leq_{K}$
5	1 4 2	latlej1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \leq_{K} (X \underset{˙}{\lor} Y)$
6	1 2	latjcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\lor} Y \in B$
7	1 4 3	latleeqm1	$⊢ (K \in Lat \land X \in B \land X \underset{˙}{\lor} Y \in B) \to (X \leq_{K} (X \underset{˙}{\lor} Y) \leftrightarrow X \underset{˙}{\land} (X \underset{˙}{\lor} Y) = X)$
8	6 7	syld3an3	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \leq_{K} (X \underset{˙}{\lor} Y) \leftrightarrow X \underset{˙}{\land} (X \underset{˙}{\lor} Y) = X)$
9	5 8	mpbid	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} (X \underset{˙}{\lor} Y) = X$

Metamath Proof Explorer