Metamath Proof Explorer

Theorem latj31

Description: Swap 2nd and 3rd members of lattice join. Lemma 2.2 in MegPav2002 p. 362. (Contributed by NM, 23-Jun-2012)

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

Proof

Step	Hyp	Ref	Expression
1		latjass.b	$⊢ B = {Base}_{K}$
2		latjass.j	$⊢ \underset{˙}{\lor} = join (K)$
3		simpl	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to K \in Lat$
4		simpr3	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Z \in B$
5		simpr1	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to X \in B$
6		simpr2	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Y \in B$
7	1 2	latj12	$⊢ (K \in Lat \land (Z \in B \land X \in B \land Y \in B)) \to Z \underset{˙}{\lor} (X \underset{˙}{\lor} Y) = X \underset{˙}{\lor} (Z \underset{˙}{\lor} Y)$
8	3 4 5 6 7	syl13anc	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Z \underset{˙}{\lor} (X \underset{˙}{\lor} Y) = X \underset{˙}{\lor} (Z \underset{˙}{\lor} Y)$
9	1 2	latjcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\lor} Y \in B$
10	9	3adant3r3	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\lor} Y \in B$
11	1 2	latjcom	$⊢ (K \in Lat \land X \underset{˙}{\lor} Y \in B \land Z \in B) \to (X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z = Z \underset{˙}{\lor} (X \underset{˙}{\lor} Y)$
12	3 10 4 11	syl3anc	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z = Z \underset{˙}{\lor} (X \underset{˙}{\lor} Y)$
13	1 2	latjcl	$⊢ (K \in Lat \land Z \in B \land Y \in B) \to Z \underset{˙}{\lor} Y \in B$
14	3 4 6 13	syl3anc	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Z \underset{˙}{\lor} Y \in B$
15	1 2	latjcom	$⊢ (K \in Lat \land Z \underset{˙}{\lor} Y \in B \land X \in B) \to (Z \underset{˙}{\lor} Y) \underset{˙}{\lor} X = X \underset{˙}{\lor} (Z \underset{˙}{\lor} Y)$
16	3 14 5 15	syl3anc	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (Z \underset{˙}{\lor} Y) \underset{˙}{\lor} X = X \underset{˙}{\lor} (Z \underset{˙}{\lor} Y)$
17	8 12 16	3eqtr4d	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z = (Z \underset{˙}{\lor} Y) \underset{˙}{\lor} X$