Metamath Proof Explorer

Theorem latmcom

Description: The join of a lattice commutes. (Contributed by NM, 6-Nov-2011)

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

Proof

Step	Hyp	Ref	Expression
1		latmcom.b	$⊢ B = {Base}_{K}$
2		latmcom.m	$⊢ \underset{˙}{\land} = meet (K)$
3		opelxpi	$⊢ (X \in B \land Y \in B) \to ⟨X, Y⟩ \in (B \times B)$
4	3	3adant1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ⟨X, Y⟩ \in (B \times B)$
5		eqid	$⊢ join (K) = join (K)$
6	1 5 2	islat	$⊢ K \in Lat \leftrightarrow (K \in Poset \land (dom join (K) = B \times B \land dom \underset{˙}{\land} = B \times B))$
7		simprr	$⊢ (K \in Poset \land (dom join (K) = B \times B \land dom \underset{˙}{\land} = B \times B)) \to dom \underset{˙}{\land} = B \times B$
8	6 7	sylbi	$⊢ K \in Lat \to dom \underset{˙}{\land} = B \times B$
9	8	3ad2ant1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to dom \underset{˙}{\land} = B \times B$
10	4 9	eleqtrrd	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ⟨X, Y⟩ \in dom \underset{˙}{\land}$
11		opelxpi	$⊢ (Y \in B \land X \in B) \to ⟨Y, X⟩ \in (B \times B)$
12	11	ancoms	$⊢ (X \in B \land Y \in B) \to ⟨Y, X⟩ \in (B \times B)$
13	12	3adant1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ⟨Y, X⟩ \in (B \times B)$
14	13 9	eleqtrrd	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ⟨Y, X⟩ \in dom \underset{˙}{\land}$
15	10 14	jca	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (⟨X, Y⟩ \in dom \underset{˙}{\land} \land ⟨Y, X⟩ \in dom \underset{˙}{\land})$
16		latpos	$⊢ K \in Lat \to K \in Poset$
17	1 2	meetcom	$⊢ ((K \in Poset \land X \in B \land Y \in B) \land (⟨X, Y⟩ \in dom \underset{˙}{\land} \land ⟨Y, X⟩ \in dom \underset{˙}{\land})) \to X \underset{˙}{\land} Y = Y \underset{˙}{\land} X$
18	16 17	syl3anl1	$⊢ ((K \in Lat \land X \in B \land Y \in B) \land (⟨X, Y⟩ \in dom \underset{˙}{\land} \land ⟨Y, X⟩ \in dom \underset{˙}{\land})) \to X \underset{˙}{\land} Y = Y \underset{˙}{\land} X$
19	15 18	mpdan	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y = Y \underset{˙}{\land} X$