Metamath Proof Explorer

Theorem odudlatb

Description: The dual of a distributive lattice is a distributive lattice and conversely. (Contributed by Stefan O'Rear, 30-Jan-2015)

Ref Expression
Hypothesis odudlat.d ⊢ D = ODual ⁡ K
Assertion odudlatb ⊢ K ∈ V → K ∈ DLat ↔ D ∈ DLat

Proof

Step Hyp Ref Expression
1 odudlat.d ⊢ D = ODual ⁡ K
2 eqid ⊢ Base K = Base K
3 eqid ⊢ join ⁡ K = join ⁡ K
4 eqid ⊢ meet ⁡ K = meet ⁡ K
5 2 3 4 latdisd ⊢ K ∈ Lat → ∀ x ∈ Base K ∀ y ∈ Base K ∀ z ∈ Base K x join ⁡ K y meet ⁡ K z = x join ⁡ K y meet ⁡ K x join ⁡ K z ↔ ∀ x ∈ Base K ∀ y ∈ Base K ∀ z ∈ Base K x meet ⁡ K y join ⁡ K z = x meet ⁡ K y join ⁡ K x meet ⁡ K z
6 5 bicomd ⊢ K ∈ Lat → ∀ x ∈ Base K ∀ y ∈ Base K ∀ z ∈ Base K x meet ⁡ K y join ⁡ K z = x meet ⁡ K y join ⁡ K x meet ⁡ K z ↔ ∀ x ∈ Base K ∀ y ∈ Base K ∀ z ∈ Base K x join ⁡ K y meet ⁡ K z = x join ⁡ K y meet ⁡ K x join ⁡ K z
7 6 pm5.32i ⊢ K ∈ Lat ∧ ∀ x ∈ Base K ∀ y ∈ Base K ∀ z ∈ Base K x meet ⁡ K y join ⁡ K z = x meet ⁡ K y join ⁡ K x meet ⁡ K z ↔ K ∈ Lat ∧ ∀ x ∈ Base K ∀ y ∈ Base K ∀ z ∈ Base K x join ⁡ K y meet ⁡ K z = x join ⁡ K y meet ⁡ K x join ⁡ K z
8 1 odulatb ⊢ K ∈ V → K ∈ Lat ↔ D ∈ Lat
9 8 anbi1d ⊢ K ∈ V → K ∈ Lat ∧ ∀ x ∈ Base K ∀ y ∈ Base K ∀ z ∈ Base K x join ⁡ K y meet ⁡ K z = x join ⁡ K y meet ⁡ K x join ⁡ K z ↔ D ∈ Lat ∧ ∀ x ∈ Base K ∀ y ∈ Base K ∀ z ∈ Base K x join ⁡ K y meet ⁡ K z = x join ⁡ K y meet ⁡ K x join ⁡ K z
10 7 9 bitrid ⊢ K ∈ V → K ∈ Lat ∧ ∀ x ∈ Base K ∀ y ∈ Base K ∀ z ∈ Base K x meet ⁡ K y join ⁡ K z = x meet ⁡ K y join ⁡ K x meet ⁡ K z ↔ D ∈ Lat ∧ ∀ x ∈ Base K ∀ y ∈ Base K ∀ z ∈ Base K x join ⁡ K y meet ⁡ K z = x join ⁡ K y meet ⁡ K x join ⁡ K z
11 2 3 4 isdlat ⊢ K ∈ DLat ↔ K ∈ Lat ∧ ∀ x ∈ Base K ∀ y ∈ Base K ∀ z ∈ Base K x meet ⁡ K y join ⁡ K z = x meet ⁡ K y join ⁡ K x meet ⁡ K z
12 1 2 odubas ⊢ Base K = Base D
13 1 4 odujoin ⊢ meet ⁡ K = join ⁡ D
14 1 3 odumeet ⊢ join ⁡ K = meet ⁡ D
15 12 13 14 isdlat ⊢ D ∈ DLat ↔ D ∈ Lat ∧ ∀ x ∈ Base K ∀ y ∈ Base K ∀ z ∈ Base K x join ⁡ K y meet ⁡ K z = x join ⁡ K y meet ⁡ K x join ⁡ K z
16 10 11 15 3bitr4g ⊢ K ∈ V → K ∈ DLat ↔ D ∈ DLat