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