Metamath Proof Explorer

Theorem latjcom

Description: The join of a lattice commutes. ( chjcom analog.) (Contributed by NM, 16-Sep-2011)

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

Proof

Step	Hyp	Ref	Expression
1		latjcom.b	$⊢ B = {Base}_{K}$
2		latjcom.j	$⊢ \underset{˙}{\lor} = join (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	$⊢ meet (K) = meet (K)$
6	1 2 5	islat	$⊢ K \in Lat \leftrightarrow (K \in Poset \land (dom \underset{˙}{\lor} = B \times B \land dom meet (K) = B \times B))$
7		simprl	$⊢ (K \in Poset \land (dom \underset{˙}{\lor} = B \times B \land dom meet (K) = B \times B)) \to dom \underset{˙}{\lor} = B \times B$
8	6 7	sylbi	$⊢ K \in Lat \to dom \underset{˙}{\lor} = B \times B$
9	8	3ad2ant1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to dom \underset{˙}{\lor} = B \times B$
10	4 9	eleqtrrd	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ⟨X, Y⟩ \in dom \underset{˙}{\lor}$
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{˙}{\lor}$
15	10 14	jca	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (⟨X, Y⟩ \in dom \underset{˙}{\lor} \land ⟨Y, X⟩ \in dom \underset{˙}{\lor})$
16		latpos	$⊢ K \in Lat \to K \in Poset$
17	1 2	joincom	$⊢ ((K \in Poset \land X \in B \land Y \in B) \land (⟨X, Y⟩ \in dom \underset{˙}{\lor} \land ⟨Y, X⟩ \in dom \underset{˙}{\lor})) \to X \underset{˙}{\lor} Y = Y \underset{˙}{\lor} X$
18	16 17	syl3anl1	$⊢ ((K \in Lat \land X \in B \land Y \in B) \land (⟨X, Y⟩ \in dom \underset{˙}{\lor} \land ⟨Y, X⟩ \in dom \underset{˙}{\lor})) \to X \underset{˙}{\lor} Y = Y \underset{˙}{\lor} X$
19	15 18	mpdan	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\lor} Y = Y \underset{˙}{\lor} X$