latm4

Description: Rearrangement of lattice meet of 4 classes. ( in4 analog.) (Contributed by NM, 8-Nov-2011)

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

Proof

Step	Hyp	Ref	Expression
1		olmass.b	$⊢ B = {Base}_{K}$
2		olmass.m	$⊢ \underset{˙}{\land} = meet (K)$
3		simp1	$⊢ (K \in OL \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to K \in OL$
4		simp2r	$⊢ (K \in OL \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to Y \in B$
5		simp3l	$⊢ (K \in OL \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to Z \in B$
6		simp3r	$⊢ (K \in OL \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to W \in B$
7	1 2	latm12	$⊢ (K \in OL \land (Y \in B \land Z \in B \land W \in B)) \to Y \underset{˙}{\land} (Z \underset{˙}{\land} W) = Z \underset{˙}{\land} (Y \underset{˙}{\land} W)$
8	3 4 5 6 7	syl13anc	$⊢ (K \in OL \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to Y \underset{˙}{\land} (Z \underset{˙}{\land} W) = Z \underset{˙}{\land} (Y \underset{˙}{\land} W)$
9	8	oveq2d	$⊢ (K \in OL \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to X \underset{˙}{\land} (Y \underset{˙}{\land} (Z \underset{˙}{\land} W)) = X \underset{˙}{\land} (Z \underset{˙}{\land} (Y \underset{˙}{\land} W))$
10		simp2l	$⊢ (K \in OL \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to X \in B$
11		ollat	$⊢ K \in OL \to K \in Lat$
12	11	3ad2ant1	$⊢ (K \in OL \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to K \in Lat$
13	1 2	latmcl	$⊢ (K \in Lat \land Z \in B \land W \in B) \to Z \underset{˙}{\land} W \in B$
14	12 5 6 13	syl3anc	$⊢ (K \in OL \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to Z \underset{˙}{\land} W \in B$
15	1 2	latmassOLD	$⊢ (K \in OL \land (X \in B \land Y \in B \land Z \underset{˙}{\land} W \in B)) \to (X \underset{˙}{\land} Y) \underset{˙}{\land} (Z \underset{˙}{\land} W) = X \underset{˙}{\land} (Y \underset{˙}{\land} (Z \underset{˙}{\land} W))$
16	3 10 4 14 15	syl13anc	$⊢ (K \in OL \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to (X \underset{˙}{\land} Y) \underset{˙}{\land} (Z \underset{˙}{\land} W) = X \underset{˙}{\land} (Y \underset{˙}{\land} (Z \underset{˙}{\land} W))$
17	1 2	latmcl	$⊢ (K \in Lat \land Y \in B \land W \in B) \to Y \underset{˙}{\land} W \in B$
18	12 4 6 17	syl3anc	$⊢ (K \in OL \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to Y \underset{˙}{\land} W \in B$
19	1 2	latmassOLD	$⊢ (K \in OL \land (X \in B \land Z \in B \land Y \underset{˙}{\land} W \in B)) \to (X \underset{˙}{\land} Z) \underset{˙}{\land} (Y \underset{˙}{\land} W) = X \underset{˙}{\land} (Z \underset{˙}{\land} (Y \underset{˙}{\land} W))$
20	3 10 5 18 19	syl13anc	$⊢ (K \in OL \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to (X \underset{˙}{\land} Z) \underset{˙}{\land} (Y \underset{˙}{\land} W) = X \underset{˙}{\land} (Z \underset{˙}{\land} (Y \underset{˙}{\land} W))$
21	9 16 20	3eqtr4d	$⊢ (K \in OL \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to (X \underset{˙}{\land} Y) \underset{˙}{\land} (Z \underset{˙}{\land} W) = (X \underset{˙}{\land} Z) \underset{˙}{\land} (Y \underset{˙}{\land} W)$

Metamath Proof Explorer

Theorem latm4

Proof