Metamath Proof Explorer

Theorem paddasslem13

Description: Lemma for paddass . The case when r .<_ ( x .\/ y ) . (Unlike the proof in Maeda and Maeda, we don't need x =/= y .) (Contributed by NM, 11-Jan-2012)

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

Proof

Step Hyp Ref Expression
1 paddasslem.l ⊢ ≤ = ( le ‘ 𝐾 )
2 paddasslem.j ⊢ ∨ = ( join ‘ 𝐾 )
3 paddasslem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 paddasslem.p ⊢ + = ( +𝑃 ‘ 𝐾 )
5 simpl1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝐾 ∈ HL )
6 simpl21 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑋 ⊆ 𝐴 )
7 simpl22 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑌 ⊆ 𝐴 )
8 3 4 paddssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 + 𝑌 ) ⊆ 𝐴 )
9 5 6 7 8 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → ( 𝑋 + 𝑌 ) ⊆ 𝐴 )
10 simpl23 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑍 ⊆ 𝐴 )
11 3 4 sspadd1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 + 𝑌 ) ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) → ( 𝑋 + 𝑌 ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
12 5 9 10 11 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → ( 𝑋 + 𝑌 ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
13 5 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝐾 ∈ Lat )
14 simprll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑥 ∈ 𝑋 )
15 simprlr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑦 ∈ 𝑌 )
16 simpl3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑝 ∈ 𝐴 )
17 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
18 17 3 atbase ⊢ ( 𝑝 ∈ 𝐴 → 𝑝 ∈ ( Base ‘ 𝐾 ) )
19 16 18 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑝 ∈ ( Base ‘ 𝐾 ) )
20 6 14 sseldd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑥 ∈ 𝐴 )
21 17 3 atbase ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( Base ‘ 𝐾 ) )
22 20 21 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑥 ∈ ( Base ‘ 𝐾 ) )
23 simpl3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑟 ∈ 𝐴 )
24 17 3 atbase ⊢ ( 𝑟 ∈ 𝐴 → 𝑟 ∈ ( Base ‘ 𝐾 ) )
25 23 24 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑟 ∈ ( Base ‘ 𝐾 ) )
26 17 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑟 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑥 ∨ 𝑟 ) ∈ ( Base ‘ 𝐾 ) )
27 13 22 25 26 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → ( 𝑥 ∨ 𝑟 ) ∈ ( Base ‘ 𝐾 ) )
28 7 15 sseldd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑦 ∈ 𝐴 )
29 17 3 atbase ⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ( Base ‘ 𝐾 ) )
30 28 29 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑦 ∈ ( Base ‘ 𝐾 ) )
31 17 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑥 ∨ 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
32 13 22 30 31 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → ( 𝑥 ∨ 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
33 simprrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) )
34 17 1 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → 𝑥 ≤ ( 𝑥 ∨ 𝑦 ) )
35 13 22 30 34 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑥 ≤ ( 𝑥 ∨ 𝑦 ) )
36 simprrl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) )
37 17 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑟 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑥 ∨ 𝑦 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑥 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) ↔ ( 𝑥 ∨ 𝑟 ) ≤ ( 𝑥 ∨ 𝑦 ) ) )
38 13 22 25 32 37 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → ( ( 𝑥 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) ↔ ( 𝑥 ∨ 𝑟 ) ≤ ( 𝑥 ∨ 𝑦 ) ) )
39 35 36 38 mpbi2and ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → ( 𝑥 ∨ 𝑟 ) ≤ ( 𝑥 ∨ 𝑦 ) )
40 17 1 13 19 27 32 33 39 lattrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑝 ≤ ( 𝑥 ∨ 𝑦 ) )
41 1 2 3 4 elpaddri ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑦 ) ) ) → 𝑝 ∈ ( 𝑋 + 𝑌 ) )
42 13 6 7 14 15 16 40 41 syl322anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑝 ∈ ( 𝑋 + 𝑌 ) )
43 12 42 sseldd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )