Metamath Proof Explorer

Theorem 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 ⊢ ≤ ˙ = ≤ K
latlej.j ⊢ ∨ ˙ = join ⁡ K
Assertion latjlej1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ≤ ˙ Y → X ∨ ˙ Z ≤ ˙ Y ∨ ˙ Z

Proof

Step Hyp Ref Expression
1 latlej.b ⊢ B = Base K
2 latlej.l ⊢ ≤ ˙ = ≤ K
3 latlej.j ⊢ ∨ ˙ = join ⁡ K
4 1 2 3 latlej1 ⊢ K ∈ Lat ∧ Y ∈ B ∧ Z ∈ B → Y ≤ ˙ Y ∨ ˙ Z
5 4 3adant3r1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Y ≤ ˙ Y ∨ ˙ Z
6 simpl ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → K ∈ Lat
7 simpr1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∈ B
8 simpr2 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Y ∈ B
9 1 3 latjcl ⊢ K ∈ Lat ∧ Y ∈ B ∧ Z ∈ B → Y ∨ ˙ Z ∈ B
10 9 3adant3r1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Y ∨ ˙ Z ∈ B
11 1 2 lattr ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Y ∨ ˙ Z ∈ B → X ≤ ˙ Y ∧ Y ≤ ˙ Y ∨ ˙ Z → X ≤ ˙ Y ∨ ˙ Z
12 6 7 8 10 11 syl13anc ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ≤ ˙ Y ∧ Y ≤ ˙ Y ∨ ˙ Z → X ≤ ˙ Y ∨ ˙ Z
13 5 12 mpan2d ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ≤ ˙ Y → X ≤ ˙ Y ∨ ˙ Z
14 1 2 3 latlej2 ⊢ K ∈ Lat ∧ Y ∈ B ∧ Z ∈ B → Z ≤ ˙ Y ∨ ˙ Z
15 14 3adant3r1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Z ≤ ˙ Y ∨ ˙ Z
16 13 15 jctird ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ≤ ˙ Y → X ≤ ˙ Y ∨ ˙ Z ∧ Z ≤ ˙ Y ∨ ˙ Z
17 simpr3 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Z ∈ B
18 7 17 10 3jca ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∈ B ∧ Z ∈ B ∧ Y ∨ ˙ Z ∈ B
19 1 2 3 latjle12 ⊢ K ∈ Lat ∧ X ∈ B ∧ Z ∈ B ∧ Y ∨ ˙ Z ∈ B → X ≤ ˙ Y ∨ ˙ Z ∧ Z ≤ ˙ Y ∨ ˙ Z ↔ X ∨ ˙ Z ≤ ˙ Y ∨ ˙ Z
20 18 19 syldan ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ≤ ˙ Y ∨ ˙ Z ∧ Z ≤ ˙ Y ∨ ˙ Z ↔ X ∨ ˙ Z ≤ ˙ Y ∨ ˙ Z
21 16 20 sylibd ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ≤ ˙ Y → X ∨ ˙ Z ≤ ˙ Y ∨ ˙ Z