Metamath Proof Explorer

Theorem latmrot

Description: Rotate lattice meet of 3 classes. (Contributed by NM, 9-Oct-2012)

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

Proof

Step	Hyp	Ref	Expression
1		olmass.b	$⊢ B = {Base}_{K}$
2		olmass.m	$⊢ \underset{˙}{\land} = meet (K)$
3		ollat	$⊢ K \in OL \to K \in Lat$
4	3	adantr	$⊢ (K \in OL \land (X \in B \land Y \in B \land Z \in B)) \to K \in Lat$
5		simpr1	$⊢ (K \in OL \land (X \in B \land Y \in B \land Z \in B)) \to X \in B$
6		simpr2	$⊢ (K \in OL \land (X \in B \land Y \in B \land Z \in B)) \to Y \in B$
7	1 2	latmcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y \in B$
8	4 5 6 7	syl3anc	$⊢ (K \in OL \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\land} Y \in B$
9		simpr3	$⊢ (K \in OL \land (X \in B \land Y \in B \land Z \in B)) \to Z \in B$
10	1 2	latmcom	$⊢ (K \in Lat \land X \underset{˙}{\land} Y \in B \land Z \in B) \to (X \underset{˙}{\land} Y) \underset{˙}{\land} Z = Z \underset{˙}{\land} (X \underset{˙}{\land} Y)$
11	4 8 9 10	syl3anc	$⊢ (K \in OL \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\land} Y) \underset{˙}{\land} Z = Z \underset{˙}{\land} (X \underset{˙}{\land} Y)$
12		simpl	$⊢ (K \in OL \land (X \in B \land Y \in B \land Z \in B)) \to K \in OL$
13	1 2	latmassOLD	$⊢ (K \in OL \land (Z \in B \land X \in B \land Y \in B)) \to (Z \underset{˙}{\land} X) \underset{˙}{\land} Y = Z \underset{˙}{\land} (X \underset{˙}{\land} Y)$
14	12 9 5 6 13	syl13anc	$⊢ (K \in OL \land (X \in B \land Y \in B \land Z \in B)) \to (Z \underset{˙}{\land} X) \underset{˙}{\land} Y = Z \underset{˙}{\land} (X \underset{˙}{\land} Y)$
15	11 14	eqtr4d	$⊢ (K \in OL \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\land} Y) \underset{˙}{\land} Z = (Z \underset{˙}{\land} X) \underset{˙}{\land} Y$