Database
BASIC ORDER THEORY
Posets and lattices using extensible structures
Distributive lattices
dlatl
Next ⟩
odudlatb
Metamath Proof Explorer
Ascii
Unicode
Theorem
dlatl
Description:
A distributive lattice is a lattice.
(Contributed by
Stefan O'Rear
, 30-Jan-2015)
Ref
Expression
Assertion
dlatl
⊢
K
∈
DLat
→
K
∈
Lat
Proof
Step
Hyp
Ref
Expression
1
eqid
⊢
Base
K
=
Base
K
2
eqid
⊢
join
⁡
K
=
join
⁡
K
3
eqid
⊢
meet
⁡
K
=
meet
⁡
K
4
1
2
3
isdlat
⊢
K
∈
DLat
↔
K
∈
Lat
∧
∀
x
∈
Base
K
∀
y
∈
Base
K
∀
z
∈
Base
K
x
meet
⁡
K
y
join
⁡
K
z
=
x
meet
⁡
K
y
join
⁡
K
x
meet
⁡
K
z
5
4
simplbi
⊢
K
∈
DLat
→
K
∈
Lat