Description: A distributive lattice is a lattice. (Contributed by Stefan O'Rear, 30-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | dlatl | ⊢ ( 𝐾 ∈ DLat → 𝐾 ∈ Lat ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) | |
2 | eqid | ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 ) | |
3 | eqid | ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 ) | |
4 | 1 2 3 | isdlat | ⊢ ( 𝐾 ∈ DLat ↔ ( 𝐾 ∈ Lat ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) ( 𝑦 ( join ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑥 ( meet ‘ 𝐾 ) 𝑦 ) ( join ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) 𝑧 ) ) ) ) |
5 | 4 | simplbi | ⊢ ( 𝐾 ∈ DLat → 𝐾 ∈ Lat ) |