Metamath Proof Explorer

Theorem paddasslem12

Description: Lemma for paddass . The case when x = y . (Contributed by NM, 11-Jan-2012)

Ref Expression
Hypotheses paddasslem.l ⊢ ≤ = ( le ‘ 𝐾 )
paddasslem.j ⊢ ∨ = ( join ‘ 𝐾 )
paddasslem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
paddasslem.p ⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion paddasslem12 ( ( ( ( 𝐾 ∈ 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 5 9 10 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → ( 𝐾 ∈ HL ∧ ( 𝑋 + 𝑌 ) ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) )
12 3 4 sspadd2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → 𝑌 ⊆ ( 𝑋 + 𝑌 ) )
13 5 7 6 12 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑌 ⊆ ( 𝑋 + 𝑌 ) )
14 3 4 paddss1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 + 𝑌 ) ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) → ( 𝑌 ⊆ ( 𝑋 + 𝑌 ) → ( 𝑌 + 𝑍 ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
15 11 13 14 sylc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → ( 𝑌 + 𝑍 ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
16 5 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝐾 ∈ Lat )
17 simprll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑦 ∈ 𝑌 )
18 simprlr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑧 ∈ 𝑍 )
19 simpl3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑝 ∈ 𝐴 )
20 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
21 20 3 atbase ⊢ ( 𝑝 ∈ 𝐴 → 𝑝 ∈ ( Base ‘ 𝐾 ) )
22 19 21 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑝 ∈ ( Base ‘ 𝐾 ) )
23 7 17 sseldd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑦 ∈ 𝐴 )
24 20 3 atbase ⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ( Base ‘ 𝐾 ) )
25 23 24 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑦 ∈ ( Base ‘ 𝐾 ) )
26 simpl3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑟 ∈ 𝐴 )
27 20 3 atbase ⊢ ( 𝑟 ∈ 𝐴 → 𝑟 ∈ ( Base ‘ 𝐾 ) )
28 26 27 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑟 ∈ ( Base ‘ 𝐾 ) )
29 20 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑟 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑦 ∨ 𝑟 ) ∈ ( Base ‘ 𝐾 ) )
30 16 25 28 29 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → ( 𝑦 ∨ 𝑟 ) ∈ ( Base ‘ 𝐾 ) )
31 10 18 sseldd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑧 ∈ 𝐴 )
32 20 3 atbase ⊢ ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ( Base ‘ 𝐾 ) )
33 31 32 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑧 ∈ ( Base ‘ 𝐾 ) )
34 20 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑦 ∨ 𝑧 ) ∈ ( Base ‘ 𝐾 ) )
35 16 25 33 34 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → ( 𝑦 ∨ 𝑧 ) ∈ ( Base ‘ 𝐾 ) )
36 simpl1r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑥 = 𝑦 )
37 simprrl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) )
38 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∨ 𝑟 ) = ( 𝑦 ∨ 𝑟 ) )
39 38 breq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ↔ 𝑝 ≤ ( 𝑦 ∨ 𝑟 ) ) )
40 39 biimpa ⊢ ( ( 𝑥 = 𝑦 ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) → 𝑝 ≤ ( 𝑦 ∨ 𝑟 ) )
41 36 37 40 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑝 ≤ ( 𝑦 ∨ 𝑟 ) )
42 20 1 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → 𝑦 ≤ ( 𝑦 ∨ 𝑧 ) )
43 16 25 33 42 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑦 ≤ ( 𝑦 ∨ 𝑧 ) )
44 simprrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) )
45 20 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑟 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑦 ∨ 𝑧 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑦 ≤ ( 𝑦 ∨ 𝑧 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ↔ ( 𝑦 ∨ 𝑟 ) ≤ ( 𝑦 ∨ 𝑧 ) ) )
46 16 25 28 35 45 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → ( ( 𝑦 ≤ ( 𝑦 ∨ 𝑧 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ↔ ( 𝑦 ∨ 𝑟 ) ≤ ( 𝑦 ∨ 𝑧 ) ) )
47 43 44 46 mpbi2and ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → ( 𝑦 ∨ 𝑟 ) ≤ ( 𝑦 ∨ 𝑧 ) )
48 20 1 16 22 30 35 41 47 lattrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑝 ≤ ( 𝑦 ∨ 𝑧 ) )
49 1 2 3 4 elpaddri ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑝 ∈ ( 𝑌 + 𝑍 ) )
50 16 7 10 17 18 19 48 49 syl322anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑝 ∈ ( 𝑌 + 𝑍 ) )
51 15 50 sseldd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )