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	$$⊢\mathrm{DLat}=\left\{k\in \mathrm{Lat}|\underset{\dot{}}{[}{\mathrm{Base}}_k/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{join}\left(k\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{meet}\left(k\right)/m\underset{\dot{}}{]}\forall x\in b\forall y\in b\forall z\in bxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdlat	$$class\mathrm{DLat}$$
1		vk	$$setvark$$
2		clat	$$class\mathrm{Lat}$$
3		cbs	$$class\mathrm{Base}$$
4	1	cv	$$setvark$$
5	4 3	cfv	$$class{\mathrm{Base}}_k$$
6		vb	$$setvarb$$
7		cjn	$$class\mathrm{join}$$
8	4 7	cfv	$$class\mathrm{join}\left(k\right)$$
9		vj	$$setvarj$$
10		cmee	$$class\mathrm{meet}$$
11	4 10	cfv	$$class\mathrm{meet}\left(k\right)$$
12		vm	$$setvarm$$
13		vx	$$setvarx$$
14	6	cv	$$setvarb$$
15		vy	$$setvary$$
16		vz	$$setvarz$$
17	13	cv	$$setvarx$$
18	12	cv	$$setvarm$$
19	15	cv	$$setvary$$
20	9	cv	$$setvarj$$
21	16	cv	$$setvarz$$
22	19 21 20	co	$$class\left(yjz\right)$$
23	17 22 18	co	$$class\left(xm\left(yjz\right)\right)$$
24	17 19 18	co	$$class\left(xmy\right)$$
25	17 21 18	co	$$class\left(xmz\right)$$
26	24 25 20	co	$$class\left(\left(xmy\right)j\left(xmz\right)\right)$$
27	23 26	wceq	$$wffxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)$$
28	27 16 14	wral	$$wff\forall z\in bxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)$$
29	28 15 14	wral	$$wff\forall y\in b\forall z\in bxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)$$
30	29 13 14	wral	$$wff\forall x\in b\forall y\in b\forall z\in bxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)$$
31	30 12 11	wsbc	$$wff\underset{\dot{}}{[}\mathrm{meet}\left(k\right)/m\underset{\dot{}}{]}\forall x\in b\forall y\in b\forall z\in bxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)$$
32	31 9 8	wsbc	$$wff\underset{\dot{}}{[}\mathrm{join}\left(k\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{meet}\left(k\right)/m\underset{\dot{}}{]}\forall x\in b\forall y\in b\forall z\in bxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)$$
33	32 6 5	wsbc	$$wff\underset{\dot{}}{[}{\mathrm{Base}}_k/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{join}\left(k\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{meet}\left(k\right)/m\underset{\dot{}}{]}\forall x\in b\forall y\in b\forall z\in bxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)$$
34	33 1 2	crab	$$class\left\{k\in \mathrm{Lat}|\underset{\dot{}}{[}{\mathrm{Base}}_k/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{join}\left(k\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{meet}\left(k\right)/m\underset{\dot{}}{]}\forall x\in b\forall y\in b\forall z\in bxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)\right\}$$
35	0 34	wceq	$$wff\mathrm{DLat}=\left\{k\in \mathrm{Lat}|\underset{\dot{}}{[}{\mathrm{Base}}_k/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{join}\left(k\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{meet}\left(k\right)/m\underset{\dot{}}{]}\forall x\in b\forall y\in b\forall z\in bxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)\right\}$$