latjlej2

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

	Ref	Expression
Hypotheses	latlej.b	$⊢ B = {Base}_{K}$
	latlej.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	latlej.j	$⊢ \underset{˙}{\lor} = join (K)$
Assertion	latjlej2	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\leq} Y \to (Z \underset{˙}{\lor} X) \underset{˙}{\leq} (Z \underset{˙}{\lor} Y))$

Step	Hyp	Ref	Expression
1		latlej.b	$⊢ B = {Base}_{K}$
2		latlej.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		latlej.j	$⊢ \underset{˙}{\lor} = join (K)$
4	1 2 3	latjlej1	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\leq} Y \to (X \underset{˙}{\lor} Z) \underset{˙}{\leq} (Y \underset{˙}{\lor} Z))$
5	1 3	latjcom	$⊢ (K \in Lat \land X \in B \land Z \in B) \to X \underset{˙}{\lor} Z = Z \underset{˙}{\lor} X$
6	5	3adant3r2	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\lor} Z = Z \underset{˙}{\lor} X$
7	1 3	latjcom	$⊢ (K \in Lat \land Y \in B \land Z \in B) \to Y \underset{˙}{\lor} Z = Z \underset{˙}{\lor} Y$
8	7	3adant3r1	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Y \underset{˙}{\lor} Z = Z \underset{˙}{\lor} Y$
9	6 8	breq12d	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{\lor} Z) \underset{˙}{\leq} (Y \underset{˙}{\lor} Z) \leftrightarrow (Z \underset{˙}{\lor} X) \underset{˙}{\leq} (Z \underset{˙}{\lor} Y))$
10	4 9	sylibd	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\leq} Y \to (Z \underset{˙}{\lor} X) \underset{˙}{\leq} (Z \underset{˙}{\lor} Y))$

Metamath Proof Explorer