This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem latmlej11

Description: Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012)

Ref Expression
Hypotheses latledi.b ⊢ B = Base K
latledi.l ⊢ ≤ ˙ = ≤ K
latledi.j ⊢ ∨ ˙ = join ⁡ K
latledi.m ⊢ ∧ ˙ = meet ⁡ K
Assertion latmlej11 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∧ ˙ Y ≤ ˙ X ∨ ˙ Z

Proof

Step Hyp Ref Expression
1 latledi.b ⊢ B = Base K
2 latledi.l ⊢ ≤ ˙ = ≤ K
3 latledi.j ⊢ ∨ ˙ = join ⁡ K
4 latledi.m ⊢ ∧ ˙ = meet ⁡ K
5 simpl ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → K ∈ Lat
6 1 4 latmcl ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X ∧ ˙ Y ∈ B
7 6 3adant3r3 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∧ ˙ Y ∈ B
8 simpr1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∈ B
9 1 3 latjcl ⊢ K ∈ Lat ∧ X ∈ B ∧ Z ∈ B → X ∨ ˙ Z ∈ B
10 9 3adant3r2 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∨ ˙ Z ∈ B
11 1 2 4 latmle1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X ∧ ˙ Y ≤ ˙ X
12 11 3adant3r3 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∧ ˙ Y ≤ ˙ X
13 1 2 3 latlej1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Z ∈ B → X ≤ ˙ X ∨ ˙ Z
14 13 3adant3r2 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ≤ ˙ X ∨ ˙ Z
15 1 2 5 7 8 10 12 14 lattrd ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∧ ˙ Y ≤ ˙ X ∨ ˙ Z