Metamath Proof Explorer

Theorem latjlej12

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

Ref Expression
Hypotheses latlej.b ⊢ B = Base K
latlej.l ⊢ ≤ ˙ = ≤ K
latlej.j ⊢ ∨ ˙ = join ⁡ K
Assertion latjlej12 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ W ∈ B → X ≤ ˙ Y ∧ Z ≤ ˙ W → X ∨ ˙ Z ≤ ˙ Y ∨ ˙ W

Proof

Step Hyp Ref Expression
1 latlej.b ⊢ B = Base K
2 latlej.l ⊢ ≤ ˙ = ≤ K
3 latlej.j ⊢ ∨ ˙ = join ⁡ K
4 simp1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ W ∈ B → K ∈ Lat
5 simp2l ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ W ∈ B → X ∈ B
6 simp2r ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ W ∈ B → Y ∈ B
7 simp3l ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ W ∈ B → Z ∈ B
8 1 2 3 latjlej1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ≤ ˙ Y → X ∨ ˙ Z ≤ ˙ Y ∨ ˙ Z
9 4 5 6 7 8 syl13anc ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ W ∈ B → X ≤ ˙ Y → X ∨ ˙ Z ≤ ˙ Y ∨ ˙ Z
10 simp3r ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ W ∈ B → W ∈ B
11 1 2 3 latjlej2 ⊢ K ∈ Lat ∧ Z ∈ B ∧ W ∈ B ∧ Y ∈ B → Z ≤ ˙ W → Y ∨ ˙ Z ≤ ˙ Y ∨ ˙ W
12 4 7 10 6 11 syl13anc ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ W ∈ B → Z ≤ ˙ W → Y ∨ ˙ Z ≤ ˙ Y ∨ ˙ W
13 1 3 latjcl ⊢ K ∈ Lat ∧ X ∈ B ∧ Z ∈ B → X ∨ ˙ Z ∈ B
14 4 5 7 13 syl3anc ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ W ∈ B → X ∨ ˙ Z ∈ B
15 1 3 latjcl ⊢ K ∈ Lat ∧ Y ∈ B ∧ Z ∈ B → Y ∨ ˙ Z ∈ B
16 4 6 7 15 syl3anc ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ W ∈ B → Y ∨ ˙ Z ∈ B
17 1 3 latjcl ⊢ K ∈ Lat ∧ Y ∈ B ∧ W ∈ B → Y ∨ ˙ W ∈ B
18 4 6 10 17 syl3anc ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ W ∈ B → Y ∨ ˙ W ∈ B
19 1 2 lattr ⊢ K ∈ Lat ∧ X ∨ ˙ Z ∈ B ∧ Y ∨ ˙ Z ∈ B ∧ Y ∨ ˙ W ∈ B → X ∨ ˙ Z ≤ ˙ Y ∨ ˙ Z ∧ Y ∨ ˙ Z ≤ ˙ Y ∨ ˙ W → X ∨ ˙ Z ≤ ˙ Y ∨ ˙ W
20 4 14 16 18 19 syl13anc ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ W ∈ B → X ∨ ˙ Z ≤ ˙ Y ∨ ˙ Z ∧ Y ∨ ˙ Z ≤ ˙ Y ∨ ˙ W → X ∨ ˙ Z ≤ ˙ Y ∨ ˙ W
21 9 12 20 syl2and ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ W ∈ B → X ≤ ˙ Y ∧ Z ≤ ˙ W → X ∨ ˙ Z ≤ ˙ Y ∨ ˙ W