Definition df-dlat 17192

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

Assertion

Ref	Expression
df-dlat	|- DLat = { k e. Lat | [. ( Base ` k ) / b ]. [. ( join ` k ) / j ]. [. ( meet ` k ) / m ]. A. x e. b A. y e. b A. z e. b ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) ) }

Distinct variable group:   k, b, j, m, x, y, z

Detailed syntax breakdown of Definition df-dlat

Step	Hyp	Ref	Expression
1		cdlat 17191	. 2 class DLat
2		vx	. . . . . . . . . . . 12 setvar x
3	2	cv 1482	. . . . . . . . . . 11 class x
4		vy	. . . . . . . . . . . . 13 setvar y
5	4	cv 1482	. . . . . . . . . . . 12 class y
6		vz	. . . . . . . . . . . . 13 setvar z
7	6	cv 1482	. . . . . . . . . . . 12 class z
8		vj	. . . . . . . . . . . . 13 setvar j
9	8	cv 1482	. . . . . . . . . . . 12 class j
10	5, 7, 9	co 6650	. . . . . . . . . . 11 class ( y j z )
11		vm	. . . . . . . . . . . 12 setvar m
12	11	cv 1482	. . . . . . . . . . 11 class m
13	3, 10, 12	co 6650	. . . . . . . . . 10 class ( x m ( y j z ) )
14	3, 5, 12	co 6650	. . . . . . . . . . 11 class ( x m y )
15	3, 7, 12	co 6650	. . . . . . . . . . 11 class ( x m z )
16	14, 15, 9	co 6650	. . . . . . . . . 10 class ( ( x m y ) j ( x m z ) )
17	13, 16	wceq 1483	. . . . . . . . 9 wff ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) )
18		vb	. . . . . . . . . 10 setvar b
19	18	cv 1482	. . . . . . . . 9 class b
20	17, 6, 19	wral 2912	. . . . . . . 8 wff A. z e. b ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) )
21	20, 4, 19	wral 2912	. . . . . . 7 wff A. y e. b A. z e. b ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) )
22	21, 2, 19	wral 2912	. . . . . 6 wff A. x e. b A. y e. b A. z e. b ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) )
23		vk	. . . . . . . 8 setvar k
24	23	cv 1482	. . . . . . 7 class k
25		cmee 16945	. . . . . . 7 class meet
26	24, 25	cfv 5888	. . . . . 6 class ( meet ` k )
27	22, 11, 26	wsbc 3435	. . . . 5 wff [. ( meet ` k ) / m ]. A. x e. b A. y e. b A. z e. b ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) )
28		cjn 16944	. . . . . 6 class join
29	24, 28	cfv 5888	. . . . 5 class ( join ` k )
30	27, 8, 29	wsbc 3435	. . . 4 wff [. ( join ` k ) / j ]. [. ( meet ` k ) / m ]. A. x e. b A. y e. b A. z e. b ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) )
31		cbs 15857	. . . . 5 class Base
32	24, 31	cfv 5888	. . . 4 class ( Base ` k )
33	30, 18, 32	wsbc 3435	. . 3 wff [. ( Base ` k ) / b ]. [. ( join ` k ) / j ]. [. ( meet ` k ) / m ]. A. x e. b A. y e. b A. z e. b ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) )
34		clat 17045	. . 3 class Lat
35	33, 23, 34	crab 2916	. 2 class { k e. Lat | [. ( Base ` k ) / b ]. [. ( join ` k ) / j ]. [. ( meet ` k ) / m ]. A. x e. b A. y e. b A. z e. b ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) ) }
36	1, 35	wceq 1483	1 wff DLat = { k e. Lat | [. ( Base ` k ) / b ]. [. ( join ` k ) / j ]. [. ( meet ` k ) / m ]. A. x e. b A. y e. b A. z e. b ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) ) }

This definition is referenced by:  isdlat  17193