Metamath Proof Explorer

Theorem latmmdiN

Description: Lattice meet distributes over itself. ( inindi analog.) (Contributed by NM, 8-Nov-2011) (New usage is discouraged.)

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

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	1 2	latmidm	$⊢ (K \in Lat \land X \in B) \to X \underset{˙}{\land} X = X$
7	4 5 6	syl2anc	$⊢ (K \in OL \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\land} X = X$
8	7	oveq1d	$⊢ (K \in OL \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\land} 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		simpr2	$⊢ (K \in OL \land (X \in B \land Y \in B \land Z \in B)) \to Y \in B$
11		simpr3	$⊢ (K \in OL \land (X \in B \land Y \in B \land Z \in B)) \to Z \in B$
12	1 2	latm4	$⊢ (K \in OL \land (X \in B \land X \in B) \land (Y \in B \land Z \in B)) \to (X \underset{˙}{\land} X) \underset{˙}{\land} (Y \underset{˙}{\land} Z) = (X \underset{˙}{\land} Y) \underset{˙}{\land} (X \underset{˙}{\land} Z)$
13	9 5 5 10 11 12	syl122anc	$⊢ (K \in OL \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\land} X) \underset{˙}{\land} (Y \underset{˙}{\land} Z) = (X \underset{˙}{\land} Y) \underset{˙}{\land} (X \underset{˙}{\land} Z)$
14	8 13	eqtr3d	$⊢ (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} (X \underset{˙}{\land} Z)$