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

Metamath Proof Explorer

Theorem paddasslem14

Description: Lemma for paddass . Remove p =/= z , x =/= y , and -. r .<_ ( x .\/ y ) from antecedent of paddasslem10 , using paddasslem11 , paddasslem12 , and paddasslem13 . (Contributed by NM, 11-Jan-2012)

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

Proof

Step Hyp Ref Expression
1 paddasslem.l ⊢ ≤ = ( le ‘ 𝐾 )
2 paddasslem.j ⊢ ∨ = ( join ‘ 𝐾 )
3 paddasslem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 paddasslem.p ⊢ + = ( +𝑃 ‘ 𝐾 )
5 1 2 3 4 paddasslem11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 = 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) ∧ 𝑧 ∈ 𝑍 ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
6 5 3ad2antr3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 = 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
7 6 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑝 = 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
8 7 adantrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑝 = 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
9 8 a1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑝 = 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) )
10 9 exp31 ⊢ ( 𝐾 ∈ HL → ( 𝑝 = 𝑧 → ( ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) → ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) ) ) )
11 3simpb ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 = 𝑦 ) → ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) )
12 11 3anim1i ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) → ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) )
13 3simpc ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) → ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) )
14 13 anim1i ⊢ ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) )
15 1 2 3 4 paddasslem12 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
16 12 14 15 syl2an ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
17 16 3exp1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 = 𝑦 ) → ( ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) → ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) ) )
18 17 3expia ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) → ( 𝑥 = 𝑦 → ( ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) → ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) ) ) )
19 3simpa ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) → ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) )
20 19 3anim1i ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) → ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) )
21 3simpa ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) → ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) )
22 3simpa ⊢ ( ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) → ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) )
23 21 22 anim12i ⊢ ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) )
24 1 2 3 4 paddasslem13 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
25 20 23 24 syl2an ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
26 25 expr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ) → ( ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
27 26 3expd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ) → ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) → ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) → ( 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) ) )
28 1 2 3 4 paddasslem10 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
29 28 expr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ) → ( ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
30 29 3expd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ) → ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) → ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) → ( 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) ) )
31 27 30 pm2.61d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ) → ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) → ( 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) )
32 31 impd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ) → ( ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
33 32 expimpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) → ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
34 33 3exp ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ) → ( ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) → ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) ) )
35 34 3expia ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) → ( 𝑥 ≠ 𝑦 → ( ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) → ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) ) ) )
36 18 35 pm2.61dne ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) → ( ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) → ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) ) )
37 36 ex ⊢ ( 𝐾 ∈ HL → ( 𝑝 ≠ 𝑧 → ( ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) → ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) ) ) )
38 10 37 pm2.61dne ⊢ ( 𝐾 ∈ HL → ( ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) → ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) ) )
39 38 3imp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )