latjlej1

Description: Add join to both sides of a lattice ordering. ( chlej1i 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	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))$

Proof

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	latlej1	$⊢ (K \in Lat \land Y \in B \land Z \in B) \to Y \underset{˙}{\leq} (Y \underset{˙}{\lor} Z)$
5	4	3adant3r1	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Y \underset{˙}{\leq} (Y \underset{˙}{\lor} Z)$
6		simpl	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to K \in Lat$
7		simpr1	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to X \in B$
8		simpr2	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Y \in B$
9	1 3	latjcl	$⊢ (K \in Lat \land Y \in B \land Z \in B) \to Y \underset{˙}{\lor} Z \in B$
10	9	3adant3r1	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Y \underset{˙}{\lor} Z \in B$
11	1 2	lattr	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Y \underset{˙}{\lor} Z \in B)) \to ((X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} (Y \underset{˙}{\lor} Z)) \to X \underset{˙}{\leq} (Y \underset{˙}{\lor} Z))$
12	6 7 8 10 11	syl13anc	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} (Y \underset{˙}{\lor} Z)) \to X \underset{˙}{\leq} (Y \underset{˙}{\lor} Z))$
13	5 12	mpan2d	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\leq} Y \to X \underset{˙}{\leq} (Y \underset{˙}{\lor} Z))$
14	1 2 3	latlej2	$⊢ (K \in Lat \land Y \in B \land Z \in B) \to Z \underset{˙}{\leq} (Y \underset{˙}{\lor} Z)$
15	14	3adant3r1	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Z \underset{˙}{\leq} (Y \underset{˙}{\lor} Z)$
16	13 15	jctird	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\leq} Y \to (X \underset{˙}{\leq} (Y \underset{˙}{\lor} Z) \land Z \underset{˙}{\leq} (Y \underset{˙}{\lor} Z)))$
17		simpr3	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Z \in B$
18	7 17 10	3jca	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \in B \land Z \in B \land Y \underset{˙}{\lor} Z \in B)$
19	1 2 3	latjle12	$⊢ (K \in Lat \land (X \in B \land Z \in B \land Y \underset{˙}{\lor} Z \in B)) \to ((X \underset{˙}{\leq} (Y \underset{˙}{\lor} Z) \land Z \underset{˙}{\leq} (Y \underset{˙}{\lor} Z)) \leftrightarrow (X \underset{˙}{\lor} Z) \underset{˙}{\leq} (Y \underset{˙}{\lor} Z))$
20	18 19	syldan	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{\leq} (Y \underset{˙}{\lor} Z) \land Z \underset{˙}{\leq} (Y \underset{˙}{\lor} Z)) \leftrightarrow (X \underset{˙}{\lor} Z) \underset{˙}{\leq} (Y \underset{˙}{\lor} Z))$
21	16 20	sylibd	$⊢ (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))$

Metamath Proof Explorer

Theorem latjlej1

Proof