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