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

Metamath Proof Explorer

Theorem dlatmjdi

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

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

Proof

Step Hyp Ref Expression
1 isdlat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 isdlat.j ⊢ ∨ = ( join ‘ 𝐾 )
3 isdlat.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 1 2 3 isdlat ⊢ ( 𝐾 ∈ DLat ↔ ( 𝐾 ∈ Lat ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ∧ ( 𝑦 ∨ 𝑧 ) ) = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ 𝑧 ) ) ) )
5 4 simprbi ⊢ ( 𝐾 ∈ DLat → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ∧ ( 𝑦 ∨ 𝑧 ) ) = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ 𝑧 ) ) )
6 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∧ ( 𝑦 ∨ 𝑧 ) ) = ( 𝑋 ∧ ( 𝑦 ∨ 𝑧 ) ) )
7 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∧ 𝑦 ) = ( 𝑋 ∧ 𝑦 ) )
8 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∧ 𝑧 ) = ( 𝑋 ∧ 𝑧 ) )
9 7 8 oveq12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ 𝑧 ) ) = ( ( 𝑋 ∧ 𝑦 ) ∨ ( 𝑋 ∧ 𝑧 ) ) )
10 6 9 eqeq12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ∧ ( 𝑦 ∨ 𝑧 ) ) = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ 𝑧 ) ) ↔ ( 𝑋 ∧ ( 𝑦 ∨ 𝑧 ) ) = ( ( 𝑋 ∧ 𝑦 ) ∨ ( 𝑋 ∧ 𝑧 ) ) ) )
11 oveq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 ∨ 𝑧 ) = ( 𝑌 ∨ 𝑧 ) )
12 11 oveq2d ⊢ ( 𝑦 = 𝑌 → ( 𝑋 ∧ ( 𝑦 ∨ 𝑧 ) ) = ( 𝑋 ∧ ( 𝑌 ∨ 𝑧 ) ) )
13 oveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 ∧ 𝑦 ) = ( 𝑋 ∧ 𝑌 ) )
14 13 oveq1d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 ∧ 𝑦 ) ∨ ( 𝑋 ∧ 𝑧 ) ) = ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑧 ) ) )
15 12 14 eqeq12d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 ∧ ( 𝑦 ∨ 𝑧 ) ) = ( ( 𝑋 ∧ 𝑦 ) ∨ ( 𝑋 ∧ 𝑧 ) ) ↔ ( 𝑋 ∧ ( 𝑌 ∨ 𝑧 ) ) = ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑧 ) ) ) )
16 oveq2 ⊢ ( 𝑧 = 𝑍 → ( 𝑌 ∨ 𝑧 ) = ( 𝑌 ∨ 𝑍 ) )
17 16 oveq2d ⊢ ( 𝑧 = 𝑍 → ( 𝑋 ∧ ( 𝑌 ∨ 𝑧 ) ) = ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) )
18 oveq2 ⊢ ( 𝑧 = 𝑍 → ( 𝑋 ∧ 𝑧 ) = ( 𝑋 ∧ 𝑍 ) )
19 18 oveq2d ⊢ ( 𝑧 = 𝑍 → ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑧 ) ) = ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) )
20 17 19 eqeq12d ⊢ ( 𝑧 = 𝑍 → ( ( 𝑋 ∧ ( 𝑌 ∨ 𝑧 ) ) = ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑧 ) ) ↔ ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) = ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ) )
21 10 15 20 rspc3v ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ∧ ( 𝑦 ∨ 𝑧 ) ) = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ 𝑧 ) ) → ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) = ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ) )
22 5 21 mpan9 ⊢ ( ( 𝐾 ∈ DLat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) = ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) )