Metamath Proof Explorer

Theorem latj32

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

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

Proof

Step	Hyp	Ref	Expression
1		latjass.b	$⊢ B = {Base}_{K}$
2		latjass.j	$⊢ \underset{˙}{\lor} = join (K)$
3	1 2	latjcom	$⊢ (K \in Lat \land Y \in B \land Z \in B) \to Y \underset{˙}{\lor} Z = Z \underset{˙}{\lor} Y$
4	3	3adant3r1	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Y \underset{˙}{\lor} Z = Z \underset{˙}{\lor} Y$
5	4	oveq2d	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z) = X \underset{˙}{\lor} (Z \underset{˙}{\lor} Y)$
6	1 2	latjass	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z = X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z)$
7		simpr1	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to X \in B$
8		simpr3	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Z \in B$
9		simpr2	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Y \in B$
10	7 8 9	3jca	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \in B \land Z \in B \land Y \in B)$
11	1 2	latjass	$⊢ (K \in Lat \land (X \in B \land Z \in B \land Y \in B)) \to (X \underset{˙}{\lor} Z) \underset{˙}{\lor} Y = X \underset{˙}{\lor} (Z \underset{˙}{\lor} Y)$
12	10 11	syldan	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\lor} Z) \underset{˙}{\lor} Y = X \underset{˙}{\lor} (Z \underset{˙}{\lor} Y)$
13	5 6 12	3eqtr4d	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z = (X \underset{˙}{\lor} Z) \underset{˙}{\lor} Y$