This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem paddasslem10

Description: Lemma for paddass . Use paddasslem4 to eliminate s from paddasslem9 . (Contributed by NM, 9-Jan-2012)

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

Proof

Step Hyp Ref Expression
1 paddasslem.l ⊢ ≤ = ( le ‘ 𝐾 )
2 paddasslem.j ⊢ ∨ = ( join ‘ 𝐾 )
3 paddasslem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 paddasslem.p ⊢ + = ( +𝑃 ‘ 𝐾 )
5 simpl11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝐾 ∈ HL )
6 simpl3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑝 ∈ 𝐴 )
7 simpl3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑟 ∈ 𝐴 )
8 5 6 7 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) )
9 an6 ⊢ ( ( ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ) ↔ ( ( 𝑋 ⊆ 𝐴 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑌 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑍 ⊆ 𝐴 ∧ 𝑧 ∈ 𝑍 ) ) )
10 ssel2 ⊢ ( ( 𝑋 ⊆ 𝐴 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝐴 )
11 ssel2 ⊢ ( ( 𝑌 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ 𝐴 )
12 ssel2 ⊢ ( ( 𝑍 ⊆ 𝐴 ∧ 𝑧 ∈ 𝑍 ) → 𝑧 ∈ 𝐴 )
13 10 11 12 3anim123i ⊢ ( ( ( 𝑋 ⊆ 𝐴 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑌 ⊆ 𝐴 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑍 ⊆ 𝐴 ∧ 𝑧 ∈ 𝑍 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) )
14 9 13 sylbi ⊢ ( ( ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) )
15 14 3ad2antl2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) )
16 15 adantrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) )
17 simpl12 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑝 ≠ 𝑧 )
18 simpl13 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑥 ≠ 𝑦 )
19 simprr1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) )
20 17 18 19 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → ( 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ∧ ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) )
21 simprr2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) )
22 simprr3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) )
23 1 2 3 paddasslem4 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ∧ ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → ∃ 𝑠 ∈ 𝐴 ( 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) )
24 8 16 20 21 22 23 syl32anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → ∃ 𝑠 ∈ 𝐴 ( 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) )
25 simpl2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) )
26 simpl3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) )
27 5 25 26 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) )
28 27 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) ) → ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) )
29 simplrl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) ) → ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) )
30 19 22 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) )
31 30 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) ) → ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) )
32 simprl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) ) → 𝑠 ∈ 𝐴 )
33 simprrl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) ) → 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) )
34 simprrr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) ) → 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) )
35 32 33 34 3jca ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) ) → ( 𝑠 ∈ 𝐴 ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) )
36 1 2 3 4 paddasslem9 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
37 28 29 31 35 36 syl13anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
38 24 37 rexlimddv ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )