Metamath Proof Explorer

Theorem paddasslem16

Description: Lemma for paddass . Use elpaddn0 to eliminate x and r from paddasslem15 . (Contributed by NM, 11-Jan-2012)

Ref Expression
Hypotheses paddasslem.l ⊢ ≤ = ( le ‘ 𝐾 )
paddasslem.j ⊢ ∨ = ( join ‘ 𝐾 )
paddasslem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
paddasslem.p ⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion paddasslem16 ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ) → ( 𝑋 + ( 𝑌 + 𝑍 ) ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )

Proof

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 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ) → ( 𝑋 + ( 𝑌 + 𝑍 ) ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )