Metamath Proof Explorer


Theorem latmlej21

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 latmlej21 K Lat X B Y B Z B Y ˙ X ˙ 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 1 4 latmcom K Lat X B Y B X ˙ Y = Y ˙ X
6 5 3adant3r3 K Lat X B Y B Z B X ˙ Y = Y ˙ X
7 1 2 3 4 latmlej11 K Lat X B Y B Z B X ˙ Y ˙ X ˙ Z
8 6 7 eqbrtrrd K Lat X B Y B Z B Y ˙ X ˙ X ˙ Z