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 = k ∈ Lat | [˙Base k / b]˙ [˙ join ⁡ k / j]˙ [˙ meet ⁡ k / m]˙ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x m y j z = x m y j x m z

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdlat class DLat
1 vk setvar k
2 clat class Lat
3 cbs class Base
4 1 cv setvar k
5 4 3 cfv class Base k
6 vb setvar b
7 cjn class join
8 4 7 cfv class join ⁡ k
9 vj setvar j
10 cmee class meet
11 4 10 cfv class meet ⁡ k
12 vm setvar m
13 vx setvar x
14 6 cv setvar b
15 vy setvar y
16 vz setvar z
17 13 cv setvar x
18 12 cv setvar m
19 15 cv setvar y
20 9 cv setvar j
21 16 cv setvar z
22 19 21 20 co class y j z
23 17 22 18 co class x m y j z
24 17 19 18 co class x m y
25 17 21 18 co class x m z
26 24 25 20 co class x m y j x m z
27 23 26 wceq wff x m y j z = x m y j x m z
28 27 16 14 wral wff ∀ z ∈ b x m y j z = x m y j x m z
29 28 15 14 wral wff ∀ y ∈ b ∀ z ∈ b x m y j z = x m y j x m z
30 29 13 14 wral wff ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x m y j z = x m y j x m z
31 30 12 11 wsbc wff [˙ meet ⁡ k / m]˙ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x m y j z = x m y j x m z
32 31 9 8 wsbc wff [˙ join ⁡ k / j]˙ [˙ meet ⁡ k / m]˙ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x m y j z = x m y j x m z
33 32 6 5 wsbc wff [˙Base k / b]˙ [˙ join ⁡ k / j]˙ [˙ meet ⁡ k / m]˙ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x m y j z = x m y j x m z
34 33 1 2 crab class k ∈ Lat | [˙Base k / b]˙ [˙ join ⁡ k / j]˙ [˙ meet ⁡ k / m]˙ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x m y j z = x m y j x m z
35 0 34 wceq wff DLat = k ∈ Lat | [˙Base k / b]˙ [˙ join ⁡ k / j]˙ [˙ meet ⁡ k / m]˙ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x m y j z = x m y j x m z