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

Definition df-dlat 17800
Description: A distributive lattice is a lattice in which meets distribute over joins, or equivalently (latdisd 17798) joins distribute over meets. (Contributed by Stefan O'Rear, 30-Jan-2015.)
Assertion
Ref Expression
df-dlat DLat = {𝑘 ∈ Lat ∣ [(Base‘𝑘) / 𝑏][(join‘𝑘) / 𝑗][(meet‘𝑘) / 𝑚]𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧))}
Distinct variable group:   𝑘,𝑏,𝑗,𝑚,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-dlat
StepHypRef Expression
1 cdlat 17799 . 2 class DLat
2 vx . . . . . . . . . . . 12 setvar 𝑥
32cv 1537 . . . . . . . . . . 11 class 𝑥
4 vy . . . . . . . . . . . . 13 setvar 𝑦
54cv 1537 . . . . . . . . . . . 12 class 𝑦
6 vz . . . . . . . . . . . . 13 setvar 𝑧
76cv 1537 . . . . . . . . . . . 12 class 𝑧
8 vj . . . . . . . . . . . . 13 setvar 𝑗
98cv 1537 . . . . . . . . . . . 12 class 𝑗
105, 7, 9co 7146 . . . . . . . . . . 11 class (𝑦𝑗𝑧)
11 vm . . . . . . . . . . . 12 setvar 𝑚
1211cv 1537 . . . . . . . . . . 11 class 𝑚
133, 10, 12co 7146 . . . . . . . . . 10 class (𝑥𝑚(𝑦𝑗𝑧))
143, 5, 12co 7146 . . . . . . . . . . 11 class (𝑥𝑚𝑦)
153, 7, 12co 7146 . . . . . . . . . . 11 class (𝑥𝑚𝑧)
1614, 15, 9co 7146 . . . . . . . . . 10 class ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧))
1713, 16wceq 1538 . . . . . . . . 9 wff (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧))
18 vb . . . . . . . . . 10 setvar 𝑏
1918cv 1537 . . . . . . . . 9 class 𝑏
2017, 6, 19wral 3133 . . . . . . . 8 wff 𝑧𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧))
2120, 4, 19wral 3133 . . . . . . 7 wff 𝑦𝑏𝑧𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧))
2221, 2, 19wral 3133 . . . . . 6 wff 𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧))
23 vk . . . . . . . 8 setvar 𝑘
2423cv 1537 . . . . . . 7 class 𝑘
25 cmee 17553 . . . . . . 7 class meet
2624, 25cfv 6344 . . . . . 6 class (meet‘𝑘)
2722, 11, 26wsbc 3758 . . . . 5 wff [(meet‘𝑘) / 𝑚]𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧))
28 cjn 17552 . . . . . 6 class join
2924, 28cfv 6344 . . . . 5 class (join‘𝑘)
3027, 8, 29wsbc 3758 . . . 4 wff [(join‘𝑘) / 𝑗][(meet‘𝑘) / 𝑚]𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧))
31 cbs 16481 . . . . 5 class Base
3224, 31cfv 6344 . . . 4 class (Base‘𝑘)
3330, 18, 32wsbc 3758 . . 3 wff [(Base‘𝑘) / 𝑏][(join‘𝑘) / 𝑗][(meet‘𝑘) / 𝑚]𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧))
34 clat 17653 . . 3 class Lat
3533, 23, 34crab 3137 . 2 class {𝑘 ∈ Lat ∣ [(Base‘𝑘) / 𝑏][(join‘𝑘) / 𝑗][(meet‘𝑘) / 𝑚]𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧))}
361, 35wceq 1538 1 wff DLat = {𝑘 ∈ Lat ∣ [(Base‘𝑘) / 𝑏][(join‘𝑘) / 𝑗][(meet‘𝑘) / 𝑚]𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧))}
Colors of variables: wff setvar class
This definition is referenced by:  isdlat  17801
  Copyright terms: Public domain W3C validator