Theorem dlatl

Description: A distributive lattice is a lattice. (Contributed by Stefan O'Rear, 30-Jan-2015)

	Ref	Expression
Assertion	dlatl	$$⊢K\in \mathrm{DLat}\to K\in \mathrm{Lat}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
2		eqid	$$⊢\mathrm{join}\left(K\right)=\mathrm{join}\left(K\right)$$
3		eqid	$$⊢\mathrm{meet}\left(K\right)=\mathrm{meet}\left(K\right)$$
4	1 2 3	isdlat	$$⊢K\in \mathrm{DLat}\leftrightarrow \left(K\in \mathrm{Lat}\wedge \forall x\in {\mathrm{Base}}_K\forall y\in {\mathrm{Base}}_K\forall z\in {\mathrm{Base}}_{K}x\mathrm{meet}\left(K\right)\left(y\mathrm{join}\left(K\right)z\right)=\left(x\mathrm{meet}\left(K\right)y\right)\mathrm{join}\left(K\right)\left(x\mathrm{meet}\left(K\right)z\right)\right)$$
5	4	simplbi	$$⊢K\in \mathrm{DLat}\to K\in \mathrm{Lat}$$