MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-dlat Unicode version

Definition df-dlat 14295
Description: A distributive lattice is a lattice in which meets distribute over joins, or equivalently (latdisd 14293) 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
StepHypRef Expression
1 cdlat 14294 . 2  class DLat
2 vx . . . . . . . . . . . 12  set  x
32cv 1622 . . . . . . . . . . 11  class  x
4 vy . . . . . . . . . . . . 13  set  y
54cv 1622 . . . . . . . . . . . 12  class  y
6 vz . . . . . . . . . . . . 13  set  z
76cv 1622 . . . . . . . . . . . 12  class  z
8 vj . . . . . . . . . . . . 13  set  j
98cv 1622 . . . . . . . . . . . 12  class  j
105, 7, 9co 5858 . . . . . . . . . . 11  class  ( y j z )
11 vm . . . . . . . . . . . 12  set  m
1211cv 1622 . . . . . . . . . . 11  class  m
133, 10, 12co 5858 . . . . . . . . . 10  class  ( x m ( y j z ) )
143, 5, 12co 5858 . . . . . . . . . . 11  class  ( x m y )
153, 7, 12co 5858 . . . . . . . . . . 11  class  ( x m z )
1614, 15, 9co 5858 . . . . . . . . . 10  class  ( ( x m y ) j ( x m z ) )
1713, 16wceq 1623 . . . . . . . . 9  wff  ( x m ( y j z ) )  =  ( ( x m y ) j ( x m z ) )
18 vb . . . . . . . . . 10  set  b
1918cv 1622 . . . . . . . . 9  class  b
2017, 6, 19wral 2543 . . . . . . . 8  wff  A. z  e.  b  ( x m ( y j z ) )  =  ( ( x m y ) j ( x m z ) )
2120, 4, 19wral 2543 . . . . . . 7  wff  A. y  e.  b  A. z  e.  b  ( x m ( y j z ) )  =  ( ( x m y ) j ( x m z ) )
2221, 2, 19wral 2543 . . . . . 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  set  k
2423cv 1622 . . . . . . 7  class  k
25 cmee 14079 . . . . . . 7  class  meet
2624, 25cfv 5255 . . . . . 6  class  ( meet `  k )
2722, 11, 26wsbc 2991 . . . . 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 14078 . . . . . 6  class  join
2924, 28cfv 5255 . . . . 5  class  ( join `  k )
3027, 8, 29wsbc 2991 . . . 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 13148 . . . . 5  class  Base
3224, 31cfv 5255 . . . 4  class  ( Base `  k )
3330, 18, 32wsbc 2991 . . 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 14151 . . 3  class  Lat
3533, 23, 34crab 2547 . 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 ) ) }
361, 35wceq 1623 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 ) ) }
Colors of variables: wff set class
This definition is referenced by:  isdlat  14296
  Copyright terms: Public domain W3C validator