Definition df-dlat 17015

Description: A distributive lattice is a lattice in which meets distribute over joins, or equivalently (latdisd 17013) 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

Step	Hyp	Ref	Expression
1		cdlat 17014	. 2 class DLat
2		vx	. . . . . . . . . . . 12 setvar 𝑥
3	2	cv 1474	. . . . . . . . . . 11 class 𝑥
4		vy	. . . . . . . . . . . . 13 setvar 𝑦
5	4	cv 1474	. . . . . . . . . . . 12 class 𝑦
6		vz	. . . . . . . . . . . . 13 setvar 𝑧
7	6	cv 1474	. . . . . . . . . . . 12 class 𝑧
8		vj	. . . . . . . . . . . . 13 setvar 𝑗
9	8	cv 1474	. . . . . . . . . . . 12 class 𝑗
10	5, 7, 9	co 6549	. . . . . . . . . . 11 class (𝑦𝑗𝑧)
11		vm	. . . . . . . . . . . 12 setvar 𝑚
12	11	cv 1474	. . . . . . . . . . 11 class 𝑚
13	3, 10, 12	co 6549	. . . . . . . . . 10 class (𝑥𝑚(𝑦𝑗𝑧))
14	3, 5, 12	co 6549	. . . . . . . . . . 11 class (𝑥𝑚𝑦)
15	3, 7, 12	co 6549	. . . . . . . . . . 11 class (𝑥𝑚𝑧)
16	14, 15, 9	co 6549	. . . . . . . . . 10 class ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧))
17	13, 16	wceq 1475	. . . . . . . . 9 wff (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧))
18		vb	. . . . . . . . . 10 setvar 𝑏
19	18	cv 1474	. . . . . . . . 9 class 𝑏
20	17, 6, 19	wral 2896	. . . . . . . 8 wff ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧))
21	20, 4, 19	wral 2896	. . . . . . 7 wff ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧))
22	21, 2, 19	wral 2896	. . . . . 6 wff ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧))
23		vk	. . . . . . . 8 setvar 𝑘
24	23	cv 1474	. . . . . . 7 class 𝑘
25		cmee 16768	. . . . . . 7 class meet
26	24, 25	cfv 5804	. . . . . 6 class (meet‘𝑘)
27	22, 11, 26	wsbc 3402	. . . . 5 wff [(meet‘𝑘) / 𝑚]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧))
28		cjn 16767	. . . . . 6 class join
29	24, 28	cfv 5804	. . . . 5 class (join‘𝑘)
30	27, 8, 29	wsbc 3402	. . . 4 wff [(join‘𝑘) / 𝑗][(meet‘𝑘) / 𝑚]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧))
31		cbs 15695	. . . . 5 class Base
32	24, 31	cfv 5804	. . . 4 class (Base‘𝑘)
33	30, 18, 32	wsbc 3402	. . 3 wff [(Base‘𝑘) / 𝑏][(join‘𝑘) / 𝑗][(meet‘𝑘) / 𝑚]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧))
34		clat 16868	. . 3 class Lat
35	33, 23, 34	crab 2900	. 2 class {𝑘 ∈ Lat ∣ [(Base‘𝑘) / 𝑏][(join‘𝑘) / 𝑗][(meet‘𝑘) / 𝑚]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧))}
36	1, 35	wceq 1475	1 wff DLat = {𝑘 ∈ Lat ∣ [(Base‘𝑘) / 𝑏][(join‘𝑘) / 𝑗][(meet‘𝑘) / 𝑚]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧))}

This definition is referenced by:  isdlat  17016