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=kLat|[˙Basek/b]˙[˙joink/j]˙[˙meetk/m]˙xbybzbxmyjz=xmyjxmz

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdlat classDLat
1 vk setvark
2 clat classLat
3 cbs classBase
4 1 cv setvark
5 4 3 cfv classBasek
6 vb setvarb
7 cjn classjoin
8 4 7 cfv classjoink
9 vj setvarj
10 cmee classmeet
11 4 10 cfv classmeetk
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 classyjz
23 17 22 18 co classxmyjz
24 17 19 18 co classxmy
25 17 21 18 co classxmz
26 24 25 20 co classxmyjxmz
27 23 26 wceq wffxmyjz=xmyjxmz
28 27 16 14 wral wffzbxmyjz=xmyjxmz
29 28 15 14 wral wffybzbxmyjz=xmyjxmz
30 29 13 14 wral wffxbybzbxmyjz=xmyjxmz
31 30 12 11 wsbc wff[˙meetk/m]˙xbybzbxmyjz=xmyjxmz
32 31 9 8 wsbc wff[˙joink/j]˙[˙meetk/m]˙xbybzbxmyjz=xmyjxmz
33 32 6 5 wsbc wff[˙Basek/b]˙[˙joink/j]˙[˙meetk/m]˙xbybzbxmyjz=xmyjxmz
34 33 1 2 crab classkLat|[˙Basek/b]˙[˙joink/j]˙[˙meetk/m]˙xbybzbxmyjz=xmyjxmz
35 0 34 wceq wffDLat=kLat|[˙Basek/b]˙[˙joink/j]˙[˙meetk/m]˙xbybzbxmyjz=xmyjxmz