This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐷 = ( ODual ‘ 𝐾 )
Assertion odudlatb ( 𝐾 ∈ 𝑉 → ( 𝐾 ∈ DLat ↔ 𝐷 ∈ DLat ) )

Proof

Step Hyp Ref Expression
1 odudlat.d ⊢ 𝐷 = ( ODual ‘ 𝐾 )
2 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
3 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
4 eqid ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
5 2 3 4 latdisd ⊢ ( 𝐾 ∈ Lat → ( ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( join ‘ 𝐾 ) ( 𝑦 ( meet ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑥 ( join ‘ 𝐾 ) 𝑦 ) ( meet ‘ 𝐾 ) ( 𝑥 ( join ‘ 𝐾 ) 𝑧 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) ( 𝑦 ( join ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑥 ( meet ‘ 𝐾 ) 𝑦 ) ( join ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) 𝑧 ) ) ) )
6 5 bicomd ⊢ ( 𝐾 ∈ Lat → ( ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) ( 𝑦 ( join ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑥 ( meet ‘ 𝐾 ) 𝑦 ) ( join ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) 𝑧 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( join ‘ 𝐾 ) ( 𝑦 ( meet ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑥 ( join ‘ 𝐾 ) 𝑦 ) ( meet ‘ 𝐾 ) ( 𝑥 ( join ‘ 𝐾 ) 𝑧 ) ) ) )
7 6 pm5.32i ⊢ ( ( 𝐾 ∈ Lat ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) ( 𝑦 ( join ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑥 ( meet ‘ 𝐾 ) 𝑦 ) ( join ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) 𝑧 ) ) ) ↔ ( 𝐾 ∈ Lat ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( join ‘ 𝐾 ) ( 𝑦 ( meet ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑥 ( join ‘ 𝐾 ) 𝑦 ) ( meet ‘ 𝐾 ) ( 𝑥 ( join ‘ 𝐾 ) 𝑧 ) ) ) )
8 1 odulatb ⊢ ( 𝐾 ∈ 𝑉 → ( 𝐾 ∈ Lat ↔ 𝐷 ∈ Lat ) )
9 8 anbi1d ⊢ ( 𝐾 ∈ 𝑉 → ( ( 𝐾 ∈ Lat ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( join ‘ 𝐾 ) ( 𝑦 ( meet ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑥 ( join ‘ 𝐾 ) 𝑦 ) ( meet ‘ 𝐾 ) ( 𝑥 ( join ‘ 𝐾 ) 𝑧 ) ) ) ↔ ( 𝐷 ∈ Lat ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( join ‘ 𝐾 ) ( 𝑦 ( meet ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑥 ( join ‘ 𝐾 ) 𝑦 ) ( meet ‘ 𝐾 ) ( 𝑥 ( join ‘ 𝐾 ) 𝑧 ) ) ) ) )
10 7 9 bitrid ⊢ ( 𝐾 ∈ 𝑉 → ( ( 𝐾 ∈ Lat ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) ( 𝑦 ( join ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑥 ( meet ‘ 𝐾 ) 𝑦 ) ( join ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) 𝑧 ) ) ) ↔ ( 𝐷 ∈ Lat ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( join ‘ 𝐾 ) ( 𝑦 ( meet ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑥 ( join ‘ 𝐾 ) 𝑦 ) ( meet ‘ 𝐾 ) ( 𝑥 ( join ‘ 𝐾 ) 𝑧 ) ) ) ) )
11 2 3 4 isdlat ⊢ ( 𝐾 ∈ DLat ↔ ( 𝐾 ∈ Lat ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) ( 𝑦 ( join ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑥 ( meet ‘ 𝐾 ) 𝑦 ) ( join ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) 𝑧 ) ) ) )
12 1 2 odubas ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐷 )
13 1 4 odujoin ⊢ ( meet ‘ 𝐾 ) = ( join ‘ 𝐷 )
14 1 3 odumeet ⊢ ( join ‘ 𝐾 ) = ( meet ‘ 𝐷 )
15 12 13 14 isdlat ⊢ ( 𝐷 ∈ DLat ↔ ( 𝐷 ∈ Lat ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( join ‘ 𝐾 ) ( 𝑦 ( meet ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑥 ( join ‘ 𝐾 ) 𝑦 ) ( meet ‘ 𝐾 ) ( 𝑥 ( join ‘ 𝐾 ) 𝑧 ) ) ) )
16 10 11 15 3bitr4g ⊢ ( 𝐾 ∈ 𝑉 → ( 𝐾 ∈ DLat ↔ 𝐷 ∈ DLat ) )