latmlem12

Description: Add join to both sides of a lattice ordering. ( ss2in analog.) (Contributed by NM, 10-Nov-2011)

	Ref	Expression
Hypotheses	latmle.b	$⊢ B = {Base}_{K}$
	latmle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	latmle.m	$⊢ \underset{˙}{\land} = meet (K)$
Assertion	latmlem12	$⊢ (K \in Lat \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to ((X \underset{˙}{\leq} Y \land Z \underset{˙}{\leq} W) \to (X \underset{˙}{\land} Z) \underset{˙}{\leq} (Y \underset{˙}{\land} W))$

Proof

Step	Hyp	Ref	Expression
1		latmle.b	$⊢ B = {Base}_{K}$
2		latmle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		latmle.m	$⊢ \underset{˙}{\land} = meet (K)$
4		simp1	$⊢ (K \in Lat \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to K \in Lat$
5		simp2l	$⊢ (K \in Lat \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to X \in B$
6		simp2r	$⊢ (K \in Lat \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to Y \in B$
7		simp3l	$⊢ (K \in Lat \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to Z \in B$
8	1 2 3	latmlem1	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\leq} Y \to (X \underset{˙}{\land} Z) \underset{˙}{\leq} (Y \underset{˙}{\land} Z))$
9	4 5 6 7 8	syl13anc	$⊢ (K \in Lat \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to (X \underset{˙}{\leq} Y \to (X \underset{˙}{\land} Z) \underset{˙}{\leq} (Y \underset{˙}{\land} Z))$
10		simp3r	$⊢ (K \in Lat \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to W \in B$
11	1 2 3	latmlem2	$⊢ (K \in Lat \land (Z \in B \land W \in B \land Y \in B)) \to (Z \underset{˙}{\leq} W \to (Y \underset{˙}{\land} Z) \underset{˙}{\leq} (Y \underset{˙}{\land} W))$
12	4 7 10 6 11	syl13anc	$⊢ (K \in Lat \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to (Z \underset{˙}{\leq} W \to (Y \underset{˙}{\land} Z) \underset{˙}{\leq} (Y \underset{˙}{\land} W))$
13	1 3	latmcl	$⊢ (K \in Lat \land X \in B \land Z \in B) \to X \underset{˙}{\land} Z \in B$
14	4 5 7 13	syl3anc	$⊢ (K \in Lat \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to X \underset{˙}{\land} Z \in B$
15	1 3	latmcl	$⊢ (K \in Lat \land Y \in B \land Z \in B) \to Y \underset{˙}{\land} Z \in B$
16	4 6 7 15	syl3anc	$⊢ (K \in Lat \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to Y \underset{˙}{\land} Z \in B$
17	1 3	latmcl	$⊢ (K \in Lat \land Y \in B \land W \in B) \to Y \underset{˙}{\land} W \in B$
18	4 6 10 17	syl3anc	$⊢ (K \in Lat \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	lattr	$⊢ (K \in Lat \land (X \underset{˙}{\land} Z \in B \land Y \underset{˙}{\land} Z \in B \land Y \underset{˙}{\land} W \in B)) \to (((X \underset{˙}{\land} Z) \underset{˙}{\leq} (Y \underset{˙}{\land} Z) \land (Y \underset{˙}{\land} Z) \underset{˙}{\leq} (Y \underset{˙}{\land} W)) \to (X \underset{˙}{\land} Z) \underset{˙}{\leq} (Y \underset{˙}{\land} W))$
20	4 14 16 18 19	syl13anc	$⊢ (K \in Lat \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to (((X \underset{˙}{\land} Z) \underset{˙}{\leq} (Y \underset{˙}{\land} Z) \land (Y \underset{˙}{\land} Z) \underset{˙}{\leq} (Y \underset{˙}{\land} W)) \to (X \underset{˙}{\land} Z) \underset{˙}{\leq} (Y \underset{˙}{\land} W))$
21	9 12 20	syl2and	$⊢ (K \in Lat \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to ((X \underset{˙}{\leq} Y \land Z \underset{˙}{\leq} W) \to (X \underset{˙}{\land} Z) \underset{˙}{\leq} (Y \underset{˙}{\land} W))$

Metamath Proof Explorer

Theorem latmlem12

Proof