Metamath Proof Explorer

Theorem latm32

Description: A rearrangement of lattice meet. ( in12 analog.) (Contributed by NM, 13-Nov-2012)

		Ref	Expression
	Hypotheses	olmass.b	$⊢ B = {Base}_{K}$
		olmass.m	$⊢ \underset{˙}{\land} = meet (K)$
	Assertion	latm32	$⊢ (K \in OL \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\land} Y) \underset{˙}{\land} Z = (X \underset{˙}{\land} Z) \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	1 2	latmcom	$⊢ (K \in Lat \land Y \in B \land Z \in B) \to Y \underset{˙}{\land} Z = Z \underset{˙}{\land} Y$
5	3 4	syl3an1	$⊢ (K \in OL \land Y \in B \land Z \in B) \to Y \underset{˙}{\land} Z = Z \underset{˙}{\land} Y$
6	5	3adant3r1	$⊢ (K \in OL \land (X \in B \land Y \in B \land Z \in B)) \to Y \underset{˙}{\land} Z = Z \underset{˙}{\land} Y$
7	6	oveq2d	$⊢ (K \in OL \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\land} (Y \underset{˙}{\land} Z) = X \underset{˙}{\land} (Z \underset{˙}{\land} Y)$
8	1 2	latmassOLD	$⊢ (K \in OL \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\land} Y) \underset{˙}{\land} Z = X \underset{˙}{\land} (Y \underset{˙}{\land} Z)$
9		simpl	$⊢ (K \in OL \land (X \in B \land Y \in B \land Z \in B)) \to K \in OL$
10		simpr1	$⊢ (K \in OL \land (X \in B \land Y \in B \land Z \in B)) \to X \in B$
11		simpr3	$⊢ (K \in OL \land (X \in B \land Y \in B \land Z \in B)) \to Z \in B$
12		simpr2	$⊢ (K \in OL \land (X \in B \land Y \in B \land Z \in B)) \to Y \in B$
13	1 2	latmassOLD	$⊢ (K \in OL \land (X \in B \land Z \in B \land Y \in B)) \to (X \underset{˙}{\land} Z) \underset{˙}{\land} Y = X \underset{˙}{\land} (Z \underset{˙}{\land} Y)$
14	9 10 11 12 13	syl13anc	$⊢ (K \in OL \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\land} Z) \underset{˙}{\land} Y = X \underset{˙}{\land} (Z \underset{˙}{\land} Y)$
15	7 8 14	3eqtr4d	$⊢ (K \in OL \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\land} Y) \underset{˙}{\land} Z = (X \underset{˙}{\land} Z) \underset{˙}{\land} Y$