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 ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ) → ( 𝑋 ( 𝑌 𝑍 ) ) = ( ( 𝑋 𝑌 ) ( 𝑋 𝑍 ) ) )