# Metamath Proof Explorer

## Definition df-dlat

Description: Adistributive lattice is a lattice in which meets distribute over joins, or equivalently ( latdisd ) joins distribute over meets. (Contributed by Stefan O'Rear, 30-Jan-2015)

Ref Expression
Assertion df-dlat

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cdlat ${class}\mathrm{DLat}$
1 vk ${setvar}{k}$
2 clat ${class}\mathrm{Lat}$
3 cbs ${class}\mathrm{Base}$
4 1 cv ${setvar}{k}$
5 4 3 cfv ${class}{\mathrm{Base}}_{{k}}$
6 vb ${setvar}{b}$
7 cjn ${class}\mathrm{join}$
8 4 7 cfv ${class}\mathrm{join}\left({k}\right)$
9 vj ${setvar}{j}$
10 cmee ${class}\mathrm{meet}$
11 4 10 cfv ${class}\mathrm{meet}\left({k}\right)$
12 vm ${setvar}{m}$
13 vx ${setvar}{x}$
14 6 cv ${setvar}{b}$
15 vy ${setvar}{y}$
16 vz ${setvar}{z}$
17 13 cv ${setvar}{x}$
18 12 cv ${setvar}{m}$
19 15 cv ${setvar}{y}$
20 9 cv ${setvar}{j}$
21 16 cv ${setvar}{z}$
22 19 21 20 co ${class}\left({y}{j}{z}\right)$
23 17 22 18 co ${class}\left({x}{m}\left({y}{j}{z}\right)\right)$
24 17 19 18 co ${class}\left({x}{m}{y}\right)$
25 17 21 18 co ${class}\left({x}{m}{z}\right)$
26 24 25 20 co ${class}\left(\left({x}{m}{y}\right){j}\left({x}{m}{z}\right)\right)$
27 23 26 wceq ${wff}{x}{m}\left({y}{j}{z}\right)=\left({x}{m}{y}\right){j}\left({x}{m}{z}\right)$
28 27 16 14 wral ${wff}\forall {z}\in {b}\phantom{\rule{.4em}{0ex}}{x}{m}\left({y}{j}{z}\right)=\left({x}{m}{y}\right){j}\left({x}{m}{z}\right)$
29 28 15 14 wral ${wff}\forall {y}\in {b}\phantom{\rule{.4em}{0ex}}\forall {z}\in {b}\phantom{\rule{.4em}{0ex}}{x}{m}\left({y}{j}{z}\right)=\left({x}{m}{y}\right){j}\left({x}{m}{z}\right)$
30 29 13 14 wral ${wff}\forall {x}\in {b}\phantom{\rule{.4em}{0ex}}\forall {y}\in {b}\phantom{\rule{.4em}{0ex}}\forall {z}\in {b}\phantom{\rule{.4em}{0ex}}{x}{m}\left({y}{j}{z}\right)=\left({x}{m}{y}\right){j}\left({x}{m}{z}\right)$
31 30 12 11 wsbc
32 31 9 8 wsbc
33 32 6 5 wsbc
34 33 1 2 crab
35 0 34 wceq