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

Metamath Proof Explorer

Theorem dlatjmdi

Description: In a distributive lattice, joins distribute over meets. (Contributed by Stefan O'Rear, 30-Jan-2015)

Ref Expression
Hypotheses dlatjmdi.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dlatjmdi.j ⊢ ∨ = ( join ‘ 𝐾 )
dlatjmdi.m ⊢ ∧ = ( meet ‘ 𝐾 )
Assertion dlatjmdi ( ( 𝐾 ∈ DLat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) = ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 dlatjmdi.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dlatjmdi.j ⊢ ∨ = ( join ‘ 𝐾 )
3 dlatjmdi.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 eqid ⊢ ( ODual ‘ 𝐾 ) = ( ODual ‘ 𝐾 )
5 4 odudlatb ⊢ ( 𝐾 ∈ DLat → ( 𝐾 ∈ DLat ↔ ( ODual ‘ 𝐾 ) ∈ DLat ) )
6 5 ibi ⊢ ( 𝐾 ∈ DLat → ( ODual ‘ 𝐾 ) ∈ DLat )
7 4 1 odubas ⊢ 𝐵 = ( Base ‘ ( ODual ‘ 𝐾 ) )
8 4 3 odujoin ⊢ ∧ = ( join ‘ ( ODual ‘ 𝐾 ) )
9 4 2 odumeet ⊢ ∨ = ( meet ‘ ( ODual ‘ 𝐾 ) )
10 7 8 9 dlatmjdi ⊢ ( ( ( ODual ‘ 𝐾 ) ∈ DLat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) = ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ 𝑍 ) ) )
11 6 10 sylan ⊢ ( ( 𝐾 ∈ DLat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) = ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ 𝑍 ) ) )