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 
|- 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 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdlat 
 |-  DLat
1 vk 
 |-  k
2 clat 
 |-  Lat
3 cbs 
 |-  Base
4 1 cv 
 |-  k
5 4 3 cfv 
 |-  ( Base ` k )
6 vb 
 |-  b
7 cjn 
 |-  join
8 4 7 cfv 
 |-  ( join ` k )
9 vj 
 |-  j
10 cmee 
 |-  meet
11 4 10 cfv 
 |-  ( meet ` k )
12 vm 
 |-  m
13 vx 
 |-  x
14 6 cv 
 |-  b
15 vy 
 |-  y
16 vz 
 |-  z
17 13 cv 
 |-  x
18 12 cv 
 |-  m
19 15 cv 
 |-  y
20 9 cv 
 |-  j
21 16 cv 
 |-  z
22 19 21 20 co 
 |-  ( y j z )
23 17 22 18 co 
 |-  ( x m ( y j z ) )
24 17 19 18 co 
 |-  ( x m y )
25 17 21 18 co 
 |-  ( x m z )
26 24 25 20 co 
 |-  ( ( x m y ) j ( x m z ) )
27 23 26 wceq 
 |-  ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) )
28 27 16 14 wral 
 |-  A. z e. b ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) )
29 28 15 14 wral 
 |-  A. y e. b A. z e. b ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) )
30 29 13 14 wral 
 |-  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 30 12 11 wsbc 
 |-  [. ( 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 ) )
32 31 9 8 wsbc 
 |-  [. ( 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 ) )
33 32 6 5 wsbc 
 |-  [. ( 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 33 1 2 crab 
 |-  { 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 ) ) }
35 0 34 wceq 
 |-  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 ) ) }