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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cdlat | |
|
1 | vk | |
|
2 | clat | |
|
3 | cbs | |
|
4 | 1 | cv | |
5 | 4 3 | cfv | |
6 | vb | |
|
7 | cjn | |
|
8 | 4 7 | cfv | |
9 | vj | |
|
10 | cmee | |
|
11 | 4 10 | cfv | |
12 | vm | |
|
13 | vx | |
|
14 | 6 | cv | |
15 | vy | |
|
16 | vz | |
|
17 | 13 | cv | |
18 | 12 | cv | |
19 | 15 | cv | |
20 | 9 | cv | |
21 | 16 | cv | |
22 | 19 21 20 | co | |
23 | 17 22 18 | co | |
24 | 17 19 18 | co | |
25 | 17 21 18 | co | |
26 | 24 25 20 | co | |
27 | 23 26 | wceq | |
28 | 27 16 14 | wral | |
29 | 28 15 14 | wral | |
30 | 29 13 14 | wral | |
31 | 30 12 11 | wsbc | |
32 | 31 9 8 | wsbc | |
33 | 32 6 5 | wsbc | |
34 | 33 1 2 | crab | |
35 | 0 34 | wceq | |