Step |
Hyp |
Ref |
Expression |
1 |
|
paddasslem.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
2 |
|
paddasslem.j |
⊢ ∨ = ( join ‘ 𝐾 ) |
3 |
|
paddasslem.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
4 |
|
paddasslem.p |
⊢ + = ( +𝑃 ‘ 𝐾 ) |
5 |
|
hllat |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat ) |
6 |
5
|
3ad2ant1 |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ) → 𝐾 ∈ Lat ) |
7 |
|
simp21 |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ) → 𝑋 ⊆ 𝐴 ) |
8 |
|
simp1 |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ) → 𝐾 ∈ HL ) |
9 |
|
simp22 |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ) → 𝑌 ⊆ 𝐴 ) |
10 |
|
simp23 |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ) → 𝑍 ⊆ 𝐴 ) |
11 |
3 4
|
paddssat |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) → ( 𝑌 + 𝑍 ) ⊆ 𝐴 ) |
12 |
8 9 10 11
|
syl3anc |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ) → ( 𝑌 + 𝑍 ) ⊆ 𝐴 ) |
13 |
|
simp3l |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ) → ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ) |
14 |
1 2 3 4
|
elpaddn0 |
⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ ( 𝑌 + 𝑍 ) ⊆ 𝐴 ) ∧ ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ) → ( 𝑝 ∈ ( 𝑋 + ( 𝑌 + 𝑍 ) ) ↔ ( 𝑝 ∈ 𝐴 ∧ ∃ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ( 𝑌 + 𝑍 ) 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) |
15 |
6 7 12 13 14
|
syl31anc |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ) → ( 𝑝 ∈ ( 𝑋 + ( 𝑌 + 𝑍 ) ) ↔ ( 𝑝 ∈ 𝐴 ∧ ∃ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ( 𝑌 + 𝑍 ) 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) |
16 |
|
simpr |
⊢ ( ( ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) → ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) |
17 |
1 2 3 4
|
paddasslem15 |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) |
18 |
16 17
|
syl3anl3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) |
19 |
18
|
3exp2 |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ) → ( 𝑝 ∈ 𝐴 → ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) → ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) ) ) |
20 |
19
|
imp |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ) ∧ 𝑝 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ( 𝑌 + 𝑍 ) ) → ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) ) |
21 |
20
|
rexlimdvv |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ) ∧ 𝑝 ∈ 𝐴 ) → ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ( 𝑌 + 𝑍 ) 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) |
22 |
21
|
expimpd |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ) → ( ( 𝑝 ∈ 𝐴 ∧ ∃ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ( 𝑌 + 𝑍 ) 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) |
23 |
15 22
|
sylbid |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ) → ( 𝑝 ∈ ( 𝑋 + ( 𝑌 + 𝑍 ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) |
24 |
23
|
ssrdv |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ) → ( 𝑋 + ( 𝑌 + 𝑍 ) ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) |