latmass

Description: Lattice meet is associative. (Contributed by Stefan O'Rear, 30-Jan-2015)

	Ref	Expression
Hypotheses	latmass.b	$⊢ B = {Base}_{K}$
	latmass.m	$⊢ \underset{˙}{\land} = meet (K)$
Assertion	latmass	$⊢ (K \in Lat \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)$

Step	Hyp	Ref	Expression
1		latmass.b	$⊢ B = {Base}_{K}$
2		latmass.m	$⊢ \underset{˙}{\land} = meet (K)$
3		eqid	$⊢ ODual (K) = ODual (K)$
4	3	odulat	$⊢ K \in Lat \to ODual (K) \in Lat$
5	3 1	odubas	$⊢ B = {Base}_{ODual (K)}$
6	3 2	odujoin	$⊢ \underset{˙}{\land} = join (ODual (K))$
7	5 6	latjass	$⊢ (ODual (K) \in Lat \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)$
8	4 7	sylan	$⊢ (K \in Lat \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)$

Metamath Proof Explorer